Martin Escardo, 2 May 2014.

Squashed sum.

See remarks below for an explanation.

\begin{code}

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

open import SpartanMLTT
open import UF-FunExt

module SquashedSum (fe : FunExt) where

private
 feβ‚€ : funext 𝓀₀ 𝓀₀
 feβ‚€ = fe 𝓀₀ 𝓀₀

open import Two-Properties
open import Plus-Properties
open import Density
open import GenericConvergentSequence
open import CompactTypes
open import ConvergentSequenceCompact feβ‚€
open import InjectiveTypes fe
open import ExtendedSumCompact fe
open import DiscreteAndSeparated
open import CanonicalMapNotation
open import SigmaDiscreteAndTotallySeparated
open import PairFun

open import UF-Base
open import UF-Subsingletons
open import UF-Equiv
open import UF-Embeddings
open import UF-Miscelanea

\end{code}

Recall that the map

  ΞΉ : β„• β†’ β„•βˆž

is the canonical embedding. Given a type family X : β„• β†’ 𝓀 Μ‡, we take its
right Kan extension

  X / ΞΉ : β„•βˆž β†’ 𝓀 Μ‡

and then its sum, which we call the squashed sum of X and write

  Σ¹ X.

We have that (X / ΞΉ) ∞ ≃ πŸ™. What is interesting is that if each
X n is compact then so is its squashed sum Σ¹ X.

\begin{code}

Σ¹ :(β„• β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
Σ¹ X = Σ (X / ι)

Σ¹-compactβˆ™ : (X : β„• β†’ 𝓀 Μ‡ )
            β†’ ((n : β„•) β†’ compactβˆ™(X n))
            β†’ compactβˆ™(Σ¹ X)
Σ¹-compactβˆ™ X Ξ΅ = extended-sum-compactβˆ™
                   β„•-to-β„•βˆž
                   (β„•-to-β„•βˆž-is-embedding feβ‚€)
                   Ξ΅
                   β„•βˆž-compactβˆ™
\end{code}

Added 26 July 2018 (implementing ideas of several years ago).

We now develop a discrete (but not compact) version Σ₁ X of Σ¹ X
with a dense embedding into Σ¹ X, where an embedding is called dense
if the complement of its image is empty. Recall that the function

  ΞΉπŸ™ : β„• + πŸ™ β†’ β„•βˆž

is the canonical embedding that maps the added isolated point to ∞,
which is dense.

\begin{code}

over : β„• β†’ β„• + πŸ™
over = inl {𝓀₀} {𝓀₀}

over-embedding : is-embedding over
over-embedding = inl-is-embedding β„• πŸ™

Σ₁ :(β„• β†’ 𝓀 Μ‡ ) β†’ 𝓀 Μ‡
Σ₁ X = Ξ£ (X / over)

ΞΉπŸ™-over : (n : β„•) β†’ ΞΉπŸ™ (over n) ≑ ΞΉ n
ΞΉπŸ™-over n = refl

over-is-discrete : (X : β„• β†’ 𝓀 Μ‡ )
                 β†’ ((n : β„•) β†’ is-discrete (X n))
                 β†’ (z : β„• + πŸ™) β†’ is-discrete ((X / over) z)
over-is-discrete X d (inl n) = retract-is-discrete
                                 (≃-gives-◁
                                   (Ξ -extension-property X over
                                      over-embedding n))
                                 (d n)
over-is-discrete X d (inr *) = retract-is-discrete {𝓀₀}
                                 (≃-gives-◁
                                   (Ξ -extension-out-of-range X over (inr *)
                                       (Ξ» n β†’ +disjoint)))
                                 πŸ™-is-discrete

Σ₁-is-discrete : (X : β„• β†’ 𝓀 Μ‡ )
               β†’ ((n : β„•) β†’ is-discrete(X n))
               β†’ is-discrete (Σ₁ X)
Σ₁-is-discrete X d = Ξ£-is-discrete
                       (+-is-discrete β„•-is-discrete πŸ™-is-discrete)
                       (over-is-discrete X d)
\end{code}

The type (X / over) z is densely embedded into the type (X / ΞΉ) (ΞΉπŸ™ z):

\begin{code}

over-ΞΉ : (X : β„• β†’ 𝓀 Μ‡ ) (z : β„• + πŸ™)
       β†’ (X / over) z β†ͺᡈ (X / ΞΉ) (ΞΉπŸ™ z)
over-ΞΉ X (inl n) = equiv-dense-embedding (
 (X / over) (over n)   β‰ƒβŸ¨ Ξ -extension-property X over over-embedding n ⟩
 X n                   β‰ƒβŸ¨ ≃-sym (Ξ -extension-property X β„•-to-β„•βˆž (β„•-to-β„•βˆž-is-embedding feβ‚€) n) ⟩
 (X / ΞΉ) (ΞΉ n) β– )
over-ΞΉ X (inr *) = equiv-dense-embedding (
 (X / over) (inr *) β‰ƒβŸ¨ Ξ -extension-out-of-range X over (inr *) (Ξ» x β†’ +disjoint ) ⟩
 πŸ™ {𝓀₀}             β‰ƒβŸ¨ ≃-sym (Ξ -extension-out-of-range X ΞΉ ∞ (Ξ» n p β†’ ∞-is-not-finite n (p ⁻¹))) ⟩
 (X / ΞΉ) ∞      β–  )

over-ΞΉ-map : (X : β„• β†’ 𝓀 Μ‡ ) (z : β„• + πŸ™)
               β†’ (X / over) z β†’ (X / ΞΉ) (ΞΉπŸ™ z)
over-ΞΉ-map X z = detofun (over-ΞΉ X z)

over-ΞΉ-map-dense : (X : β„• β†’ 𝓀 Μ‡ ) (z : β„• + πŸ™)
                     β†’ is-dense (over-ΞΉ-map X z)
over-ΞΉ-map-dense X z = is-dense-detofun (over-ΞΉ X z)

over-ΞΉ-map-left : (X : β„• β†’ 𝓀 Μ‡ ) (n : β„•)
                      (Ο† : (w : fiber over (inl n)) β†’ X (pr₁ w))
                    β†’ over-ΞΉ-map X (inl n) Ο† (n , refl)
                    ≑ Ο† (n , refl)
over-ΞΉ-map-left X n Ο† =
 transport
  (Ξ» - β†’ over-ΞΉ-map X (inl n) Ο† (n , refl)
       ≑ transport (Ξ» - β†’ X (pr₁ -)) - (Ο† (n , refl)))
  (props-are-sets
    (β„•-to-β„•βˆž-is-embedding feβ‚€ (ΞΉ n))
    (β„•-to-β„•βˆž-is-embedding feβ‚€ (ΞΉ n) (n , refl) (n , refl))
    refl)
  (f (n , refl))
 where
  -- We define this for the sake of clarity only:
  f : (t : fiber ΞΉ (ΞΉ n))
    β†’ over-ΞΉ-map X (inl n) Ο† t
    ≑ transport (Ξ» - β†’ X (pr₁ -))
                 (β„•-to-β„•βˆž-is-embedding feβ‚€ (ΞΉ n) (n , refl) t)
                 (Ο† (n , refl))
  f t = refl

\end{code}

The discrete type Σ₁ X is densely embedded into
the compact type Σ¹ X:

\begin{code}

Ξ£-up : (X : β„• β†’ 𝓀 Μ‡ ) β†’ Σ₁ X β†’ Σ¹ X
Ξ£-up X = pair-fun ΞΉπŸ™ (over-ΞΉ-map X)

Ξ£-up-embedding : (X : β„• β†’ 𝓀 Μ‡ ) β†’ is-embedding (Ξ£-up X)
Ξ£-up-embedding X = pair-fun-is-embedding
                    ΞΉπŸ™
                    (over-ΞΉ-map X)
                    (ΞΉπŸ™-is-embedding feβ‚€)
                    (Ξ» z β†’ is-embedding-detofun (over-ΞΉ X z))

Ξ£-up-dense : (X : β„• β†’ 𝓀 Μ‡ ) β†’ is-dense (Ξ£-up X)
Ξ£-up-dense X = pair-fun-dense ΞΉπŸ™
                (over-ΞΉ-map X)
                (ΞΉπŸ™-dense feβ‚€)
                (Ξ» z β†’ is-dense-detofun (over-ΞΉ X z))

\end{code}

But this is not enough: we need a map

  Σ↑ : Σ₁ X β†’ Σ¹ Y,

given maps

  f n : X n β†’ Y n,

which has to preserve dense embeddings.

\begin{code}

Over : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
       (f : (n : β„•) β†’ X n β†’ Y n)
     β†’ (z : β„• + πŸ™) β†’ (X / over) z β†’ (Y / over) z
Over X Y f (inl n) =
  ⌜ Π-extension-property Y over over-embedding n ⌝⁻¹ ∘
  f n ∘
  ⌜ Π-extension-property X over over-embedding n ⌝
Over X Y f (inr *) =
  _∘_ {_} {𝓀₀}
   ⌜ Ξ -extension-out-of-range Y over (inr *) (Ξ» _ β†’ +disjoint) ⌝⁻¹
   ⌜ Ξ -extension-out-of-range X over (inr *) (Ξ» _ β†’ +disjoint) ⌝

Over-inl : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ ) (f : (n : β„•) β†’ X n β†’ Y n)
         β†’ (n : β„•) β†’ Over X Y f (inl n)
         ≑ Ξ» (Ο† : (X / over) (inl n)) (w : fiber over (inl n)) β†’
             transport (Ξ» - β†’ Y (pr₁ -))
                       (inl-is-embedding β„• πŸ™ (inl n) (n , refl) w)
                       (f n (Ο† (n , refl)))
Over-inl X Y f n = refl

Over-inr : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ ) (f : (n : β„•) β†’ X n β†’ Y n)
         β†’ Over X Y f (inr ⋆) ≑ Ξ» Ο† w β†’ 𝟘-elim (+disjoint (prβ‚‚ w))
Over-inr X Y f = refl

\end{code}

The following two proofs look complicated, but are rather simple:
composition preserves dense maps and embeddings, and equivalences are
dense embeddings.

\begin{code}

Over-dense : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
             (f : (n : β„•) β†’ X n β†’ Y n)
           β†’ ((n : β„•) β†’ is-dense (f n))
           β†’ (z : β„• + πŸ™) β†’ is-dense (Over X Y f z)
Over-dense X Y f d (inl n) =
 comp-is-dense
  (comp-is-dense
    (equivs-are-dense
      ⌜ Π-extension-property X over over-embedding n ⌝
      (⌜⌝-is-equiv (Π-extension-property X over over-embedding n)))
    (d n))
  (equivs-are-dense
    ⌜ Π-extension-property Y over over-embedding n ⌝⁻¹
    (⌜⌝-is-equiv (≃-sym (Ξ -extension-property Y over over-embedding n))))
Over-dense X Y f d (inr ⋆) =
 comp-is-dense {_} {𝓀₀}
  (equivs-are-dense
    ⌜ Ξ -extension-out-of-range X over (inr ⋆) (Ξ» x β†’ +disjoint) ⌝
    (⌜⌝-is-equiv (Ξ -extension-out-of-range X over (inr ⋆) (Ξ» x β†’ +disjoint))))
  (equivs-are-dense
    ⌜ Ξ -extension-out-of-range Y over (inr ⋆) (Ξ» x β†’ +disjoint) ⌝⁻¹
   (⌜⌝-is-equiv (≃-sym (Ξ -extension-out-of-range Y over (inr ⋆) (Ξ» x β†’ +disjoint)))))

Over-embedding : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
                 (f : (n : β„•) β†’ X n β†’ Y n)
               β†’ ((n : β„•) β†’ is-embedding (f n))
               β†’ (z : β„• + πŸ™) β†’ is-embedding (Over X Y f z)
Over-embedding {𝓀} X Y f d (inl n) =
 ∘-is-embedding
  (∘-is-embedding
    (equivs-are-embeddings
      ⌜ Π-extension-property X over over-embedding n ⌝
      (⌜⌝-is-equiv (Π-extension-property X over over-embedding n)))
    (d n))
  (equivs-are-embeddings
    ⌜ Π-extension-property Y over over-embedding n ⌝⁻¹
   (⌜⌝-is-equiv (≃-sym (Ξ -extension-property Y over over-embedding n))))
Over-embedding {𝓀} X Y f d (inr ⋆) =
 ∘-is-embedding {𝓀} {𝓀₀}
  (equivs-are-embeddings
    ⌜ Ξ -extension-out-of-range X over (inr ⋆) (Ξ» x β†’ +disjoint) ⌝
    (⌜⌝-is-equiv (Ξ -extension-out-of-range X over (inr ⋆) (Ξ» x β†’ +disjoint))))
  (equivs-are-embeddings
    ⌜ Ξ -extension-out-of-range Y over (inr ⋆) (Ξ» x β†’ +disjoint) ⌝⁻¹
   (⌜⌝-is-equiv (≃-sym (Ξ -extension-out-of-range Y over (inr ⋆) (Ξ» x β†’ +disjoint)))))

Σ₁-functor : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ ) (f : (n : β„•) β†’ X n β†’ Y n)
           β†’ Σ₁ X β†’ Σ₁ Y
Σ₁-functor X Y f = pair-fun id (Over X Y f)

Σ₁-functor-dense : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
                   (f : (n : β„•) β†’ X n β†’ Y n)
                 β†’ ((n : β„•) β†’ is-dense (f n))
                 β†’ is-dense (Σ₁-functor X Y f)
Σ₁-functor-dense X Y f d = pair-fun-dense
                            id
                            (Over X Y f)
                            id-is-dense
                            (Over-dense X Y f d)

Σ₁-functor-embedding : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
                       (f : (n : β„•) β†’ X n β†’ Y n)
                     β†’ ((n : β„•) β†’ is-embedding (f n))
                     β†’ is-embedding (Σ₁-functor X Y f)
Σ₁-functor-embedding X Y f e = pair-fun-is-embedding
                                id
                                (Over X Y f)
                                id-is-embedding
                                (Over-embedding X Y f e)

Σ↑ : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
     (f : (n : β„•) β†’ X n β†’ Y n)
   β†’ Σ₁ X β†’ Σ¹ Y
Σ↑ X Y f = Ξ£-up Y ∘ Σ₁-functor X Y f

Σ↑-dense : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
           (f : (n : β„•) β†’ X n β†’ Y n)
         β†’ ((n : β„•) β†’ is-dense (f n))
         β†’ is-dense (Σ↑ X Y f)
Σ↑-dense X Y f d = comp-is-dense (Σ₁-functor-dense X Y f d) (Ξ£-up-dense Y)

Σ↑-embedding : (X : β„• β†’ 𝓀 Μ‡ ) (Y : β„• β†’ 𝓀 Μ‡ )
               (f : (n : β„•) β†’ X n β†’ Y n)
             β†’ ((n : β„•) β†’ is-embedding (f n))
             β†’ is-embedding (Σ↑ X Y f)
Σ↑-embedding X Y f d = ∘-is-embedding (Σ₁-functor-embedding X Y f d) (Ξ£-up-embedding Y)

\end{code}

We don't need this for the moment:

\begin{code}

ΞΉπŸ™-over-extension : {X : β„• β†’ 𝓀 Μ‡ } (u : β„•βˆž)
                      β†’ ((X / over) / ΞΉπŸ™) u ≃ (X / ΞΉ) u
ΞΉπŸ™-over-extension = iterated-extension over ΞΉπŸ™

\end{code}

End. What follows is an old version of part of the above.

The original version of the compactness of the squashed sum, given
below was much more convoluted, as it didn't use injective types, but
equivalent, as also shown below.

December 2012, going back to work done circa 2010.

The theorem here is that the "squashed sum" of any countable family of
compactβˆ™ sets is itself compact (see the module CompactTypes,
imported below, for the definition and fundamental facts about the
notion).

(The terminology "squashed sum" comes from the paper "Infinite sets
that satisfy the principle of omniscience in all varieties of
constructive mathematics", where this concept is investigated within
the Cantor type β„• β†’ β‚‚, which makes the squashing self-evident.)

Given a countable family of sets.

   X : β„• β†’ 𝓀₀ Μ‡,

extend it to a β„•βˆž-indexed family of sets as follows

  _[_] : (β„• β†’ 𝓀₀ Μ‡ ) β†’ (β„•βˆž β†’ 𝓀₀ Μ‡ )
  X [ u ] = (k : β„•) β†’ ΞΉ k ≑ u β†’ X k

where u ranges over β„•βˆž, the one-point compactification of the natural
numbers β„•, defined in the module GenericConvergentSequence.

The squashed sum of X : β„• β†’ 𝓀₀ Μ‡ is defined to be

   Ξ£α΄΅ X = Ξ£ u κž‰ β„•βˆž , X [ u ]

Intuitively, the squashed sum is the disjoint sum with an added limit
point at infinity.

Assuming excluded middle, Ξ£α΄΅ X is isomorphic to (Ξ£ n κž‰ β„• , X n) ⊎ 1
where 1 is the one-point type.

Assuming Brouwerian continuity axioms, Ξ£α΄΅ X is the one-point
compactification of the disjoint sum (Ξ£ n κž‰ β„• , X n).

But we don't assume excluded middle or continuiy axioms here. We work
within intensional MLTT with function extensionality as a postulate
(rather than as a meta-theoretical rule).

\begin{code}

module original-version-and-equivalence-with-new-version where

 _[_] : (β„• β†’ 𝓀₀ Μ‡ ) β†’ (β„•βˆž β†’ 𝓀₀ Μ‡ )
 X [ u ] = (k : β„•) β†’ ΞΉ k ≑ u β†’ X k

 Ξ£α΄΅ : (β„• β†’ 𝓀₀ Μ‡ ) β†’ 𝓀₀ Μ‡
 Ξ£α΄΅ X = Ξ£ u κž‰ β„•βˆž , X [ u ]

 βˆžβ‚ : {X : β„• β†’ 𝓀₀ Μ‡ } β†’ Ξ£α΄΅ X
 βˆžβ‚ = ∞ , Ξ» k r β†’ 𝟘-elim (∞-is-not-finite k (r ⁻¹))

\end{code}

 This point at infinity is unique assuming extensionality, because:

\begin{code}

 H : {X : β„• β†’ 𝓀₀ Μ‡ } β†’ (u : β„•βˆž) β†’ u ≑ ∞ β†’ (y y' : X [ u ]) β†’ y ≑ y'
 H {X} u r y y' = dfunext feβ‚€ (Ξ» k β†’ dfunext feβ‚€ (Ξ» s β†’ lemma k s))
  where
   lemma : (k : β„•) (s : ΞΉ k ≑ u) β†’ y k s ≑ y' k s
   lemma k s = 𝟘-elim(∞-is-not-finite k (r ⁻¹ βˆ™ s ⁻¹))

\end{code}

 Next we have an isomorphism X [ u ] β‰… X n if ΞΉ n ≑ u:

\begin{code}

 F : {X : β„• β†’ 𝓀₀ Μ‡ } (n : β„•) (u : β„•βˆž) β†’ ΞΉ n ≑ u β†’ X n β†’ X [ u ]
 F {X} n u r x k s = transport X (β„•-to-β„•βˆž-lc (r βˆ™ s ⁻¹)) x

 G : {X : β„• β†’ 𝓀₀ Μ‡ } (n : β„•) (u : β„•βˆž) β†’ ΞΉ n ≑ u β†’ X [ u ] β†’ X n
 G n u r y = y n r

 FG : {X : β„• β†’ 𝓀₀ Μ‡ } (n : β„•) (u : β„•βˆž) (r : ΞΉ n ≑ u) (y : (k : β„•)
   β†’ ΞΉ k ≑ u β†’ X k) β†’ F n u r (G n u r y) ≑ y
 FG {X} n u r y = dfunext feβ‚€ (Ξ» k β†’ dfunext feβ‚€ (Ξ» s β†’ lemma k s))
  where
   f : {m n : β„•} β†’ m ≑ n β†’ X m β†’ X n
   f = transport X

   t : (k : β„•) β†’ ΞΉ k ≑ u β†’ n ≑ k
   t k s = β„•-to-β„•βˆž-lc (r βˆ™ s ⁻¹)

   A :  (n k : β„•) β†’ n ≑ k β†’ 𝓀₀ Μ‡
   A n k t = (u : β„•βˆž) (r : ΞΉ n ≑ u) (s : ΞΉ k ≑ u) (y : X [ u ]) β†’ f t (y n r) ≑ y k s

   Ο† : (n : β„•) β†’ A n n refl
   Ο† n = Ξ» u r s y β†’ ap (y n) (β„•βˆž-is-set feβ‚€ r s)

   lemma : (k : β„•) (s : ΞΉ k ≑ u) β†’ f (β„•-to-β„•βˆž-lc (r βˆ™ s ⁻¹)) (y n r) ≑ y k s
   lemma k s = J A Ο† {n} {k} (t k s) u r s y

 GF : {X : β„• β†’ 𝓀₀ Μ‡ } (n : β„•) (u : β„•βˆž) (r : ΞΉ n ≑ u) (x : X n) β†’ G {X} n u r (F n u r x) ≑ x
 GF {X} n u r x = s
  where
   f : {m n : β„•} β†’ m ≑ n β†’ X m β†’ X n
   f = transport X

   claimβ‚€ : f (β„•-to-β„•βˆž-lc (r βˆ™ r ⁻¹)) x ≑ f (β„•-to-β„•βˆž-lc refl) x
   claimβ‚€ = ap (Ξ» - β†’ f (β„•-to-β„•βˆž-lc -) x) (trans-sym' r)

   claim₁ : f (β„•-to-β„•βˆž-lc refl) x ≑ x
   claim₁ = ap (Ξ» - β†’ f - x) (β„•-to-β„•βˆž-lc-refl n)

   s : f (β„•-to-β„•βˆž-lc (r βˆ™ r ⁻¹)) x ≑ x
   s = claimβ‚€ βˆ™ claim₁

\end{code}

 We now can show that the type X [ u ] is compact for every u : β„•βˆž
 provided the type X n is compact for every n : β„•. This is tricky,
 because a priory it is not enough to consider the cases ΞΉ n ≑ u and u ≑ ∞.

 The above isomorphism is used to prove the correctness of the witness
 yβ‚€ below, which is easily defined (using one direction of the
 isomorphism):

\begin{code}

 extension-compactβˆ™ : {X : β„• β†’ 𝓀₀ Μ‡ } β†’ ((n : β„•) β†’ compactβˆ™(X n)) β†’ (u : β„•βˆž) β†’ compactβˆ™(X [ u ])
 extension-compactβˆ™ {X} Ξ΅ u p = yβ‚€ , lemma
  where
   Y : 𝓀₀ Μ‡
   Y = X [ u ]
   -- Ξ΅ : (n : β„•) β†’ compactβˆ™(X n)
   -- u : β„•βˆž
   -- p  : Y β†’ β‚‚

   yβ‚€ : Y
   yβ‚€ n r = pr₁(Ξ΅ n (p ∘ (F n u r)))

   lemma₁ : (n : β„•) β†’ ΞΉ n ≑ u β†’ p yβ‚€ ≑ ₁ β†’ (y : Y) β†’ p y ≑ ₁
   lemma₁ n r e = claim₃
    where
     claimβ‚€ : (y : Y) β†’ p (F n u r (G n u r y)) ≑ p y
     claimβ‚€ y = ap p (FG n u r y)

     claim₁ : p (F n u r (G n u r yβ‚€)) ≑ ₁ β†’ (x : X n) β†’ p (F n u r x) ≑ ₁
     claim₁ =  prβ‚‚(Ξ΅ n (p ∘ (F n u r)))

     claimβ‚‚ : (x : X n) β†’ p (F n u r x) ≑ ₁
     claimβ‚‚ = claim₁ (claimβ‚€ yβ‚€ βˆ™ e)

     claim₃ : (y : Y) β†’ p y ≑ ₁
     claim₃ y = (claimβ‚€ y)⁻¹ βˆ™ claimβ‚‚ (G n u r y)

   lemmaβ‚‚ : u ≑ ∞ β†’ p yβ‚€ ≑ ₁ β†’ (y : Y) β†’ p y ≑ ₁
   lemmaβ‚‚ r e y = ap p (H u r y yβ‚€) βˆ™ e

   lemma₁' : p yβ‚€ ≑ ₁ β†’ (y : Y) β†’ p y ≑ β‚€ β†’ (n : β„•) β†’ ΞΉ n β‰’ u
   lemma₁' e y s n r = zero-is-not-one (s ⁻¹ βˆ™ lemma₁ n r e y)

   lemmaβ‚‚' : p yβ‚€ ≑ ₁ β†’ (y : Y) β†’ p y ≑ β‚€ β†’ u β‰’ ∞
   lemmaβ‚‚' e y s r = zero-is-not-one (s ⁻¹ βˆ™ lemmaβ‚‚ r e y)

   lemma : p yβ‚€ ≑ ₁ β†’ (y : Y) β†’ p y ≑ ₁
   lemma r y = different-from-β‚€-equal-₁
                (Ξ» s β†’ lemmaβ‚‚' r y s
                        (not-finite-is-∞ feβ‚€
                          (Ξ» n q β†’ lemma₁' r y s n (q ⁻¹))))

\end{code}

 Finally, we can show that the squashed sum of any sequence of
 compact sets is itself compact, as claimed above:

\begin{code}

 Ξ£α΄΅-compactβˆ™ : {X : β„• β†’ 𝓀₀ Μ‡ } β†’ ((n : β„•) β†’ compactβˆ™(X n)) β†’ compactβˆ™(Ξ£α΄΅ X)
 Ξ£α΄΅-compactβˆ™ {X} f = Ξ£-compactβˆ™ β„•βˆž-compactβˆ™ (extension-compactβˆ™ {X} f)

\end{code}

 Added 2 May 2014.

 We show that the old and new squashed sums agree.

\begin{code}

 open import UF-EquivalenceExamples

 agreement-lemma : (X : β„• β†’ 𝓀₀ Μ‡ ) (u : β„•βˆž)
                 β†’ (X / ΞΉ) u ≃ Ξ  (Ξ» x β†’ ΞΉ x ≑ u β†’ X x)
 agreement-lemma X = 2nd-Ξ -extension-formula X ΞΉ

 agreement : (X : β„• β†’ 𝓀₀ Μ‡ ) β†’ Σ¹ X ≃ Ξ£α΄΅ X
 agreement X = Ξ£-cong (agreement-lemma X)

\end{code}