forked from HoTT/Coq-HoTT
-
Notifications
You must be signed in to change notification settings - Fork 0
/
HoTT.v
154 lines (128 loc) · 5.25 KB
/
HoTT.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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
(** A convenience file that loads most of the HoTT library.
You can use it with "Require Import HoTT" in your files.
But please do not use it in the HoTT library itself, or
you are likely going to create a dependency loop. *)
Require Export HoTT.Basics.
Require Export HoTT.Types.
Require Export HoTT.WildCat.
Require Export HoTT.Cubical.
Require Export HoTT.Pointed.
Require Export HoTT.Truncations.
Require Export HoTT.HFiber.
Require Export HoTT.HProp.
Require Export HoTT.Projective.
Require Export HoTT.HSet.
Require Export HoTT.EquivGroupoids.
Require Export HoTT.Equiv.BiInv.
Require Export HoTT.Equiv.PathSplit.
Require Export HoTT.Equiv.Relational.
Require Export HoTT.Extensions.
Require Export HoTT.Misc.
Require Export HoTT.PathAny.
Require Export HoTT.Functorish.
Require Export HoTT.Factorization.
Require Export HoTT.Constant.
Require Export HoTT.ObjectClassifier.
Require Export HoTT.TruncType.
Require Export HoTT.DProp.
Require Export HoTT.NullHomotopy.
Require Export HoTT.Idempotents.
Require Export HoTT.ExcludedMiddle.
Require Export HoTT.BoundedSearch.
Require Export HoTT.PropResizing.PropResizing.
(* Don't export the rest of [PropResizing] *)
Require Export HoTT.HIT.Interval.
Require Export HoTT.HIT.Coeq.
Require Export HoTT.HIT.Flattening.
Require Export HoTT.HIT.FreeIntQuotient.
Require Export HoTT.HIT.SetCone.
Require Export HoTT.HIT.epi.
Require Export HoTT.HIT.unique_choice.
Require Export HoTT.HIT.iso.
Require Export HoTT.HIT.quotient.
Require Export HoTT.HIT.V.
Require Export HoTT.Diagrams.Graph.
Require Export HoTT.Diagrams.Diagram.
Require Export HoTT.Diagrams.Cone.
Require Export HoTT.Diagrams.Cocone.
Require Export HoTT.Diagrams.DDiagram.
Require Export HoTT.Diagrams.ConstantDiagram.
Require Export HoTT.Diagrams.CommutativeSquares.
Require Export HoTT.Diagrams.Sequence.
Require Export HoTT.Diagrams.Span.
Require Export HoTT.Diagrams.ParallelPair.
Require Export HoTT.Limits.Pullback.
Require Export HoTT.Limits.Equalizer.
Require Export HoTT.Limits.Limit.
Require Export HoTT.Colimits.Pushout.
Require Export HoTT.Colimits.SpanPushout.
Require Export HoTT.Colimits.Quotient.
Require Export HoTT.Colimits.MappingCylinder.
Require Export HoTT.Colimits.Colimit.
Require Export HoTT.Colimits.Colimit_Pushout.
Require Export HoTT.Colimits.Colimit_Coequalizer.
Require Export HoTT.Colimits.Colimit_Flattening.
Require Export HoTT.Colimits.Colimit_Prod.
Require Export HoTT.Colimits.Colimit_Pushout_Flattening.
Require Export HoTT.Colimits.Colimit_Sigma.
Require Export HoTT.Modalities.ReflectiveSubuniverse.
Require Export HoTT.Modalities.Modality.
Require Export HoTT.Modalities.Accessible.
Require Export HoTT.Modalities.Notnot.
Require Export HoTT.Modalities.Identity.
Require Export HoTT.Modalities.Localization.
Require Export HoTT.Modalities.Nullification.
Require Export HoTT.Modalities.Descent.
Require Export HoTT.Modalities.Separated.
Require Export HoTT.Modalities.Lex.
Require Export HoTT.Modalities.Topological.
Require Export HoTT.Modalities.Open.
Require Export HoTT.Modalities.Closed.
Require Export HoTT.Modalities.Fracture.
Require Export HoTT.Modalities.CoreflectiveSubuniverse.
Require Export HoTT.Spaces.Nat.
Require Export HoTT.Spaces.Int.
Require Export HoTT.Spaces.Pos.
Require Export HoTT.Spaces.Cantor.
Require Export HoTT.Spaces.Circle.
Require Export HoTT.Spaces.TwoSphere.
Require Export HoTT.Spaces.Spheres.
Require Export HoTT.Spaces.BAut.
Require Export HoTT.Spaces.BAut.Cantor.
Require Export HoTT.Spaces.BAut.Bool.
Require Export HoTT.Spaces.BAut.Bool.IncoherentIdempotent.
Require Export HoTT.Spaces.BAut.Rigid.
Require Export HoTT.Spaces.Finite.
Require Export HoTT.Spaces.No.
Require Export HoTT.Spaces.Universe.
Require Export HoTT.Spaces.Torus.Torus.
Require Export HoTT.Spaces.Torus.TorusEquivCircles.
Require Export HoTT.Spaces.Torus.TorusHomotopy.
Require Export HoTT.Algebra.ooGroup.
Require Export HoTT.Algebra.Aut.
Require Export HoTT.Algebra.ooAction.
Require Export HoTT.Algebra.AbGroups.
Require Export HoTT.Algebra.Groups.
Require Export HoTT.Algebra.Rings.
Require Export HoTT.Homotopy.HomotopyGroup.
Require Export HoTT.Homotopy.Pi1S1.
Require Export HoTT.Homotopy.WhiteheadsPrinciple.
Require Export HoTT.Homotopy.BlakersMassey.
Require Export HoTT.Homotopy.Freudenthal.
Require Export HoTT.Homotopy.Suspension.
Require Export HoTT.Homotopy.Smash.
Require Export HoTT.Homotopy.Wedge.
Require Export HoTT.Homotopy.Join.
Require Export HoTT.Homotopy.HSpace.
Require Export HoTT.Homotopy.ClassifyingSpace.
Require Export HoTT.Spectra.Spectrum.
Require Export HoTT.Tactics.
Require Export HoTT.Tactics.BinderApply.
Require Export HoTT.Tactics.EquivalenceInduction.
Require Export HoTT.Tactics.EvalIn.
Require Export HoTT.Tactics.Nameless.
Require Export HoTT.Tactics.RewriteModuloAssociativity.
(** We do _not_ export [UnivalenceAxiom], [FunextAxiom], or any of the files in [Metatheory] from this file. Thus, importing this file does not prevent you from tracking usage of [Univalence] and [Funext] theorem-by-theorem in the same way that the library does. If you want any of those files, you should import them separately. *)
(** We check that UnivalenceAxiom, FunextAxiom aren't being leaked. This is so that these can be imported seperately. *)
Fail Check HoTT.UnivalenceAxiom.univalence_axiom.
Fail Check HoTT.FunextAxiom.funext_axiom.