-
Notifications
You must be signed in to change notification settings - Fork 1
/
GroundZero.lean
94 lines (94 loc) · 3.18 KB
/
GroundZero.lean
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
-- Automatically generated by `lake script run updateIndex`, do not edit it manually.
import GroundZero.Algebra.Basic
import GroundZero.Algebra.Boolean
import GroundZero.Algebra.Category
import GroundZero.Algebra.EilenbergMacLane
import GroundZero.Algebra.Geometry
import GroundZero.Algebra.Group.Action
import GroundZero.Algebra.Group.Alternating
import GroundZero.Algebra.Group.Automorphism
import GroundZero.Algebra.Group.Basic
import GroundZero.Algebra.Group.Differential
import GroundZero.Algebra.Group.Factor
import GroundZero.Algebra.Group.Finite
import GroundZero.Algebra.Group.Free
import GroundZero.Algebra.Group.Homotopy
import GroundZero.Algebra.Group.Isomorphism
import GroundZero.Algebra.Group.Lemmas
import GroundZero.Algebra.Group.Periodic
import GroundZero.Algebra.Group.Presentation
import GroundZero.Algebra.Group.Product
import GroundZero.Algebra.Group.Semidirect
import GroundZero.Algebra.Group.Subgroup
import GroundZero.Algebra.Group.Symmetric
import GroundZero.Algebra.Group.Z
import GroundZero.Algebra.Monoid
import GroundZero.Algebra.Orgraph
import GroundZero.Algebra.Reals
import GroundZero.Algebra.Ring
import GroundZero.Algebra.Transformational
import GroundZero.Cubical.Connection
import GroundZero.Cubical.Cubes
import GroundZero.Cubical.Example
import GroundZero.Cubical.Path
import GroundZero.Cubical.V
import GroundZero.Exercises.Chap1
import GroundZero.Exercises.Chap2
import GroundZero.Exercises.Chap3
import GroundZero.Exercises.Chap4
import GroundZero.Exercises.Chap5
import GroundZero.HITs.Circle
import GroundZero.HITs.Coequalizer
import GroundZero.HITs.Colimit
import GroundZero.HITs.Flattening
import GroundZero.HITs.Generalized
import GroundZero.HITs.Int
import GroundZero.HITs.Interval
import GroundZero.HITs.Join
import GroundZero.HITs.Merely
import GroundZero.HITs.Moebius
import GroundZero.HITs.Pushout
import GroundZero.HITs.Quotient
import GroundZero.HITs.Reals
import GroundZero.HITs.Setquot
import GroundZero.HITs.Sphere
import GroundZero.HITs.Suspension
import GroundZero.HITs.Trunc
import GroundZero.HITs.Wedge
import GroundZero.Meta.Basic
import GroundZero.Meta.HottTheory
import GroundZero.Meta.Notation
import GroundZero.Meta.Tactic
import GroundZero.Meta.Trust
import GroundZero.Modal.Disc
import GroundZero.Modal.Etale
import GroundZero.Modal.Infinitesimal
import GroundZero.Proto
import GroundZero.Structures
import GroundZero.Theorems.Classical
import GroundZero.Theorems.Connectedness
import GroundZero.Theorems.Equiv
import GroundZero.Theorems.Fibration
import GroundZero.Theorems.Functions
import GroundZero.Theorems.Funext
import GroundZero.Theorems.Hopf
import GroundZero.Theorems.Nat
import GroundZero.Theorems.Ontological
import GroundZero.Theorems.Pullback
import GroundZero.Theorems.Univalence
import GroundZero.Theorems.Weak
import GroundZero.Types.Category
import GroundZero.Types.CellComplex
import GroundZero.Types.Coproduct
import GroundZero.Types.Ens
import GroundZero.Types.Equiv
import GroundZero.Types.HEq
import GroundZero.Types.Id
import GroundZero.Types.Integer
import GroundZero.Types.Lost
import GroundZero.Types.Nat
import GroundZero.Types.Precategory
import GroundZero.Types.Product
import GroundZero.Types.Setquot
import GroundZero.Types.Sigma
import GroundZero.Types.Unit