Canonicity of Weak ω-groupoid Laws Using Parametricity Theory
Résumé
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.
Domaines
Informatique
Origine : Fichiers produits par l'(les) auteur(s)
Loading...