[Agda] Are there unicorns in Agda?

[Martin Escardo]

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.


Now I realize that what you describe actually does happen in classical 
topology too.

Let U be an indiscrete space with two distinct points a and b, and let 
Bool have the discrete topology. Now define the space

    U'={(x,p)  in X x Bool | p=False -> x=a, p=True -> x=b}

The first projection into U is a monomorphism, but U' is not a subspace 
of U, because the second projection is a monomorphism too, which forces 
the topology of U' to be discrete.

When you "compile" the formula you give above in the topological topos, 
you get something like U', by definition of the interpretation of Sigma.

This is why you got the discrete topology.

Similarly, the space Q={(x,m,n) in R x Z x N | x=m/(n+1) and gcd(m,n)=1}
is discrete, even though the first projection into R is a monomorphism. 
This is what the topological-topos compiler produces when you take the 
subspace of rational numbers. In practice, it becomes discrete because 
you can decide equality on Q. (As you showed above in your example.)

Martin