[Agda] Absurd patterns and HoTT

[Martin Escardo]

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

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe