Canonicity of Weak ω-groupoid Laws Using Parametricity Theory
Marc Lasson · Electronic Notes in Theoretical Computer Science · 2014
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.