Part 6
Equality, Computed
- 214Two-Level Type Theory and Strict EqualityCore route
- 215Observational Equality and Computational ExtensionalityCore route
- 216Intrinsic Topology of the UniverseOptional
- 217Cubical Type Theory I: De Morgan CubesCore route
- 218Cubical Type Theory II: Cartesian Cubes and ComputationCore route
- 219Guarded Cubical Type TheoryOptional
- 220XTT and Computational Bishop SetsOptional
- 221Parametric Cubical Type Theory and HIT Free TheoremsOptional
- 222Higher Observational Type Theory: From Bridges to FibrancyTerminal