A syntactical approach to weak omega-groupoids
From MaRDI portal
Publication:4649535
DOI10.4230/LIPICS.CSL.2012.16zbMATH Open1252.68058MaRDI QIDQ4649535FDOQ4649535
Authors: Thorsten Altenkirch, Ondrej Rypacek 
Publication date: 22 November 2012
Recommendations
- Types are weak \(\omega \)-groupoids
- Homotopy theoretic models of identity types
- Weak omega-categories from intensional type theory
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)
Cited In (8)
- Monoidal weak ω-categories as models of a type theory
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
- Note on the construction of globular weak omega-groupoids from types, topological spaces\dots
- Hom weak ω-categories of a weak ω-category
- Constructing higher inductive types as groupoid quotients
- Weak omega-categories from intensional type theory
- The construction of set-truncated higher inductive types
- Types are weak \(\omega \)-groupoids
This page was built for publication: A syntactical approach to weak omega-groupoids
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649535)
