Lectures onType Theory
Part 5
Part 5

Homotopy Type Theory and Univalent Mathematics

  1. 187Elementary Topology and Classical HomotopyCore route
  2. 188Fibrations, Homotopy Groups, and Exact SequencesCore route
  3. 189Types as ∞-GroupoidsCore route
  4. 190Simplicial Sets, Horns, and Kan FibrationsCore route
  5. 191Model Categories and Simplicial Semantics of Type TheoryCore route
  6. 192A Homotopical Model of UnivalenceCore route
  7. 193UnivalenceCore route
  8. 194Proof and Program Transfer Modulo EquivalenceOptional
  9. 195Truncation Levels, Propositions, and LogicCore route
  10. 196Connected Maps, Factorization, and ModalitiesCore route
  11. 197Localization and Its Universal PropertyOptional
  12. 198Higher Inductive Types and Homotopy-InitialityCore route
  13. 199QIIT and QWI Schemas, Elimination, and InitialityOptional
  14. 200Join Constructions and ConnectivityCore route
  15. 201Type-Theoretic Replacement and Univalent CompletionOptional
  16. 202Coverings, van Kampen, and the Fundamental GroupCore route
  17. 203Fiber Sequences and Suspension MethodsCore route
  18. 204Higher Groups, Spectra, and StabilizationOptional
  19. 205Eilenberg–Mac Lane SpacesOptional
  20. 206Ordinary CohomologyOptional
  21. 207Univalent Categories and Rezk CompletionCore route
  22. 208Adjunctions, Limits, and Colimits in Univalent CategoriesCore route
  23. 209Simplicial Type Theory and Synthetic Infinity-CategoriesOptional
  24. 210Set-Level Mathematics in Univalent FoundationsCore route
  25. 211Completions and the Real NumbersCore route
  26. 212Choice-Free HII Cauchy CompletionOptional
  27. 213Displayed Type Theory and Semisimplicial TypesOptional

Search the book

Type to search the local edition.