[Agda] Are there unicorns in Agda?

[Martin Escardo]

Your observation also shows that my audacious conjecture in the note may 
indeed be a bit too audacious! Martin

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