[Agda] Absurd question

[Martin Escardo]

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