Homotopy limits in type theory

Abstract

Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.

33 pages; v3: theorem numbering changed since v2 to match journal version

References in corpus (3)

• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• Univalent categories and the Rezk completion

Cited by in corpus (5)

• The homotopy theory of type theories
• Nilpotent Types and Fracture Squares in Homotopy Type Theory
• Locally Cartesian Closed Quasicategories from Type Theory
• Indexed type theories
• Homotopical inverse diagrams in categories with attributes