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__).