Homotopy theoretic models of identity types

Abstract

This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.

11 pages

Cited by in corpus (27)

• Univalent categories and the Rezk completion
• Algebraic weak factorisation systems I: accessible AWFS
• The local universes model: an overlooked coherence construction for dependent type theories
• Univalence for inverse diagrams and homotopy canonicity
• Two-dimensional models of type theory
• Quotient inductive-inductive types
• An introduction to univalent foundations for mathematicians
• Semantics of higher inductive types
• Homotopy Type Theory in Lean
• Homotopy limits in type theory
• Homotopy Theoretic Models of Type Theory
• Intensionality, Definability and Computation
• Towards a constructive simplicial model of Univalent Foundations
• Database queries and constraints via lifting problems
• Topological Quantum Gates in Homotopy Type Theory
• Models of Martin-Löf type theory from algebraic weak factorisation systems
• A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
• The Quantum Monadology
• Modal Fracture of Higher Groups
• On the $\infty$-topos semantics of homotopy type theory
• Identity types and weak factorization systems in Cauchy complete categories
• First-order homotopical logic
• The effective model structure and $\infty$-groupoid objects
• Comparing semantic frameworks for dependently-sorted algebraic theories
• Zigzag normalisation for associative $n$-categories
• Towards enriched universal algebra
• Naive cubical type theory