# Theory ConcreteCategory

chapter "Concrete Categories"
text ‹
In this section we define a locale ‹concrete_category›, which provides a uniform
(and more traditional) way to construct a category from specified sets of objects and arrows,
with specified identity objects and composition of arrows.
We prove that the identities and arrows of the constructed category are appropriately
in bijective correspondence with the given sets and that domains, codomains, and composition
in the constructed category are as expected according to this correspondence.
In the later theory ‹Functor›, once we have defined functors and isomorphisms of categories,
we will show a stronger property of this construction: if ‹C› is any category,
then ‹C› is isomorphic to the concrete category formed from it in the obvious way by taking
the identities of ‹C› as objects, the set of arrows of ‹C› as arrows, the identities of
‹C› as identity objects, and defining composition of arrows using the composition of ‹C›.
Thus no information about ‹C› is lost by extracting its objects, arrows, identities, and
composition and rebuilding it as a concrete category.
We note, however, that we do not assume that the composition function given as parameter
to the concrete category construction is ``extensional'', so in general it will contain
incidental information about composition of non-composable arrows, and this information
is not preserved by the concrete category construction.
›
theory ConcreteCategory
imports Category
begin
locale concrete_category =
fixes Obj :: "'o set"
and Hom :: "'o ⇒ 'o ⇒ 'a set"
and Id :: "'o ⇒ 'a"
and Comp :: "'o ⇒ 'o ⇒ 'o ⇒ 'a ⇒ 'a ⇒'a"
assumes Id_in_Hom: "A ∈ Obj ⟹ Id A ∈ Hom A A"
and Comp_in_Hom: "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; f ∈ Hom A B; g ∈ Hom B C ⟧
⟹ Comp C B A g f ∈ Hom A C"
and Comp_Hom_Id: "⟦ A ∈ Obj; B ∈ Obj; f ∈ Hom A B ⟧ ⟹ Comp B A A f (Id A) = f"
and Comp_Id_Hom: "⟦ A ∈ Obj; B ∈ Obj; f ∈ Hom A B ⟧ ⟹ Comp B B A (Id B) f = f"
and Comp_assoc: "⟦ A ∈ Obj; B ∈ Obj; C ∈ Obj; D ∈ Obj;
f ∈ Hom A B; g ∈ Hom B C; h ∈ Hom C D ⟧ ⟹
Comp D C A h (Comp C B A g f) = Comp D B A (Comp D C B h g) f"
begin