Martin Escardo, 2 May 2014

We show that the old and new squashed sums agree.


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

module SquashedAgreement where

open import GenericConvergentSequence
open import Naturals
open import InjectivityOfTheUniverse
open import SquashedSum
open import SquashedSumOld renaming (Σ¹ to Σ¹-old) hiding (squashed-sum-searchable)
open import Isomorphism

agreement-lemma : (X :   Set) (u : ℕ∞)  (X / under) u  (X [ u ]) 
agreement-lemma X = 2nd-extension-formula X under

agreement : (X :   Set)  Σ¹ X  Σ¹-old X
agreement X = Σ-congruence ℕ∞ (X / under)  u  X [ u ]) (agreement-lemma X)