Martin Escardo 29 April 2014. An hprop-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 hpropositions, 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 an hproposition X amounts to X=0 or X=1, so that Y^X is searchable if Y is searchable and X is an hproposition. 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 an hproposition 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 #-} module HProp-Tychonoff where open import Searchable open import HSets open import HProp-indexed-product open import Equality open import Two open import SetsAndFunctions open import CurryHoward open import Isomorphism \end{code} Let Z = ((x : X) → Y x). A crucial lemma is hprop-indexed-product : hprop X → (a : X) → Z ≅ Y a This is proved in the module HProp-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} hprop-tychonoff : {X : Set} {Y : X → Set} → hprop X → ((x : X) → searchable(Y x)) → searchable((x : X) → Y x) hprop-tychonoff {X} {Y} hp ε p = z₀ , z₀-is-universal-witness where -- hp : hprop X -- ε : (x : X) → searchable(Y x) -- p : Z → ₂ Z = (x : X) → Y x hip : (x : X) → Z ≅ Y x hip = hprop-indexed-product hp -- The essence of the first part of the proof is this: not-useful : X → searchable Z not-useful x = iso-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 hprop-indexed-product, abstractly: f : (x : X) → Z → Y x f x = π₀(hip x) g : (x : X) → Y x → Z g x = π₀(π₁(hip x)) fg : (x : X) (y : Y x) → f x (g x y) ≡ y -- Not used. fg x = π₀(π₁(π₁(hip x))) gf : (x : X) (z : Z) → g x (f x z) ≡ z -- Crucially used. gf x = π₁(π₁(π₁(hip 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(g 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 = π₀(ε x (q x)) -- By hypothesis, it satisfies: z₀-spec : (x : X) → q x (z₀ x) ≡ ₁ → (y : Y x) → q x y ≡ ₁ z₀-spec x = π₁(ε x (q x)) -- By expanding the definitions, this amounts to: z₀-spec₀ : (x : X) → p(g x (z₀ x)) ≡ ₁ → (y : Y x) → p(g x y) ≡ ₁ z₀-spec₀ = z₀-spec -- By the definition of f in hprop-indexed-product (namely f x z = z x): z₀-spec₁ : (x : X) → p(g x (f x z₀)) ≡ ₁ → (y : Y x) → p(g x y) ≡ ₁ z₀-spec₁ = z₀-spec₀ -- (So we can't abstract away the definition/proof of -- hprop-indexed-product.) -- In particular, with y = f x z, we get: z₀-spec₁-particular-case : (x : X) → p(g x (f x z₀)) ≡ ₁ → (z : Z) → p(g 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 (cong p (sym (gf x z))) (z₀-spec₁-particular-case x (trans (cong p (gf 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 (cong p claim) r where open import Extensionality 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 (an hprop) to X being subfinite (embedded into a finite type).) A particular case is the following: \begin{code} hprop-tychonoff-corollary : {X Y : Set} → hprop X → searchable Y → searchable(X → Y) hprop-tychonoff-corollary hp ε = hprop-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} hprop-tychonoff-corollary' : {X Y : Set} → hprop X → (X → searchable Y) → searchable(X → Y) hprop-tychonoff-corollary' hp ε = hprop-tychonoff hp ε \end{code}