[Agda] Absurd patterns and HoTT

[Martin Escardo]

On 20/05/2021 18:43, Jesper at sikanda.be wrote:
> Hi Felix and Martin
> 
> My thesis (and Conor McBride's before that) presents exactly what
> features you need in your type theory for absurd matches to be
> permissible: a universe and large elimination into this universe. This
> allows you to construct the type NoConfusion stating structural equality
> of two elements of a datatype, and the proof noConfusion that
> NoConfusion holds on the diagonal. From this, injectivity and
> disjointness of constructors follows. These principles are used in turn
> by the unification algorithm that is used during the elaboration of
> pattern matching (well, "used" in theory, since Agda does not actually
> perform the translation to eliminators). The equations package for Coq
> actually implements the translation, so you could try that if you don't
> believe me and want to see the elaborated terms :)

OK. I believe you. But let me understand what I am believing: what is
exactly the meta-theorem you prove?

Thanks,
Martin