Martin Escardo 29 April 2014. A prop-indexed product of searchable sets is itself searchable. The definition of the searchability of a type A is searchable A = (p : A → ₂) → Σ \(a₀ : A) → p a₀ ≡ ₁ → (a : A) → p a ≡ ₁ With excluded middle for propositions, the above claim is not surprising, because (0 → Y) = Y^0 = 1 (which is always searchable), (1 → Y) = Y^1 = Y (which is searchable if Y is), and excluded middle for a proposition X amounts to X=0 or X=1, so that Y^X is searchable if Y is searchable and X is a proposition. The point is that (1) We can reach this conclusion without excluded middle. (2) This also holds for dependent products: Π(x:X).Y x is searchable if X is a proposition and Y x is searchable for every x:X. (This product is written (x : X) → Y x in Agda.) Our Agda proof below can be written rather concisely by expanding the definitions. We deliberately don't do that, so that we have a rigorous informal proof side-by-side with the formal proof. We proceed in a series of trivial steps, hopefully in the most natural way (although we had a convoluted path to this supposedly natural way). \begin{code} {-# OPTIONS --without-K --exact-split --safe #-} module Prop-Tychonoff where open import SpartanMLTT open import Two open import Searchable open import Sets open import Prop-indexed-product open import Equivalence \end{code} Let Z = ((x : X) → Y x). A crucial lemma is prop-indexed-product : isProp X → (a : X) → Z ≅ Y a This is proved in the module Prop-indexed-product. Although it has a subtle proof, it should be intuitively clear, as X has at most one element by hypothesis, and if the element is a:X then the product Z should be isomorphic to its only factor Y a. With this observation, the following proof should be self-contained, if we recall again the definition of searchable set from the module Searchable: searchable A = (p : A → ₂) → Σ \(a₀ : A) → p a₀ ≡ ₁ → (a : A) → p a ≡ ₁ Recall also that such an a₀ is called a universal witness for the predicate p. \begin{code} prop-tychonoff : {X : U} {Y : X → U} → isProp X → ((x : X) → searchable(Y x)) → searchable((x : X) → Y x) prop-tychonoff {X} {Y} hp ε p = z₀ , z₀-is-universal-witness where -- hp : isProp X -- ε : (x : X) → searchable(Y x) -- p : Z → ₂ Z = (x : X) → Y x hip : (x : X) → Z ≃ Y x hip = prop-indexed-product hp -- The essence of the first part of the proof is this: not-useful : X → searchable Z not-useful x = equiv-searchable (≃-sym(hip x)) (ε x) -- But this is very crude for our purposes (or so it seems). -- So we instead proceed as follows. -- The following is what we get from prop-indexed-product, abstractly: f : (x : X) → Z → Y x f x = pr₁(hip x) hrf : (x : X) → hasRetraction(f x) hrf x = pr₂(pr₂(hip x)) h : (x : X) → Y x → Z h x = pr₁(hrf x) hf : (x : X) (z : Z) → h x (f x z) ≡ z hf x = pr₂(hrf x) -- We define a predicate q x: Y x → ₂, for each x:X, from the -- predicate p:Z→₂ via (part of) the above isomorphism: q : (x : X) → Y x → 𝟚 q x y = p(h x y) -- We argue that the following is a universal witness for the -- searchability of the type Z wrt the predicate p: z₀ : Z z₀ x = pr₁(ε x (q x)) -- By hypothesis, it satisfies: z₀-spec : (x : X) → q x (z₀ x) ≡ ₁ → (y : Y x) → q x y ≡ ₁ z₀-spec x = pr₂(ε x (q x)) -- By expanding the definitions, this amounts to: z₀-spec₀ : (x : X) → p(h x (z₀ x)) ≡ ₁ → (y : Y x) → p(h x y) ≡ ₁ z₀-spec₀ = z₀-spec -- By the definition of f in prop-indexed-product (namely f x z = z x): z₀-spec₁ : (x : X) → p(h x (f x z₀)) ≡ ₁ → (y : Y x) → p(h x y) ≡ ₁ z₀-spec₁ = z₀-spec₀ -- (So we can't abstract away the definition/proof of -- prop-indexed-product.) -- In particular, with y = f x z, we get: z₀-spec₁-particular-case : (x : X) → p(h x (f x z₀)) ≡ ₁ → (z : Z) → p(h x (f x z)) ≡ ₁ z₀-spec₁-particular-case x r z = z₀-spec₁ x r (f x z) -- Using the fact that g x (f x z) = z for any x:X, we get: z₀-is-universal-witness-assuming-X : X → p z₀ ≡ ₁ → (z : Z) → p z ≡ ₁ z₀-is-universal-witness-assuming-X x r z = trans (ap p (sym (hf x z))) (z₀-spec₁-particular-case x (trans (ap p (hf x z₀)) r) z) -- Notice that the point x:X vanishes from the conclusion, and so we -- are able to omit it from the hypothesis, which is crucial for -- what follows. -- We get the same conclusion if X is empty: z₀-is-universal-witness-assuming-X→∅ : (X → ∅) → p z₀ ≡ ₁ → (z : Z) → p z ≡ ₁ z₀-is-universal-witness-assuming-X→∅ u r z = trans (ap p claim) r where open import FunExt claim : z ≡ z₀ claim = funext(λ x → unique-from-∅(u x)) -- So we would get what we want if we had excluded middle, because -- the above shows that both X and X→∅ give the desired conclusion -- that z₀ is a universal witness. But excluded middle is not needed. -- We shuffle the arguments of z₀-is-universal-witness-assuming-X: claim₀ : p z₀ ≡ ₁ → (z : Z) → X → p z ≡ ₁ claim₀ r z x = z₀-is-universal-witness-assuming-X x r z -- We then take the contra-positive of the conclusion X → p z ≡ ₁, -- and use the fact that if a point of the two-point type 𝟚 is ₀, -- then it is not ₁: Claim₁ : p z₀ ≡ ₁ → (z : Z) → p z ≡ ₀ → (X → ∅) Claim₁ r z = contra-positive(claim₀ r z) ∘ Lemma[b≡₀→b≢₁] -- This concludes the first part of the argument. -- We now shuffle the arguments of z₀-is-universal-witness-assuming-X→∅: Claim₂ : p z₀ ≡ ₁ → (z : Z) → (X → ∅) → p z ≡ ₁ Claim₂ r z u = z₀-is-universal-witness-assuming-X→∅ u r z -- Combining the two last claims, we get: Claim₃ : p z₀ ≡ ₁ → (z : Z) → p z ≡ ₀ → p z ≡ ₁ Claim₃ r z = Claim₂ r z ∘ Claim₁ r z -- Finally, we do case analysis on the value of p z: z₀-is-universal-witness : p z₀ ≡ ₁ → (z : Z) → p z ≡ ₁ z₀-is-universal-witness r z = two-equality-cases (Claim₃ r z) id \end{code} And we are done. (9 Sep 2015: We can generalize from X being a subsingleton (a proposition) to X being subfinite (embedded into a finite type).) A particular case is the following: \begin{code} prop-tychonoff-corollary : {X Y : U} → isProp X → searchable Y → searchable(X → Y) prop-tychonoff-corollary hp ε = prop-tychonoff hp (λ x → ε) \end{code} This holds even for undecided X (such as X=LPO), or when we have no idea whether X or (X→∅), and hence whether (X→Y) is 1 or Y (or none, if this is undecided)! Better (9 Sep 2015): \begin{code} prop-tychonoff-corollary' : {X Y : U} → isProp X → (X → searchable Y) → searchable(X → Y) prop-tychonoff-corollary' hp ε = prop-tychonoff hp ε \end{code}