[Agda] Are there unicorns in Agda?

[Martin Escardo]

I want to advertise the secret powers of topological thinking in
constructive mathematics and type theory, and hence in Agda.

http://www.cs.bham.ac.uk/~mhe/papers/universe/RicesTheoremForTheUniverse.html

http://www.cs.bham.ac.uk/~mhe/papers/universe/TheTopologyOfTheUniverse.html

A while ago I asked whether there are "unicorns" in type theory.

The best answer I got is that they are ruled out by
parametricity. And this was a good answer. This technique is
really nice, and congratulations to those who extended it to
dependent types! It also gives that all definable closed terms are
extensional, which I love, and which is absolutely essential to do
any kind of serious work in constructive mathematics in Agda.

Here I offer a different kind of answer to the unicorn question,
going beyond the original question. Inside type theory, we can
show that the hypothetical existence of a unicorn allows you to
solve the Halting Problem (technically, to derive WLPO). This
development is syntax-free, in fact. Now matter how many axioms
you postulate in type theory, sensible or not, the Unicorn Theorem
survives: Unicorns can only exist in a world where WLPO exists
(WLPO is a unicorn of constructive mathematics).

Say that a decidable property P : Set → Bool (a unicorn) is
extensional if it has the same boolean value for any two
isomorphic types in Set.

Rice's Theorem holds for the universe Set: there is no
non-trivial, extensional, decidable property of the universe. Here
is a proof written in Agda:

http://www.cs.bham.ac.uk/~mhe/papers/universe/RicesTheoremForTheUniverse.html

I assume extensionality to prove it, BUT a meta-corollary is that,
even without assuming extensionality, there are no definable
unicorns, as is explained in that file, again in a syntax-free way.

But the non-trivial and interesting technical work is not done in
the above file. It is done in

http://www.cs.bham.ac.uk/~mhe/papers/universe/TheTopologyOfTheUniverse.html

which proves a stronger result: the intrinsic topology of Set,
accessible within Agda without any axioms other than
extensionality, is indiscrete: every sequence of types has any
desired type as its limit.

Best wishes,
Martin

On 11/11/11 01:13, Martin Escardo wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe