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