-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathProductLaws.v
137 lines (114 loc) · 4.79 KB
/
ProductLaws.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
Require Export NatCategory ProductCategory.
Require Import Common Notations.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Local Open Scope category_scope.
Section swap.
Definition SwapFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD)
: SpecializedFunctor (C * D) (D * C)
:= Build_SpecializedFunctor (C * D) (D * C)
(fun cd => (snd cd, fst cd))
(fun _ _ m => (snd m, fst m))
(fun _ _ _ _ _ => eq_refl)
(fun _ => eq_refl).
Lemma ProductLawSwap `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD)
: ComposeFunctors (SwapFunctor C D) (SwapFunctor D C) = IdentityFunctor _.
functor_eq; intuition.
Qed.
End swap.
Section Law0.
Context `(C : @SpecializedCategory objC).
Definition ProductLaw0Functor : SpecializedFunctor (C * 0) 0.
refine (Build_SpecializedFunctor (C * 0) 0
(@snd _ _)
(fun _ _ => @snd _ _)
_
_);
abstract (
intros;
destruct_head_hnf @prod;
destruct_head Empty_set
).
Defined.
Definition ProductLaw0Functor_Inverse : SpecializedFunctor 0 (C * 0).
repeat esplit;
intros; destruct_head_hnf Empty_set.
Grab Existential Variables.
intros; destruct_head_hnf Empty_set.
intros; destruct_head_hnf Empty_set.
Defined.
Lemma ProductLaw0 : ComposeFunctors ProductLaw0Functor ProductLaw0Functor_Inverse = IdentityFunctor _ /\
ComposeFunctors ProductLaw0Functor_Inverse ProductLaw0Functor = IdentityFunctor _.
Proof.
split; functor_eq;
destruct_head_hnf @prod;
destruct_head_hnf Empty_set.
Qed.
End Law0.
Section Law0'.
Context `(C : @SpecializedCategory objC).
Let ProductLaw0'Functor' : SpecializedFunctor (0 * C) 0.
functor_simpl_abstract_trailing_props (ComposeFunctors (ProductLaw0Functor C) (SwapFunctor _ _)).
Defined.
Definition ProductLaw0'Functor : SpecializedFunctor (0 * C) 0 := Eval hnf in ProductLaw0'Functor'.
Let ProductLaw0'Functor_Inverse' : SpecializedFunctor 0 (0 * C).
functor_simpl_abstract_trailing_props (ComposeFunctors (SwapFunctor _ _) (ProductLaw0Functor_Inverse C)).
Defined.
Definition ProductLaw0'Functor_Inverse : SpecializedFunctor 0 (0 * C) := Eval hnf in ProductLaw0'Functor_Inverse'.
Lemma ProductLaw0' : ComposeFunctors ProductLaw0'Functor ProductLaw0'Functor_Inverse = IdentityFunctor _ /\
ComposeFunctors ProductLaw0'Functor_Inverse ProductLaw0'Functor = IdentityFunctor _.
Proof.
split; functor_eq;
destruct_head_hnf @prod;
destruct_head_hnf Empty_set.
Qed.
End Law0'.
Section Law1.
Context `(C : @SpecializedCategory objC).
Let ProductLaw1Functor' : SpecializedFunctor (C * 1) C.
functor_simpl_abstract_trailing_props (fst_Functor (C := C) (D := 1)).
Defined.
Definition ProductLaw1Functor : SpecializedFunctor (C * 1) C
:= Eval hnf in ProductLaw1Functor'.
Definition ProductLaw1Functor_Inverse : SpecializedFunctor C (C * 1).
refine (Build_SpecializedFunctor C (C * 1)
(fun c => (c, tt))
(fun s d m => (m, eq_refl))
_
_);
abstract (
intros; simpl in *; simpl_eq; reflexivity
).
Defined.
Lemma ProductLaw1 : ComposeFunctors ProductLaw1Functor ProductLaw1Functor_Inverse = IdentityFunctor _ /\
ComposeFunctors ProductLaw1Functor_Inverse ProductLaw1Functor = IdentityFunctor _.
Proof.
split; functor_eq;
destruct_head_hnf @prod;
destruct_head_hnf @eq;
destruct_head_hnf unit;
reflexivity.
Qed.
End Law1.
Section Law1'.
Context `(C : @SpecializedCategory objC).
Definition ProductLaw1'Functor' : SpecializedFunctor (1 * C) C.
functor_simpl_abstract_trailing_props (ComposeFunctors (ProductLaw1Functor C) (SwapFunctor _ _)).
Defined.
Definition ProductLaw1'Functor : SpecializedFunctor (1 * C) C := Eval hnf in ProductLaw1'Functor'.
Let ProductLaw1'Functor_Inverse' : SpecializedFunctor C (1 * C).
functor_simpl_abstract_trailing_props (ComposeFunctors (SwapFunctor _ _) (ProductLaw1Functor_Inverse C)).
Defined.
Definition ProductLaw1'Functor_Inverse : SpecializedFunctor C (1 * C) := Eval hnf in ProductLaw1'Functor_Inverse'.
Lemma ProductLaw1' : ComposeFunctors ProductLaw1'Functor ProductLaw1'Functor_Inverse = IdentityFunctor _ /\
ComposeFunctors ProductLaw1'Functor_Inverse ProductLaw1'Functor = IdentityFunctor _.
Proof.
split; functor_eq;
destruct_head_hnf @prod;
destruct_head_hnf @eq;
destruct_head_hnf unit;
reflexivity.
Qed.
End Law1'.