[Agda] Absurd patterns and HoTT

[Jesper Cockx]

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 :)

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).

Cheers,
Jesper

On Thu, May 20, 2021 at 6:43 PM Felix Cherubini <felix.wellen at posteo.de>
wrote:

> 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
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210520/56feebe4/attachment.html>