[Agda] Absurd question

[Andreas Abel]

Agda does not have extensionality for functions over the empty type 
(hard to check, since emptiness is not decidable).

However, it could accept absurd lambdas as equal.

I created a ticket for this:

   http://code.google.com/p/agda/issues/detail?id=857

I guess Ulf did not consider \() worthy of being an expression in the 
internal language of Agda, hence the trickery with creating local 
functions with absurd matches.

Cheers,
Andreas

On 24.05.2013 19:33, Martin Escardo wrote:
> Nice, Andrea. I now fully understand the two questions I made:
>
> On 24/05/13 18:02, Andrea Vezzosi wrote:
>> The crucial point is that (\()) is not equal to (\()),
>
> Fair enough, an absurd question deserves an absurd answer.
>
>> main : P (\())
>> main = lemma (\())
>
> You are saying this would only type-check if \() in the first line
> where the same as \() in the second line, which it isn't.
>
> Here is a further simplification of your example:
>
> module simpler where
>
> data _==_ {X : Set} : X -> X -> Set where
>    refl : {x : X} -> x == x
>
> data Empty : Set where
>
> _===_ : (Empty -> Empty) -> (Empty -> Empty) -> Set
> f === g = f == g
>
> absurd-equality : (\()) === (\())
> absurd-equality = { }
>
> Now, the type of the goal is
>
>   ?0 : .simpler.absurd == .simpler.absurd
>
> If you try to put refl in the hole, Agda tells you:
>
>   .simpler.absurd x != .simpler.absurd x of type Empty
>   when checking that the expression refl has type
>   .simpler.absurd == .simpler.absurd
>
> Best,
> Martin



-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/