/
_CoqProject
230 lines (230 loc) · 5.3 KB
/
_CoqProject
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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
-R . Category
Adjunction/Diagonal/Product.v
Adjunction/Hom.v
Adjunction/Natural/Transformation.v
Adjunction/Natural/Transformation/Opposite.v
Adjunction/Natural/Transformation/Universal.v
Adjunction/Opposite.v
Construction/Arrow.v
Construction/Cayley.v
Construction/Comma.v
Construction/Comma/Adjunction.v
Construction/Comma/Isomorphism.v
Construction/Comma/Natural/Transformation.v
Construction/Coproduct.v
Construction/Enriched.v
Construction/Free.v
Construction/Groupoid.v
Construction/Opposite.v
Construction/Product.v
Construction/Product/Comma.v
Construction/Slice.v
Construction/Slice/Pullback.v
Construction/Subcategory.v
Construction/Free/Quiver.v
Functor/Applicative.v
Functor/Bifunctor.v
Functor/Construction/Product.v
Functor/Construction/Product/Monoidal.v
Functor/Construction/Product/Strong.v
Functor/Coproduct.v
Functor/Diagonal.v
Functor/Hom.v
Functor/Hom/Internal.v
Functor/Hom/Yoneda.v
Functor/Opposite.v
Functor/Product.v
Functor/Product/Internal.v
Functor/Representable.v
Functor/Strong.v
Functor/Strong/Product.v
Functor/Structure/Cartesian.v
Functor/Structure/Cartesian/Closed.v
Functor/Structure/Constant.v
Functor/Structure/Monoidal.v
Functor/Structure/Monoidal/Compose.v
Functor/Structure/Monoidal/Id.v
Functor/Structure/Monoidal/Pure.v
Functor/Structure/Terminal.v
Functor/Traversable.v
Functor/Traversable/Product.v
Instance/AST.v
Instance/Adj.v
Instance/Adjoints.v
Instance/Cat.v
Instance/Cat/Cartesian.v
Instance/Cat/Cartesian/Closed.v
Instance/Cat/Cocartesian.v
Instance/StrictCat.v
Instance/Comp.v
Instance/Cones.v
Instance/Cones/Comma.v
Instance/Cones/Limit.v
Instance/Coq.v
Instance/Coq/Applicative.v
Instance/Coq/Monad.v
Instance/Coq/Par.v
Instance/Coq/ParE.v
Instance/Ens.v
Instance/Fact.v
Instance/Fun.v
Instance/Fun/Cartesian.v
Instance/Lambda.v
Instance/Lambda/Eval.v
Instance/Lambda/Example.v
Instance/Lambda/Exp.v
Instance/Lambda/Full.v
Instance/Lambda/Log.v
Instance/Lambda/Ltac.v
Instance/Lambda/Multi.v
Instance/Lambda/Norm.v
Instance/Lambda/Ren.v
Instance/Lambda/Sem.v
Instance/Lambda/Sound.v
Instance/Lambda/Step.v
Instance/Lambda/Sub.v
Instance/Lambda/Ty.v
Instance/Lambda/Value.v
Instance/One.v
Instance/One/Diagonal.v
Instance/Parallel.v
Instance/Poset.v
Instance/Props.v
Instance/Proset.v
Instance/Rel.v
Instance/Roof.v
Instance/Sets.v
Instance/Sets/Cartesian.v
Instance/Sets/Cartesian/Closed.v
Instance/Sets/Cocartesian.v
Instance/Sets/Par.v
Instance/Shapes.v
Instance/Two.v
Instance/Two/Discrete.v
Instance/Zero.v
Lib.v
Lib/Datatypes.v
Lib/FMapExt.v
Lib/Foundation.v
Lib/IList.v
Lib/MapDecide.v
Lib/NETList.v
Lib/Setoid.v
Lib/TList.v
Lib/Tactics.v
Lib/Tactics2.v
Monad/Adjunction.v
Monad/Algebra.v
Monad/Compose.v
Monad/Distributive.v
Monad/Eilenberg/Moore.v
Monad/Kleisli.v
Monad/Monoid.v
Monad/Transformer.v
Natural/Transformation/Applicative.v
Natural/Transformation/Monoidal.v
Natural/Transformation/Opposite.v
Natural/Transformation/Strong.v
Solver.v
Solver/Decide.v
Solver/Denote.v
Solver/Expr.v
Solver/Normal.v
Solver/Reify.v
Structure/BiCCC.v
Structure/Bicartesian.v
Structure/Binoidal.v
Structure/Cartesian.v
Structure/Cartesian/Closed.v
Structure/Cartesian/Closed/Product.v
Structure/Cartesian/Product.v
Structure/Closed.v
Structure/Cocartesian.v
Structure/Complete.v
Structure/Cone.v
Structure/Cone/Const.v
Structure/Cone/Natural/Transformation.v
Structure/Constant.v
Structure/Discrete.v
Structure/Distributive.v
Structure/End.v
Structure/Equalizer.v
Structure/Group.v
Structure/Group/Proofs.v
Structure/Initial.v
Structure/Limit.v
Structure/Limit/Cartesian.v
Structure/Limit/Kan/Extension.v
Structure/Limit/Terminal.v
Structure/Monoid.v
Structure/Monoidal.v
Structure/Monoidal/Balanced.v
Structure/Monoidal/Braided.v
Structure/Monoidal/Cartesian.v
Structure/Monoidal/Cartesian/Cartesian.v
Structure/Monoidal/Cartesian/Proofs.v
Structure/Monoidal/Closed.v
Structure/Monoidal/Commutative.v
Structure/Monoidal/Compose.v
Structure/Monoidal/Internal/Product.v
Structure/Monoidal/Naturality.v
Structure/Monoidal/Product.v
Structure/Monoidal/Proofs.v
Structure/Monoidal/Relevance.v
Structure/Monoidal/Semicartesian.v
Structure/Monoidal/Semicartesian/Proofs.v
Structure/Monoidal/Semicartesian/Terminal.v
Structure/Monoidal/Semicocartesian.v
Structure/Monoidal/Symmetric.v
Structure/Monoidal/Traced.v
Structure/Pullback.v
Structure/Pullback/Limit.v
Structure/Span.v
Structure/Terminal.v
Structure/UniversalProperty.v
Structure/UniversalProperty/Cartesian.v
Structure/UniversalProperty/Limit.v
Structure/UniversalProperty/Universal/Arrow.v
Structure/Wedge.v
Theory.v
Theory/Adjunction.v
Theory/Algebra.v
Theory/Bicategory.v
Theory/Category.v
Theory/Category/Raw.v
Theory/Category/Semi.v
Theory/Coq.v
Theory/Coq/Applicative.v
Theory/Coq/Applicative/Proofs.v
Theory/Coq/Either.v
Theory/Coq/Either/Proofs.v
Theory/Coq/Foldable.v
Theory/Coq/Functor.v
Theory/Coq/Functor/Proofs.v
Theory/Coq/List.v
Theory/Coq/List/Proofs.v
Theory/Coq/Map.v
Theory/Coq/Maybe.v
Theory/Coq/Maybe/Proofs.v
Theory/Coq/Monad.v
Theory/Coq/Monad/Proofs.v
Theory/Coq/Monoid.v
Theory/Coq/Semigroup.v
Theory/Coq/Traversable.v
Theory/Coq/Tuple.v
Theory/Coq/Tuple/Proofs.v
Theory/Dinatural.v
Theory/Functor.v
Theory/Isomorphism.v
Theory/Kan/Extension.v
Theory/Metacategory.v
Theory/Metacategory/ArrowsOnly.v
Theory/Metacategory/DecideExample.v
Theory/Monad.v
Theory/Morphisms.v
Theory/Natural/Transformation.v
Theory/Naturality.v
Theory/Sheaf.v
Theory/Universal/Arrow.v
Tools/Abstraction.v
Tools/Represented.v