[Agda] Are there unicorns in Agda?

[Martin Escardo]

Ok, that would count as a nice syntactical answer. (I am still 
interested in knowing what happens in the models.)

But what is precisely your answer? For example, although there may not 
be non-constant maps F:Set->X with X:Set, there certainly are 
non-constant maps F':Set->Set. What is the precise formulation of 
parametricity for ML type theory with a chain of universes, at least 
specialized to these small examples, that allows to see the absence of 
unicorns? (I explicitly said that the universes under consideration 
don't have eliminators.)

Martin

On 11/11/11 05:53, Dan Doel wrote:
> On Thu, Nov 10, 2011 at 5:13 PM, Martin Escardo<m.escardo at cs.bham.ac.uk>  wrote:
>> My question is, can one replace the final postulate by an actual
>> construction of a unicorn? (So that the resulting Agda code makes sense in
>> ML type theory.) More generally, are there non-constant maps F : Set → X
>> where X : Set? This more general question is not formulated in the Agda file
>> below, but it could.
>
> The answer should be no. Set is expected to have parametricity
> theorems similar to those in System F and the like. The free theorem
> for F : Set ->  X---for any particular X : Set---is:
>
>      forall A B : Set. F A = F B
>
> The same should be true for ML universes that don't have
> induction-recursion style eliminators (although whether they do
> depends on who you ask, I guess).
>
> -- Dan