<div dir="ltr"><div>Hi Martin,<br></div><div><br></div><div>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.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, May 20, 2021 at 8:56 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
<br>
On 20/05/2021 18:43, <a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a> wrote:<br>
> Hi Felix and Martin<br>
> <br>
> My thesis (and Conor McBride's before that) presents exactly what<br>
> features you need in your type theory for absurd matches to be<br>
> permissible: a universe and large elimination into this universe. This<br>
> allows you to construct the type NoConfusion stating structural equality<br>
> of two elements of a datatype, and the proof noConfusion that<br>
> NoConfusion holds on the diagonal. From this, injectivity and<br>
> disjointness of constructors follows. These principles are used in turn<br>
> by the unification algorithm that is used during the elaboration of<br>
> pattern matching (well, "used" in theory, since Agda does not actually<br>
> perform the translation to eliminators). The equations package for Coq<br>
> actually implements the translation, so you could try that if you don't<br>
> believe me and want to see the elaborated terms :)<br>
<br>
OK. I believe you. But let me understand what I am believing: what is<br>
exactly the meta-theorem you prove?<br>
<br>
Thanks,<br>
Martin<br>
</blockquote></div>