-
-
Save yam6da/eab6068b24695d3bb2d1 to your computer and use it in GitHub Desktop.
3-Object Category in Coq with ConCaT
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* 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 *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment