[Agda] Are there unicorns in Agda?

[Martin Escardo]

This is an interesting phenomenon, which seems to contradict topological 
intuition: a subspace of an indiscrete space must be indiscrete!

What is going on here is that subobject doesn't coincide with subspace. 
Already in the topological topos briefly mentioned in my note, the 
subobject of rational numbers of the Dedekind reals has the discrete 
topology, but the reals have the Euclidean topology which induces a 
non-discrete subspace topology on the reals.

In fact, even in the category of topological spaces, subobject is not 
the same thing as subspace (the example of the discrete rationals in the 
Euclidean reals works there).

In topology, the correct notion of subobject, to capture subspace, is 
*regular* monomorphism.

So your example must be failing to be a subspace of the universe, 
although it is certainly a subobject.

Martin

On 10/02/12 12:22, Vladimir Voevodsky wrote:
> A comment. While, as Martin shows,  the intrinsic topology of the universe may be indiscrete (any sequences converges to any point) this is not true of the subtypes of the universe. For example the subtype consisting of the types which are isomorphic to the unit type or the empty type admits a function to bool.
>
> Vladimir.
>
>
> On Feb 9, 2012, at 8:27 PM, Martin Escardo wrote:
>
>>
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>