Homotopy-theoretic models of type theory

DOI10.1007/978-3-642-21691-6_7MaRDI QIDQ3007656zbMATH OpenOpenAlexFDO

Authors Krzysztof Kapulkin, P. F. Arndt

Publication date 17 June 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Categorical logic, topoi (03G30)

Abstract: We introduce the notion of a logical model category which is a Quillen model category satisfying some additional conditions. Those conditions provide enough expressive power that one can soundly interpret dependent products and sums in it. On the other hand, those conditions are easy to check and provide a wide class of models some of which are listed in the paper.

Recommendations

• Homotopy theoretic models of identity types
• Natural models of homotopy type theory
• A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
• Topological and simplicial models of identity types
• Model structures on categories of models of type theories

Cites work

• \(\mathbb{A}^1\)-homotopy theory
• \(\mathbb{A}^1\)-homotopy theory of schemes
• Every homotopy theory of simplicial algebras admits a proper model
• Higher Topos Theory (AM-170)
• Homotopical algebra
• Homotopy theoretic models of identity types
• Homotopy-theoretic models of type theory
• scientific article; zbMATH DE number 2134022 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1226952 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1860105 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Locally cartesian closed categories and type theory
• Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
• On left and right model categories and left and right Bousfield localizations
• Polynomial functors and polynomial monads
• The identity type weak factorisation system
• Théories homotopiques dans les topos. (Homotopy theories in topoi)
• Topological and simplicial models of identity types
• Type theory and homotopy
• Weak omega-categories from intensional type theory

Cited in

(28)

• The homotopy theory of type theories
• The simplicial model of univalent foundations (after Voevodsky)
• Univalence and completeness of Segal objects
• On a model invariance problem in homotopy type theory
• Algebraic models for homotopy types
• Modeling Martin-Löf type theory in categories
• Homotopy Type Theory
• Topological and simplicial models of identity types
• The local universes model: an overlooked coherence construction for dependent type theories
• Homotopy-theoretic models of type theory
• A homotopy-theoretic model of function extensionality in the effective topos
• Natural models of homotopy type theory
• Mathesis Universalis and Homotopy Type Theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Combinatorial realizability models of type theory
• Models of type theory based on Moore paths
• Semantics of higher inductive types
• Model structure on the universe of all types in interval type theory
• Homotopy Type Theory: A synthetic approach to higher equalities
• Synthetic topology in Homotopy Type Theory for probabilistic programming
• Models of Type Theory Based on Moore Paths
• Fibred fibration categories
• Dialectica models of type theory
• Modalities in homotopy type theory
• Univalence in locally Cartesian closed categories
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• -type theories
• Limits and colimits in synthetic -categories

This page was built for publication: Homotopy-theoretic models of type theory

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