Empty Category

ZERO.v

Require Export Category.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive Empty : Type := .

(* The category Zero *)

Definition Zero_ob : Type := Empty.

Definition Zero_mor (a : Zero_ob) (b : Zero_ob) : Type := Empty.

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.
red.
trivial.
apply Build_Partial_equivalence.
red.
trivial.
red.
trivial.
Qed.

Canonical Structure Zero_mor_setoid : Setoid := Equal_Zero_mor_equiv.

End equal_zero_mor.

Print Congl_law.

Definition Comp_Zero_mor (a b c : Zero_ob) (f : Zero_mor a b) (g : Zero_mor b c) : Zero_mor a c := 
  match f with
  end. 

Lemma Comp_Zero_mor_congl : Congl_law Comp_Zero_mor.
Proof.
red.
intro a.
destruct a.
Qed.

Lemma Comp_Zero_mor_congr : Congr_law Comp_Zero_mor.
Proof.
red.
intro a.
destruct a.
Qed.

Definition Comp_Zero := Build_Comp Comp_Zero_mor_congl Comp_Zero_mor_congr.

Lemma Assoc_Zero : Assoc_law Comp_Zero.
Proof.
red.
intro a.
destruct a.
Qed.

Definition Id_Zero (a : Zero_ob) : Zero_mor_setoid a a :=
  match a with
  end.

Lemma Idl_Zero : Idl_law Comp_Zero Id_Zero.
Proof.
red.
intro a.
destruct a.
Qed.

Lemma Idr_Zero : Idr_law Comp_Zero Id_Zero.
Proof.
red.
intro a.
destruct a.
Qed.

Canonical Structure Zero := Build_Category Assoc_Zero Idl_Zero Idr_Zero.