[Agda] Absurd question

[Martin Escardo]

On 24/05/13 18:33, Martin Escardo wrote:
> 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.

(Of course, this was an irresistible joke.)

The "crucial point" allowed me to streamline, as I wanted, my proof. 
Before I was fighting blindly against Agda without knowing what was 
wrong, but now, knowing what the problem is, I could write a nicer 
version of the proof.

Andreas (Abel) proposed a ticket to let \() be the same as \(), as it 
should. My streamlined version of the proof wouldn't benefit from that. 
But this equality would have saved several hours of my fruitless 
attempts, and so I think this ticket is important (everybody often 
writes an ugly proof first, and a number of us try to make it look 
prettier after success.)

Very many thanks to those who made me understand the problem.

Best,
Martin