Zero Category.

ZERO.v

Require Export ConCaT.CATEGORY_THEORY.CATEGORY.Category.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Zero_ob : Type :=.

Inductive Zero_mor : Zero_ob -> Zero_ob -> Type :=.

 Section equal_zero_mor.

 Variable a b : Zero_ob.

 Definition Equal_Zero_mor (f g : Zero_mor a b) := True.

 Lemma Equal_Zero_mor_equiv : Equivalence Equal_Zero_mor.
 Proof.
   unfold Equal_Zero_mor.
   apply Build_Equivalence.
   auto.
   auto.
 Qed.

 Canonical Structure Zero_mor_setoid : Setoid := Equal_Zero_mor_equiv.
 
 End equal_zero_mor.

Definition Comp_Zero_mor (a b c : Zero_ob) (f: Zero_mor_setoid a b) (g: Zero_mor_setoid b c) : Zero_mor_setoid a c.
Proof.
  contradiction.
Defined.

Lemma Comp_Zero_mor_congl : Congl_law Comp_Zero_mor.
Proof.
  unfold Congl_law, Comp_Zero_mor.
  simpl.
  intros.
  unfold Equal_Zero_mor.
  trivial.
Qed.

Lemma Comp_Zero_mor_congr : Congr_law Comp_Zero_mor.
Proof.
unfold Congr_law, Comp_Zero_mor in |- *; simpl in |- *;
 unfold Equal_Zero_mor in |- *; trivial.
Qed.

Definition Comp_Zero := Build_Comp Comp_Zero_mor_congl Comp_Zero_mor_congr.

Lemma Assoc_Zero : Assoc_law Comp_Zero.
Proof.
  unfold Assoc_law.
  simpl.
  unfold Comp_Zero, Equal_Zero_mor.
  trivial.
Qed.

Definition Id_Zero (a : Zero_ob) : Zero_mor_setoid a a.
Proof.
  contradiction.
Defined.

Lemma Idl_Zero : Idl_law Comp_Zero Id_Zero.
Proof.
  unfold Idl_law. 
  intros.
  contradiction.
Qed.

Lemma Idr_Zero : Idr_law Comp_Zero Id_Zero.
Proof.
  unfold Idr_law.
  intros.
  contradiction.
Qed.

Canonical Structure Zero := Build_Category Assoc_Zero Idl_Zero Idr_Zero.