Require Export cat.
Require Export cat_.
Implicit Arguments On.
Small Categories |
The following parametrized module builds the term of a category (of type Cat_.Cat) associated to every module of signature Cat_Sig.
|
Module Make_Small_Cat [C:Cat_Sig] <: A_Cat_.
Export Cat_.
Section Make_Small_Cat.
Local B : Cat_Data :=
(!Build_Cat_Data C.Obj C.Morph C.morph_comp C.morph_id).
Remark B_th : (Cat_Theory (!oo B) (!ii B)).
Proof.
Split.
Apply C.morph_comp_assoc.
Apply C.morph_id_sx.
Apply C.morph_id_dx.
Qed.
Definition A : Obj.
Proof.
Split with B; Exact B_th.
Defined.
End Make_Small_Cat.
End Make_Small_Cat.
Category of small categories. |
The module Cat itself gives produce a term of type Cat_.Cat.
|
Module Small_Cat : A_Cat_ := (Make_Small_Cat Cat).