Canonicity of weak \(\omega\)-groupoid laws using parametricity theory

DOI10.1016/J.ENTCS.2014.10.013zbMath1337.03016OpenAlexW2036487200WikidataQ113317841 ScholiaQ113317841MaRDI QIDQ283766

Marc Lasson

Publication date: 13 May 2016

Full work available at URL: https://doi.org/10.1016/j.entcs.2014.10.013

zbMATH Keywords

loop spacesgroupoidstype theoryidentity typesparametricity

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topological categories, foundations of homotopy theory (55U40)

Related Items (3)

Unnamed Item ⋮ The \textsc{MetaCoq} project ⋮ A Syntax for Higher Inductive-Inductive Types

Uses Software

• Automath

Cites Work

• Unnamed Item
• Inductive families
• Proofs for free
• Types are weak ω -groupoids
• Weak ω-Categories from Intensional Type Theory
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: Canonicity of weak \(\omega\)-groupoid laws using parametricity theory