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.


{-# 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) (ε  π₀))