[Agda] Are there unicorns in Agda?

[Martin Escardo]

Thanks for this.

On 11/11/11 13:37, Altenkirch Thorsten wrote:
> I believe using Jean-Phillipes general version of parametricity the 
> interpretation of Set -> Bool gives rise to the following relation f ~ g 
> = (A B : Set)(R : A -> B -> Set) -> f A = g B. In particular an element 
> is only related to itself, if it is a constant function. 

And for the other comments too.

Best,
Martin