Homotopy limits in type theory

DOI10.1017/S0960129514000498zbMath1362.18004arXiv1304.0680MaRDI QIDQ5740649

Peter LeFanu Lumsdaine, Krzysztof Kapulkin, Jeremy Avigad

Publication date: 27 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1304.0680

Mathematics Subject Classification ID

Topological categories, foundations of homotopy theory (55U40) Foundations, relations to logic and deductive systems (18A15)

Related Items (13)

Localization in Homotopy Type Theory ⋮ Constructive sheaf models of type theory ⋮ Frames in cofibration categories ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Unnamed Item ⋮ Homotopy groups of cubical sets ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Nilpotent types and fracture squares in homotopy type theory ⋮ Indexed type theories ⋮ Exact completion of path categories and algebraic set theory. I: Exact completion of path categories ⋮ Quasicategories of frames of cofibration categories ⋮ The homotopy theory of type theories ⋮ Model structures on categories of models of type theories

Uses Software

• Coq

Cites Work

• The identity type weak factorisation system
• Homotopy limits, completions and localizations
• Types are weak ω -groupoids
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• Pull-Backs in Homotopy Theory
• A Machine-Checked Proof of the Odd Order Theorem
• Abstract homotopy theory and generalized sheaf cohomology

This page was built for publication: Homotopy limits in type theory