A syntactical approach to weak omega-groupoids

DOI10.4230/LIPICS.CSL.2012.16MaRDI QIDQ4649535zbMATH OpenFDO

Authors Thorsten Altenkirch, Ondrej Rypacek

Publication date 22 November 2012

zbMATH Keywords

category theorytype theoryhigher-dimensional structures

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)

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 -groupoid laws using parametricity theory

Cited in

(8)

• Monoidal weak ω-categories as models of a type theory
• Constructing higher inductive types as groupoid quotients
• Types are weak \(\omega \)-groupoids
• Canonicity of weak \(\omega\)-groupoid laws using parametricity theory
• Weak omega-categories from intensional type theory
• The construction of set-truncated higher inductive types
• Hom weak ω-categories of a weak ω-category
• Note on the construction of globular weak omega-groupoids from types, topological spaces\dots

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)