3-Object Category in Coq with ConCaT

Cat3.v

(* Wed May  4 16:13:02 2011 *)

Require Export ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Obs3 : Type :=
  | Ob1 : Obs3
  | Ob2 : Obs3
  | Ob3 : Obs3.

Inductive Cat3_Mor : Obs3 -> Obs3 -> Type :=
  | Id_Ob1 : Cat3_Mor Ob1 Ob1
  | Id_Ob2 : Cat3_Mor Ob2 Ob2
  | Id_Ob3 : Cat3_Mor Ob3 Ob3
  | Mor12  : Cat3_Mor Ob1 Ob2
  | Mor23  : Cat3_Mor Ob2 Ob3
  | Mor31  : Cat3_Mor Ob3 Ob1
  | Mor21  : Cat3_Mor Ob2 Ob1
  | Mor32  : Cat3_Mor Ob3 Ob2
  | Mor13  : Cat3_Mor Ob1 Ob3.

Section Equal_Cat3_Mor.
  
  Variable a b : Obs3.
  Definition Equal_Cat3_Mor (f g : Cat3_Mor a b) := f = g.
  
  Lemma Equal_Cat3_Mor_equiv : Equivalence Equal_Cat3_Mor.
    Proof.
      unfold Equal_Cat3_Mor in |- *; apply Build_Equivalence.
      red. trivial.
      apply Build_Partial_equivalence.
      red in |- *. 
      intros.
      congruence.
      unfold Symmetric.
      intros.
      congruence.
    Qed.

Canonical Structure Cat3_Mor_Setoid : Setoid := Equal_Cat3_Mor_equiv.

End Equal_Cat3_Mor.

Definition Composite_Cat3_Mor
  (a b c : Obs3) (f : Cat3_Mor_Setoid a b) (g : Cat3_Mor_Setoid b c)
  : Cat3_Mor_Setoid a c.
  destruct a; destruct c; info constructor.
Defined.

(* Wed May  4 17:11:09 2011 *)
Lemma Composite_Cat3_Mor_Congl : Congl_law Composite_Cat3_Mor.
  Proof.
  unfold Congl_law, Composite_Cat3_Mor in |- *; simpl in |- *.
  unfold Equal_Cat3_Mor in |- *; trivial.
  intros.
  destruct a; destruct c ; trivial.
Qed.  

Lemma Composite_Cat3_Mor_Congr : Congr_law Composite_Cat3_Mor.
  unfold Congr_law, Composite_Cat3_Mor in |- *; simpl in |-*.
  unfold Equal_Cat3_Mor in |- *.
 destruct a; destruct c; trivial.
Qed.

Definition Composite_Cat3 := 
  Build_Comp Composite_Cat3_Mor_Congl Composite_Cat3_Mor_Congr.

Lemma Assoc_Cat3 : Assoc_law Composite_Cat3.
  unfold Assoc_law in |- *; simpl in |- *.
  unfold Equal_Cat3_Mor.
  destruct f; destruct h; info trivial.
Qed.
(* Wed May  4 18:13:04 2011 *)