Homotopy-Theoretic Models of Type Theory
From MaRDI portal
Publication:3007656
DOI10.1007/978-3-642-21691-6_7zbMath1331.03044arXiv1208.5683MaRDI 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
03G30: Categorical logic, topoi
Related Items
Univalence in locally Cartesian closed categories, The simplicial model of univalent foundations (after Voevodsky), The Local Universes Model, Homotopy-Theoretic Models of Type Theory
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
