Homotopy theoretic models of identity types

DOI10.1017/S0305004108001783MaRDI QIDQ3598111zbMATH OpenWikidataFDO

Authors Michael A. Warren, Steve Awodey

Publication date 30 January 2009

Published in Mathematical Proceedings of the Cambridge Philosophical Society (Search for Journal in Brave)

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

zbMATH Keywords

homotopy theoryQuillen model categoriestype theory

Mathematics Subject Classification ID

Structure of proofs (03F07) Metamathematics of constructive systems (03F50) Homotopy extension properties, cofibrations in algebraic topology (55P05) Homotopy equivalences in algebraic topology (55P10)

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.

Recommendations

• The strict \(\omega\)-groupoid interpretation of type theory
• On the identity type as the type of computational paths
• Elementary fibrations of enriched groupoids
• Generalizations of Hedberg's theorem
• Martin Hofmann’s contributions to type theory: Groupoids and univalence
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• The category of equilogical spaces and the effective topos as homotopical quotients
• Topological and simplicial models of identity types
• The genesis of the groupoid model
• The justification of identity elimination in Martin-Löf's type theory

Cites work

• \(\mathbb{A}^1\)-homotopy theory of schemes
• Constructions of factorization systems in categories
• Fibered categories and the foundations of naive category theory
• Homotopical algebra
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• Locally cartesian closed categories and type theory
• Quasi-categories and Kan complexes

Cited in

(only showing first 100 items - show all)

• Game semantics for dependent types
• Homotopy type theory in Lean
• Meaning explanations at higher dimension
• Univalent foundations as structuralist foundations
• Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
• Univalence as a principle of logic
• A cubical model of homotopy type theory
• The simplicial model of univalent foundations (after Voevodsky)
• A meaning explanation for HoTT
• A characterisation of elementary fibrations
• Revisiting the categorical interpretation of dependent type theory
• The univalence axiom in cubical sets
• Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics
• Mathematical models of abstract systems: knowing abstract geometric forms
• Identity and intensionality in univalent foundations and philosophy
• Modeling Martin-Löf type theory in categories
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Canonicity of weak -groupoid laws using parametricity theory
• Homotopy type theory and Voevodsky's univalent foundations
• Topological and simplicial models of identity types
• The local universes model: an overlooked coherence construction for dependent type theories
• Notions of anonymous existence in Martin-Löf type theory
• Homotopy-theoretic models of type theory
• 2010 North American Annual Meeting of the Association for Symbolic Logic
• The strict \(\omega\)-groupoid interpretation of type theory
• A homotopy-theoretic model of function extensionality in the effective topos
• The Cayley-Dickson construction in homotopy type theory
• Natural models of homotopy type theory
• Homotopies in Grothendieck fibrations
• Mathesis Universalis and Homotopy Type Theory
• From mathesis universalis to provability, computability, and constructivity
• Two-dimensional models of type theory
• Games for dependent types
• Weak ω-Categories from Intensional Type Theory
• Martin-Löf complexes
• Combinatorial realizability models of type theory
• A coherence theorem for Martin-Löf's type theory
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• Path categories and propositional identity types
• Models of type theory based on Moore paths
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• A syntactical approach to weak omega-groupoids
• An introduction to univalent foundations for mathematicians
• Categorical foundations of mathematics. Or how to provide foundations for abstract mathematics.
• Semantics of higher inductive types
• Constructing higher inductive types as groupoid quotients
• Model structure on the universe of all types in interval type theory
• Internal parametricity for cubical type theory
• Naive cubical type theory
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• A cubical language for Bishop sets
• Identity types and weak factorization systems in Cauchy complete categories
• Models of Type Theory Based on Moore Paths
• Typal heterogeneous equality types
• Five stages of accepting constructive mathematics
• Denotational semantics for guarded dependent type theory
• Univalence in locally Cartesian closed categories
• Type theory and homotopy
• Generalizations of Hedberg's theorem
• Homotopical patch theory
• 2-Dimensional Directed Type Theory
• Database queries and constraints via lifting problems
• Introduction -- from type theory and homotopy theory to univalent foundations
• Homotopy limits in type theory
• A generalization of the Takeuti-Gandy interpretation
• A notion of homotopy for the effective topos
• Univalence for inverse diagrams and homotopy canonicity
• The effective model structure and \(\infty\)-groupoid objects
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• A rewriting coherence theorem with applications in homotopy type theory
• A formal logic for formal category theory
• Martin-Löf identity types in C-systems
• On the ∞$\infty$‐topos semantics of homotopy type theory
• Steps toward a philosophy for mathematicians
• Towards a constructive simplicial model of Univalent Foundations
• Internal sums for synthetic fibered (,1)-categories
• Poincaré on the value of reasoning machines
• Topological quantum gates in homotopy type theory
• Kripke-Joyal forcing for type theory and uniform fibrations
• Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories
• Modal fracture of higher groups
• Syllepsis in homotopy type theory
• Zigzag normalisation for associative n-categories
• Towards enriched universal algebra
• Covering spaces in homotopy type theory
• Formalizing the algebraic small object argument in UniMath
• Frobenius structure and the Beck-Chevalley condition for algebraic weak factorization systems
• Cubical approximation for directed topology. II
• -type theories
• Toward a geometry for syntax
• Computational paths -- a weak groupoid
• The quantum monadology
• First-order homotopical logic
• Delooping cyclic groups with lens spaces in homotopy type theory
• On symmetries of spheres in univalent foundations
• The category of -finite spaces
• The univalence principle
• A toolkit for structured lifts
• The equivariant model structure on cartesian cubical sets
• Isomorphism is equality

This page was built for publication: Homotopy theoretic models of identity types

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