Type Theory and Homotopy

DOI10.1007/978-94-007-4435-6_9zbMath1314.03013arXiv1010.1810OpenAlexW1481038699WikidataQ56450152 ScholiaQ56450152MaRDI QIDQ5253928

Steven Awodey

Publication date: 5 June 2015

Published in: Epistemology versus Ontology (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Homotopy theory (55P99) Second- and higher-order arithmetic and fragments (03F35)

Related Items (max. 100)

Homotopy type theory and Voevodsky’s univalent foundations ⋮ Martin-Löf complexes ⋮ Combinatorial realizability models of type theory ⋮ The Local Universes Model ⋮ Combining higher-order logic with set theory formalizations ⋮ Carnap and the invariance of logical truth ⋮ Idempotents in intensional type theory ⋮ Homotopy-Theoretic Models of Type Theory ⋮ A univalent formalization of the p-adic numbers ⋮ Univalence as a principle of logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic model structures
• The identity type weak factorisation system
• Generalized algebraic theories and contextual categories
• Constructions of factorization systems in categories
• Monoidal globular categories as a natural environment for the theory of weak \(n\)-categories
• Categorical logic and type theory
• Wellfounded trees in categories
• The petit topos of globular sets
• Quasi-categories and Kan complexes
• An \(\omega\)-category with all duals is an \(\omega\)-groupoid
• Homotopical algebra
• Topological and Simplicial Models of Identity Types
• Types are weak ω -groupoids
• Locally cartesian closed categories and type theory
• An extension of the Galois theory of Grothendieck
• Two-dimensional models of type theory
• Homotopy theoretic models of identity types
• Weak ω-Categories from Intensional Type Theory
• From Groups to Groupoids: a Brief Survey
• Strong stacks and classifying spaces
• Internal type theory
• Higher Topos Theory (AM-170)
• Understanding the small object argument
• \(\mathbb{A}^1\)-homotopy theory of schemes
• Type theories, toposes and constructive set theory: Predicative aspects of AST

This page was built for publication: Type Theory and Homotopy