1
Syntax of H0TT
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
H0TT 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
Groupoid Model of H0TT in Lean 4
Steve Awodey, Sina Hazratpour, Joseph Hua, Wojciech Nawrocki, Spencer Woolfson
1
Syntax of H0TT
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
H0TT 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