Homotopy-Theoretic Models of Type Theory

DOI10.1007/978-3-642-21691-6_7zbMath1331.03044arXiv1208.5683OpenAlexW2120323684MaRDI QIDQ3007656

Krzysztof Kapulkin, Peter 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)

Related Items (5)

The Local Universes Model ⋮ Homotopy-Theoretic Models of Type Theory ⋮ Univalence in locally Cartesian closed categories ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Univalence and completeness of Segal objects

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On left and right model categories and left and right Bousfield localizations
• Lectures on the Curry-Howard isomorphism
• The identity type weak factorisation system
• \(\mathbb{A}^1\)-homotopy theory
• Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
• Théories homotopiques dans les topos. (Homotopy theories in topoi)
• Homotopical algebra
• Weak omega-categories from intensional type theory
• Topological and Simplicial Models of Identity Types
• Homotopy-Theoretic Models of Type Theory
• Locally cartesian closed categories and type theory
• Homotopy theoretic models of identity types
• Polynomial functors and polynomial monads
• Type Theory and Homotopy
• Higher Topos Theory (AM-170)
• \(\mathbb{A}^1\)-homotopy theory of schemes
• Every homotopy theory of simplicial algebras admits a proper model

This page was built for publication: Homotopy-Theoretic Models of Type Theory