[Agda] Are there unicorns in Agda?

[Martin Escardo]

I would like to know whether there are unicorns in Martin-Lof type 
theory with universes. By a universe I don't mean an inductively defined 
gadget, but simply something like Set in Agda.

A unicorn is a map F : Set → Two, where Two is the two-element set, such 
that there are sets X and Y with F X ≠ F Y.

Agda allows one to formalize the specification of a unicorn, and I 
believe this makes sense in ML type theory too (but please correct me if 
I am wrong). This is done in the short module enclosed below, which
type checks and compiles. It ends by postulating unicorns.

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.

I am looking for syntactical, model-theoretic, and philosophical 
arguments regarding the (non-)existence of unicorns.

There was a discussion in this list that allowed to find unicorns by 
pattern matching with type constructors. But this is syntactical and 
intrinsically non-extensional, and it is not in the realm of ML type 
theory. (And had the philosophical problems you discussed in that thread.)

(The reason I am interested in (the non-existence of) unicorns is that, 
together with someone else, I am trying to find a topological model of 
type theory with a chain of universes, such as "Set i" in Agda. With 
just one universe, such models are known to exist. A unicorn would be a 
non-trivial definable clopen of the first universe "Set 0", before we 
know what the topological model is. The existence of unicorns one of the 
first natural questions regarding the topology of universes.)

Martin
--
module Unicorn where

data Two : Set₀ where
  zero : Two
  one  : Two

Prp₀ = Set₀

data _≡₀_ {X : Set₀} : X → X → Prp₀ where
   refl : {x : X} → x ≡₀ x

Prp₁ = Set₁

data _∧₁_ (A B : Prp₁) : Prp₁ where
   ∧₁-intro : A → B → A ∧₁ B

data ∃₁ {X : Set₁} (A : X → Prp₁) : Prp₁ where
      ∃₁-intro : (x : X) → A x → ∃₁ \(x : X) → A x

data Up (X : Set₀) : Set₁ where
      up : X → Up X

unicorn : (Set₀ → Two) → Prp₁
unicorn F = ∃₁ \(X : Set) → ∃₁ \(Y : Set) →
             Up(F X ≡₀ zero) ∧₁ Up(F Y ≡₀ one)

postulate a-unicorn : ∃₁ \(F : Set → Two) → unicorn F

-- Can this be proved in Agda or ML type theory?

not-a-unicorn : Set → Two
not-a-unicorn X = zero