[Agda] Absurd patterns and HoTT

[Dan Doel]

Some absurd patterns are usable with HoTT. The obvious one is the absurd
match on the empty type:

    data Empty : Set where

Cubical Agda will let you absurd match on that type.

The absurd pattern in your example is supposed to be justified by the fact
that constructors are always disjoint (and injective). So, if unification fails
between two concrete terms, then the identity type is empty and the absurd
match is valid. This is no longer universally true in HoTT. The whole point of
HITs, for instance, is to add examples where this reasoning fails, so e.g. the
constructors for propositional truncation are not disjoint/injective.

It is still the case that absurd matches on the identity type would be justified
for booleans. However, since it's not justified in general, you have
to write the
proof yourself, because you can't just assume that you could always write
the universe-based proof (and Agda has no mechanism for specifying which
particular types it would still work for).

On Thu, May 20, 2021 at 11:59 AM Felix Cherubini <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