Martin Escardo, 2 May 2014

This improves the module SquashedSumOld. See the comments in that module
for an informal explanation of the squashed sum.


{-# OPTIONS --without-K #-}

module SquashedSum where

open import GenericConvergentSequence
open import Naturals
open import SetsAndFunctions
open import Searchable
open import ConvergentSequenceSearchable
open import InjectivityOfTheUniverse
open import ExtendedSumSearchable
open import Embedding

Σ¹ : (  Set)  Set
Σ¹ X = Σ (X / under)

squashed-sum-searchable : {X :   Set}  ((n : )  searchable(X n))  searchable(Σ¹ X)
squashed-sum-searchable {X} ε = extended-sum-searchable under under-embedding ε ℕ∞-is-searchable