Homotopy theoretic models of identity types
From MaRDI portal
Publication:3598111
DOI10.1017/S0305004108001783zbMath1205.03065arXiv0709.0248WikidataQ56831024 ScholiaQ56831024MaRDI QIDQ3598111
Michael A. Warren, Steven 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
Homotopy equivalences in algebraic topology (55P10) Homotopy extension properties, cofibrations in algebraic topology (55P05) Structure of proofs (03F07) Metamathematics of constructive systems (03F50)
Related Items
Homotopies in Grothendieck fibrations, 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, Unnamed Item, A characterisation of elementary fibrations, Homotopical patch theory, Games for Dependent Types, Naive cubical type theory, Game semantics for dependent types, Homotopy type theory and Voevodsky’s univalent foundations, Martin-Löf complexes, Algebraic weak factorisation systems. I: Accessible AWFS., Unnamed Item, Homotopy type theory in Lean, Meaning explanations at higher dimension, A formal logic for formal category theory, The Local Universes Model, Identity types and weak factorization systems in Cauchy complete categories, 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, Identity and intensionality in univalent foundations and philosophy, Five stages of accepting constructive mathematics, Univalent foundations as structuralist foundations, Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics, Mathematical models of abstract systems: knowing abstract geometric forms, Unnamed Item, Denotational semantics for guarded dependent type theory, Mathesis Universalis and Homotopy Type Theory, From Mathesis Universalis to Provability, Computability, and Constructivity, Brouwer's fixed-point theorem in real-cohesive homotopy type theory, Homotopy-Theoretic Models of Type Theory, Exact completion of path categories and algebraic set theory. I: Exact completion of path categories, Unnamed Item, Univalence in locally Cartesian closed categories, The identity type weak factorisation system, Revisiting the categorical interpretation of dependent type theory, CATEGORICAL FOUNDATIONS OF MATHEMATICS OR HOW TO PROVIDE FOUNDATIONS FORABSTRACTMATHEMATICS, 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, An introduction to univalent foundations for mathematicians, Unnamed Item, Univalence as a principle of logic, The simplicial model of univalent foundations (after Voevodsky), Semantics of higher inductive types, A cubical model of homotopy type theory, Isomorphism is equality, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, 2010 North American Annual Meeting of the Association for Symbolic Logic, A meaning explanation for HoTT, Weak ω-Categories from Intensional Type Theory, Two-dimensional models of type theory, The univalence axiom in cubical sets, A homotopy-theoretic model of function extensionality in the effective topos, Type Theory and Homotopy, Natural models of homotopy type theory, The effective model structure and -groupoid objects, MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS, A rewriting coherence theorem with applications in homotopy type theory
Cites Work
