Martin Escardo 29 April 2014. This generalizes squashed sums and their searchability (module SquashedSum.lagda), when X = ℕ K = ℕ∞ j = under Y : ℕ → Set (Y / j)(k) = Y [ k ] Σ¹ Y = Σ \(k : K) → (Y / j)(k) Moreover, the proof given here is more conceptual, decomposed in meaningful smaller steps (developed in other modules for this purpose). Here Y / j is the (right Kan) extension of Y along j by the injectivity of the universe Set of all types. \begin{code} {-# OPTIONS --without-K #-} module ExtendedSumSearchable where open import Embedding open import Searchable open import SetsAndFunctions open import InjectivityOfTheUniverse open import HProp-Tychonoff extended-sum-searchable : {X K : Set} {Y : X → Set} (j : X → K) → embedding j → ((x : X) → searchable(Y x)) → searchable K → searchable(Σ(Y / j)) extended-sum-searchable j e ε δ = sums-preserve-searchability δ (λ k → hprop-tychonoff (e k) (ε ∘ π₀)) \end{code}