HoTTLean :
Formalizing the Meta-Theory of HoTT in Lean
1
Syntax of HoTT0
2
Natural Models
▶
2.1
Interpretation of syntax
2.2
Natural model
2.3
Pi types
2.4
Sigma types
2.5
Identity types
2.6
Binary products and Exponentials
2.7
Univalence
2.8
Extensional identity types and UIP
3
HoTT0 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 HoTT0 interpreted in natural models