<div dir="ltr"><div>Hi Felix and Martin<br></div><div><br></div><div>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 :)</div><div><br></div><div>Cubical Agda will make a distinction between regular datatypes and HITs, and it will only apply injectivity and disjointness for the former ones. So long story short, you should absolutely not worry about using absurd patterns in either standard Agda or Cubical Agda (unless you somehow don't want to assume the existence of a universe or large elimination, in which case Agda is perhaps not the right tool for you).<br></div><div><br></div><div>Cheers,</div><div>Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, May 20, 2021 at 6:43 PM Felix Cherubini <<a href="mailto:felix.wellen@posteo.de">felix.wellen@posteo.de</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">Thanks Martin!<br>
Does it mean I shouldn't use absurd patterns (except if they clearly <br>
correspond to the elimination rule for the Empty type) when using Agda <br>
as a proof assistant for HoTT?<br>
Is it possible to enforce that? I didn't find an option mentioning <br>
anything about absurd...<br>
<br>
<br>
On 5/20/21 6:34 PM, Martin Escardo wrote:<br>
> In MLTT, the underlying type theory of Book-HoTT, you can't prove true<br>
> == false -> Empty without a universe. Your "ok" proof doesn't use a<br>
> universe. It is not clear what kind of type theory Agda is implementing<br>
> here. Martin<br>
> <br>
> On 20/05/2021 16:59, <a href="mailto:felix.wellen@posteo.de" target="_blank">felix.wellen@posteo.de</a> wrote:<br>
>> Dear all,<br>
>><br>
>> are function definitions using the absurd pattern compatible with<br>
>> Book-HoTT?<br>
>><br>
>> With compatible, I mean, that there should be a general procedure that<br>
>> translates definitions by pattern matching from Agda to Book-HoTT.<br>
>><br>
>> Here is an example: Let Bool be the type with constructors true and<br>
>> false and Empty the type without constructors, then<br>
>><br>
>> ok : true == false -> Empty<br>
>> ok ()<br>
>><br>
>> works in Agda (for the usual inductive definition of ==). As I<br>
>> understand it, Agda checks if for any constructor of the domain, the<br>
>> unification problems for all arguments end in conflict. Or in other<br>
>> words, the absurd pattern is a valid definition for a function on an<br>
>> inductive type, if it is not possible to find a constructor of the<br>
>> inductive type together with arguments make it have the right type.<br>
>><br>
>> This is very different from any proof of that fact I know in Book-HoTT<br>
>> (one would be use a transport along the equality true==false that lands<br>
>> in Empty). And I also don't know how the general argument ("there is no<br>
>> valid constructor call, therefore...") could be done in HoTT.<br>
>><br>
>> Thanks in advance for sheding any light on the matter!<br>
>> Best,<br>
>> Felix<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> <br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>