Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Zero Category.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment