HoTTLean
Formalizing the Meta-Theory of HoTT in Lean
W
arning: this blueprint is very outdated. Consult the GitHub README instead.
1
Syntax of HoTT\(0\)
2
Natural Models
▶
2.1
Interpretation of syntax
2.2
Natural model
2.3
Product types
2.4
Sum types
2.5
Identity types
2.6
Binary products and Exponentials
2.7
Univalence
2.8
Extensional identity types and UIP
3
HoTT\(0\) interpreted in natural models
4
The Groupoid Model
▶
4.1
Classifying display maps
4.2
Groupoid fibrations
4.3
Classifying type dependency
4.4
Pi and Sigma structure
4.5
Identity types
4.6
Universe of Discrete Groupoids
5
Polynomial Endofunctors
6
Bibliography
Dependency graph
3 HoTT\(0\) interpreted in natural models