Types are weak ω -groupoids
From MaRDI portal
Publication:3079518
DOI10.1112/PLMS/PDQ026zbMath1229.18007arXiv0812.0298OpenAlexW3100912421WikidataQ59757172 ScholiaQ59757172MaRDI QIDQ3079518
Richard Garner, Benno van den Berg
Publication date: 2 March 2011
Published in: Proceedings of the London Mathematical Society (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0812.0298
Related Items (31)
Modeling Martin-Löf type theory in categories ⋮ Canonicity of weak \(\omega\)-groupoid laws using parametricity theory ⋮ The construction of set-truncated higher inductive types ⋮ Homotopical patch theory ⋮ Hom weak ω-categories of a weak ω-category ⋮ Homotopy type theory and Voevodsky’s univalent foundations ⋮ A proof of the existence of Batanin's initial operad ⋮ Martin-Löf complexes ⋮ Internal languages of finitely complete \((\infty , 1)\)-categories ⋮ Unnamed Item ⋮ Meaning explanations at higher dimension ⋮ Martin-Löf identity types in C-systems ⋮ Monoidal weak ω-categories as models of a type theory ⋮ Bicategorical type theory: semantics and syntax ⋮ On the ∞$\infty$‐topos semantics of homotopy type theory ⋮ Homotopical inverse diagrams in categories with attributes ⋮ Unnamed Item ⋮ A type theory for synthetic $\infty$-categories ⋮ Mathesis Universalis and Homotopy Type Theory ⋮ Univalence in locally Cartesian closed categories ⋮ 2-Dimensional Directed Type Theory ⋮ Introduction – from type theory and homotopy theory to univalent foundations ⋮ Homotopy limits in type theory ⋮ A notion of homotopy for the effective topos ⋮ Univalence for inverse diagrams and homotopy canonicity ⋮ Unnamed Item ⋮ The simplicial model of univalent foundations (after Voevodsky) ⋮ Weak ω-Categories from Intensional Type Theory ⋮ A homotopy-theoretic model of function extensionality in the effective topos ⋮ Type Theory and Homotopy ⋮ A rewriting coherence theorem with applications in homotopy type theory
This page was built for publication: Types are weak ω -groupoids
