Require Export make_small_cat.

Implicit Arguments On.

Module Set_Cat <: Cat_Sig.

Export Misc.

Definition Obj := Type.

Definition Morph [A,B:Obj] := A->B.

Definition morph_id : (x:Obj) (Morph x x) := [x:Obj; u:x] u.

Definition morph_comp : (x,y,z:Obj; g:(Morph y z); f:(Morph x y))
 (Morph x z) :=
 [x,y,z:Obj; g:(Morph y z); f:(Morph x y); u:x] (g (f u)).

Lemma morph_comp_assoc : (A,B,C,D:Obj)
 (H:(Morph C D); G:(Morph B C); F:(Morph A B))
 (morph_comp H (morph_comp G F))==(morph_comp (morph_comp H G) F).
Proof.
  Unfold Obj Morph morph_comp; Intros.
  Apply nondep_extensionality; Reflexivity.
Qed.

Definition morph_id_sx : (A,B:Obj; F:(Morph A B))
 (morph_comp (!morph_id B) F)==F.
Proof.
  Unfold Obj Morph morph_comp morph_id; Intros.
  Apply nondep_extensionality; Reflexivity.
Qed.

Definition morph_id_dx : (A,B:Obj; F:(Morph A B))
 (morph_comp F (!morph_id A))==F.
Proof.
  Unfold Obj Morph morph_comp morph_id; Intros.
  Apply nondep_extensionality; Reflexivity.
Qed.

End Set_Cat.