[Agda] Are there unicorns in Agda?

[Dan Doel]

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