[Agda] Absurd patterns and HoTT

[Felix Cherubini]

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