[Agda] Absurd patterns and HoTT

[Jesper Cockx]

Hi Martin,

The meta-theorem is that for any definition by dependent pattern matching,
there exists an equivalent one that only uses basic datatype eliminators,
and that satisfies (at least) the same definitional equalities.

-- Jesper

On Thu, May 20, 2021 at 8:56 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

>
>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210520/297dee1d/attachment.html>