Canonicity of Weak ω-groupoid Laws Using Parametricity Theory

Marc Lasson (1, 2)

1 PPS - Preuves, Programmes et Systèmes
2 PI.R2 - Design, study and implementation of languages for proofs and programs

We show that terms witnessing a groupoid law from the ω-groupoid structure of types are all propositionally equal. Our proof reduce this problem to the unicity of the canonical point in the n-th loop space and conclude using Bernardy's parametricity theory for dependent types.

Mots clés: type theory; parametricity; loop spaces; groupoids; identity types

Domaines: Informatique

Marc Lasson. Canonicity of Weak ω-groupoid Laws Using Parametricity Theory. MFPS 2014, Jun 2014, Ithaca, United States. pp.229 - 244, ⟨10.1016/j.entcs.2014.10.013⟩. ⟨hal-01105252⟩