Canonicity of Weak ω-groupoid Laws Using Parametricity Theory

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.