[Agda] Absurd patterns and HoTT

[Felix Cherubini]

Thanks Martin!
Does it mean I shouldn't use absurd patterns (except if they clearly 
correspond to the elimination rule for the Empty type) when using Agda 
as a proof assistant for HoTT?
Is it possible to enforce that? I didn't find an option mentioning 
anything about absurd...


On 5/20/21 6:34 PM, Martin Escardo wrote:
> In MLTT, the underlying type theory of Book-HoTT, you can't prove true
> == false -> Empty without a universe. Your "ok" proof doesn't use a
> universe. It is not clear what kind of type theory Agda is implementing
> here. Martin
> 
> On 20/05/2021 16:59, felix.wellen at posteo.de wrote:
>> Dear all,
>>
>> are function definitions using the absurd pattern compatible with
>> Book-HoTT?
>>
>> With compatible, I mean, that there should be a general procedure that
>> translates definitions by pattern matching from Agda to Book-HoTT.
>>
>> Here is an example: Let Bool be the type with constructors true and
>> false and Empty the type without constructors, then
>>
>> ok : true == false -> Empty
>> ok ()
>>
>> works in Agda (for the usual inductive definition of ==). As I
>> understand it, Agda checks if for any constructor of the domain, the
>> unification problems for all arguments end in conflict. Or in other
>> words, the absurd pattern is a valid definition for a function on an
>> inductive type, if it is not possible to find a constructor of the
>> inductive type together with arguments make it have the right type.
>>
>> This is very different from any proof of that fact I know in Book-HoTT
>> (one would be use a transport along the equality true==false that lands
>> in Empty). And I also don't know how the general argument ("there is no
>> valid constructor call, therefore...") could be done in HoTT.
>>
>> Thanks in advance for sheding any light on the matter!
>> Best,
>> Felix
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>