-
Notifications
You must be signed in to change notification settings - Fork 2
/
CategoryEquality.v
106 lines (83 loc) · 3.47 KB
/
CategoryEquality.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
Require Import ProofIrrelevance JMeq.
Require Export Category FEqualDep.
Require Import Common Notations StructureEquality SpecializedCategory.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Infix "==" := JMeq.
Section Categories_Equal.
Lemma Category_eq : forall (A B : Category),
Object A = Object B
-> Morphism A == Morphism B
-> @Identity _ A == @Identity _ B
-> @Compose _ A == @Compose _ B
-> A = B.
unfold Object, Morphism, Identity, Compose; intros;
destruct_type @Category; destruct_type @SpecializedCategory; simpl in *;
subst_body; repeat subst.
repeat f_equal; apply proof_irrelevance.
Qed.
Lemma SmallCategory_eq : forall (A B : SmallCategory),
SObject A = SObject B
-> Morphism A == Morphism B
-> @Identity _ A == @Identity _ B
-> @Compose _ A == @Compose _ B
-> A = B.
unfold SObject, Morphism, Identity, Compose; intros;
destruct_type @SmallCategory; destruct_type @SmallSpecializedCategory; simpl in *;
subst_body; repeat (subst; JMeq_eq).
repeat f_equal; apply proof_irrelevance.
Qed.
Lemma LocallySmallCategory_eq : forall (A B : LocallySmallCategory),
LSObject A = LSObject B
-> Morphism A == Morphism B
-> @Identity _ A == @Identity _ B
-> @Compose _ A == @Compose _ B
-> A = B.
unfold LSObject, Morphism, Identity, Compose; intros;
destruct_type @LocallySmallCategory; destruct_type @LocallySmallSpecializedCategory; simpl in *;
subst_body; repeat (subst; JMeq_eq).
repeat f_equal; apply proof_irrelevance.
Qed.
End Categories_Equal.
Ltac cat_eq_step_with tac :=
structures_eq_step_with_tac
ltac:(apply SmallCategory_eq || apply LocallySmallCategory_eq || apply Category_eq)
tac.
Ltac cat_eq_with tac := repeat cat_eq_step_with tac.
Ltac cat_eq_step := cat_eq_step_with idtac.
Ltac cat_eq := cat_eq_with idtac.
Section RoundtripCat.
Context `(C : @SpecializedCategory obj).
Variable C' : Category.
Lemma SpecializedCategory_Category_SpecializedCategory_Id : ((C : Category) : SpecializedCategory _) = C.
spcat_eq.
Qed.
Lemma Category_SpecializedCategory_Category_Id : ((C' : SpecializedCategory _) : Category) = C'.
cat_eq.
Qed.
End RoundtripCat.
Hint Rewrite @SpecializedCategory_Category_SpecializedCategory_Id @Category_SpecializedCategory_Category_Id : category.
Section RoundtripLSCat.
Context `(C : @LocallySmallSpecializedCategory obj).
Variable C' : LocallySmallCategory.
Lemma LocallySmall_SpecializedCategory_Category_SpecializedCategory_Id : ((C : LocallySmallCategory) : LocallySmallSpecializedCategory _) = C.
spcat_eq.
Qed.
Lemma LocallySmall_Category_SpecializedCategory_Category_Id : ((C' : LocallySmallSpecializedCategory _) : LocallySmallCategory) = C'.
cat_eq.
Qed.
End RoundtripLSCat.
Hint Rewrite @LocallySmall_SpecializedCategory_Category_SpecializedCategory_Id LocallySmall_Category_SpecializedCategory_Category_Id : category.
Section RoundtripSCat.
Context `(C : @SmallSpecializedCategory obj).
Variable C' : SmallCategory.
Lemma Small_SpecializedCategory_Category_SpecializedCategory_Id : ((C : SmallCategory) : SmallSpecializedCategory _) = C.
spcat_eq.
Qed.
Lemma Small_Category_SpecializedCategory_Category_Id : ((C' : SmallSpecializedCategory _) : SmallCategory) = C'.
cat_eq.
Qed.
End RoundtripSCat.
Hint Rewrite @Small_SpecializedCategory_Category_SpecializedCategory_Id Small_Category_SpecializedCategory_Category_Id : category.