Homotopy limits in type theory

DOI10.1017/S0960129514000498MaRDI QIDQ5740649zbMATH OpenFDO

Authors Jeremy Avigad, Krzysztof Kapulkin, Peter Lefanu Lumsdaine

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

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

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.

Recommendations

• Sequential colimits in homotopy type theory
• Inductive types in homotopy type theory
• Homotopy type theory in Lean
• Homotopy type theory and Voevodsky's univalent foundations
• Homotopical inverse diagrams in categories with attributes

Cites work

• A machine-checked proof of the odd order theorem
• Abstract homotopy theory and generalized sheaf cohomology
• Homotopy limits, completions and localizations
• Homotopy theoretic models of identity types
• Pull-Backs in Homotopy Theory
• The identity type weak factorisation system
• Types are weak -groupoids
• Weak ω-Categories from Intensional Type Theory

Cited in

(22)

• Bounding homotopy types by geometry
• Homotopy type theory in Lean
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• The homotopy theory of type theories
• Quasicategories of frames of cofibration categories
• Homotopical inverse diagrams in categories with attributes
• Frames in cofibration categories
• Internal languages of finitely complete ( , 1)-categories
• Model structures on categories of models of type theories
• Constructing higher inductive types as groupoid quotients
• Constructive sheaf models of type theory
• Cellular cohomology in homotopy type theory
• Nilpotent types and fracture squares in homotopy type theory
• Coherence via well-foundedness. Taming set-quotients in homotopy type theory
• Sequential colimits in homotopy type theory
• Indexed type theories
• Localization in Homotopy Type Theory
• The Seifert-van Kampen Theorem in Homotopy Type Theory
• Homotopy groups of cubical sets
• -type theories
• Extensional concepts in intensional type theory, revisited
• Automated reasoning for mathematics

Describes a project that uses

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740649)