Skip to content
HoTT Book formalisation in Rzk proof assistant
2.11 Identity type
Initializing search
rzk-lang/hottbook
HoTT Book formalisation in Rzk proof assistant
rzk-lang/hottbook
General
Foundations
Foundations
1 Type Theory
1 Type Theory
1.4 Dependent function types
1.5 Product types
1.6 Dependent pair types
1.7 Coproduct types
1.8 The type of booleans
1.9 The natural numbers
1.10 Pattern matching and recursion
1.11 Propositions as types
1.12 Identity types
Exercises
2 Homotopy Type Theory
2 Homotopy Type Theory
2.1 Types are higher groupoids
2.2 Functions are functors
2.3 Type families are fibrations
2.4 Homotopies and equivalences
2.5 The higher groupoid structure of type formers
2.6 Cartesian product types
2.7 Σ-types
2.8 The unit type
2.9 Π-types and the function extensionality axiom
2.10 Universes and univalence axiom
2.11 Identity type
2.12 Coproducts
2.13 Natural numbers
2.14 Example: equality of structures
2.15 Universal properties
Exercises
3 Sets and Logic
3 Sets and Logic
3.1 Sets and n-types
3.2 Propositions as Types?
3.3 Mere propositions
3.11 Contractibility
2.11 Identity type
¶
This is a literate Rzk file:
#lang
rzk-1