T h e   i n t r i n s i c   t o p o l o g y   o f   a
  M a r t i n - L o f   u n i v e r s e


    Martin Escardo, University of Birmingham, UK.
    February 2012, last updated 17 Feb 2012.
    
    This is a proof in intensional Martin-Lof type theory,
    extended with the propositional axiom of extensionality as a
    postulate, written in Agda notation. The K-rule or UIP axiom
    are not used, except in a few instances where they can be
    proved. The proof type-checks in Agda 2.3.0.


A b s t r a c t. We show that a Martin-Lof universe `a la Russell
is topologically indiscrete in a precise sense defined below. As a
corollary, we derive Rice's Theorem for the universe: it has no
non-trivial, decidable, extensional properties.


I n t r o d u c t i o n

This universe indiscreteness theorem may be surprising, because
types like the Cantor space of infinite binary sequences are far
from indiscrete in the sense considered here, as they have plenty
of decidable properties. The Cantor space also fails to be
discrete, because it doesn't have decidable equality, and this
fact shows up in the proof of Rice's Theorem.

We need to postulate the axiom of extensionality, but nothing else
(the univalence axiom would give a slightly sharper result). In
particular, Brouwerian continuity axioms are not postulated, even
though this is about topology in constructive mathematics.

We show that the universe Set, in Agda notation, is indiscrete, in
the sense that every sequence of types converges to any desired
type. Convergence is defined using ℕ∞, the generic convergent
sequence, constructed in the module GenericConvergentSequence, but
briefly introduced below.

For the sake of motivation, let's define convergence for sequences
of elements of types first.

We say that a sequence x : ℕ → X in a type X converges to a limit
x∞ : X if one can construct a "limiting sequence" x' : ℕ∞ → X such
that

     x n = x'(under n)
      x∞ = x' ∞

where under : ℕ → ℕ∞ (standing for "underline") is the embedding
of ℕ into ℕ∞. It is easy to see that every function of any two
types now becomes automatically continuous in the sense that it
preserves limits, without considering any model or any continuity
axiom within type theory. The collection of convergent sequences
defined above constitutes the intrinsic topology of the type X.

This is motivated as follows. There is an interpretation of type
theory (Johnstone's topological topos) in which types are spaces
and all functions are continuous. In this interpretation, ℕ is the
discrete space of natural numbers and the space ℕ∞ is the
one-point compactification of ℕ. Moreover, in this interpretation,
convergence defined in the above sense coincides with topological
convergence.

Using a general construction by Streicher, assuming a Grothendieck
universe in set theory, one can build a space in the topological
topos that is the interpretation of the universe.  Voevodsky asked
what the topology of this interpretation of the Martin-Lof
universe is. I don't know the answer, but it follows from what we
prove here that the quotient by type isomorphism is the indiscrete
topology.  (Moreover, I conjecture that the Grothendieck universe
with the indiscrete topology can be given the structure needed to
interpret a Martin-Lof universe `a la Russell. But this may be a
bit too audacious.)

A space is indiscrete if the only open sets are the empty set and
the whole space. It is an easy exercise, if one knows basic
topology, to show that this is equivalent to saying that every
sequence converges to any point.

The appropriate notion of equality for elements of the universe
Set of types is isomorphism. Hence we reformulate the above
definition for limits of sequences of types as follows.

We say that a sequence of types X : ℕ → Set converges to a limit
X∞ : Set if one can find a "limiting sequence" X' : ℕ∞ → X such
that

     X n ≅ X'(under n)
      X∞ ≅ X' ∞

If one assumes the univalence axiom, one can replace the
isomorphisms by equalities to get an equivalent notion. But notice
that in the topological topos isomorphism is not the same thing as
equality.

In this Agda module we show that every sequence of types converges
to any type whatsoever. This explains, in particular, why there
can't be non-trivial extensional functions Set → ₂, where ₂ is the
discrete type of binary numbers. Such functions are the
(continuous characteristic functions of) clopen sets of the
universe, and indiscreteness shows that there can be only two of
them, so to speak. This is Rice's Theorem for the universe Set.

(NB. The auxiliary modules develop much more material than we need
(and many silly things on the way - apologies).)

\begin{code}

{-# OPTIONS --without-K #-}

module TheTopologyOfTheUniverse where

open import Cantor
open import CurryHoward
open import Equality
open import Extensionality
open import GenericConvergentSequence
open import Isomorphism
open import Naturals
open import SetsAndFunctions
open import Two

\end{code}

The following is the crucial construction. It attaches the
singleton type ① as the limit to any given sequence of types.

The idea is that for any u : ℕ∞, the type Σ \(n : ℕ) → u ≣ n has
at most one element, namely n if u ≣ n, and none if u = ∞. In the
latter case we get a function with empty graph as the only
inhabitant, making this into a singleton type.  In the former
case, we get X n back.

\begin{code}

attach-① : (ℕ → Set) → (ℕ∞ → Set)
attach-① X u = (s : Σ \(n : ℕ) → u ≣ n) → X(π₀ s)

\end{code}

We first show that the constructed limiting sequence extends the
given sequence:

\begin{code}

_[_] : (ℕ∞ → Set) → (ℕ → Set)
X [ i ] = X(under i)


attach-①-lemma :

 ∀(X : ℕ → Set) → ∀ i → attach-① X [ i ] ≅  X i

attach-①-lemma X i =
 (g i , f i , extensionality(S i) , extensionality(R i))
 where
  f : ∀ i → X i → attach-① X [ i ]
  f i x (n , r) = subst {ℕ} {X} (under-mono r) x

  g : ∀ i → attach-① X [ i ] → X i
  g i h = h(i , refl)

  R-lemma :

   ∀ i n → ∀(r : under i ≡ under n) → ∀(h : attach-① X [ i ])
        → subst (under-mono {i} {n} r) (h(i , refl)) ≡ h(n , r)

  R-lemma i n r h =
   trans (lemma q h) (cong (λ p  → h(n , p)) (UIP ℕ∞ (cong under q) r))
   where
    open import UIP
    q : i ≡ n
    q = under-mono r
    A : ∀ i n → i ≡ n → Prp
    A i n q = ∀(h : attach-① X [ i ])
             → subst q (h(i , refl)) ≡ h(n , cong under q)
    lemma : ∀{i n} → ∀(q : i ≡ n) → A i n q
    lemma = J A (λ i h → cong (λ p → h(i , p)) refl)

  R : ∀ i → ∀ h → f i (g i h) ≡ h
  R i h = extensionality(lemma i h)
   where
    lemma : ∀ i → ∀ (h : attach-① X [ i ])
          → ∀ s → f i (g i h) s ≡ h s
    lemma i h (n , r) = R-lemma i n r h

  S : ∀ i → ∀ x → g i (f i x) ≡ x
  S i x = cong (λ r → subst {ℕ} {X} r x) lemma
   where
    open import UIP
    lemma : under-mono refl ≡ refl
    lemma = UIP ℕ (under-mono refl) refl

\end{code}

And then we show that the added limit point is what we claimed:

\begin{code}

attach-①-lemma∞ :

  ∀(X : ℕ → Set) → attach-① X ∞ ≅ ①

attach-①-lemma∞ X = only-one-iso the-only-element lemma₁
 where
  the-only-element : attach-① X ∞
  the-only-element (n , r) = unique-from-∅(∞-is-not-ℕ n r)

  lemma₀ : ∀(f g : attach-① X ∞)
         → ∀(s : Σ \(n : ℕ) → ∞ ≣ n) → f s ≡ g s
  lemma₀ f g (n , r) = unique-from-∅(∞-is-not-ℕ n r)

  lemma₁ : ∀(f g : attach-① X ∞) → f ≡ g
  lemma₁ f g = extensionality(lemma₀ f g)

\end{code}

The following follows the above pattern: We give a series of
constructions of limiting sequences, each one followed by two
lemmas, one saying what the limiting sequence is and the other
saying what its limit (value at ∞) is.

We begin with a particular case of the above, for the sake of
clarity, and because it is used twice: the constant sequence ∅,
where ∅ is the empty type, converges to the singleton type ①:

\begin{code}

constant-∅-converging-to-① : ℕ∞ → Set
constant-∅-converging-to-① = attach-①(λ i → ∅)


constant-∅-converging-to-①-lemma :

  ∀(i : ℕ) → constant-∅-converging-to-① [ i ] ≅ ∅

constant-∅-converging-to-①-lemma = attach-①-lemma(λ i → ∅)


constant-∅-converging-to-①-lemma∞ :

 constant-∅-converging-to-① ∞ ≅ ①

constant-∅-converging-to-①-lemma∞ = attach-①-lemma∞(λ i → ∅)

\end{code}

The constant sequence ∅ converges to any desired type Y, by
multiplying the previous sequence pointwise by Y:

\begin{code}

constant-∅-converging-to-anything : Set → (ℕ∞ → Set)
constant-∅-converging-to-anything Y u = (constant-∅-converging-to-① u) × Y


constant-∅-converging-to-anything-lemma :

 ∀(Y : Set) → ∀(i : ℕ) → constant-∅-converging-to-anything Y [ i ] ≅ ∅

constant-∅-converging-to-anything-lemma Y i =
 ≅-trans (lemma[X≅X'→X×Y≅X'×Y] (constant-∅-converging-to-①-lemma i))
          lemma[∅×Y≅∅]


constant-∅-converging-to-anything-lemma∞ :

 ∀(Y : Set) → constant-∅-converging-to-anything Y ∞ ≅ Y

constant-∅-converging-to-anything-lemma∞ Y =
 ≅-trans (lemma[X≅X'→X×Y≅X'×Y] constant-∅-converging-to-①-lemma∞)
          lemma[①×Y≅Y]

\end{code}

The constant sequence ① converges to ∅, by applying the
"negation" function X ↦ (X → ∅) to the constant sequence ∅ that
converges to ①.

\begin{code}

constant-①-converging-to-∅ : ℕ∞ → Set
constant-①-converging-to-∅ u = (constant-∅-converging-to-① u) → ∅


constant-①-converging-to-∅-lemma :

 ∀(i : ℕ) → constant-①-converging-to-∅ [ i ] ≅ ①

constant-①-converging-to-∅-lemma i =
 ≅-trans (lemma[X≅X'→[X→Y]≅[X'→Y]] (constant-∅-converging-to-①-lemma i))
          lemma[[∅→∅]≅①]


constant-①-converging-to-∅-lemma∞ :

 constant-①-converging-to-∅ ∞ ≅ ∅

constant-①-converging-to-∅-lemma∞ =
 ≅-trans (lemma[X≅X'→[X→Y]≅[X'→Y]] constant-∅-converging-to-①-lemma∞)
          lemma[[①→∅]≅∅]

\end{code}

By multiplying the previous limiting sequence pointwise with the
sequence that converges to one, we get that any sequence converges
to ∅:

\begin{code}

attach-∅ : (ℕ → Set) → (ℕ∞ → Set)
attach-∅ X u = (attach-① X u) × (constant-①-converging-to-∅ u)


attach-∅-lemma :

 ∀(X : ℕ → Set) → ∀(i : ℕ) → attach-∅ X [ i ] ≅ X i

attach-∅-lemma X i =
 ≅-trans (lemma[X≅X'→Y≅Y'→[X×Y]≅[X'×Y']]
                (attach-①-lemma X i)
                (constant-①-converging-to-∅-lemma i))
          lemma[Y×①≅Y]


attach-∅-lemma∞ :

 ∀(X : ℕ → Set) → attach-∅ X ∞ ≅ ∅

attach-∅-lemma∞ X =
 ≅-trans (lemma[X≅X'→Y≅Y'→[X×Y]≅[X'×Y']]
                (attach-①-lemma∞ X)
                (constant-①-converging-to-∅-lemma∞))
          lemma[Y×∅≅∅]

\end{code}

Finally, by adding pointwise a sequence that converges to ∅ to the
constant sequence ∅ converging to anything, we get any sequence X to
converge to any type Y we please:

\begin{code}

attach : (ℕ → Set) → Set → (ℕ∞ → Set)
attach X Y u =
 (attach-∅ X u) + (constant-∅-converging-to-anything Y u)


attach-lemma :

 ∀(X : ℕ → Set) → ∀(Y : Set) → ∀ i → attach X Y [ i ] ≅ X i

attach-lemma X Y i =
 ≅-trans (lemma[X≅X'→Y≅Y'→[X+Y]≅[X'+Y']]
                (attach-∅-lemma X i)
                (constant-∅-converging-to-anything-lemma Y i))
          lemma[Y+∅≅Y]


attach-lemma∞ :

 ∀(X : ℕ → Set) → ∀(Y : Set) → attach X Y ∞ ≅ Y

attach-lemma∞ X Y =
 ≅-trans (lemma[X≅X'→Y≅Y'→[X+Y]≅[X'+Y']]
                (attach-∅-lemma∞ X)
                (constant-∅-converging-to-anything-lemma∞ Y))
          lemma[∅+Y≅Y]

\end{code}

We pack the previous three lemmas together to get the Universe
Indiscreteness Theorem, which says that any type Y : Set can be
attached as a limit of any given sequence X : ℕ → Set:

\begin{code}

Universe-Indiscreteness-Theorem : ∀(X : ℕ → Set) → ∀(Y : Set) →

  (∀ i → attach X Y [ i ] ≅ X i)  ∧  attach X Y ∞ ≅ Y

Universe-Indiscreteness-Theorem X Y =
 ∧-intro (attach-lemma X Y) (attach-lemma∞ X Y)

\end{code}

As a corollary of The Universe Indiscreteness Theorem, we get Rice's
Theorem for the universe, which can be found in the module
RicesTheoremForTheUniverse.