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
HoTTLean :
Formalizing the Meta-Theory of HoTT in Lean
Steve Awodey, Mario Carneiro, Sina Hazratpour, Joseph Hua, Wojciech Nawrocki, Spencer Woolfson
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