Martin Escardo 29 April 2014.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module ExtendedSumSearchable where

open import SpartanMLTT
open import Embedding
open import Searchable 
open import InjectivityOfTheUniverse
open import Prop-Tychonoff

extended-sum-searchable : {X K : U} {Y : X  U} (j : X  K)  embedding j
   ((x : X)  searchable(Y x))  searchable K  searchable(Σ(Y / j))
extended-sum-searchable j e ε δ = sums-preserve-searchability δ  k  prop-tychonoff (e k) (ε  pr₁))

\end{code}