Category Theory. Proof of Two Object Category.

TWO.v

Require Export ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Two_ob : Type :=
  | obone : Two_ob
  | obtwo : Two_ob.

Inductive Two_mor : Two_ob -> Two_ob -> Type :=
  | Id_obtwo : Two_mor obtwo obtwo
  | Id_obone : Two_mor obone obone
  | two_one : Two_mor obtwo obone
  | one_two : Two_mor obone obtwo.

Section equal_two_mor.

  Variable a b : Two_ob.

  Definition Equal_Two_mor (f g:Two_mor a b) := f = g.

  Lemma Equal_Two_mor_equiv : Equivalence Equal_Two_mor.
  Proof.
  unfold Equal_Two_mor in |- * ; apply Build_Equivalence.
  red in |- *. trivial.
  apply Build_Partial_equivalence.
  red in |- *.
  intros.  
  congruence.
  unfold Symmetric.
  intros.
  congruence.
  Qed.

  Canonical Structure Two_mor_setoid : Setoid := Equal_Two_mor_equiv.

End equal_two_mor.

Definition Comp_Two_mor (a b c: Two_ob) (f : Two_mor_setoid a b) ( g: Two_mor_setoid b c) : Two_mor_setoid a c.
Proof.  
  destruct a; destruct c; try constructor.
Defined.

Lemma Comp_Two_mor_congl : Congl_law Comp_Two_mor.
Proof.
  unfold Congl_law, Comp_Two_mor in |- *; simpl in |- *.
  unfold Equal_Two_mor in |- * ; trivial.