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 2 May 2014 to make it way more conceptual and concise. 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.6.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 U, 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. The answer is that its topological reflection is indiscrete: http://www.cs.bham.ac.uk/~mhe/papers/universe-indiscrete.pdf http://www.sciencedirect.com/science/article/pii/S0168007216300409 M.H. Escardo and T. Streicher. The intrinsic topology of Martin-Lof universes. Version of Feb 2016. In Annals of Pure and Applied Logic, Volume 167, Issue 9, September 2016, Pages 794-805. 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 U 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 : ℕ → U converges to a limit X∞ : U if one can find a "limiting sequence" X' : ℕ∞ → U 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 U → ₂, 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 U. (NB. The auxiliary modules develop much more material than we need (and many silly things on the way - apologies).) \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} module TheTopologyOfTheUniverse where open import SpartanMLTT open import Two open import Naturals open import Sets open import Equivalence open import GenericConvergentSequence open import SquashedSum open import InjectivityOfTheUniverse \end{code} The following is the crucial construction, developed in the module InjectivityOfTheUniverse. \begin{code} attach-𝟙 : (ℕ → U) → (ℕ∞ → U) attach-𝟙 X = X / under \end{code} We first show that the constructed limiting sequence extends the given sequence: \begin{code} attach-𝟙-lemma : (X : ℕ → U) (i : ℕ) → attach-𝟙 X (under i) ≃ X i attach-𝟙-lemma X = extension-in-range X under under-embedding \end{code} And then we show that the added limit point is what we claimed: \begin{code} attach-𝟙-lemma∞ : (X : ℕ → U) → attach-𝟙 X ∞ ≃ 𝟙 attach-𝟙-lemma∞ X = extension-out-of-range X under ∞ ∞-is-not-ℕ \end{code} Then we show that the constant sequence 𝟙 converges to any type Y we wish: \begin{code} constant-𝟙-converging-to : (Y : U) → ℕ∞ → U constant-𝟙-converging-to Y u = u ≡ ∞ → Y constant-𝟙-converging-to-lemma : (Y : U) (i : ℕ) → constant-𝟙-converging-to Y (under i) ≃ 𝟙 constant-𝟙-converging-to-lemma Y i = f , (g , fg) , (g , gf) where f : ((under i) ≡ ∞ → Y) → 𝟙 f φ = * g : 𝟙 → ((under i) ≡ ∞ → Y) g * r = unique-from-∅ (∞-is-not-ℕ i (sym r)) fg : (u : 𝟙) → * ≡ u fg * = refl open import FunExt gf : (φ : ((under i) ≡ ∞ → Y)) → g * ≡ φ gf φ = funext (λ r → unique-from-∅ (∞-is-not-ℕ i (sym r))) constant-𝟙-converging-to-lemma∞ : (Y : U) → constant-𝟙-converging-to Y ∞ ≃ Y constant-𝟙-converging-to-lemma∞ Y = f , (g , fg) , (g , gf) where f : (∞ ≡ ∞ → Y) → Y f φ = φ refl g : Y → ∞ ≡ ∞ → Y g y r = y fg : (y : Y) → f(g y) ≡ y fg y = refl open import FunExt gf : (φ : ∞ ≡ ∞ → Y) → g(f φ) ≡ φ gf φ = funext claim where claim : (r : ∞ ≡ ∞) → f φ ≡ φ r claim r = ap φ (ℕ∞-hset refl r) \end{code} Putting the above to facts together, we get what we claimed above: \begin{code} attach : (ℕ → U) → U → (ℕ∞ → U) attach X Y u = attach-𝟙 X u × constant-𝟙-converging-to Y u attach-lemma : (X : ℕ → U) (Y : U) (i : ℕ) → attach X Y (under 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-lemma Y i)) lemma[Y×𝟙≃Y] attach-lemma∞ : (X : ℕ → U) (Y : U) → attach X Y ∞ ≃ Y attach-lemma∞ X Y = ≃-trans (lemma[X≃X'→Y≃Y'→[X×Y]≃[X'×Y']] (attach-𝟙-lemma∞ X) (constant-𝟙-converging-to-lemma∞ Y)) lemma[𝟙×Y≃Y] \end{code} This gives the Indiscreteness Theorem, which says that any type Y : U can be attached as a limit of any given sequence X : ℕ → U: \begin{code} Universe-Indiscreteness-Theorem : (X : ℕ → U) (Y : U) → ((i : ℕ) → attach X Y (under i) ≃ X i) × (attach X Y ∞ ≃ Y) Universe-Indiscreteness-Theorem X Y = (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.