From 53e400eca9b78a6589f85b6908d7a0ae2cc95680 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Axel=20Ljungstr=C3=B6m?=
 <49276137+aljungstrom@users.noreply.github.com>
Date: Thu, 19 Sep 2024 10:13:34 +0200
Subject: [PATCH] Connected CW complexes (#1133)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* t

* duplicate

* wups

* rme

* ganea stuff

* w

* w

* w

* fix

* stuff

* stuff

* more

* ..

* done?

* wups

* wups

* wups

* fixes

* ugh...

* wups

* stuff

* stuff

* stuff

* stuf

* More

* stuff

* stuff

* stuff

* done?

* stuff

* cleanup

* readme

* wups

* ugh

* wups

* broken code

* ojdå

* comments

* Pointed

* done?

* p2

* stuff

* wip...

* stuff

* almost

* pretty much done

* cleaning

* cleaning

* connected done?

* connected clean

* minor

* fixes
---
 Cubical/CW/Base.agda                          |    8 +
 Cubical/CW/Connected.agda                     | 1323 +++++++++++++++++
 Cubical/CW/Properties.agda                    |   35 +
 Cubical/CW/Subcomplex.agda                    |   74 +-
 Cubical/Data/Fin/Inductive/Base.agda          |    3 +
 Cubical/Data/Fin/Inductive/Properties.agda    |  205 ++-
 Cubical/Data/List/Base.agda                   |    4 +
 Cubical/Data/Sequence/Base.agda               |   26 +
 Cubical/Data/Sequence/Properties.agda         |  186 ++-
 Cubical/Data/Sum/Properties.agda              |   64 +
 Cubical/Foundations/Prelude.agda              |    4 +
 Cubical/HITs/Pushout/Properties.agda          |  691 ++++++++-
 .../HITs/SequentialColimit/Properties.agda    |  103 +-
 Cubical/HITs/SphereBouquet/Properties.agda    |   38 +
 Cubical/HITs/Wedge/Properties.agda            |  385 ++++-
 Cubical/Homotopy/Connected.agda               |    6 +
 Cubical/Relation/Nullary/Properties.agda      |    6 +
 17 files changed, 3065 insertions(+), 96 deletions(-)
 create mode 100644 Cubical/CW/Connected.agda

diff --git a/Cubical/CW/Base.agda b/Cubical/CW/Base.agda
index 8f94d5531e..6b9cf256c5 100644
--- a/Cubical/CW/Base.agda
+++ b/Cubical/CW/Base.agda
@@ -7,6 +7,7 @@ module Cubical.CW.Base where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Pointed
 
 open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
 open import Cubical.Data.Nat.Order
@@ -102,6 +103,9 @@ isFinCW {ℓ = ℓ} X =
 finCW : (ℓ : Level) → Type (ℓ-suc ℓ)
 finCW ℓ = Σ[ A ∈ Type ℓ ] ∥ isFinCW A ∥₁
 
+finCW∙ : (ℓ : Level) → Type (ℓ-suc ℓ)
+finCW∙ ℓ = Σ[ A ∈ Pointed ℓ ] ∥ isFinCW (fst A) ∥₁
+
 finCWexplicit : (ℓ : Level) → Type (ℓ-suc ℓ)
 finCWexplicit ℓ = Σ[ A ∈ Type ℓ ] (isFinCW A)
 
@@ -147,6 +151,10 @@ to_cofibCW n C x = inr x
 CW↪∞ : (C : CWskel ℓ) → (n : ℕ) → fst C n → realise C
 CW↪∞ C n x = incl x
 
+CW↪Iterate : ∀ {ℓ} (T : CWskel ℓ) (n m : ℕ) → fst T n → fst T (m +ℕ n)
+CW↪Iterate T n zero = idfun _
+CW↪Iterate T n (suc m) x = CW↪ T (m +ℕ n) (CW↪Iterate T n m x)
+
 finCW↑ : (n m : ℕ) → (m ≥ n) → finCWskel ℓ n → finCWskel ℓ m
 fst (finCW↑ m n p C) = fst C
 fst (snd (finCW↑ m n p C)) = snd C .fst
diff --git a/Cubical/CW/Connected.agda b/Cubical/CW/Connected.agda
new file mode 100644
index 0000000000..07e8376331
--- /dev/null
+++ b/Cubical/CW/Connected.agda
@@ -0,0 +1,1323 @@
+{-# OPTIONS --safe --lossy-unification #-}
+
+{-
+This file contains the definition of an n-connected CW complex. This
+is defined by saying that it has non-trivial cells only in dimension
+≥n.
+
+The main result is packaged up in makeConnectedCW. This says that the
+usual notion of connectedness in terms of truncations (merely)
+coincides with the above definition for CW complexes.
+-}
+
+module Cubical.CW.Connected where
+
+open import Cubical.CW.Base
+open import Cubical.CW.Properties
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Transport
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Order.Inductive
+open import Cubical.Data.Fin.Inductive.Base
+open import Cubical.Data.Fin.Inductive.Properties as Ind
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sequence
+open import Cubical.Data.Unit
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool
+
+open import Cubical.HITs.Sn
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Susp
+open import Cubical.HITs.SequentialColimit
+open import Cubical.HITs.SphereBouquet
+open import Cubical.HITs.PropositionalTruncation as PT
+open import Cubical.HITs.Truncation as TR
+open import Cubical.HITs.Wedge
+
+open import Cubical.Axiom.Choice
+open import Cubical.Relation.Nullary
+
+open import Cubical.Homotopy.Connected
+
+open Sequence
+
+private
+  variable
+    ℓ ℓ' ℓ'' : Level
+
+------ Definitions ------
+
+-- An n-connected CW complex has one 0-cell and no m<n-cells.
+yieldsConnectedCWskel : (A : ℕ → Type ℓ) (n : ℕ) → Type _
+yieldsConnectedCWskel A k =
+  Σ[ sk ∈ yieldsCWskel A ] ((sk .fst 0 ≡ 1) × ((n : ℕ) → n <ᵗ k → sk .fst (suc n) ≡ 0))
+
+-- Alternatively, we may say that its colimit is n-connected
+yieldsCombinatorialConnectedCWskel : (A : ℕ → Type ℓ) (n : ℕ) → Type _
+yieldsCombinatorialConnectedCWskel A n =
+  Σ[ sk ∈ yieldsCWskel A ] isConnected (2 +ℕ n) (realise (_ , sk))
+
+connectedCWskel : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
+connectedCWskel ℓ n = Σ[ X ∈ (ℕ → Type ℓ) ] (yieldsConnectedCWskel X n)
+
+combinatorialConnectedCWskel : (ℓ : Level) (n : ℕ) → Type (ℓ-suc ℓ)
+combinatorialConnectedCWskel ℓ n =
+  Σ[ X ∈ (ℕ → Type ℓ) ] (yieldsCombinatorialConnectedCWskel X n)
+
+isConnectedCW : ∀ {ℓ} (n : ℕ) → Type ℓ → Type (ℓ-suc ℓ)
+isConnectedCW {ℓ = ℓ} n A =
+  Σ[ sk ∈ connectedCWskel ℓ n ] realise (_ , (snd sk .fst)) ≃ A
+
+isConnectedCW' : ∀ {ℓ} (n : ℕ) → Type ℓ → Type (ℓ-suc ℓ)
+isConnectedCW' {ℓ = ℓ} n A =
+  Σ[ sk ∈ combinatorialConnectedCWskel ℓ n ] realise (_ , (snd sk .fst)) ≃ A
+
+--- Goal: show that these two definitions coincide (note that indexing is off by 2) ---
+-- For the base case, we need to analyse α₀ : Fin n × S⁰ → X₁ (recall,
+-- indexing of skeleta is shifted by 1). In partiuclar, we will need
+-- to show that if X is connected, then either X₁ is contractible or
+-- there is some a ∈ Fin n s.t. α₀(a,-) is injective. This will allow
+-- us to iteratively shrink X₁ by contracting the image of α₀(a,-).
+
+-- Decision producedures
+inhabitedFibres?-Fin×S⁰ : {A : Type ℓ}
+  (da : Discrete A) (n : ℕ) (f : Fin n × S₊ 0 → A)
+  → inhabitedFibres? f
+inhabitedFibres?-Fin×S⁰ {A = A} da n =
+  subst (λ C → (f : C → A) → inhabitedFibres? f)
+        (isoToPath (invIso Iso-Fin×Bool-Fin))
+        (inhabitedFibres?Fin da _)
+
+private
+  allConst? : {A : Type ℓ} {n : ℕ} (dis : Discrete A)
+    → (t : Fin n → S₊ 0 → A)
+    → ((x : Fin n) → t x ≡ λ _ → t x true)
+     ⊎ (Σ[ x ∈ Fin n ] ¬ (t x true ≡ t x false))
+  allConst? {n = zero} dis t = inl λ {()}
+  allConst? {n = suc n} dis t
+    with (dis (t fzero true) (t fzero false))
+       | (allConst? {n = n} dis λ x p → t (fsuc x) p)
+  ... | yes p | inl x =
+    inl (Ind.elimFin-alt (funExt
+          (λ { false → sym p ; true → refl})) x)
+  ... | yes p | inr x = inr (_ , (snd x))
+  ... | no ¬p | q = inr (_ , ¬p)
+
+-- α₀ must have a section
+isSurj-α₀ : (n m : ℕ) (f : Fin n × S₊ 0 → Fin (suc (suc m)))
+  → isConnected 2 (Pushout f fst)
+  → (y : _) → Σ[ x ∈ _ ] f x ≡ y
+isSurj-α₀ n m f c y with (inhabitedFibres?-Fin×S⁰ DiscreteFin n f y)
+... | inl x = x
+isSurj-α₀ n m f c x₀ | inr q = ⊥.rec nope
+  where
+  F∘inl : Fin (suc (suc m)) → Type
+  F∘inl = elimFinChoose x₀ ⊥ λ _ _ → Unit
+
+  lem : (fa : _) (a : _) → f a ≡ fa → F∘inl fa ≡ Unit
+  lem = elimFinChoose x₀
+        (λ s t → ⊥.rec (q _ t))
+         λ s t b c → elimFinChooseβ x₀ ⊥ (λ _ _ → Unit) .snd s t
+
+  F : Pushout f fst → Type
+  F (inl x) = F∘inl x
+  F (inr x) = Unit
+  F (push a i) = lem (f a) a refl i
+
+  nope : ⊥
+  nope = TR.rec isProp⊥
+            (λ q → transport (elimFinChooseβ x₀ ⊥ (λ _ _ → Unit) .fst)
+                     (subst F (sym q)
+                       (transport (sym (elimFinChooseβ x₀ ⊥
+                         (λ _ _ → Unit) .snd _
+                           (containsTwoFin x₀ .snd ∘ sym))) tt)))
+            (Iso.fun (PathIdTruncIso 1)
+              (isContr→isProp c
+               ∣ inl x₀ ∣
+               ∣ inl (containsTwoFin x₀ .fst) ∣))
+
+-- α₀ can't be constant in every component (as this would imply that
+-- the 1-skeleton X₂ is a disconnected set of loops).
+notAllLoops-α₀ : (n m : ℕ) (f : Fin n × S₊ 0 → Fin (suc (suc m)))
+  → isConnected 2 (Pushout f fst)
+  → Σ[ x ∈ Fin n ] (¬ f (x , true) ≡ f (x , false))
+notAllLoops-α₀ n m f c with (allConst? DiscreteFin (λ x y → f (x , y)))
+... | inr x = x
+notAllLoops-α₀ n m f c | inl q =
+  ⊥.rec (TR.rec isProp⊥ (λ p → subst T p tt)
+           (Iso.fun(PathIdTruncIso 1)
+             (isContr→isProp c
+               ∣ inl flast ∣ ∣ inl fzero ∣)))
+  where
+  inrT : Fin n → Type
+  inrT x with (DiscreteFin (f (x , true)) fzero)
+  ... | yes p = ⊥
+  ... | no ¬p = Unit
+
+  inlT : Fin (suc (suc m)) → Type
+  inlT (zero , p) = ⊥
+  inlT (suc x , p) = Unit
+
+  inlrT-pre : (a : _) → inlT (f (a , true)) ≡ inrT a
+  inlrT-pre a with ((DiscreteFin (f (a , true)) fzero))
+  ... | yes p = cong inlT p
+  inlrT-pre s | no ¬p with (f (s , true))
+  ... | zero , tt = ⊥.rec (¬p refl)
+  ... | suc q , t = refl
+
+  inlrT : (a : _) → inlT (f a) ≡ inrT (fst a)
+  inlrT (b , false) = cong inlT (funExt⁻ (q b) false) ∙ inlrT-pre b
+  inlrT (b , true) = inlrT-pre b
+
+  T : Pushout f fst → Type
+  T (inl x) = inlT x
+  T (inr x) = inrT x
+  T (push a i) = inlrT a i
+
+{- Technical lemma: given a map f : A × Bool → Unit ⊎ B with B
+pointed, this map can be extended to a map F : (Unit ⊎ A) × Bool →
+Unit ⊎ B defined by sending
+
+(inl tt , false) ↦ inl tt, and
+(inl tt , true) ↦ inr b₀
+
+Consider the pushout
+(Unit ⊎ A) × Bool -fst--→ Unit ⊎ A
+      |                        ∣
+      F                        ∣
+      |                        ∣
+      ↓                     ⌜  ↓
+   Unit ⊎ B ---------------→ P
+
+P is equivalent to the pushout
+
+Consider the pushout
+    A × Bool ----fst--------→ A
+      |                        |
+      f                        |
+      ↓                        |
+   Unit ⊎ B                   |
+      |                        |
+ const⋆ ⊎ id                  |
+      ↓                     ⌜  ↓
+      B --------------------→ Q
+-}
+
+module shrinkPushoutLemma (A : Type ℓ) (B : Type ℓ')
+  (f : A × Bool → Unit ⊎ B) (b₀ : B) where
+
+  F : (Unit ⊎ A) × Bool → Unit ⊎ B
+  F (inl tt , false) = inl tt
+  F (inl tt , true) = inr b₀
+  F (inr a , x) = f (a , x)
+
+  g : Unit ⊎ B → B
+  g (inl x) = b₀
+  g (inr x) = x
+
+  Unit⊎A→Pushout-g∘f : (x : Unit ⊎ A) → Pushout (g ∘ f) fst
+  Unit⊎A→Pushout-g∘f (inl x) = inl b₀
+  Unit⊎A→Pushout-g∘f (inr x) = inr x
+
+  Unit⊎A→Pushout-g∘f-fst : (a : _)
+    → inl (g (F a)) ≡ Unit⊎A→Pushout-g∘f (fst a)
+  Unit⊎A→Pushout-g∘f-fst (inl x , false) = refl
+  Unit⊎A→Pushout-g∘f-fst (inl x , true) = refl
+  Unit⊎A→Pushout-g∘f-fst (inr x , false) = push (x , false)
+  Unit⊎A→Pushout-g∘f-fst (inr x , true) = push (x , true)
+
+  PushoutF→Pushout-g∘f : Pushout F fst → Pushout (g ∘ f) fst
+  PushoutF→Pushout-g∘f (inl x) = inl (g x)
+  PushoutF→Pushout-g∘f (inr x) = Unit⊎A→Pushout-g∘f x
+  PushoutF→Pushout-g∘f (push a i) = Unit⊎A→Pushout-g∘f-fst a i
+
+  Unit⊎A→Pushout-g∘f-fst₂ : (a : _) (b : _)
+    → Path (Pushout F fst)
+            (inl (inr (g (f (a , b))))) (inl (f (a , b)))
+  Unit⊎A→Pushout-g∘f-fst₂ a b with (f (a , b))
+  Unit⊎A→Pushout-g∘f-fst₂ a b | inl x =
+    (push (inl tt , true)) ∙ sym (push (inl tt , false))
+  ... | inr x = refl
+
+  Pushout-g∘f-fst→Unit⊎A : Pushout (g ∘ f) fst → Pushout F fst
+  Pushout-g∘f-fst→Unit⊎A (inl x) = inl (inr x)
+  Pushout-g∘f-fst→Unit⊎A (inr x) = inr (inr x)
+  Pushout-g∘f-fst→Unit⊎A (push (a , false) i) =
+    (Unit⊎A→Pushout-g∘f-fst₂ a false ∙ push (inr a , false)) i
+  Pushout-g∘f-fst→Unit⊎A (push (a , true) i) =
+    (Unit⊎A→Pushout-g∘f-fst₂ a true ∙ push (inr a , true)) i
+
+  PushoutF→Pushout-g∘f→Unit⊎Aₗ : (x : _)
+    → Pushout-g∘f-fst→Unit⊎A (PushoutF→Pushout-g∘f (inl x)) ≡ (inl x)
+  PushoutF→Pushout-g∘f→Unit⊎Aₗ (inl x) =
+    push (inl tt , true) ∙ sym (push (inl tt , false))
+  PushoutF→Pushout-g∘f→Unit⊎Aₗ (inr x) = refl
+
+  PushoutF→Pushout-g∘f→Unit⊎Aᵣ : (x : _)
+    → Pushout-g∘f-fst→Unit⊎A (PushoutF→Pushout-g∘f (inr x)) ≡ (inr x)
+  PushoutF→Pushout-g∘f→Unit⊎Aᵣ (inl x) = push (inl tt , true)
+  PushoutF→Pushout-g∘f→Unit⊎Aᵣ (inr x) = refl
+
+  private
+    lem₁ : (x : A) → PushoutF→Pushout-g∘f→Unit⊎Aₗ (f (x , false))
+                   ≡ Unit⊎A→Pushout-g∘f-fst₂ x false
+    lem₁ x with (f (x , false))
+    ... | inl x₁ = refl
+    ... | inr x₁ = refl
+
+    lem₂ : (x : A) → PushoutF→Pushout-g∘f→Unit⊎Aₗ (f (x , true))
+                   ≡ Unit⊎A→Pushout-g∘f-fst₂ x true
+    lem₂ x with (f (x , true))
+    ... | inl x₁ = refl
+    ... | inr x₁ = refl
+
+  Pushout-g∘f→PushoutF→Pushout-g∘f : (x : _)
+    → Pushout-g∘f-fst→Unit⊎A (PushoutF→Pushout-g∘f x) ≡ x
+  Pushout-g∘f→PushoutF→Pushout-g∘f (inl x) = PushoutF→Pushout-g∘f→Unit⊎Aₗ x
+  Pushout-g∘f→PushoutF→Pushout-g∘f (inr x) = PushoutF→Pushout-g∘f→Unit⊎Aᵣ x
+  Pushout-g∘f→PushoutF→Pushout-g∘f (push (inl x , false) i) j =
+    compPath-filler (push (inl tt , true)) (sym (push (inl tt , false))) (~ i) j
+  Pushout-g∘f→PushoutF→Pushout-g∘f (push (inr x , false) i) j =
+    (lem₁ x
+    ◁ flipSquare
+       (symP (compPath-filler'
+         (Unit⊎A→Pushout-g∘f-fst₂ x false) (push (inr x , false))))) i j
+  Pushout-g∘f→PushoutF→Pushout-g∘f (push (inl x , true) i) j =
+    push (inl x , true) (i ∧ j)
+  Pushout-g∘f→PushoutF→Pushout-g∘f (push (inr x , true) i) j =
+    (lem₂ x
+    ◁ flipSquare
+       (symP (compPath-filler'
+         (Unit⊎A→Pushout-g∘f-fst₂ x true) (push (inr x , true))))) i j
+
+  PushoutF→Pushout-g∘f→Unit⊎A-push : (b : _) (a : _)
+    → cong PushoutF→Pushout-g∘f (Unit⊎A→Pushout-g∘f-fst₂ b a) ≡ refl
+  PushoutF→Pushout-g∘f→Unit⊎A-push b a with (f (b , a))
+  ... | inl x = cong-∙ PushoutF→Pushout-g∘f
+                       (push (inl tt , true)) (sym (push (inl tt , false)))
+              ∙ sym (rUnit refl)
+  ... | inr x = refl
+
+  PushoutF→Pushout-g∘f→PushoutF : (x : _)
+    → PushoutF→Pushout-g∘f (Pushout-g∘f-fst→Unit⊎A x) ≡ x
+  PushoutF→Pushout-g∘f→PushoutF (inl x) = refl
+  PushoutF→Pushout-g∘f→PushoutF (inr x) = refl
+  PushoutF→Pushout-g∘f→PushoutF (push (b , false) i) j =
+    (cong-∙ PushoutF→Pushout-g∘f
+      (Unit⊎A→Pushout-g∘f-fst₂ b false) (push (inr b , false))
+    ∙ cong (_∙ push (b , false)) (PushoutF→Pushout-g∘f→Unit⊎A-push b false)
+    ∙ sym (lUnit _)) j i
+  PushoutF→Pushout-g∘f→PushoutF (push (b , true) i) j =
+    (cong-∙ PushoutF→Pushout-g∘f
+      (Unit⊎A→Pushout-g∘f-fst₂ b true) (push (inr b , true))
+    ∙ cong (_∙ push (b , true)) (PushoutF→Pushout-g∘f→Unit⊎A-push b true)
+    ∙ sym (lUnit _)) j i
+
+  Iso-PushoutF-Pushout-g∘f : Iso (Pushout F fst) (Pushout (g ∘ f) fst)
+  Iso.fun Iso-PushoutF-Pushout-g∘f = PushoutF→Pushout-g∘f
+  Iso.inv Iso-PushoutF-Pushout-g∘f = Pushout-g∘f-fst→Unit⊎A
+  Iso.rightInv Iso-PushoutF-Pushout-g∘f = PushoutF→Pushout-g∘f→PushoutF
+  Iso.leftInv Iso-PushoutF-Pushout-g∘f = Pushout-g∘f→PushoutF→Pushout-g∘f
+
+
+module CWLemmas-0Connected where
+  -- For any (attaching) map f : Fin (2 + n) × S⁰ → Fin (2 + m) with
+  -- f(1 + n, -) non-constant yields has the same pushout as some f' : Fin
+  -- k × S⁰ → Fin (1 + n).
+  shrinkImageAttachingMapLem : (n m : ℕ)
+       (f : Fin (suc (suc n)) × S₊ 0 → Fin (suc (suc m)))
+    → f (flast , false) ≡ flast
+    → (t : f (flast , true) .fst <ᵗ suc m)
+    → Σ[ k ∈ ℕ ] Σ[ f' ∈ (Fin k × S₊ 0 → Fin (suc m)) ]
+         Iso (Pushout f fst)
+             (Pushout f' fst)
+  shrinkImageAttachingMapLem n m f p q = (suc n)
+    , _
+    , compIso (invIso (pushoutIso _ _ _ _
+                (isoToEquiv (Σ-cong-iso-fst (invIso Iso-Fin-Unit⊎Fin)))
+                (isoToEquiv (invIso Iso-Fin-Unit⊎Fin))
+                (isoToEquiv (invIso Iso-Fin-Unit⊎Fin))
+                (funExt (uncurry help))
+                (funExt λ x → refl)))
+       (Iso-PushoutF-Pushout-g∘f
+                 (λ x → Fin→Unit⊎Fin (f ((injectSuc (fst x)) , (snd x))))
+                 (f (flast , true) .fst , q))
+    where
+    open shrinkPushoutLemma (Fin (suc n)) (Fin (suc m))
+
+    help : (y : Unit ⊎ Fin (suc n)) (x : Bool)
+      → Unit⊎Fin→Fin
+          (F (λ x₁ → Ind.elimFin (inl tt) inr (f (injectSuc (fst x₁) , snd x₁)))
+          (f (flast , true) .fst , q) (y , x))
+       ≡ f (Unit⊎Fin→Fin y , x)
+    help (inl a) false = sym p
+    help (inl b) true = Σ≡Prop (λ _ → isProp<ᵗ) refl
+    help (inr a) false = Iso.leftInv Iso-Fin-Unit⊎Fin _
+    help (inr a) true = Iso.leftInv Iso-Fin-Unit⊎Fin _
+
+  -- If the domain of f is instead Fin 1 × S⁰, this must also be the
+  -- codomain of f.
+  Fin1×Bool≅ImageAttachingMap : (m : ℕ)
+    (f : Fin 1 × S₊ 0 → Fin (suc (suc m)))
+    → isConnected 2 (Pushout f fst)
+    → Iso (Fin 1 × S₊ 0) (Fin (suc (suc m)))
+  Fin1×Bool≅ImageAttachingMap m f c = mainIso
+    where
+    f' : Bool → Fin (suc (suc m))
+    f' = f ∘ (fzero ,_)
+
+    f'-surj : (x : _) → Σ[ t ∈ Bool ] (f' t ≡ x)
+    f'-surj x =
+      isSurj-α₀ (suc zero) m f c x .fst .snd
+      , cong f (ΣPathP (isPropFin1 _ _ , refl))
+      ∙ isSurj-α₀ (suc zero) m f c x .snd
+    f-true≠f-false : (x : _) → f' true ≡ x →  ¬ f' true ≡ f' false
+    f-true≠f-false (zero , q) p r = lem (f'-surj fone)
+      where
+      lem : Σ[ t ∈ Bool ] (f' t ≡ fone) → ⊥
+      lem (false , s) = snotz (cong fst (sym s ∙ sym r ∙ p))
+      lem (true , s) = snotz (cong fst (sym s ∙ p))
+    f-true≠f-false (suc x , q) p r = lem (f'-surj fzero)
+      where
+      lem : Σ[ t ∈ Bool ] (f' t ≡ fzero) → ⊥
+      lem (false , s) = snotz (cong fst (sym p ∙ r ∙ s))
+      lem (true , s) = snotz (cong fst (sym p ∙ s))
+
+    f-inj : (x y : _) → f x ≡ f y → x ≡ y
+    f-inj ((zero , tt) , false) ((zero , tt) , false) p = refl
+    f-inj ((zero , tt) , false) ((zero , tt) , true) p =
+      ⊥.rec (f-true≠f-false _ refl (sym p))
+    f-inj ((zero , tt) , true) ((zero , tt) , false) p =
+      ⊥.rec (f-true≠f-false _ refl p)
+    f-inj ((zero , tt) , true) ((zero , tt) , true) p = refl
+
+    mainIso : Iso (Fin 1 × S₊ 0) (Fin (suc (suc m)))
+    Iso.fun mainIso = f
+    Iso.inv mainIso x = isSurj-α₀ (suc zero) m f c x .fst
+    Iso.rightInv mainIso x = isSurj-α₀ 1 m f c x .snd
+    Iso.leftInv mainIso ((zero , tt) , x) =
+     (f-inj _ _ (isSurj-α₀ 1 m f c (f (fzero , x)) .snd))
+
+  -- Strengthening of shrinkImageAttachingMapLem for domain of f of
+  -- arbitrary cardinality.
+  shrinkImageAttachingMap : (n m : ℕ) (f : Fin n × S₊ 0 → Fin (suc (suc m)))
+    → isConnected 2 (Pushout f fst)
+    → Σ[ k ∈ ℕ ] Σ[ f' ∈ (Fin k × S₊ 0 → Fin (suc m)) ]
+         Iso (Pushout f fst)
+             (Pushout f' fst)
+  shrinkImageAttachingMap zero m f c =
+    ⊥.rec (snd (notAllLoops-α₀ zero m f c .fst))
+  shrinkImageAttachingMap (suc zero) zero f c =
+    0 , ((λ ()) , compIso isoₗ (PushoutEmptyFam (snd ∘ fst) snd))
+    where
+    isoₗ : Iso (Pushout f fst) (Fin 1)
+    isoₗ = PushoutAlongEquiv
+           (isoToEquiv (Fin1×Bool≅ImageAttachingMap zero f c)) fst
+  shrinkImageAttachingMap (suc zero) (suc m) f c =
+    ⊥.rec (Fin≠Fin (snotz ∘ sym ∘ cong (predℕ ∘ predℕ))
+          mainIso)
+    where
+    mainIso : Iso (Fin 2) (Fin (3 +ℕ m))
+    mainIso =
+      compIso
+        (compIso
+          (invIso rUnit×Iso)
+          (compIso
+            (Σ-cong-iso
+              (invIso Iso-Bool-Fin2)
+              (λ _ → isContr→Iso (tt , (λ _ → refl))
+                        (inhProp→isContr fzero isPropFin1)))
+              Σ-swap-Iso))
+        (Fin1×Bool≅ImageAttachingMap (suc m) f c)
+  shrinkImageAttachingMap (suc (suc n)) m f c =
+      main .fst , main .snd .fst
+    , compIso correctIso (main .snd .snd)
+    where
+    t = notAllLoops-α₀ (suc (suc n)) m f c
+
+    abstract
+      x₀ : Fin (suc (suc n))
+      x₀ = fst t
+
+      xpath : ¬ (f (x₀ , true) ≡ f (x₀ , false))
+      xpath = snd t
+
+    Fin×S⁰-swapIso : Iso (Fin (suc (suc n)) × S₊ 0) (Fin (suc (suc n)) × S₊ 0)
+    Fin×S⁰-swapIso = Σ-cong-iso-fst (swapFinIso flast x₀)
+
+    FinIso2 : Iso (Fin (suc (suc m))) (Fin (suc (suc m)))
+    FinIso2 = swapFinIso (f (x₀ , false)) flast
+
+    f' : Fin (suc (suc n)) × S₊ 0 → Fin (suc (suc m))
+    f' = Iso.fun FinIso2 ∘ f ∘ Iso.fun Fin×S⁰-swapIso
+
+    f'≡flast : f' (flast , false) ≡ flast
+    f'≡flast = cong (Iso.fun FinIso2 ∘ f)
+            (cong (_, false) (swapFinβₗ flast x₀))
+        ∙ swapFinβₗ (f (x₀ , false)) flast
+
+    ¬f'≡flast : ¬ (f' (flast , true) ≡ flast)
+    ¬f'≡flast p = xpath (cong f (ΣPathP (sym (swapFinβₗ flast x₀) , refl))
+                  ∙ sym (Iso.rightInv FinIso2 _)
+                  ∙ cong (Iso.inv FinIso2) (p ∙ sym f'≡flast)
+                  ∙ Iso.rightInv FinIso2 _
+                  ∙ cong f (ΣPathP (swapFinβₗ flast x₀ , refl)))
+
+    f'-bound : fst (f' (flast , true)) <ᵗ suc m
+    f'-bound = ≠flast→<ᵗflast _ ¬f'≡flast
+
+    main = shrinkImageAttachingMapLem _ _ f' f'≡flast f'-bound
+
+    correctIso : Iso (Pushout f fst) (Pushout f' fst)
+    correctIso = pushoutIso _ _ _ _
+      (isoToEquiv Fin×S⁰-swapIso)
+      (isoToEquiv FinIso2)
+      (isoToEquiv (swapFinIso flast x₀))
+      (funExt (λ x → cong (FinIso2 .Iso.fun ∘ f)
+                      (sym (Iso.rightInv Fin×S⁰-swapIso x))))
+      refl
+
+  -- the main lemma: a pushout of f : Fin n × S⁰ → Fin m is equivalent
+  -- to one of the constant funktion Fin k × S⁰ → Fin 1 for some k.
+
+  Contract1Skel : (n m : ℕ) (f : Fin n × S₊ 0 → Fin m)
+    → isConnected 2 (Pushout f fst)
+    → Σ[ k ∈ ℕ ]
+         Iso (Pushout f fst)
+             (Pushout {A = Fin k × S₊ 0} {B = Fin 1} (λ _ → fzero) fst)
+  Contract1Skel zero zero f c = ⊥.rec (TR.rec (λ()) help (fst c))
+    where
+    help : ¬ Pushout f fst
+    help = elimProp _ (λ _ → λ ()) snd snd
+  Contract1Skel (suc n) zero f c = ⊥.rec (f (fzero , true) .snd)
+  Contract1Skel n (suc zero) f c = n
+    , pushoutIso _ _ _ _ (idEquiv _) (idEquiv _) (idEquiv _)
+      (funExt (λ x → isPropFin1 _ _)) refl
+  Contract1Skel zero (suc (suc m)) f c =
+    ⊥.rec (TR.rec (λ()) (snotz ∘ sym ∘ cong fst)
+            (Iso.fun (PathIdTruncIso _)
+              (isContr→isProp (subst (isConnected 2) (isoToPath help) c)
+                ∣ fzero ∣ ∣ fone ∣)))
+    where
+    help : Iso (Pushout f fst) (Fin (suc (suc m)))
+    help = invIso (PushoutEmptyFam (λ()) λ())
+  Contract1Skel (suc n) (suc (suc m)) f c
+    with (Contract1Skel _ (suc m)
+          (shrinkImageAttachingMap (suc n) m f c .snd .fst)
+         (subst (isConnected 2)
+           (isoToPath
+             (shrinkImageAttachingMap (suc n) m f c .snd .snd)) c))
+  ... | (k , e) = k
+    , compIso (shrinkImageAttachingMap (suc n) m f c .snd .snd) e
+
+-- Uning this, we can show that a 0-connected CW complex can be
+-- approximated by one with trivial 1-skeleton.
+module _ (A : ℕ → Type ℓ) (sk+c : yieldsCombinatorialConnectedCWskel A 0) where
+  private
+    open CWLemmas-0Connected
+    c = snd sk+c
+    sk = fst sk+c
+    c' = isConnectedColim→isConnectedSkel (_ , sk) 2 c
+
+    module AC = CWskel-fields (_ , sk)
+
+    e₁ : Iso (Pushout (fst (CW₁-discrete (_ , sk)) ∘ AC.α 1) fst) (A 2)
+    e₁ = compIso (PushoutCompEquivIso (idEquiv _)
+                   (CW₁-discrete (A , sk)) (AC.α 1) fst)
+                 (equivToIso (invEquiv (AC.e 1)))
+
+    liftStr = Contract1Skel _ _ (fst (CW₁-discrete (_ , sk)) ∘ AC.α 1)
+                (isConnectedRetractFromIso 2 e₁ c')
+
+  collapse₁card : ℕ → ℕ
+  collapse₁card zero = 1
+  collapse₁card (suc zero) = fst liftStr
+  collapse₁card (suc (suc x)) = AC.card (suc (suc x))
+
+  collapse₁CWskel : ℕ → Type _
+  collapse₁CWskel zero = Lift ⊥
+  collapse₁CWskel (suc zero) = Lift (Fin 1)
+  collapse₁CWskel (suc (suc n)) = A (suc (suc n))
+
+  collapse₁α : (n : ℕ)
+    → Fin (collapse₁card n) × S⁻ n → collapse₁CWskel n
+  collapse₁α (suc zero) (x , p) = lift fzero
+  collapse₁α (suc (suc n)) = AC.α (2 +ℕ n)
+
+  connectedCWskel→ : yieldsConnectedCWskel collapse₁CWskel 0
+  fst (fst connectedCWskel→) = collapse₁card
+  fst (snd (fst connectedCWskel→)) = collapse₁α
+  fst (snd (snd (fst connectedCWskel→))) = λ()
+  snd (snd (snd (fst connectedCWskel→))) zero =
+    isContr→Equiv (isOfHLevelLift 0 (inhProp→isContr fzero isPropFin1))
+                       ((inr fzero)
+                 , (λ { (inr x) j → inr (isPropFin1 fzero x j) }))
+  snd (snd (snd (fst connectedCWskel→))) (suc zero) =
+    compEquiv (invEquiv (isoToEquiv e₁))
+      (compEquiv (isoToEquiv (snd liftStr))
+      (isoToEquiv (pushoutIso _ _ _ _
+        (idEquiv _) LiftEquiv (idEquiv _)
+        (funExt cohₗ) (funExt cohᵣ))))
+    where
+    -- Agda complains if these proofs are inlined...
+    cohₗ : (x : _) → collapse₁α 1 x ≡ collapse₁α 1 x
+    cohₗ (x , p) = refl
+
+    cohᵣ : (x : Fin (fst liftStr) × Bool) → fst x ≡ fst x
+    cohᵣ x = refl
+  snd (snd (snd (fst connectedCWskel→))) (suc (suc n)) = AC.e (suc (suc n))
+  snd connectedCWskel→ = refl , (λ _ → λ ())
+
+  collapse₁Equiv : (n : ℕ)
+    → realise (_ , sk) ≃ realise (_ , connectedCWskel→ .fst)
+  collapse₁Equiv n =
+    compEquiv
+      (isoToEquiv (Iso-SeqColim→SeqColimShift _ 3))
+      (compEquiv (pathToEquiv (cong SeqColim
+        (cong₂ sequence (λ _ m → A (3 +ℕ m))
+                        λ _ {z} → CW↪ (A , sk) (suc (suc (suc z))))))
+        (invEquiv (isoToEquiv (Iso-SeqColim→SeqColimShift _ 3))))
+
+isConnectedCW→Contr : ∀ {ℓ} (n : ℕ)
+  (sk : connectedCWskel ℓ n) (m : Fin (suc n))
+  → isContr (fst sk (suc (fst m)))
+isConnectedCW→Contr zero sk (zero , p) =
+  isOfHLevelRetractFromIso 0 (equivToIso (CW₁-discrete (_ , snd sk .fst)))
+    (subst isContr (cong Fin (sym (snd sk .snd .fst)))
+      (flast , isPropFin1 _))
+isConnectedCW→Contr (suc n) sk (zero , p) =
+  subst isContr (ua (symPushout _ _)
+               ∙ ua (invEquiv (sk .snd .fst .snd .snd .snd 0)))
+        (isOfHLevelRetractFromIso 0
+          (invIso (PushoutEmptyFam (λ()) (snd sk .fst .snd .snd .fst)))
+            (subst (isContr ∘ Fin) (sym (snd sk .snd .fst))
+              (flast , isPropFin1 _)))
+isConnectedCW→Contr (suc n) sk (suc x , p)
+  with (isConnectedCW→Contr n
+        (fst sk , (snd sk .fst) , ((snd sk .snd .fst)
+                , (λ p w → snd sk .snd .snd p (<ᵗ-trans w <ᵗsucm))))
+                             (x , p))
+... | ind = subst isContr
+               (ua (invEquiv (sk .snd .fst .snd .snd .snd (suc x))))
+               (isOfHLevelRetractFromIso 0
+                 (invIso
+                   (PushoutEmptyFam
+                  (λ p' → ¬Fin0 (subst Fin
+                     (snd sk .snd .snd x p) (fst p')))
+                   λ p' → ¬Fin0 (subst Fin
+                     (snd sk .snd .snd x p) p')))
+                 ind)
+
+makeConnectedCW : ∀ {ℓ} (n : ℕ) {C : Type ℓ}
+  → isCW C
+  → isConnected (suc (suc n)) C
+  → ∥ isConnectedCW n C ∥₁
+makeConnectedCW zero {C = C} (cwsk , e) cA =
+  ∣ (_ , (M .fst , refl , λ p → λ()))
+  , compEquiv (invEquiv (collapse₁Equiv _ _ 0)) (invEquiv e) ∣₁
+  where
+  M = connectedCWskel→ (cwsk .fst)
+       (snd cwsk , subst (isConnected 2) (ua e) cA)
+makeConnectedCW {ℓ = ℓ} (suc n) {C = C} (cwsk , eqv) cA with
+  (makeConnectedCW n (cwsk , eqv) (isConnectedSubtr (suc (suc n)) 1 cA))
+... | s = PT.rec squash₁
+  (λ s → PT.rec squash₁
+    (λ α-pt* → PT.rec squash₁
+      (λ α-pt2*
+        → PT.rec squash₁
+          (λ vanish*
+            → PT.map (uncurry (isConnectedCW-C' s α-pt* α-pt2* vanish*))
+          (∃Improvedβ s α-pt* α-pt2* vanish*))
+          (sphereBouquetVanish s α-pt* α-pt2*
+            (const→C4+n s α-pt* α-pt2*)))
+              (α-pt∙₂ s α-pt*)) (α'2+n∙ s)) s
+  where
+  module _ (ind : isConnectedCW n C) where
+    open CWskel-fields (_ , ind .fst .snd .fst)
+    -- By the induction hypothesis we get a CW structure on C with C (suc n) trivial
+
+    -- some basic abbreviations and lemmas
+    module _ where
+      C* = ind .fst .fst
+
+      2+n = suc (suc n)
+      3+n = suc 2+n
+      4+n = suc 3+n
+
+      C1+n = C* (suc n)
+      C2+n = C* 2+n
+      C3+n = C* 3+n
+      C4+n = C* 4+n
+
+      α2+n = α 2+n
+
+      isConnectedC4+n : isConnected 3+n C4+n
+      isConnectedC4+n = isConnectedCW→isConnectedSkel
+                 (_ , ind .fst .snd .fst) 4+n
+                   (3+n , <ᵗ-trans <ᵗsucm <ᵗsucm)
+                   (subst (isConnected 3+n) (ua (invEquiv (ind .snd)))
+                   cA)
+
+      isConnected3+n : isConnected 2+n C3+n
+      isConnected3+n = isConnectedCW→isConnectedSkel
+                 (_ , ind .fst .snd .fst) 3+n
+                   (2+n , <ᵗ-trans <ᵗsucm <ᵗsucm)
+                   (subst (isConnected 2+n) (ua (invEquiv (ind .snd)))
+                   (isConnectedSubtr 2+n 1 cA))
+
+    -- C₁₊ₙ is trivial
+    Iso-C1+n-Fin1 : Iso C1+n (Fin 1)
+    Iso-C1+n-Fin1 =
+      isContr→Iso (isConnectedCW→Contr n (ind .fst) (n , <ᵗsucm))
+                   (flast , isPropFin1 _)
+
+    -- C₂₊ₙ is a bouquet of spheres
+    Iso-C2+n-SphereBouquet : Iso C2+n (SphereBouquet (suc n) (A (suc n)))
+    Iso-C2+n-SphereBouquet = compIso (equivToIso
+             (ind .fst .snd .fst .snd .snd .snd (suc n)))
+             (compIso
+               (compIso
+                 (compIso
+                   (pushoutIso _ _ _ _ (idEquiv _)
+                     (isoToEquiv (compIso Iso-C1+n-Fin1
+                       (isContr→Iso (flast , isPropFin1 _)
+                         (tt , λ _ → refl))))
+                     (idEquiv _)
+                     refl
+                     refl)
+                   (⋁-cofib-Iso _ (const∙ _ _)))
+                 PushoutSuspIsoSusp )
+               sphereBouquetSuspIso)
+
+    -- We rewrite α along this iso.
+    α'2+n : A 2+n × S₊ (suc n) → SphereBouquet (suc n) (A (suc n))
+    α'2+n = Iso.fun Iso-C2+n-SphereBouquet ∘ α 2+n
+
+    opaque
+      Iso-C3+n-Pushoutα'2+n : Iso (C* 3+n)
+                 (Pushout α'2+n fst)
+      Iso-C3+n-Pushoutα'2+n = compIso (equivToIso (e 2+n))
+                        (pushoutIso _ _ _ _ (idEquiv _)
+                          (isoToEquiv Iso-C2+n-SphereBouquet)
+                          (idEquiv _)
+                          refl
+                          refl)
+
+    -- α is merely pointed
+    α'2+n∙ : ∥ ((x : _) → α'2+n (x , ptSn (suc n)) ≡ inl tt) ∥₁
+    α'2+n∙ = invEq propTrunc≃Trunc1 (invEq (_ , InductiveFinSatAC _ _ _)
+             λ a → isConnectedPath 1
+               (isConnectedSubtr' n 2
+                 (isConnectedSphereBouquet' {n = n})) _ _ .fst)
+
+    -- Let us assume it is pointed (we are proving a proposition in the end)...
+    module _ (α-pt∙ : (x : _) → α'2+n (x , ptSn (suc n)) ≡ inl tt) where
+
+      -- Doing so allows us to lift it to a map of sphere bouquets
+      α∙ : SphereBouquet∙ (suc n) (A 2+n)
+        →∙ SphereBouquet∙ (suc n) (A (suc n))
+      fst α∙ (inl x) = inl tt
+      fst α∙ (inr x) = α'2+n x
+      fst α∙ (push a i) = α-pt∙ a (~ i)
+      snd α∙ = refl
+
+      -- The cofibre of α∙ is C₃₊ₙ
+      opaque
+        Iso-C3+n-cofibα : Iso C3+n
+                   (cofib (fst α∙))
+        Iso-C3+n-cofibα = compIso Iso-C3+n-Pushoutα'2+n (⋁-cofib-Iso _ α∙)
+
+      -- This iso is also merely pointed:
+      α-pt∙₂ : ∥ ((x : A 3+n)
+               → Iso.fun Iso-C3+n-cofibα (α 3+n (x , north)) ≡ inl tt) ∥₁
+      α-pt∙₂ = invEq propTrunc≃Trunc1 (invEq (_ , InductiveFinSatAC _ _ _)
+             λ a → isConnectedPath 1
+                     (isConnectedRetractFromIso 2 (invIso Iso-C3+n-cofibα)
+                     (isConnectedSubtr' n 2 isConnected3+n) ) _ _ .fst)
+
+      -- But again, let us assume it is...
+      module _ (α-pt∙₂ : (x : A 3+n)
+             → Iso.fun Iso-C3+n-cofibα (α 3+n (x , north)) ≡ inl tt) where
+
+        -- Doing so, we can lift α yet again this time to a map
+        -- α↑ : ⋁S²⁺ⁿ → cofib α
+        α↑ : SphereBouquet∙ 2+n (A 3+n)
+         →∙ (cofib (fst α∙) , inl tt)
+        fst α↑ (inl x) = inl tt
+        fst α↑ (inr x) = Iso.fun Iso-C3+n-cofibα (α 3+n x)
+        fst α↑ (push a i) = α-pt∙₂ a (~ i)
+        snd α↑ = refl
+
+        -- The cofibre of this map is C₄₊ₙ
+        Iso-C4+n-cofibα↑ : Iso (C* (4 +ℕ n)) (cofib (fst α↑))
+        Iso-C4+n-cofibα↑ = compIso (equivToIso (e 3+n))
+                (compIso
+                  (pushoutIso _ _ _ _
+                    (idEquiv _)
+                    (isoToEquiv Iso-C3+n-cofibα)
+                    (idEquiv _) refl refl)
+                  (⋁-cofib-Iso _ α↑))
+
+
+
+        opaque
+          Iso-cofibαinr-SphereBouquet :
+            Iso (Pushout {B = cofib (fst α∙)} inr (λ _ → tt))
+                (SphereBouquet 2+n (A 2+n))
+          Iso-cofibαinr-SphereBouquet = compIso (equivToIso (symPushout _ _))
+                    (compIso (Iso-cofibInr-Susp α∙)
+                      sphereBouquetSuspIso)
+
+          Iso-cofibαinr-SphereBouquet∙ :
+            Iso.fun Iso-cofibαinr-SphereBouquet (inl (inl tt)) ≡ inl tt
+          Iso-cofibαinr-SphereBouquet∙ = refl
+
+        -- composing the above iso with α↑ lets us define a map of sphere bouquets:
+        β : SphereBouquet 2+n (A 3+n)
+         → SphereBouquet 2+n (A 2+n)
+        β = (Iso.fun Iso-cofibαinr-SphereBouquet ∘ inl) ∘ fst α↑
+
+        β∙ : SphereBouquet∙ 2+n (A 3+n)
+          →∙ SphereBouquet∙ 2+n (A 2+n)
+        fst β∙ = β
+        snd β∙ = Iso-cofibαinr-SphereBouquet∙
+
+        -- The goal now: show that the cofibre of β is C₄₊ₙ ⋁ S²⁺ⁿ
+        C⋆ = Iso-C4+n-cofibα↑ .Iso.inv (inl tt)
+
+        -- Abbreviation of C₄₊ₙ ⋁ S²⁺ⁿ:
+        C₄₊ₙ⋁SphereBouquet = (C4+n , C⋆)
+           ⋁ SphereBouquet∙ 2+n (A 2+n)
+
+
+        -- Intermediate alternative definition of C₄₊ₙ ⋁ S²⁺ⁿ:
+        C₄₊ₙ⋁SphereBouquetAsPushout =
+          Pushout (Iso.inv Iso-C4+n-cofibα↑ ∘ inr)
+                  (λ x → Iso.fun Iso-cofibαinr-SphereBouquet (inl x))
+
+        -- We geta a map ⋁Sⁿ⁺¹ → C4+n. It is merely constant for
+        -- connectedness reasons and its cofibre is
+        -- C₄₊ₙ⋁SphereBouquetAsPushout by a simple pasting argument.
+        const→C4+n : SphereBouquet (suc n) (A (suc n)) → C4+n
+        const→C4+n x = Iso.inv Iso-C4+n-cofibα↑ (inr (inr x))
+
+        -- Settting up the pushout-pastings:
+        open commSquare
+        open 3-span
+
+        commSquare₁ : commSquare
+        A0 (sp commSquare₁) = cofib (fst α∙)
+        A2 (sp commSquare₁) = SphereBouquet 2+n (A 3+n)
+        A4 (sp commSquare₁) = Unit
+        f1 (sp commSquare₁) = fst α↑
+        f3 (sp commSquare₁) = λ _ → tt
+        P commSquare₁ = cofib (fst α↑)
+        inlP commSquare₁ = inr
+        inrP commSquare₁ = inl
+        comm commSquare₁ = funExt λ x → sym (push x)
+
+        pushoutSquare₁ : PushoutSquare
+        fst pushoutSquare₁ = commSquare₁
+        snd pushoutSquare₁ =
+          subst isEquiv (funExt
+            (λ { (inl x) → refl
+               ; (inr x) → refl
+               ; (push a i) → refl}))
+            (symPushout _ _ .snd)
+
+        commSquare₂ : commSquare
+        A0 (sp commSquare₂) = cofib (fst α∙)
+        A2 (sp commSquare₂) = SphereBouquet (suc n) (A (suc n))
+        A4 (sp commSquare₂) = Unit
+        f1 (sp commSquare₂) = inr
+        f3 (sp commSquare₂) = _
+        P commSquare₂ = SphereBouquet 2+n (A 2+n)
+        inlP commSquare₂ x = Iso.fun Iso-cofibαinr-SphereBouquet (inl x)
+        inrP commSquare₂ _ = Iso.fun Iso-cofibαinr-SphereBouquet (inr tt)
+        comm commSquare₂ =
+          funExt λ x → cong (Iso.fun Iso-cofibαinr-SphereBouquet) (push x)
+
+        pushoutSquare₂ : PushoutSquare
+        fst pushoutSquare₂ = commSquare₂
+        snd pushoutSquare₂ =
+          subst isEquiv (funExt coh)
+            (isoToIsEquiv Iso-cofibαinr-SphereBouquet)
+          where
+          coh : (x : _) → Iso.fun Iso-cofibαinr-SphereBouquet x
+                         ≡ Pushout→commSquare commSquare₂ x
+          coh (inl x) = refl
+          coh (inr x) = refl
+          coh (push x i₁) = refl
+
+        module L→R =
+          PushoutPasteDown pushoutSquare₂ {B = C₄₊ₙ⋁SphereBouquetAsPushout}
+               (Iso.inv Iso-C4+n-cofibα↑ ∘ inr) inl inr (funExt push)
+
+        -- First equivalence
+        C₄₊ₙ⋁SphereBouquetAsPushout≃cofib-const :
+          C₄₊ₙ⋁SphereBouquetAsPushout ≃ cofib const→C4+n
+        C₄₊ₙ⋁SphereBouquetAsPushout≃cofib-const =
+          compEquiv
+           (invEquiv (_ , isPushoutTot))
+           (symPushout _ _)
+           where
+          isPushoutTot =
+            L→R.isPushoutBottomSquare→isPushoutTotSquare
+              (subst isEquiv (funExt (λ { (inl x) → refl
+                                        ; (inr x) → refl
+                                        ; (push a i) → refl}))
+              (idIsEquiv _))
+
+        -- The map we have called constant is actually (merely constant):
+        sphereBouquetVanish : ∀ {k : ℕ}
+          (f : SphereBouquet (suc n) (Fin k) → C4+n)
+          → ∥ f ≡ (λ _ → C⋆) ∥₁
+        sphereBouquetVanish {k = k} f =
+          TR.rec (isProp→isOfHLevelSuc (suc n) squash₁)
+            (λ p → PT.rec squash₁
+            (λ q → ∣ funExt
+              (λ { (inl x) → p
+                 ; (inr (x , y)) → (q x y ∙ sym (q x (ptSn (suc n))))
+                                  ∙ cong f (sym (push x)) ∙ p
+                 ; (push a i) j → (cong (_∙ cong f (sym (push a)) ∙ p)
+                                         (rCancel (q a (ptSn (suc n))))
+                                  ∙ sym (lUnit _)
+                                  ◁ (symP (compPath-filler'
+                                      (cong f (sym (push a))) p))) (~ i) j}) ∣₁)
+            lem)
+            pted
+          where
+          sphereVanish : (f : S₊ (suc n) → C4+n)
+                      → ∥ ((x : S₊ (suc n)) → f x ≡ C⋆) ∥₁
+          sphereVanish f =
+            sphereToTrunc (suc n)
+              λ x → isConnectedPath 2+n isConnectedC4+n _ _ .fst
+
+          pted = Iso.fun (PathIdTruncIso 2+n)
+                           (isContr→isProp isConnectedC4+n  ∣ f (inl tt) ∣ₕ ∣ C⋆ ∣ₕ)
+
+          lem : ∥ ((x : Fin k) → (y :  _) → f (inr (x , y)) ≡ C⋆) ∥₁
+          lem = invEq propTrunc≃Trunc1
+            (invEq (_ , InductiveFinSatAC _ _ _)
+              λ x → PT.rec (isOfHLevelTrunc 1)
+                ∣_∣ₕ
+                (sphereVanish λ y → f (inr (x , y))))
+
+        -- For now, we asssume it's constant
+        module _ (vanish : const→C4+n ≡ λ _ → C⋆) where
+
+          -- Abbreviation: (⋁S⁴⁺ⁿ) ∨ C₄₊ₙ
+          SphereBouquet⋁C₄₊ₙ =
+            SphereBouquet∙ 2+n (A (suc n)) ⋁ (C4+n , C⋆)
+
+          -- Connectedness of this space
+          isConnectedSphereBouquet⋁C₄₊ₙ :
+            isConnected 3+n SphereBouquet⋁C₄₊ₙ
+          fst isConnectedSphereBouquet⋁C₄₊ₙ = ∣ inl (inl tt) ∣ₕ
+          snd isConnectedSphereBouquet⋁C₄₊ₙ =
+            TR.elim (λ _ → isOfHLevelPath 3+n
+                            (isOfHLevelTrunc 3+n) _ _)
+              λ { (inl x) → inlEq x
+                ; (inr x) → SP ∙ inrEq x
+                ; (push tt i) j →
+                  (compPath-filler (inlEq (inl tt)) (cong ∣_∣ₕ (push tt))
+                ▷ (rUnit SP ∙ cong (SP ∙_) (sym inrEq∙))) i j}
+            where
+            inlEq : (x : _)
+              → Path (hLevelTrunc 3+n SphereBouquet⋁C₄₊ₙ)
+                ∣ inl (inl tt) ∣ ∣ inl x ∣
+            inlEq x = TR.rec (isOfHLevelTrunc 3+n _ _)
+              (λ p i → ∣ inl (p i) ∣ₕ)
+              (Iso.fun (PathIdTruncIso _)
+                (isContr→isProp
+                  (isConnectedSphereBouquet' {n = suc n})
+                    ∣ inl tt ∣ ∣ x ∣))
+
+            G :  (x : C4+n) → ∥ C⋆ ≡ x ∥ 2+n
+            G x = Iso.fun (PathIdTruncIso _)
+                    (isContr→isProp isConnectedC4+n ∣ C⋆ ∣ₕ ∣ x ∣ₕ)
+
+            G∙ : G C⋆ ≡ ∣ refl ∣ₕ
+            G∙ = cong (Iso.fun (PathIdTruncIso _))
+                  (isProp→isSet (isContr→isProp isConnectedC4+n) _ _
+                    (isContr→isProp isConnectedC4+n ∣ C⋆ ∣ₕ ∣ C⋆ ∣ₕ) refl)
+               ∙ cong ∣_∣ₕ (transportRefl refl)
+
+            inrEq : (x : C4+n)
+              → Path (hLevelTrunc 3+n SphereBouquet⋁C₄₊ₙ)
+                      ∣ inr C⋆ ∣ₕ ∣ inr x ∣ₕ
+            inrEq x = TR.rec (isOfHLevelTrunc 3+n _ _)
+                             (λ p i → ∣ inr (p i) ∣ₕ) (G x)
+
+            inrEq∙ : inrEq C⋆ ≡ refl
+            inrEq∙ = cong (TR.rec (isOfHLevelTrunc 3+n _ _)
+                             (λ p i → ∣ inr (p i) ∣ₕ)) G∙
+
+            SP = inlEq (inl tt) ∙ cong ∣_∣ₕ (push tt)
+
+
+          -- Equivalence of our C₄₊ₙ⋁SphereBouquet and SphereBouquet⋁C₄₊ₙ
+          C₄₊ₙ⋁SphereBouquetAsPushout≃SphereBouquet⋁C₄₊ₙ :
+              C₄₊ₙ⋁SphereBouquetAsPushout ≃ SphereBouquet⋁C₄₊ₙ
+          C₄₊ₙ⋁SphereBouquetAsPushout≃SphereBouquet⋁C₄₊ₙ =
+            compEquiv C₄₊ₙ⋁SphereBouquetAsPushout≃cofib-const
+              (isoToEquiv
+                (compIso (cofibConst-⋁-Iso' {A = _ , inl tt} {B = _ , C⋆}
+                           (const→C4+n , funExt⁻ vanish _)
+                           (funExt⁻ vanish))
+                (pushoutIso _ _ _ _
+                  (idEquiv _)
+                  (isoToEquiv sphereBouquetSuspIso)
+                  (idEquiv _)
+                  refl
+                  refl)))
+
+          module T→B = PushoutPasteDown pushoutSquare₁
+            {B = C₄₊ₙ⋁SphereBouquetAsPushout}
+            (λ x → Iso.fun Iso-cofibαinr-SphereBouquet (inl x)) inr
+            (λ x → inl (Iso.inv Iso-C4+n-cofibα↑ x))
+            (sym (funExt push))
+
+          -- Finally, the first main lemma: the cofibre of β is S¹⁺ⁿ ∨ C₄₊ₙ
+          cofibβ≃SphereBouquet⋁C₄₊ₙ : cofib β ≃ SphereBouquet⋁C₄₊ₙ
+          cofibβ≃SphereBouquet⋁C₄₊ₙ =
+            compEquiv (compEquiv (symPushout _ _)
+              (_ , T→B.isPushoutBottomSquare→isPushoutTotSquare
+                (subst isEquiv (funExt helpIsoCoh) (isoToIsEquiv helpIso))))
+              C₄₊ₙ⋁SphereBouquetAsPushout≃SphereBouquet⋁C₄₊ₙ
+            where
+            helpIso : Iso (spanPushout (sp T→B.bottomSquare))
+                                       (P T→B.bottomSquare)
+            helpIso = compIso (equivToIso (symPushout _ _))
+                              (pushoutIso _ _ _ _ (idEquiv _)
+                                (invEquiv (isoToEquiv Iso-C4+n-cofibα↑))
+                                (idEquiv _) refl refl)
+
+            helpIsoCoh : (x : _) → Iso.fun helpIso x
+                                  ≡ Pushout→commSquare T→B.bottomSquare x
+            helpIsoCoh (inl x) = refl
+            helpIsoCoh (inr x) = refl
+            helpIsoCoh (push a i) j = sym (rUnit (sym (push a))) j i
+
+          -- If we could adjust β somewhat, killing off S¹⁺ⁿ in S¹⁺ⁿ ∨
+          -- C₄₊ₙ, we would be done.
+
+
+          -- We prove the mere existence of such an `improved β':
+          ∃Improvedβ : ∃[ F ∈ (SphereBouquet∙ 2+n (A (suc n))
+                          →∙ SphereBouquet∙ 2+n (A 2+n)) ]
+                   ((x : _) → Path SphereBouquet⋁C₄₊ₙ
+                                (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst
+                                  (inr (fst F x))) (inl x))
+          ∃Improvedβ = TR.rec (isProp→isOfHLevelSuc (suc n) squash₁)
+            (λ coh₁ → PT.rec squash₁ (λ F → TR.rec squash₁
+            (λ h → TR.rec squash₁ (λ q → ∣ (Improvedβ F coh₁ h , refl) ,
+                                            (coh F coh₁ h q) ∣₁)
+            (makeCoh F coh₁ h))
+            (F∙ F coh₁))
+            ∃Improvedβ-inr)
+              (isConnectedPath _ isConnectedSphereBouquet⋁C₄₊ₙ
+                (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst
+                  (inr (inl tt))) (inl (inl tt)) .fst)
+            where
+            ∃Improvedβ-inr : ∥ ((x : A (suc n)) (y : S₊ 2+n)
+              → Σ[ t ∈ SphereBouquet 2+n (A 2+n) ]
+                    (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst (inr t)
+                   ≡ inl (inr (x , y)))) ∥₁
+            ∃Improvedβ-inr =
+              invEq propTrunc≃Trunc1
+                (invEq (_ , InductiveFinSatAC _ _ _)
+                  λ x → fst propTrunc≃Trunc1
+                    (sphereToTrunc 2+n
+                      λ y → isConnectedInr-cofib∘inr (inl (inr (x , y))) .fst))
+              where
+              isConnectedInr-cofibβ :
+                isConnectedFun 3+n {B = cofib β} inr
+              isConnectedInr-cofibβ = inrConnected 3+n _ _
+                λ b → isOfHLevelRetractFromIso 0 (mapCompIso fiberUnitIso)
+                        isConnectedSphereBouquet'
+
+              isConnectedInr-cofib∘inr : isConnectedFun 3+n
+                {B = SphereBouquet⋁C₄₊ₙ}
+                (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst ∘ inr)
+              isConnectedInr-cofib∘inr =
+                isConnectedComp
+                  (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst) inr 3+n
+                  (isEquiv→isConnected _
+                    (cofibβ≃SphereBouquet⋁C₄₊ₙ .snd) 3+n)
+                    isConnectedInr-cofibβ
+
+            -- We asumme the full existence of such an improved β (F below)
+            module _
+              (F : ((x : A (suc n)) (y : S₊ 2+n)
+               → Σ[ t ∈ SphereBouquet 2+n (A 2+n) ]
+                     (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst (inr t)
+                   ≡ inl (inr (x , y)))))
+              (coh₁ : Path SphereBouquet⋁C₄₊ₙ
+                           (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst (inr (inl tt)))
+                           (inl (inl tt)))
+              where
+              -- mere pointedness
+              F∙ : hLevelTrunc 1 ((x : Fin _) → F x north .fst ≡ inl tt)
+              F∙ =
+                invEq (_ , InductiveFinSatAC _ _ _)
+                  λ a → isConnectedPath 1 (isConnectedSubtr 2 (suc n)
+                    (subst (λ x → isConnected x (SphereBouquet 2+n
+                                    (A 2+n)))
+                                    (cong suc (+-comm 2 n))
+                                    isConnectedSphereBouquet')) _ _ .fst
+
+              -- ... which we assume, as usual.
+              module _ (h  : (x : Fin _) → F x north .fst ≡ inl tt) where
+                Improvedβ : (SphereBouquet 2+n (A (suc n))
+                   → SphereBouquet 2+n (A 2+n))
+                Improvedβ (inl x) = inl tt
+                Improvedβ (inr (x , y)) = F x y .fst
+                Improvedβ (push a i) = h  a (~ i)
+
+                -- We also want the following coherencet to be satisfied
+                cohTy : Type _
+                cohTy = (a : A (suc n))
+                  → Square (λ i → cofibβ≃SphereBouquet⋁C₄₊ₙ .fst
+                                    (inr (h a (~ i))))
+                            (λ i → inl (push a i))
+                            coh₁ (F a north .snd)
+
+                -- It merely is...
+                makeCoh : hLevelTrunc 1 cohTy
+                makeCoh = invEq (_ , InductiveFinSatAC _ _ _)
+                  λ a → isConnectedPathP 1
+                    (isConnectedSubtr' n 2
+                      (isConnectedPath _
+                        isConnectedSphereBouquet⋁C₄₊ₙ _ _)) _ _ .fst
+
+                -- so we assume it, giving us the main coherence we need
+                module _ (coh₂ : cohTy) where
+                  coh : (x : _) → Path SphereBouquet⋁C₄₊ₙ
+                                    (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst
+                                      (inr (Improvedβ x)))
+                                    (inl x)
+                  coh (inl x) = coh₁
+                  coh (inr (x , y)) = F x y .snd
+                  coh (push a i) j = coh₂ a j i
+
+          -- Now, assuming the exisetence of Imrpovedβ and the coherence above,
+          -- we can finally endow C₄₊ₙ with the appropriate cell structure
+          module _ (F : (SphereBouquet∙ 2+n (A (suc n))
+                     →∙ SphereBouquet∙ 2+n (A 2+n)))
+                   (h : (x : _) → Path SphereBouquet⋁C₄₊ₙ
+                                    (cofibβ≃SphereBouquet⋁C₄₊ₙ .fst
+                                      (inr (fst F x)))
+                                    (inl x))
+            where
+            -- The cardinality of the ₄₊ₙ-cells
+            N = card (suc n) +ℕ card 3+n
+
+            -- Techincal ⋁-distributivity lemma
+            Iso-SphereBouquetN : Iso (SphereBouquet 2+n (Fin N))
+                       (SphereBouquet∙ 2+n (A (suc n))
+                     ⋁ SphereBouquet∙ 2+n (A 3+n))
+            Iso-SphereBouquetN = compIso
+              (pathToIso
+                ((λ i → ⋁gen (isoToPath
+                  (Iso-Fin⊎Fin-Fin+
+                    {n = card (suc n)}
+                    {m = card 3+n}) (~ i))
+                    (λ _ → S₊∙ 2+n))
+                  ∙ cong (⋁gen (A (suc n) ⊎ A 3+n))
+                         (funExt (⊎.elim (λ _ → refl) (λ _ → refl)))))
+                (invIso ⋁gen⊎Iso)
+
+            -- Finally, we have shown that C₄₊ₙ is the cofibre of F ∨→
+            -- β → C4+n
+            Iso-cofib-C₄₊ₙ : Iso (cofib (F ∨→ β∙)) C4+n
+            Iso-cofib-C₄₊ₙ = compIso (cofib∨→compIsoᵣ  F β∙)
+                 (compIso
+                   (pathToIso (cong cofib (funExt lem)))
+                   (compIso
+                     (equivToIso (symPushout _ _))
+                     (compIso
+                       (PushoutCompEquivIso
+                         (idEquiv (SphereBouquet 2+n (A (suc n))))
+                         (invEquiv cofibβ≃SphereBouquet⋁C₄₊ₙ) inl (λ _ → tt))
+                       (compIso (equivToIso (symPushout _ _)) cofibInl-⋁))))
+              where
+              lem : (x : _) → inr (fst F x) ≡ invEq cofibβ≃SphereBouquet⋁C₄₊ₙ (inl x)
+              lem x = sym (retEq cofibβ≃SphereBouquet⋁C₄₊ₙ (inr (fst F x)))
+                   ∙ cong (invEq cofibβ≃SphereBouquet⋁C₄₊ₙ) (h x)
+
+            -- Let us summarise the main data: we have shown that
+            -- there is some k and a map α : ⋁ₖ Sⁿ⁺² → ⋁ Sⁿ⁺² s.t. α
+            -- defines an attaching map for C₄₊ₙ.
+            mainData : Σ[ k ∈ ℕ ] Σ[ α ∈ (SphereBouquet 2+n (Fin k)
+                                  → SphereBouquet 2+n (A 2+n)) ]
+                 (Iso (Pushout (α ∘ inr) fst) C4+n)
+            fst mainData = N
+            fst (snd mainData) = F ∨→ β∙ ∘ Iso.fun Iso-SphereBouquetN
+            snd (snd mainData) =
+              compIso
+                (compIso (⋁-cofib-Iso (_ , fst F (inl tt))
+                          ((F ∨→ β∙ ∘ Iso.fun Iso-SphereBouquetN) , refl))
+                         (invIso (PushoutCompEquivIso
+                           (invEquiv (isoToEquiv Iso-SphereBouquetN))
+                             (idEquiv Unit) _ _))) Iso-cofib-C₄₊ₙ
+
+            -- Using this, we can finally define a CW structure on C with the
+            -- desired properties
+
+            -- We parametrise with Trichotomyᵗ as it makes removes some bureaucracy later
+
+            -- The type family
+            C' : (m : ℕ)
+              → Trichotomyᵗ m 3+n → Type ℓ
+            C' zero (lt x) = ⊥*
+            C' (suc m) (lt x) = Unit*
+            C' m (eq x) =
+              Lift (SphereBouquet 2+n (A 2+n))
+            C' m (gt x) = C* m
+
+            -- Basepoints (not needed, but useful)
+            C'∙ : (m : ℕ) (q : _) → C' (suc m) q
+            C'∙ m (lt x) = tt*
+            C'∙ m (eq x) = lift (inl tt)
+            C'∙ m (gt x) = subst C* (+-comm m 1)
+              (CW↪Iterate (_ , ind .fst .snd .fst) 1 m
+                (invEq (CW₁-discrete (_ , ind .fst .snd .fst))
+                  (subst Fin (sym (ind .fst .snd .snd .fst)) flast)))
+
+            -- Cardinality of cells
+            card' : (m : ℕ) → Trichotomyᵗ m 2+n
+              → Trichotomyᵗ m 3+n → ℕ
+            card' zero (lt x) q = 1
+            card' (suc m) (lt x) q = 0
+            card' m (eq x) q = card 2+n
+            card' m (gt x) (lt x₁) = 0
+            card' m (gt x) (eq x₁) = N
+            card' m (gt x) (gt x₁) = card m
+
+            -- Connectedness
+            C'-connected : (n₁ : ℕ) → n₁ <ᵗ suc n
+              → (p : _) (q : _) → card' (suc n₁) p q ≡ 0
+            C'-connected m ineq (lt x) q = refl
+            C'-connected m ineq (eq x) q = ⊥.rec (¬m<ᵗm (subst (_<ᵗ 2+n) x ineq))
+            C'-connected m ineq (gt x) q = ⊥.rec (¬m<ᵗm (<ᵗ-trans ineq x))
+
+            -- Attaching maps
+            α' : (m : ℕ) (p : _) (q : _) → Fin (card' m p q) × S⁻ m → C' m q
+            α' (suc m) (lt x) q ()
+            α' (suc m) (eq x) (lt x₁) _ = tt*
+            α' (suc m) (eq x) (eq x₁) _ = C'∙ m (eq x₁)
+            α' (suc m) (eq x) (gt x₁) _ = C'∙ m (gt x₁)
+            α' (suc m) (gt x) (lt x₁) _ = C'∙ m (lt x₁)
+            α' (suc m) (gt x) (eq x₁) (a , p) =
+              lift (snd mainData .fst (inr (a , subst S₊ (cong predℕ x₁) p)))
+            α' (suc m) (gt x) (gt x₁) = α (suc m)
+
+            -- Equivalences
+            e' : (n₁ : ℕ) (p : _) (q : _)
+              → C' (suc n₁) (Trichotomyᵗ-suc p)
+                ≃ Pushout (α' n₁ p q) fst
+            e' zero (lt s) (lt t) =
+              isoToEquiv (isContr→Iso (tt* , (λ {tt* → refl}))
+                         ((inr flast) , λ {(inr (zero , tt)) → refl}))
+            e' zero (lt x) (eq p) = ⊥.rec (snotz (sym p))
+            e' zero (eq x) q = ⊥.rec (snotz (sym x))
+            e' (suc m) (lt x) q =
+              isoToEquiv (isContr→Iso (tt* , (λ {tt* → refl}))
+                         ((inl (C'Contr m x q .fst))
+                        , (λ { (inl t) → λ i
+                          → inl (C'Contr m x q .snd t i)})))
+              where
+              C'Contr : (m : _) (t : m <ᵗ suc n) (q : _)
+                → isContr (C' (suc m) q)
+              C'Contr m t (lt x) = tt* , λ {tt* → refl}
+              C'Contr m t (eq x) =
+                ⊥.rec (¬m<ᵗm (<ᵗ-trans (subst (_<ᵗ suc n)
+                                        (cong predℕ x) t) <ᵗsucm))
+              C'Contr m t (gt x) =
+                ⊥.rec (¬m<ᵗm (<ᵗ-trans (<ᵗ-trans x t) <ᵗsucm))
+            e' (suc m) (eq x) (lt x₁) =
+              invEquiv (isoToEquiv
+                (compIso (⋁-cofib-Iso
+                          {B = λ _ → _ , ptSn m} (_ , tt*) (_ , refl))
+                  (compIso (cofibConst-⋁-Iso {A = SphereBouquet∙ m _})
+                    (compIso ⋁-rUnitIso
+                      (compIso sphereBouquetSuspIso
+                        (compIso
+                          (pathToIso
+                            (λ i → SphereBouquet (x i) (A 2+n)))
+                          LiftIso))))))
+            e' (suc m) (eq x) (eq x₁) =
+              ⊥.rec (¬m<ᵗm (subst (_<ᵗ suc n)
+                      (cong (predℕ ∘ predℕ) (sym x ∙ x₁)) <ᵗsucm))
+            e' (suc m) (eq x) (gt y) =
+              ⊥.rec (¬m<ᵗm (<ᵗ-trans (subst (2+n <ᵗ_)
+                                   (cong predℕ x) y) <ᵗsucm))
+            e' (suc m) (gt x) (lt x₁) = ⊥.rec (¬squeeze (x , x₁))
+            e' (suc m) (gt x) (eq x₁) =
+              isoToEquiv (compIso (compIso
+                (pathToIso (λ i → C* (suc (x₁ i))))
+                (invIso (mainData .snd .snd)))
+                (invIso (pushoutIso _ _ _ _
+                  (Σ-cong-equiv-snd
+                    (λ _ → pathToEquiv (cong S₊ (cong predℕ x₁))))
+                    (invEquiv LiftEquiv) (idEquiv _) refl refl)))
+            e' (suc m) (gt x) (gt x₁) = e (suc m)
+
+            -- packaging it up into a connectedCWskel
+            C'-connectedCWskel : connectedCWskel ℓ (suc n)
+            fst C'-connectedCWskel m = C' m (m ≟ᵗ 3+n)
+            fst (fst (snd C'-connectedCWskel)) m =
+              card' m (m ≟ᵗ 2+n) (m ≟ᵗ 3+n)
+            fst (snd (fst (snd C'-connectedCWskel))) m = α' m _ _
+            fst (snd (snd (fst (snd C'-connectedCWskel)))) ()
+            snd (snd (snd (fst (snd C'-connectedCWskel)))) m = e' m _ _
+            fst (snd (snd C'-connectedCWskel)) = refl
+            snd (snd (snd C'-connectedCWskel)) m ineq = C'-connected m ineq _ _
+
+            C'-realise : (n₁ : ℕ) (q : _)
+              → Iso (C' (n₁ +ℕ 4+n) q)
+                     (C* (n₁ +ℕ 4+n))
+            C'-realise m (lt x) = ⊥.rec (¬m<m (<-trans (<ᵗ→< x) (m , refl)))
+            C'-realise m (eq x) = ⊥.rec (¬m<m (m , x))
+            C'-realise zero (gt x) = idIso
+            C'-realise (suc m) (gt x) = idIso
+
+            C'-realise-coh : (n₁ : ℕ) (q : _) (r : _)
+                (a : C' (n₁ +ℕ 4+n) q)
+                → CW↪ (fst (fst ind) , snd (fst ind) .fst) (n₁ +ℕ 4+n)
+                      (Iso.fun (C'-realise n₁ q) a)
+                ≡ Iso.fun (C'-realise (suc n₁) _)
+                    (invEq (e' (n₁ +ℕ 4+n) r q) (inl a))
+            C'-realise-coh m (lt x) r a = ⊥.rec (¬m<m (<-trans (<ᵗ→< x) (m , refl)))
+            C'-realise-coh m (eq x) r a = ⊥.rec (¬m<m (m , x))
+            C'-realise-coh m (gt x) (lt x₁) a =
+              ⊥.rec (¬m<ᵗm (<ᵗ-trans (<ᵗ-trans x x₁) <ᵗsucm))
+            C'-realise-coh m (gt x) (eq x₁) a =
+              ⊥.rec (¬m<ᵗm (<ᵗ-trans ((subst (_<ᵗ (m +ℕ 4+n)) (cong suc (sym x₁)) x)) <ᵗsucm))
+            C'-realise-coh zero (gt x) (gt x₁) a = refl
+            C'-realise-coh (suc m) (gt x) (gt x₁) a = refl
+
+            -- finally, we're done
+            isConnectedCW-C' : isConnectedCW (suc n) C
+            fst isConnectedCW-C' = C'-connectedCWskel
+            snd isConnectedCW-C' =
+              compEquiv (isoToEquiv
+                (compIso (SeqColimIso _ (4 +ℕ n))
+                  (compIso (sequenceIso→ColimIso
+                    ((λ m → C'-realise m ((m +ℕ 4+n) ≟ᵗ 3+n))
+                    , (λ n → C'-realise-coh n _ _)))
+                    (invIso (SeqColimIso _ (4 +ℕ n)))))) (ind .snd)
diff --git a/Cubical/CW/Properties.agda b/Cubical/CW/Properties.agda
index 4e481c84a8..f1a16cba59 100644
--- a/Cubical/CW/Properties.agda
+++ b/Cubical/CW/Properties.agda
@@ -20,6 +20,7 @@ open import Cubical.Foundations.Equiv.Properties
 
 open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
 open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Order.Inductive
 open import Cubical.Data.Unit
 open import Cubical.Data.Fin.Inductive.Base
 open import Cubical.Data.Fin.Inductive.Properties
@@ -249,3 +250,37 @@ isConnected-CW↪∞ (suc n) C = isConnectedIncl∞ (realiseSeq C) (suc n) (suc
     subtr : (k : ℕ) → isConnectedFun (suc n) (CW↪ C (k +ℕ (suc n)))
     subtr k = isConnectedFunSubtr (suc n) k (CW↪ C (k +ℕ (suc n)))
                                    (isConnected-CW↪ (k +ℕ (suc n)) C)
+
+-- The m-skeleton of an n-connected complex (m≤n) is n-connected
+isConnectedCW→isConnectedSkel : (C : CWskel ℓ)
+  → (m : ℕ) (n : Fin (suc m))
+  → isConnected (fst n) (realise C)
+  → isConnected (fst n) (C .fst m)
+isConnectedCW→isConnectedSkel C m (n , p) =
+  isOfHLevelRetractFromIso 0
+    (compIso (truncOfTruncIso n t₀)
+      (compIso
+        (mapCompIso
+          (subst (λ k → Iso (hLevelTrunc k (C .fst m))
+                             (hLevelTrunc k (realise C)))
+                  (sym teq)
+                  (connectedTruncIso m _
+                    (isConnected-CW↪∞ m C))))
+        (invIso (truncOfTruncIso n t₀))))
+  where
+  t = <ᵗ→< p
+  t₀ = fst t
+  teq : t₀ +ℕ n ≡ m
+  teq = cong predℕ (sym (+-suc t₀ n) ∙ snd t)
+
+truncCWIso : (A : CWskel ℓ) (n : ℕ)
+  → Iso (hLevelTrunc n (realise A)) (hLevelTrunc n (fst A n))
+truncCWIso A n = invIso (connectedTruncIso n incl (isConnected-CW↪∞ n A))
+
+isConnectedColim→isConnectedSkel :
+  (A : CWskel ℓ) (n : ℕ)
+  → isConnected n (realise A)
+  → isConnected n (fst A n)
+isConnectedColim→isConnectedSkel A n c =
+  isOfHLevelRetractFromIso 0
+    (invIso (truncCWIso A n)) c
diff --git a/Cubical/CW/Subcomplex.agda b/Cubical/CW/Subcomplex.agda
index 8cba619b94..37fbed2618 100644
--- a/Cubical/CW/Subcomplex.agda
+++ b/Cubical/CW/Subcomplex.agda
@@ -1,5 +1,19 @@
 {-# OPTIONS --safe --lossy-unification #-}
 
+{-
+This file contains a definition of a notion of (strict)
+subcomplexes of a CW complex. Here, a subomplex of a complex
+C = colim ( C₀ → C₁ → ...)
+is simply the complex
+C⁽ⁿ⁾ := colim (C₀ → ... → Cₙ = Cₙ = ...)
+
+This file contains.
+1. Definition of above
+2. A `strictification' of finite CW complexes in terms of above
+3. An elmination principle for finite CW complexes
+4. A proof that C and C⁽ⁿ⁾ has the same homolog in appropriate dimensions.
+-}
+
 module Cubical.CW.Subcomplex where
 
 open import Cubical.Foundations.Prelude
@@ -8,13 +22,14 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Nat
-open import Cubical.Data.Nat.Order.Inductive
 open import Cubical.Data.Fin.Inductive.Base
 open import Cubical.Data.Fin.Inductive.Properties
 open import Cubical.Data.Sigma
 open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Nat.Order.Inductive
 
 open import Cubical.CW.Base
 open import Cubical.CW.Properties
@@ -36,20 +51,24 @@ private
   variable
     ℓ ℓ' ℓ'' : Level
 
--- finite subcomplex of a cw complex
+-- finite subcomplex C⁽ⁿ⁾ of a cw complex C.
 module _ (C : CWskel ℓ) where
+  -- The underlying family of types is that of C but ending at some
+  -- fixed n.
   subComplexFam : (n : ℕ) (m : ℕ) → Type ℓ
   subComplexFam n m with (m ≟ᵗ n)
   ... | lt x = fst C m
   ... | eq x = fst C m
   ... | gt x = fst C n
 
+  -- Similarly for the number of cells
   subComplexCard : (n : ℕ) → ℕ → ℕ
   subComplexCard n m with (m ≟ᵗ n)
   ... | lt x = snd C .fst m
   ... | eq x = 0
   ... | gt x = 0
 
+  -- Attaching maps
   subComplexα : (n m : ℕ) → Fin (subComplexCard n m) × S⁻ m → subComplexFam n m
   subComplexα n m with (m ≟ᵗ n)
   ... | lt x = snd C .snd .fst m
@@ -61,6 +80,7 @@ module _ (C : CWskel ℓ) where
   ... | lt x = CW₀-empty C
   ... | eq x = CW₀-empty C
 
+  -- Resulting complex has CW structure
   subComplexFam≃Pushout : (n m : ℕ)
     → subComplexFam n (suc m) ≃ Pushout (subComplexα n m) fst
   subComplexFam≃Pushout n m with (m ≟ᵗ n) | ((suc m) ≟ᵗ n)
@@ -78,17 +98,19 @@ module _ (C : CWskel ℓ) where
     ⊥.rec (¬m<ᵗm (subst (n <ᵗ_) x₁ (<ᵗ-trans x <ᵗsucm)))
   ... | gt x | gt x₁ = isoToEquiv (PushoutEmptyFam (λ x → ¬Fin0 (fst x)) ¬Fin0)
 
+  -- packaging it all together
   subComplexYieldsCWskel : (n : ℕ) → yieldsCWskel (subComplexFam n)
   fst (subComplexYieldsCWskel n) = subComplexCard n
   fst (snd (subComplexYieldsCWskel n)) = subComplexα n
   fst (snd (snd (subComplexYieldsCWskel n))) = subComplex₀-empty n
   snd (snd (snd (subComplexYieldsCWskel n))) m = subComplexFam≃Pushout n m
 
+  -- main definition
   subComplex : (n : ℕ) → CWskel ℓ
   fst (subComplex n) = subComplexFam n
   snd (subComplex n) = subComplexYieldsCWskel n
 
-  -- as a finite CWskel
+  -- Let us also show that this defines a _finite_ CW complex
   subComplexFin : (m : ℕ) (n : Fin (suc m))
     → isEquiv (CW↪ (subComplexFam (fst n) , subComplexYieldsCWskel (fst n)) m)
   subComplexFin m (n , r) with (m ≟ᵗ n) | (suc m ≟ᵗ n)
@@ -128,12 +150,54 @@ module _ (C : CWskel ℓ) where
   ... | eq x = idEquiv _
   ... | gt x = ⊥.rec (¬squeeze (x , p))
 
-realiseSubComplex : (n : ℕ) (C : CWskel ℓ) → Iso (fst C n) (realise (subComplex C n))
+-- C⁽ⁿ⁾ₙ ≃ Cₙ
+realiseSubComplex : (n : ℕ) (C : CWskel ℓ)
+  → Iso (fst C n) (realise (subComplex C n))
 realiseSubComplex n C =
   compIso (equivToIso (complex≃subcomplex C n flast))
           (realiseFin n (finSubComplex C n))
 
--- Goal: Show that a cell complex C and its subcomplex Cₙ share
+-- Strictifying finCWskel
+niceFinCWskel : ∀ {ℓ} (n : ℕ) → finCWskel ℓ n → finCWskel ℓ n
+fst (niceFinCWskel n (A , AC , fin)) = finSubComplex (A , AC) n .fst
+snd (niceFinCWskel n (A , AC , fin)) = finSubComplex (A , AC) n .snd
+
+makeNiceFinCWskel : ∀ {ℓ} {A : Type ℓ} → isFinCW A → isFinCW A
+makeNiceFinCWskel {A = A} (dim , cwsk , e) = better
+  where
+  improved = finSubComplex (cwsk .fst , cwsk .snd .fst) dim
+
+  better : isFinCW A
+  fst better = dim
+  fst (snd better) = improved
+  snd (snd better) =
+    compEquiv
+      (compEquiv e (invEquiv (isoToEquiv (realiseFin dim cwsk))))
+      (isoToEquiv (realiseSubComplex dim (cwsk .fst , cwsk .snd .fst)))
+
+
+makeNiceFinCW : ∀ {ℓ} → finCW ℓ → finCW ℓ
+fst (makeNiceFinCW C) = fst C
+snd (makeNiceFinCW C) =
+  PT.map makeNiceFinCWskel (snd C)
+
+makeNiceFinCW≡ : ∀ {ℓ} (C : finCW ℓ) → makeNiceFinCW C ≡ C
+makeNiceFinCW≡ C = Σ≡Prop (λ _ → squash₁) refl
+
+-- Elimination principles
+makeNiceFinCWElim : ∀ {ℓ ℓ'} {A : finCW ℓ → Type ℓ'}
+  → ((C : finCW ℓ) → A (makeNiceFinCW C))
+  → (C : _) → A C
+makeNiceFinCWElim {A = A} ind C = subst A (makeNiceFinCW≡ C) (ind C)
+
+makeNiceFinCWElim' : ∀ {ℓ ℓ'} {C : Type ℓ} {A : ∥ isFinCW C ∥₁ → Type ℓ'}
+  → ((x : _) → isProp (A x))
+  → ((cw : isFinCW C) → A (makeNiceFinCW (C , ∣ cw ∣₁) .snd))
+  → (cw : _) → A cw
+makeNiceFinCWElim' {A = A} pr ind =
+  PT.elim pr λ cw → subst A (squash₁ _ _) (ind cw)
+
+-- Goal: Show that a cell complex C and its subcomplex C⁽ⁿ⁾ share
 -- homology in low enough dimensions
 module _ (C : CWskel ℓ) where
   ChainSubComplex : (n : ℕ) → snd C .fst n ≡ snd (subComplex C (suc n)) .fst n
diff --git a/Cubical/Data/Fin/Inductive/Base.agda b/Cubical/Data/Fin/Inductive/Base.agda
index d2280736a1..e5d0dc6365 100644
--- a/Cubical/Data/Fin/Inductive/Base.agda
+++ b/Cubical/Data/Fin/Inductive/Base.agda
@@ -34,6 +34,9 @@ snd (flast {m = m}) = <ᵗsucm {m = m}
 fzero : {m : ℕ} → Fin (suc m)
 fzero = 0 , tt
 
+fone : ∀ {m} → Fin (suc (suc m))
+fone {m} = suc zero , tt
+
 -- Sums
 sumFinGen : ∀ {ℓ} {A : Type ℓ} {n : ℕ}
   (_+_ : A → A → A) (0A : A) (f : Fin n → A) → A
diff --git a/Cubical/Data/Fin/Inductive/Properties.agda b/Cubical/Data/Fin/Inductive/Properties.agda
index 38f654fc45..9b553fd878 100644
--- a/Cubical/Data/Fin/Inductive/Properties.agda
+++ b/Cubical/Data/Fin/Inductive/Properties.agda
@@ -11,8 +11,10 @@ open import Cubical.Data.Fin.Inductive.Base
 open import Cubical.Data.Nat
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Unit
+open import Cubical.Data.Bool
 open import Cubical.Data.Sigma
-open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sum as ⊎
+open import Cubical.Data.Nat.Order as OrderOld
 open import Cubical.Data.Nat.Order.Inductive
 open import Cubical.Data.Fin.Base as FinOld
   hiding (Fin ; injectSuc ; fsuc ; fzero ; flast ; ¬Fin0 ; sumFinGen)
@@ -128,9 +130,208 @@ Iso.fun (Iso-Fin-InductiveFin m) (x , p) = x , <→<ᵗ p
 Iso.inv (Iso-Fin-InductiveFin m) (x , p) = x , <ᵗ→< p
 Iso.rightInv (Iso-Fin-InductiveFin m) (x , p) =
   Σ≡Prop (λ w → isProp<ᵗ {n = w} {m}) refl
-Iso.leftInv (Iso-Fin-InductiveFin m) _ = Σ≡Prop (λ _ → isProp≤) refl
+Iso.leftInv (Iso-Fin-InductiveFin m) _ = Σ≡Prop (λ _ → OrderOld.isProp≤) refl
 
 isSetFin : {n : ℕ} → isSet (Fin n)
 isSetFin {n = n} =
   isOfHLevelRetractFromIso 2 (invIso (Iso-Fin-InductiveFin n))
     FinOldProps.isSetFin
+
+isPropFin1 : isProp (Fin 1)
+isPropFin1 (zero , tt) (zero , tt) = refl
+
+DiscreteFin : ∀ {n} → Discrete (Fin n)
+DiscreteFin x y with discreteℕ (fst x) (fst y)
+... | yes p = yes (Σ≡Prop (λ _ → isProp<ᵗ) p)
+... | no ¬p = no λ q → ¬p (cong fst q)
+
+inhabitedFibres?Fin : ∀ {ℓ} {A : Type ℓ}
+  (da : Discrete A) (n : ℕ) (f : Fin n → A)
+  → inhabitedFibres? f
+inhabitedFibres?Fin {A = A} da zero f y = inr λ x → ⊥.rec (¬Fin0 x)
+inhabitedFibres?Fin {A = A} da (suc n) f y with da (f fzero) y
+... | yes p = inl (fzero , p)
+... | no ¬p with (inhabitedFibres?Fin da n (f ∘ fsuc) y)
+... | inl q = inl ((fsuc (fst q)) , snd q)
+... | inr q = inr (elimFin-alt ¬p q)
+
+-- Decompositions in terms of ⊎ and ×
+Iso-Fin1⊎Fin-FinSuc : {n : ℕ} → Iso (Fin 1 ⊎ Fin n) (Fin (suc n))
+Iso.fun (Iso-Fin1⊎Fin-FinSuc {n = n}) = ⊎.rec (λ _ → flast) injectSuc
+Iso.inv (Iso-Fin1⊎Fin-FinSuc {n = n}) = elimFin (inl flast) inr
+Iso.rightInv (Iso-Fin1⊎Fin-FinSuc {n = n}) =
+  elimFin (cong (⊎.rec (λ _ → flast) injectSuc)
+                 (elimFinβ (inl flast) inr .fst))
+              λ x → cong (⊎.rec (λ _ → flast) injectSuc)
+                      (elimFinβ (inl flast) inr .snd x)
+Iso.leftInv (Iso-Fin1⊎Fin-FinSuc {n = n}) (inl (zero , p)) =
+  elimFinβ (inl flast) inr .fst
+Iso.leftInv (Iso-Fin1⊎Fin-FinSuc {n = n}) (inr x) = elimFinβ (inl flast) inr .snd x
+
+Iso-Fin⊎Fin-Fin+ : {n m : ℕ} → Iso (Fin n ⊎ Fin m) (Fin (n + m))
+Iso.fun (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) (inr x) = x
+Iso.inv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) x = inr x
+Iso.rightInv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) x = refl
+Iso.leftInv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) (inr x) = refl
+Iso-Fin⊎Fin-Fin+ {n = suc n} {m = m} =
+  compIso (⊎Iso (invIso Iso-Fin1⊎Fin-FinSuc) idIso)
+    (compIso ⊎-assoc-Iso
+      (compIso (⊎Iso idIso (Iso-Fin⊎Fin-Fin+ {n = n} {m = m}))
+        Iso-Fin1⊎Fin-FinSuc))
+
+Iso-Unit-Fin1 : Iso Unit (Fin 1)
+Iso.fun Iso-Unit-Fin1 tt = fzero
+Iso.inv Iso-Unit-Fin1 (x , p) = tt
+Iso.rightInv Iso-Unit-Fin1 (zero , p) = Σ≡Prop (λ _ → isProp<ᵗ) refl
+Iso.leftInv Iso-Unit-Fin1 x = refl
+
+Iso-Bool-Fin2 : Iso Bool (Fin 2)
+Iso.fun Iso-Bool-Fin2 false = flast
+Iso.fun Iso-Bool-Fin2 true = fzero
+Iso.inv Iso-Bool-Fin2 (zero , p) = true
+Iso.inv Iso-Bool-Fin2 (suc x , p) = false
+Iso.rightInv Iso-Bool-Fin2 (zero , p) = refl
+Iso.rightInv Iso-Bool-Fin2 (suc zero , p) =
+  Σ≡Prop (λ _ → isProp<ᵗ) refl
+Iso.leftInv Iso-Bool-Fin2 false = refl
+Iso.leftInv Iso-Bool-Fin2 true = refl
+
+Iso-Fin×Fin-Fin· : {n m : ℕ} → Iso (Fin n × Fin m) (Fin (n · m))
+Iso-Fin×Fin-Fin· {n = zero} {m = m} =
+  iso (λ {()}) (λ{()}) (λ{()}) (λ{()})
+Iso-Fin×Fin-Fin· {n = suc n} {m = m} =
+  compIso
+    (compIso
+      (compIso (Σ-cong-iso-fst (invIso Iso-Fin1⊎Fin-FinSuc))
+        (compIso Σ-swap-Iso
+          (compIso ×DistR⊎Iso
+            (⊎Iso (compIso
+              (Σ-cong-iso-snd (λ _ → invIso Iso-Unit-Fin1)) rUnit×Iso)
+              Σ-swap-Iso))))
+      (⊎Iso idIso Iso-Fin×Fin-Fin·))
+    (Iso-Fin⊎Fin-Fin+ {n = m} {n · m})
+
+Iso-Fin×Bool-Fin : {n : ℕ} → Iso (Fin n × Bool) (Fin (2 · n))
+Iso-Fin×Bool-Fin =
+  compIso (compIso Σ-swap-Iso
+    (Σ-cong-iso-fst Iso-Bool-Fin2)) (Iso-Fin×Fin-Fin· {n = 2})
+
+module _ {m : ℕ} where
+  Fin→Unit⊎Fin : (x : Fin (suc m)) → Unit ⊎ Fin m
+  Fin→Unit⊎Fin = elimFin (inl tt) inr
+
+  Unit⊎Fin→Fin : Unit ⊎ Fin m → Fin (suc m)
+  Unit⊎Fin→Fin (inl x) = flast
+  Unit⊎Fin→Fin (inr x) = injectSuc x
+
+  Iso-Fin-Unit⊎Fin : Iso (Fin (suc m)) (Unit ⊎ Fin m)
+  Iso.fun Iso-Fin-Unit⊎Fin = Fin→Unit⊎Fin
+  Iso.inv Iso-Fin-Unit⊎Fin = Unit⊎Fin→Fin
+  Iso.rightInv Iso-Fin-Unit⊎Fin (inl x) = elimFinβ (inl tt) inr .fst
+  Iso.rightInv Iso-Fin-Unit⊎Fin (inr x) = elimFinβ (inl tt) inr .snd x
+  Iso.leftInv Iso-Fin-Unit⊎Fin =
+    elimFin
+      (cong Unit⊎Fin→Fin (elimFinβ (inl tt) inr .fst))
+      λ x → (cong Unit⊎Fin→Fin (elimFinβ (inl tt) inr .snd x))
+
+-- Swapping two elements in Fin n
+module _ {n : ℕ} where
+  swapFin : (x y : Fin n) → Fin n → Fin n
+  swapFin (x , xp) (y , yp) (z , zp) with (discreteℕ z x) | (discreteℕ z y)
+  ... | yes p | yes p₁ = z , zp
+  ... | yes p | no ¬p = y , yp
+  ... | no ¬p | yes p = x , xp
+  ... | no ¬p | no ¬p₁ = (z , zp)
+
+  swapFinβₗ : (x y : Fin n) → swapFin x y x ≡ y
+  swapFinβₗ (x , xp) (y , yp) with (discreteℕ x x) | discreteℕ x y
+  ... | yes p | yes p₁ = Σ≡Prop (λ _ → isProp<ᵗ) p₁
+  ... | yes p | no ¬p = refl
+  ... | no ¬p | q = ⊥.rec (¬p refl)
+
+  swapFinβᵣ : (x y : Fin n) → swapFin x y y ≡ x
+  swapFinβᵣ (x , xp) (y , yp) with (discreteℕ y y) | discreteℕ y x
+  ... | yes p | yes p₁ = Σ≡Prop (λ _ → isProp<ᵗ) p₁
+  ... | yes p | no ¬p = refl
+  ... | no ¬p | q = ⊥.rec (¬p refl)
+
+  swapFin² : (x y z : Fin n) → swapFin x y (swapFin x y z) ≡ z
+  swapFin² (x , xp) (y , yp) (z , zp) with discreteℕ z x | discreteℕ z y
+  ... | yes p | yes p₁ = help
+    where
+    help : swapFin (x , xp) (y , yp) (z , zp) ≡ (z , zp)
+    help with discreteℕ z x | discreteℕ z y
+    ... | yes p | yes p₁ = refl
+    ... | yes p | no ¬p = ⊥.rec (¬p p₁)
+    ... | no ¬p | r = ⊥.rec (¬p p)
+  ... | yes p | no ¬q = help
+    where
+    help : swapFin (x , xp) (y , yp) (y , yp) ≡ (z , zp)
+    help with discreteℕ y x | discreteℕ y y
+    ... | yes p' | yes p₁ = Σ≡Prop (λ _ → isProp<ᵗ) (p' ∙ sym p)
+    ... | no ¬p | yes p₁ = Σ≡Prop (λ _ → isProp<ᵗ)  (sym p)
+    ... | p | no ¬p = ⊥.rec (¬p refl)
+  ... | no ¬p | yes p = help
+    where
+    help : swapFin (x , xp) (y , yp) (x , xp) ≡ (z , zp)
+    help with discreteℕ x y | discreteℕ x x
+    ... | yes p₁ | yes _ = Σ≡Prop (λ _ → isProp<ᵗ) (p₁ ∙ sym p)
+    ... | no ¬p | yes _ = Σ≡Prop (λ _ → isProp<ᵗ)  (sym p)
+    ... | s | no ¬p = ⊥.rec (¬p refl)
+  ... | no ¬p | no ¬q = help
+    where
+    help : swapFin (x , xp) (y , yp) (z , zp) ≡ (z , zp)
+    help with discreteℕ z x | discreteℕ z y
+    ... | yes p | yes p₁ = refl
+    ... | yes p | no ¬b = ⊥.rec (¬p p)
+    ... | no ¬a | yes b = ⊥.rec (¬q b)
+    ... | no ¬a | no ¬b = refl
+
+  swapFinIso : (x y : Fin n) → Iso (Fin n) (Fin n)
+  Iso.fun (swapFinIso x y) = swapFin x y
+  Iso.inv (swapFinIso x y) = swapFin x y
+  Iso.rightInv (swapFinIso x y) = swapFin² x y
+  Iso.leftInv (swapFinIso x y) = swapFin² x y
+
+module _ {ℓ : Level} {n : ℕ} {A : Fin n → Type ℓ} (x₀ : Fin n)
+  (pt : A x₀) (l : (x : Fin n) → ¬ x ≡ x₀ → A x) where
+  private
+    x = fst x₀
+    p = snd x₀
+  elimFinChoose : (x : _) → A x
+  elimFinChoose (x' , q) with (discreteℕ x x')
+  ... | yes p₁ = subst A (Σ≡Prop (λ _ → isProp<ᵗ) p₁) pt
+  ... | no ¬p = l (x' , q) λ r → ¬p (sym (cong fst r))
+
+  elimFinChooseβ : (elimFinChoose x₀ ≡ pt)
+                × ((x : _) (q : ¬ x ≡ x₀) → elimFinChoose x ≡ l x q)
+  fst elimFinChooseβ with (discreteℕ x x)
+  ... | yes p₁ = (λ j → subst A (isSetFin x₀ x₀ (Σ≡Prop (λ z → isProp<ᵗ) p₁) refl j) pt)
+                ∙ transportRefl pt
+  ... | no ¬p = ⊥.rec (¬p refl)
+  snd elimFinChooseβ (x' , q) with (discreteℕ x x')
+  ... | yes p₁ = λ q → ⊥.rec (q (Σ≡Prop (λ _ → isProp<ᵗ) (sym p₁)))
+  ... | no ¬p = λ s → cong (l (x' , q)) (isPropΠ (λ _ → isProp⊥) _ _)
+
+containsTwoFin : {n : ℕ} (x : Fin (suc (suc n))) → Σ[ y ∈ Fin (suc (suc n)) ] ¬ x ≡ y
+containsTwoFin (zero , p) = (1 , p) , λ q → snotz (sym (cong fst q))
+containsTwoFin (suc x , p) = fzero , λ q → snotz (cong fst q)
+
+≠flast→<ᵗflast : {n : ℕ} → (x : Fin (suc n)) → ¬ x ≡ flast → fst x <ᵗ n
+≠flast→<ᵗflast = elimFin (λ p → ⊥.rec (p refl)) λ p _ → snd p
+
+Fin≠Fin : {n m : ℕ} → ¬ (n ≡ m) → ¬ (Iso (Fin n) (Fin m))
+Fin≠Fin {n = zero} {m = zero} p = ⊥.rec (p refl)
+Fin≠Fin {n = zero} {m = suc m} p q = Iso.inv q fzero .snd
+Fin≠Fin {n = suc n} {m = zero} p q = Iso.fun q fzero .snd
+Fin≠Fin {n = suc n} {m = suc m} p q =
+  Fin≠Fin {n = n} {m = m} (p ∘ cong suc)
+    (Iso⊎→Iso idIso help λ {(zero , tt)
+      → cong (Iso.inv Iso-Fin1⊎Fin-FinSuc) (swapFinβₗ (Iso.fun q flast) flast)
+       ∙ elimFinβ (inl flast) inr .fst})
+  where
+  q^ : Iso (Fin (suc n)) (Fin (suc m))
+  q^ = compIso q (swapFinIso (Iso.fun q flast) flast)
+
+  help : Iso (Fin 1 ⊎ Fin n) (Fin 1 ⊎ Fin m)
+  help = compIso Iso-Fin1⊎Fin-FinSuc (compIso q^ (invIso Iso-Fin1⊎Fin-FinSuc))
diff --git a/Cubical/Data/List/Base.agda b/Cubical/Data/List/Base.agda
index 2695f1de8c..e5b5dc37be 100644
--- a/Cubical/Data/List/Base.agda
+++ b/Cubical/Data/List/Base.agda
@@ -76,3 +76,7 @@ module _ {ℓ} {A : Type ℓ} where
            → List A → B
   rec b _ [] = b
   rec b f (x ∷ xs) = f x (rec b f xs)
+
+ℓ-maxList : List Level → Level
+ℓ-maxList [] = ℓ-zero
+ℓ-maxList (x ∷ x₁) = ℓ-max x (ℓ-maxList x₁)
diff --git a/Cubical/Data/Sequence/Base.agda b/Cubical/Data/Sequence/Base.agda
index 6d2521edde..cab82d8076 100644
--- a/Cubical/Data/Sequence/Base.agda
+++ b/Cubical/Data/Sequence/Base.agda
@@ -3,6 +3,7 @@ module Cubical.Data.Sequence.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Nat
 open import Cubical.Data.Fin
 
@@ -28,3 +29,28 @@ converges seq n = (k : ℕ) → isEquiv (Sequence.map seq {n = k + n})
 
 finiteSequence : (ℓ : Level) (m : ℕ) → Type (ℓ-suc ℓ)
 finiteSequence ℓ m = Σ[ S ∈ Sequence ℓ ] converges S m
+
+shiftSequence : ∀ {ℓ} → Sequence ℓ → (n : ℕ) → Sequence ℓ
+Sequence.obj (shiftSequence seq n) m = Sequence.obj seq (m + n)
+Sequence.map (shiftSequence seq n)  {n = k} x = Sequence.map seq x
+
+-- Isomorphism of sequences
+SequenceIso : (A : Sequence ℓ) (B : Sequence ℓ') → Type (ℓ-max ℓ ℓ')
+SequenceIso A B =
+  Σ[ is ∈ ((n : ℕ) → Iso (Sequence.obj A n) (Sequence.obj B n)) ]
+     ((n : ℕ) (a : Sequence.obj A n)
+       → Sequence.map B (Iso.fun (is n) a) ≡ Iso.fun (is (suc n))
+                         (Sequence.map A a))
+
+-- Equivalences of sequences
+SequenceEquiv : (A : Sequence ℓ) (B : Sequence ℓ') → Type (ℓ-max ℓ ℓ')
+SequenceEquiv A B =
+  Σ[ e ∈ (SequenceMap A B) ]
+     ((n : ℕ) → isEquiv (SequenceMap.map e n))
+
+-- Iso to equiv
+SequenceIso→SequenceEquiv : {A : Sequence ℓ} {B : Sequence ℓ'}
+  → SequenceIso A B → SequenceEquiv A B
+SequenceMap.map (fst (SequenceIso→SequenceEquiv (is , e))) x = Iso.fun (is x)
+SequenceMap.comm (fst (SequenceIso→SequenceEquiv (is , e))) = e
+snd (SequenceIso→SequenceEquiv (is , e)) n = isoToIsEquiv (is n)
diff --git a/Cubical/Data/Sequence/Properties.agda b/Cubical/Data/Sequence/Properties.agda
index b01b6d609b..6a65ba6160 100644
--- a/Cubical/Data/Sequence/Properties.agda
+++ b/Cubical/Data/Sequence/Properties.agda
@@ -2,21 +2,191 @@
 module Cubical.Data.Sequence.Properties where
 
 open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat
 open import Cubical.Foundations.Equiv
-open import Cubical.Data.Sequence.Base
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv.HalfAdjoint
 
+open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sequence.Base
 
 private
   variable
     ℓ ℓ' ℓ'' : Level
+
+open Sequence
+open SequenceMap renaming (map to smap)
+open isHAEquiv
+
+-- Identity map of sequences
 idSequenceMap : (C : Sequence ℓ) → SequenceMap C C
-SequenceMap.map (idSequenceMap C) n x = x
-SequenceMap.comm (idSequenceMap C) n x = refl
+smap (idSequenceMap C) n x = x
+comm (idSequenceMap C) n x = refl
 
+-- Composition of maps
 composeSequenceMap : {C : Sequence ℓ} {D : Sequence ℓ'} {E : Sequence ℓ''}
   (g : SequenceMap D E) (f : SequenceMap C D) → SequenceMap C E
-composeSequenceMap g f .SequenceMap.map n x = g .SequenceMap.map n (f .SequenceMap.map n x)
-composeSequenceMap g f .SequenceMap.comm n x =
-    g .SequenceMap.comm n _
-  ∙ cong (g .SequenceMap.map (suc n)) (f .SequenceMap.comm n x)
+composeSequenceMap g f .smap n x = g .smap n (f .smap n x)
+composeSequenceMap g f .comm n x =
+    g .comm n _
+  ∙ cong (g .smap (suc n)) (f .comm n x)
+
+-- Composition of isos
+compSequenceIso : {A : Sequence ℓ} {B : Sequence ℓ'} {C : Sequence ℓ''}
+  → SequenceIso A B → SequenceIso B C → SequenceIso A C
+fst (compSequenceIso e g) n = compIso (fst e n) (fst g n)
+snd (compSequenceIso e g) n a =
+  snd g n _ ∙ cong (Iso.fun (fst g (suc n))) (snd e n a)
+
+-- Identity equivalence
+idSequenceEquiv : (A : Sequence ℓ) → SequenceEquiv A A
+fst (idSequenceEquiv A) = idSequenceMap A
+snd (idSequenceEquiv A) _ = idIsEquiv _
+
+-- inversion of equivalences
+invSequenceEquiv : {A : Sequence ℓ} {B : Sequence ℓ'}
+  → SequenceEquiv A B → SequenceEquiv B A
+smap (fst (invSequenceEquiv eqs)) n = invEq (_ , snd eqs n)
+comm (fst (invSequenceEquiv {A = A} {B} eqs)) n x =
+    sym (retEq (_ , snd eqs (suc n)) (map A (invEq (_  , snd eqs n) x)))
+  ∙∙ cong (invEq (_ , snd eqs (suc n))) (sym (comm (fst eqs) n (invEq (_ , snd eqs n) x)))
+  ∙∙ cong (invEq (_ , snd eqs (suc n)) ∘ map B) (secEq (_ , snd eqs n) x)
+snd (invSequenceEquiv eqs) n = invEquiv (_ , snd eqs n) .snd
+
+-- inversion of the identity
+invIdSequenceEquiv : {A : Sequence ℓ}
+  → invSequenceEquiv (idSequenceEquiv A) ≡ idSequenceEquiv A
+invIdSequenceEquiv {A = A} =
+  Σ≡Prop (λ _ → isPropΠ (λ _ → isPropIsEquiv _)) main
+  where
+  main : invSequenceEquiv (idSequenceEquiv A) .fst ≡ idSequenceMap A
+  smap (main i) n z = z
+  comm (main i) n x j = rUnit (λ _ → map A x) (~ i) j
+
+-- ua for sequences
+uaSequence : {A B : Sequence ℓ} → SequenceEquiv A B → A ≡ B
+obj (uaSequence {A = A} {B} (e , eqv) i) n = ua (_ , eqv n) i
+map (uaSequence {A = A} {B} (e , eqv) i) {n = n} a =
+  hcomp (λ k → λ {(i = i0) → map A (retEq (_ , eqv n) a k)
+                 ; (i = i1) → (sym (comm e n (invEq (_ , eqv n) a))
+                              ∙ cong (map B) (secEq (_ , eqv n) a)) k})
+        (ua-gluePt (_ , eqv (suc n)) i
+          (map A (invEq (_ , eqv n) (ua-unglue (_ , eqv n) i a))))
+
+uaSequenceIdEquiv : ∀ {ℓ} {A : Sequence ℓ}
+  → uaSequence (idSequenceEquiv A) ≡ refl
+obj (uaSequenceIdEquiv {A = A} i j) n =
+  uaIdEquiv {A = obj A n} i j
+map (uaSequenceIdEquiv {A = A} i j) {n = n} x =
+  hcomp (λ k → λ {(i = i1) → map A x
+                 ; (j = i0) → map A x
+                 ; (j = i1) → rUnit (refl {x = map A x}) (~ i) k})
+   (glue {φ = j ∨ ~ j ∨ i}
+      (λ { (j = i0) → map A x
+         ; (j = i1) → map A x
+         ; (i = i1) → map A x})
+      (map A (unglue (j ∨ ~ j ∨ i) x)))
+
+halfAdjointSequenceEquiv : {A : Sequence ℓ} {B : Sequence ℓ'}
+  → SequenceEquiv A B → SequenceEquiv A B
+fst (halfAdjointSequenceEquiv (e , eqv)) = e
+snd (halfAdjointSequenceEquiv (e , eqv)) n =
+  isHAEquiv→isEquiv (equiv→HAEquiv (_ , eqv n) .snd)
+
+-- Contractibility of total space of (SequenceEquiv A)
+isContrTotalSequence : (A : Sequence ℓ)
+  → isContr (Σ[ B ∈ Sequence ℓ ] SequenceEquiv A B)
+fst (isContrTotalSequence A) = A , idSequenceEquiv A
+snd (isContrTotalSequence A) (B , eqv*) =
+  ΣPathP (uaSequence eqv , main)
+  where
+  eqv = halfAdjointSequenceEquiv eqv*
+
+  eqv⁻ : {n : ℕ} → obj B n → obj A n
+  eqv⁻ {n = n} = invEq (_ , snd eqv n)
+
+  haEqv : (n : ℕ) → HAEquiv (obj A n) (obj B n)
+  haEqv n = equiv→HAEquiv (_ , eqv* .snd n)
+
+
+  help : (n : ℕ) (x : obj A n)
+    → Square (cong (smap (fst eqv) (suc n) ∘ map A)
+                    (retEq (_ , snd eqv n) x))
+              (comm (fst eqv) n x)
+              (sym (comm (fst eqv) n
+                (eqv⁻ (smap (fst eqv) n x)))
+              ∙ cong (map B) (secEq (smap (fst eqv) n , snd eqv n)
+                         (smap (fst eqv) n x)))
+              refl
+  help n x = flipSquare ((compPath≡compPath' _ _
+    ∙ cong₂ _∙'_ refl λ j i
+      → map B (com
+                (equiv→HAEquiv (_ , eqv* .snd n) .snd) x (~ j) i))
+    ◁ λ i j →
+    hcomp (λ k →
+      λ {(j = i0) → comm (fst eqv) n
+                      (lUnit (cong fst
+                        (eqv* .snd n .equiv-proof (smap (fst eqv*) n x)
+                       .snd (x , refl))) k i) k
+       ; (j = i1) → comm (fst eqv) n x (i ∧ k)
+       ; (i = i0) → compPath'-filler
+                       (sym (comm (fst eqv) n (eqv⁻ (smap (fst eqv) n x))))
+                       (cong (map B) (com (haEqv n .snd) x i0)) k j
+       ; (i = i1) → comm (fst eqv) n x k
+       })
+          (map B (smap (fst eqv*) n
+            ((cong fst (eqv* .snd n .equiv-proof (smap (fst eqv*) n x)
+              .snd (x , (λ _ → smap (fst eqv*) n x)))) (i ∨ j)))))
+
+  main : PathP (λ i → SequenceEquiv A (uaSequence eqv i))
+      (idSequenceEquiv A) eqv*
+  smap (fst (main i)) n x = ua-gluePt (_ , snd eqv n) i x
+  comm (fst (main i)) n x j =
+    hcomp (λ k → λ {(i = i0) → map A
+                                  (retEq (_ , snd eqv n) x (k ∨ j))
+                   ; (i = i1) → help n x k j
+                   ; (j = i1) → ua-gluePt (_ , snd eqv (suc n)) i (map A x)})
+          (ua-gluePt (_ , snd eqv (suc n)) i
+                     (map A (retEq (_ , snd eqv n) x j)))
+  snd (main i) n =
+    isProp→PathP {B = λ i → isEquiv  (λ x → ua-gluePt (_ , snd eqv n) i x)}
+     (λ i → isPropIsEquiv _)
+     (idIsEquiv (obj A n)) (snd eqv* n) i
+
+
+-- J for sequences
+SequenceEquivJ : {A : Sequence ℓ}
+  (P : (B : Sequence ℓ) → SequenceEquiv A B → Type ℓ')
+  → P A (idSequenceEquiv A)
+  → (B : _) (e : _) → P B e
+SequenceEquivJ {ℓ = ℓ} {A = A} P ind B e = main (B , e)
+  where
+  P' : Σ[ B ∈ Sequence ℓ ] SequenceEquiv A B → Type _
+  P' (B , e) = P B e
+
+  main : (x : _) → P' x
+  main (B , e) = subst P' (isContrTotalSequence A .snd (B , e)) ind
+
+SequenceEquivJ>_ : {A : Sequence ℓ}
+  {P : (B : Sequence ℓ) → SequenceEquiv A B → Type ℓ'}
+  → P A (idSequenceEquiv A)
+  → (B : _) (e : _) → P B e
+SequenceEquivJ>_ {P = P} hyp B e = SequenceEquivJ P hyp B e
+
+SequenceEquivJRefl : ∀ {ℓ ℓ'} {A : Sequence ℓ}
+  (P : (B : Sequence ℓ) → SequenceEquiv A B → Type ℓ')
+    (id : P A (idSequenceEquiv A))
+  → SequenceEquivJ P id A (idSequenceEquiv A) ≡ id
+SequenceEquivJRefl {ℓ = ℓ} {A = A} P ids =
+  (λ j → subst P' (isProp→isSet (isContr→isProp (isContrTotalSequence A))
+                    _ _ (isContrTotalSequence A .snd
+                          (A , idSequenceEquiv A)) refl j) ids)
+  ∙ transportRefl ids
+  where
+  P' : Σ[ B ∈ Sequence ℓ ] SequenceEquiv A B → Type _
+  P' (B , e) = P B e
diff --git a/Cubical/Data/Sum/Properties.agda b/Cubical/Data/Sum/Properties.agda
index 0cc5687221..bd0d2402a6 100644
--- a/Cubical/Data/Sum/Properties.agda
+++ b/Cubical/Data/Sum/Properties.agda
@@ -293,3 +293,67 @@ leftInv ×DistR⊎Iso (a , inr c) = refl
                                              (map f g x)
                                              (map f g y) ⟩
                           map f g x ≡ map f g y ■) .snd)
+
+-- A ⊎ B ≃ C ⊎ D implies B ≃ D if the first equiv respects inl
+Iso⊎→Iso : (f : Iso A C) (e : Iso (A ⊎ B) (C ⊎ D))
+   → ((a : A) → Iso.fun e (inl a) ≡ inl (Iso.fun f a))
+   → Iso B D
+Iso⊎→Iso {A = A} {C = C} {B = B} {D = D} f e p = Iso'
+  where
+  ⊥-fib : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → A ⊎ B → Type
+  ⊥-fib (inl x) = ⊥
+  ⊥-fib (inr x) = Unit
+
+  module _ {A : Type ℓa} {B : Type ℓb} {C : Type ℓc} {D : Type ℓd}
+         (f : Iso A C)
+         (e : Iso (A ⊎ B) (C ⊎ D))
+         (p : (a : A) → Iso.fun e (inl a) ≡ inl (Iso.fun f a)) where
+    T : (b : B) → Type _
+    T b = Σ[ d' ∈ C ⊎ D ] (Iso.fun e (inr b) ≡ d')
+
+    T-elim : ∀ {ℓ} (b : B) {P : (x : T b) → Type ℓ}
+           → ((d : D) (s : _) → P (inr d , s))
+           → (x : _) → P x
+    T-elim b ind (inl x , q) =
+      ⊥.rec (subst ⊥-fib (sym (sym (Iso.leftInv e _)
+          ∙ cong (Iso.inv e)
+             (p _ ∙ cong inl (Iso.rightInv f x) ∙ sym q)
+          ∙ Iso.leftInv e _)) tt)
+    T-elim b ind (inr x , y) = ind x y
+
+  e-pres-inr-help : (b : B) → T f e p b  → D
+  e-pres-inr-help b = T-elim f e p b λ d _ → d
+
+  p' : (a : C) → Iso.inv e (inl a) ≡ inl (Iso.inv f a)
+  p' c = cong (Iso.inv e ∘ inl) (sym (Iso.rightInv f c))
+      ∙∙ cong (Iso.inv e) (sym (p (Iso.inv f c)))
+      ∙∙ Iso.leftInv e _
+
+  e⁻-pres-inr-help : (d : D) → T (invIso f) (invIso e) p' d → B
+  e⁻-pres-inr-help d = T-elim (invIso f) (invIso e) p' d λ b _ → b
+
+  e-pres-inr : B → D
+  e-pres-inr b = e-pres-inr-help b (_ , refl)
+
+  e⁻-pres-inr : D → B
+  e⁻-pres-inr d = e⁻-pres-inr-help d (_ , refl)
+
+  lem1 : (b : B) (e : T f e p b) (d : _)
+    → e⁻-pres-inr-help (e-pres-inr-help b e) d ≡ b
+  lem1 b = T-elim f e p b λ d s
+    → T-elim (invIso f) (invIso e) p' _
+      λ b' s' → invEq (_ , isEmbedding-inr _ _)
+        (sym s' ∙ cong (Iso.inv e) (sym s) ∙ Iso.leftInv e _)
+
+  lem2 : (d : D) (e : T (invIso f) (invIso e) p' d ) (t : _)
+    → e-pres-inr-help (e⁻-pres-inr-help d e) t ≡ d
+  lem2 d = T-elim (invIso f) (invIso e) p' d
+    λ b s → T-elim f e p _ λ d' s'
+    → invEq (_ , isEmbedding-inr _ _)
+         (sym s' ∙ cong (Iso.fun e) (sym s) ∙ Iso.rightInv e _)
+
+  Iso' : Iso B D
+  Iso.fun Iso' = e-pres-inr
+  Iso.inv Iso' = e⁻-pres-inr
+  Iso.rightInv Iso' x = lem2 x (_ , refl) (_ , refl)
+  Iso.leftInv Iso' x = lem1 x (_ , refl) (_ , refl)
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index 7d2151f194..5559b748bd 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -634,3 +634,7 @@ open Lift public
 
 liftExt : ∀ {A : Type ℓ} {a b : Lift {ℓ} {ℓ'} A} → (lower a ≡ lower b) → a ≡ b
 liftExt x i = lift (x i)
+
+liftFun : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'}
+  (f : A → B) → Lift {j = ℓ''} A → Lift {j = ℓ'''} B
+liftFun f (lift a) = lift (f a)
diff --git a/Cubical/HITs/Pushout/Properties.agda b/Cubical/HITs/Pushout/Properties.agda
index 03916db59d..e8fa8c5cd4 100644
--- a/Cubical/HITs/Pushout/Properties.agda
+++ b/Cubical/HITs/Pushout/Properties.agda
@@ -11,7 +11,6 @@ This file contains:
 
 - Homotopy natural equivalences of pushout spans
   (unpacked and avoiding transports)
-
 -}
 
 {-# OPTIONS --safe #-}
@@ -22,20 +21,26 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Path
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Equiv.HalfAdjoint
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Transport
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv.HalfAdjoint
+
+open import Cubical.Relation.Nullary
 
 open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Sigma
 open import Cubical.Data.Unit
 open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.List
 
 open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Susp.Base
 
 private
   variable
@@ -73,76 +78,88 @@ pushoutSwitchEquiv = isoToEquiv (iso f inv leftInv rightInv)
 {-
   Definition of pushout diagrams
 -}
-
-record 3-span : Type₁ where
-  field
-    A0 A2 A4 : Type₀
-    f1 : A2 → A0
-    f3 : A2 → A4
-
-3span : {A0 A2 A4 : Type₀} → (A2 → A0) → (A2 → A4) → 3-span
-3span f1 f3 = record { f1 = f1 ; f3 = f3 }
-
-spanPushout : (s : 3-span) → Type₀
-spanPushout s = Pushout (3-span.f1 s) (3-span.f3 s)
+module _ {ℓ₀ ℓ₂ ℓ₄ : Level} where
+  private
+    ℓ* = ℓ-maxList (ℓ₀ ∷ ℓ₂ ∷ ℓ₄ ∷ [])
+  record  3-span : Type (ℓ-suc ℓ*) where
+    field
+      A0 : Type ℓ₀
+      A2 : Type ℓ₂
+      A4 : Type ℓ₄
+      f1 : A2 → A0
+      f3 : A2 → A4
+
+  3span : {A0 : Type ℓ₀} {A2 : Type ℓ₂} {A4 : Type ℓ₄}
+    → (A2 → A0) → (A2 → A4) → 3-span
+  3span f1 f3 = record { f1 = f1 ; f3 = f3 }
+
+  spanPushout : (s : 3-span) → Type ℓ*
+  spanPushout s = Pushout (3-span.f1 s) (3-span.f3 s)
 
 {-
   Definition of a homotopy natural diagram equivalence
 -}
 
-record 3-span-equiv (s1 : 3-span) (s2 : 3-span) : Type₀ where
-   field
-     e0 : 3-span.A0 s1 ≃ 3-span.A0 s2
-     e2 : 3-span.A2 s1 ≃ 3-span.A2 s2
-     e4 : 3-span.A4 s1 ≃ 3-span.A4 s2
-     H1 : ∀ x → 3-span.f1 s2 (e2 .fst x) ≡ e0 .fst (3-span.f1 s1 x)
-     H3 : ∀ x → 3-span.f3 s2 (e2 .fst x) ≡ e4 .fst (3-span.f3 s1 x)
-
-{-
-  Proof that homotopy equivalent spans are in fact equal
--}
-spanEquivToPath : {s1 : 3-span} → {s2 : 3-span} → (e : 3-span-equiv s1 s2) → s1 ≡ s2
-spanEquivToPath {s1} {s2} e = spanPath
-  where
-    open 3-span-equiv e
-    open 3-span
+module _ {ℓ₀₀ ℓ₀₂ ℓ₀₄ : Level} {ℓ₂₀ ℓ₂₂ ℓ₂₄ : Level}  where
+  private
+    ℓ* = ℓ-maxList (ℓ₀₀ ∷ ℓ₀₂ ∷ ℓ₀₄ ∷ ℓ₂₀ ∷ ℓ₂₂ ∷ ℓ₂₄ ∷ [])
+  record 3-span-equiv (s1 : 3-span {ℓ₀₀} {ℓ₀₂} {ℓ₀₄})
+                      (s2 : 3-span {ℓ₂₀} {ℓ₂₂} {ℓ₂₄})
+                    : Type (ℓ-suc ℓ*) where
+     field
+       e0 : 3-span.A0 s1 ≃ 3-span.A0 s2
+       e2 : 3-span.A2 s1 ≃ 3-span.A2 s2
+       e4 : 3-span.A4 s1 ≃ 3-span.A4 s2
+       H1 : ∀ x → 3-span.f1 s2 (e2 .fst x) ≡ e0 .fst (3-span.f1 s1 x)
+       H3 : ∀ x → 3-span.f3 s2 (e2 .fst x) ≡ e4 .fst (3-span.f3 s1 x)
+
+  {-
+    Proof that homotopy equivalent spans are in fact equal
+  -}
+module _ {ℓ₀ ℓ₂ ℓ₄ : Level} where
+  spanEquivToPath : {s1 s2 : 3-span {ℓ₀} {ℓ₂} {ℓ₄}}
+    → (e : 3-span-equiv s1 s2) → s1 ≡ s2
+  spanEquivToPath {s1} {s2} e = spanPath
+    where
+      open 3-span-equiv e
+      open 3-span
 
-    path0 : A0 s1 ≡ A0 s2
-    path0 = ua e0
+      path0 : A0 s1 ≡ A0 s2
+      path0 = ua e0
 
-    path2 : A2 s1 ≡ A2 s2
-    path2 = ua e2
+      path2 : A2 s1 ≡ A2 s2
+      path2 = ua e2
 
-    path4 : A4 s1 ≡ A4 s2
-    path4 = ua e4
+      path4 : A4 s1 ≡ A4 s2
+      path4 = ua e4
 
-    spanPath1 : I → 3-span
-    spanPath1 i = record { A0 = path0 i ; A2 = path2 i ; A4 = path4 i ;
-                           f1 = λ x → (transp (λ j → path0 (i ∧ j)) (~ i) (f1 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) ;
-                           f3 = λ x → (transp (λ j → path4 (i ∧ j)) (~ i) (f3 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) }
+      spanPath1 : I → 3-span
+      spanPath1 i = record { A0 = path0 i ; A2 = path2 i ; A4 = path4 i ;
+                             f1 = λ x → (transp (λ j → path0 (i ∧ j)) (~ i) (f1 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) ;
+                             f3 = λ x → (transp (λ j → path4 (i ∧ j)) (~ i) (f3 s1 (transp (λ j → path2 (~ j ∧ i)) (~ i) x))) }
 
-    spanPath2 : I → 3-span
-    spanPath2 i = record { A0 = A0 s2 ; A2 = A2 s2 ; A4 = A4 s2 ; f1 = f1Path i ; f3 = f3Path i }
-      where
-        f1Path : I → A2 s2 → A0 s2
-        f1Path i x = ((uaβ e0 (f1 s1 (transport (λ j → path2 (~ j)) x)))
-                     ∙ (H1 (transport (λ j → path2 (~ j)) x)) ⁻¹
-                     ∙ (λ j → f1 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
-                     ∙ (λ j → f1 s2 (transportTransport⁻ path2 x j))) i
-
-        f3Path : I → A2 s2 → A4 s2
-        f3Path i x = ((uaβ e4 (f3 s1 (transport (λ j → path2 (~ j)) x)))
-                     ∙ (H3 (transport (λ j → path2 (~ j)) x)) ⁻¹
-                     ∙ (λ j → f3 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
-                     ∙ (λ j → f3 s2 (transportTransport⁻ path2 x j))) i
-
-    spanPath : s1 ≡ s2
-    spanPath = (λ i → spanPath1 i) ∙ (λ i → spanPath2 i)
-
--- as a corollary, they have the same pushout
-spanEquivToPushoutPath : {s1 : 3-span} → {s2 : 3-span} → (e : 3-span-equiv s1 s2)
-                         → spanPushout s1 ≡ spanPushout s2
-spanEquivToPushoutPath {s1} {s2} e = cong spanPushout (spanEquivToPath e)
+      spanPath2 : I → 3-span
+      spanPath2 i = record { A0 = A0 s2 ; A2 = A2 s2 ; A4 = A4 s2 ; f1 = f1Path i ; f3 = f3Path i }
+        where
+          f1Path : I → A2 s2 → A0 s2
+          f1Path i x = ((uaβ e0 (f1 s1 (transport (λ j → path2 (~ j)) x)))
+                       ∙ (H1 (transport (λ j → path2 (~ j)) x)) ⁻¹
+                       ∙ (λ j → f1 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
+                       ∙ (λ j → f1 s2 (transportTransport⁻ path2 x j))) i
+
+          f3Path : I → A2 s2 → A4 s2
+          f3Path i x = ((uaβ e4 (f3 s1 (transport (λ j → path2 (~ j)) x)))
+                       ∙ (H3 (transport (λ j → path2 (~ j)) x)) ⁻¹
+                       ∙ (λ j → f3 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j)))
+                       ∙ (λ j → f3 s2 (transportTransport⁻ path2 x j))) i
+
+      spanPath : s1 ≡ s2
+      spanPath = (λ i → spanPath1 i) ∙ (λ i → spanPath2 i)
+
+  -- as a corollary, they have the same pushout
+  spanEquivToPushoutPath : {s1 : 3-span} → {s2 : 3-span} → (e : 3-span-equiv s1 s2)
+                           → spanPushout s1 ≡ spanPushout s2
+  spanEquivToPushoutPath {s1} {s2} e = cong spanPushout (spanEquivToPath e)
 
 {-
 
@@ -169,9 +186,18 @@ Then the lemma states there is an equivalence A□○ ≃ A○□.
 
 -}
 
-record 3x3-span : Type₁ where
+record 3x3-span {ℓ₀₀ ℓ₀₂ ℓ₀₄ ℓ₂₀ ℓ₂₂ ℓ₂₄ ℓ₄₀ ℓ₄₂ ℓ₄₄ : Level} :
+  Type (ℓ-suc (ℓ-maxList (ℓ₀₀ ∷ ℓ₀₂ ∷ ℓ₀₄ ∷ ℓ₂₀ ∷ ℓ₂₂ ∷ ℓ₂₄ ∷ ℓ₄₀ ∷ ℓ₄₂ ∷ ℓ₄₄ ∷ []))) where
   field
-    A00 A02 A04 A20 A22 A24 A40 A42 A44 : Type₀
+    A00 : Type ℓ₀₀
+    A02 : Type ℓ₀₂
+    A04 : Type ℓ₀₄
+    A20 : Type ℓ₂₀
+    A22 : Type ℓ₂₂
+    A24 : Type ℓ₂₄
+    A40 : Type ℓ₄₀
+    A42 : Type ℓ₄₂
+    A44 : Type ℓ₄₄
 
     f10 : A20 → A00
     f12 : A22 → A02
@@ -195,13 +221,13 @@ record 3x3-span : Type₁ where
     H33 : ∀ x → f43 (f32 x) ≡ f34 (f23 x)
 
   -- pushouts of the lines
-  A□0 : Type₀
+  A□0 : Type _
   A□0 = Pushout f10 f30
 
-  A□2 : Type₀
+  A□2 : Type _
   A□2 = Pushout f12 f32
 
-  A□4 : Type₀
+  A□4 : Type _
   A□4 = Pushout f14 f34
 
   -- maps between pushouts
@@ -220,17 +246,17 @@ record 3x3-span : Type₁ where
                    ∙∙ (λ i → inr (H33 a (~ i)))) j
 
   -- total pushout
-  A□○ : Type₀
+  A□○ : Type _
   A□○ = Pushout f□1 f□3
 
   -- pushouts of the columns
-  A0□ : Type₀
+  A0□ : Type _
   A0□ = Pushout f01 f03
 
-  A2□ : Type₀
+  A2□ : Type _
   A2□ = Pushout f21 f23
 
-  A4□ : Type₀
+  A4□ : Type _
   A4□ = Pushout f41 f43
 
   -- maps between pushouts
@@ -249,7 +275,7 @@ record 3x3-span : Type₁ where
                    ∙∙ (λ i → inr (H33 a i))) j
 
   -- total pushout
-  A○□ : Type₀
+  A○□ : Type _
   A○□ = Pushout f1□ f3□
 
   -- forward map of the equivalence A□○ ≃ A○□
@@ -480,7 +506,7 @@ private
                    ∙∙ λ j → inr (refl-lem (g₁ a) i j)))
           ∙∙ sym (rUnit (push a))
 
-
+-- induced isomorphism of pushouts (see later def. pushoutIso/pushoutEquiv for a more universe polymorphic)
 module _ {ℓ : Level} {A₁ B₁ C₁ A₂ B₂ C₂ : Type ℓ}
   (f₁ : A₁ → B₁) (g₁ : A₁ → C₁)
   (f₂ : A₂ → B₂) (g₂ : A₂ → C₂)
@@ -492,15 +518,115 @@ module _ {ℓ : Level} {A₁ B₁ C₁ A₂ B₂ C₂ : Type ℓ}
     module P = PushoutIso A≃ B≃ C≃ f₁ g₁ f₂ g₂ id1 id2
     l-r-cancel = F-G-cancel A≃ B≃ C≃ f₁ g₁ f₂ g₂ id1 id2
 
+  pushoutIso' : Iso (Pushout f₁ g₁) (Pushout f₂ g₂)
+  fun pushoutIso' = P.F
+  inv pushoutIso' = P.G
+  rightInv pushoutIso' = fst l-r-cancel
+  leftInv pushoutIso' = snd l-r-cancel
+
+  pushoutEquiv' : Pushout f₁ g₁ ≃ Pushout f₂ g₂
+  pushoutEquiv' = isoToEquiv pushoutIso'
+
+-- lift induces an equivalence on Pushouts
+module _ {ℓ ℓ' ℓ'' : Level} (ℓ''' : Level)
+  {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (f : A → B) (g : A → C) where
+  PushoutLevel  : Level
+  PushoutLevel = ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ'''))
+
+  PushoutLift : Type PushoutLevel
+  PushoutLift = Pushout {A = Lift {j = ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')} A}
+                        {B = Lift {j = ℓ-max ℓ (ℓ-max ℓ'' ℓ''')} B}
+                        {C = Lift {j = ℓ-max ℓ (ℓ-max ℓ' ℓ''')} C}
+                        (liftFun f)
+                        (liftFun g)
+
+  PushoutLiftIso : Iso (Pushout f g) PushoutLift
+  Iso.fun PushoutLiftIso (inl x) = inl (lift x)
+  Iso.fun PushoutLiftIso (inr x) = inr (lift x)
+  Iso.fun PushoutLiftIso (push a i) = push (lift a) i
+  Iso.inv PushoutLiftIso (inl (lift x)) = inl x
+  Iso.inv PushoutLiftIso (inr (lift x)) = inr x
+  Iso.inv PushoutLiftIso (push (lift a) i) = push a i
+  Iso.rightInv PushoutLiftIso (inl (lift x)) = refl
+  Iso.rightInv PushoutLiftIso (inr (lift x)) = refl
+  Iso.rightInv PushoutLiftIso (push (lift a) i) = refl
+  Iso.leftInv PushoutLiftIso (inl x) = refl
+  Iso.leftInv PushoutLiftIso (inr x) = refl
+  Iso.leftInv PushoutLiftIso (push a i) = refl
+
+-- equivalence of pushouts with arbitrary univeses
+module _ {ℓA₁ ℓB₁ ℓC₁ ℓA₂ ℓB₂ ℓC₂}
+      {A₁ : Type ℓA₁} {B₁ : Type ℓB₁} {C₁ : Type ℓC₁}
+      {A₂ : Type ℓA₂} {B₂ : Type ℓB₂} {C₂ : Type ℓC₂}
+      (f₁ : A₁ → B₁) (g₁ : A₁ → C₁)
+      (f₂ : A₂ → B₂) (g₂ : A₂ → C₂)
+      (A≃ : A₁ ≃ A₂) (B≃ : B₁ ≃ B₂) (C≃ : C₁ ≃ C₂)
+      (id1 : fst B≃ ∘ f₁ ≡ f₂ ∘ fst A≃)
+      (id2 : fst C≃ ∘ g₁ ≡ g₂ ∘ fst A≃) where
+  private
+    ℓ* = ℓ-max ℓA₁ (ℓ-max ℓA₂ (ℓ-max ℓB₁ (ℓ-max ℓB₂ (ℓ-max ℓC₁ ℓC₂))))
+
+    pushoutIso→ : Pushout f₁ g₁ → Pushout f₂ g₂
+    pushoutIso→ (inl x) = inl (fst B≃ x)
+    pushoutIso→ (inr x) = inr (fst C≃ x)
+    pushoutIso→ (push a i) =
+      ((λ i → inl (id1 i a)) ∙∙ push (fst A≃ a) ∙∙ λ i → inr (id2 (~ i) a)) i
+
+    pushoutIso* : Iso (Pushout f₁ g₁) (Pushout f₂ g₂)
+    pushoutIso* =
+        compIso (PushoutLiftIso ℓ* f₁ g₁)
+          (compIso (pushoutIso' _ _ _ _
+            (Lift≃Lift A≃)
+            (Lift≃Lift B≃)
+            (Lift≃Lift C≃)
+            (funExt (λ { (lift x) → cong lift (funExt⁻ id1 x)}))
+            (funExt (λ { (lift x) → cong lift (funExt⁻ id2 x)})))
+          (invIso (PushoutLiftIso ℓ* f₂ g₂)))
+
+    pushoutIso→≡ : (x : _) → Iso.fun pushoutIso* x ≡ pushoutIso→ x
+    pushoutIso→≡ (inl x) = refl
+    pushoutIso→≡ (inr x) = refl
+    pushoutIso→≡ (push a i) j =
+      cong-∙∙ (Iso.inv (PushoutLiftIso ℓ* f₂ g₂))
+            (λ i → inl (lift (id1 i a)))
+            (push (lift (fst A≃ a)))
+            (λ i → inr (lift (id2 (~ i) a))) j i
+
   pushoutIso : Iso (Pushout f₁ g₁) (Pushout f₂ g₂)
-  fun pushoutIso = P.F
-  inv pushoutIso = P.G
-  rightInv pushoutIso = fst l-r-cancel
-  leftInv pushoutIso = snd l-r-cancel
+  fun pushoutIso = pushoutIso→
+  inv pushoutIso = inv pushoutIso*
+  rightInv pushoutIso x =
+    sym (pushoutIso→≡ (inv pushoutIso* x)) ∙ rightInv pushoutIso* x
+  leftInv pushoutIso x =
+    cong (inv pushoutIso*) (sym (pushoutIso→≡ x)) ∙ leftInv pushoutIso* x
 
   pushoutEquiv : Pushout f₁ g₁ ≃ Pushout f₂ g₂
   pushoutEquiv = isoToEquiv pushoutIso
 
+module _ {C : Type ℓ} {B : Type ℓ'} where
+  PushoutAlongEquiv→ : {A : Type ℓ}
+    (e : A ≃ C) (f : A → B) → Pushout (fst e) f → B
+  PushoutAlongEquiv→ e f (inl x) = f (invEq e x)
+  PushoutAlongEquiv→ e f (inr x) = x
+  PushoutAlongEquiv→ e f (push a i) = f (retEq e a i)
+
+  private
+    PushoutAlongEquiv→Cancel : {A : Type ℓ} (e : A ≃ C) (f : A → B)
+      → retract (PushoutAlongEquiv→ e f) inr
+    PushoutAlongEquiv→Cancel =
+      EquivJ (λ A e → (f : A → B)
+                    → retract (PushoutAlongEquiv→ e f) inr)
+            λ f → λ { (inl x) → sym (push x)
+                      ; (inr x) → refl
+                      ; (push a i) j → push a (~ j ∨ i)}
+
+  PushoutAlongEquiv : {A : Type ℓ} (e : A ≃ C) (f : A → B)
+    → Iso (Pushout (fst e) f) B
+  Iso.fun (PushoutAlongEquiv e f) = PushoutAlongEquiv→ e f
+  Iso.inv (PushoutAlongEquiv e f) = inr
+  Iso.rightInv (PushoutAlongEquiv e f) x = refl
+  Iso.leftInv (PushoutAlongEquiv e f) = PushoutAlongEquiv→Cancel e f
+
 module PushoutDistr {ℓ ℓ' ℓ'' ℓ''' : Level}
   {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''}
   (f : B → A) (g : C → B) (h : C → D) where
@@ -538,11 +664,418 @@ fun (PushoutEmptyFam ¬A ¬C) = inl
 inv (PushoutEmptyFam ¬A ¬C) (inl x) = x
 inv (PushoutEmptyFam ¬A ¬C) (inr x) = ⊥.rec (¬C x)
 inv (PushoutEmptyFam ¬A ¬C {f = f} {g = g}) (push a i) =
-  ⊥.rec {A = f a ≡ rec (¬C (g a))} (¬A a) i
+  ⊥.rec {A = f a ≡ ⊥.rec (¬C (g a))} (¬A a) i
 rightInv (PushoutEmptyFam {A = A} {B = B} ¬A ¬C) (inl x) = refl
 rightInv (PushoutEmptyFam {A = A} {B = B} ¬A ¬C) (inr x) = ⊥.rec (¬C x)
 rightInv (PushoutEmptyFam {A = A} {B = B} ¬A ¬C {f = f} {g = g}) (push a i) j =
-  ⊥.rec {A = Square (λ i →  inl (rec {A = f a ≡ rec (¬C (g a))} (¬A a) i))
-                     (push a) (λ _ → inl (f a)) (rec (¬C (g a)))}
+  ⊥.rec {A = Square (λ i →  inl (⊥.rec {A = f a ≡ ⊥.rec (¬C (g a))} (¬A a) i))
+                     (push a) (λ _ → inl (f a)) (⊥.rec (¬C (g a)))}
          (¬A a) j i
 leftInv (PushoutEmptyFam {A = A} {B = B} ¬A ¬C) x = refl
+
+PushoutCompEquivIso : ∀ {ℓA ℓA' ℓB ℓB' ℓC}
+  {A : Type ℓA} {A' : Type ℓA'} {B : Type ℓB} {B' : Type ℓB'}
+  {C : Type ℓC}
+  (e1 : A ≃ A') (e2 : B' ≃ B)
+  (f : A' → B') (g : A → C)
+  → Iso (Pushout (fst e2 ∘ f ∘ fst e1) g) (Pushout f (g ∘ invEq e1))
+PushoutCompEquivIso {ℓA = ℓA} {ℓA'} {ℓB} {ℓB'} {ℓC} e1 e2 f g =
+  compIso (pushoutIso _ _ _ _ LiftEquiv LiftEquiv LiftEquiv refl refl)
+    (compIso (PushoutCompEquivIso' {ℓ = ℓ*} {ℓ*} {ℓ*}
+      (liftEq ℓ* e1) (liftEq ℓ* e2) (liftFun f) (liftFun g))
+      (invIso (pushoutIso _ _ _ _
+               LiftEquiv LiftEquiv (LiftEquiv {ℓ' = ℓ*}) refl refl)))
+  where
+  ℓ* = ℓ-maxList (ℓA ∷ ℓA' ∷ ℓB ∷ ℓB' ∷ ℓC ∷ [])
+
+  liftEq : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (ℓ* : Level)
+    → A ≃ B → Lift {j = ℓ*} A ≃ Lift {j = ℓ*} B
+  liftEq ℓ* e = compEquiv (invEquiv LiftEquiv) (compEquiv e LiftEquiv)
+
+  PushoutCompEquivIso' : ∀ {ℓ ℓ' ℓ''} {A A' : Type ℓ} {B B' : Type ℓ'} {C : Type ℓ''}
+    (e1 : A ≃ A') (e2 : B' ≃ B)
+    (f : A' → B') (g : A → C)
+    → Iso (Pushout (fst e2 ∘ f ∘ fst e1) g) (Pushout f (g ∘ invEq e1))
+  PushoutCompEquivIso' {A = A} {A' = A'} {B} {B'} {C} =
+    EquivJ (λ A e1 → (e2 : B' ≃ B) (f : A' → B') (g : A → C)
+                   →  Iso (Pushout (fst e2 ∘ f ∘ fst e1) g)
+                           (Pushout f (g ∘ invEq e1)))
+     (EquivJ (λ B' e2 → (f : A' → B') (g : A' → C)
+                   →  Iso (Pushout (fst e2 ∘ f) g)
+                           (Pushout f g))
+       λ f g → idIso)
+
+-- Computation of cofibre of the quotient map B → B/A (where B/A
+-- denotes the cofibre of some f : B → A)
+module _ {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B) where
+  private
+    open 3x3-span
+    inst : 3x3-span
+    A00 inst = Unit
+    A02 inst = Unit
+    A04 inst = Unit
+    A20 inst = fst A
+    A22 inst = Unit
+    A24 inst = Unit
+    A40 inst = fst B
+    A42 inst = fst B
+    A44 inst = Unit
+    f10 inst = _
+    f12 inst = _
+    f14 inst = _
+    f30 inst = fst f
+    f32 inst = λ _ → pt B
+    f34 inst = _
+    f01 inst = _
+    f21 inst = λ _ → pt A
+    f41 inst = idfun (fst B)
+    f03 inst = _
+    f23 inst = _
+    f43 inst = _
+    H11 inst = (λ _ → refl)
+    H13 inst = λ _ → refl
+    H31 inst = λ _ → sym (snd f)
+    H33 inst = λ _ → refl
+
+    A□0≅cofib-f : Iso (A□0 inst) (cofib (fst f))
+    A□0≅cofib-f = idIso
+
+    A□2≅B : Iso (A□2 inst) (fst B)
+    A□2≅B = PushoutAlongEquiv (idEquiv _) λ _ → pt B
+
+    A□4≅Unit : Iso (A□4 inst) Unit
+    A□4≅Unit = PushoutAlongEquiv (idEquiv _) λ _ → tt
+
+    A0□≅Unit : Iso (A0□ inst) Unit
+    A0□≅Unit = PushoutAlongEquiv (idEquiv _) λ _ → tt
+
+    A2□≅A : Iso (A2□ inst) (fst A)
+    A2□≅A = compIso (equivToIso (invEquiv (symPushout _ _)))
+                    (PushoutAlongEquiv (idEquiv _) λ _ → pt A)
+
+    A4□≅Unit : Iso (A4□ inst) Unit
+    A4□≅Unit = PushoutAlongEquiv (idEquiv _) λ _ → tt
+
+    A□○≅cofibInr : Iso (A□○ inst) (cofib {B = cofib (fst f)} inr)
+    A□○≅cofibInr = compIso (invIso (equivToIso (symPushout _ _)))
+                           (pushoutIso _ _ _ _
+                             (isoToEquiv A□2≅B)
+                             (isoToEquiv A□4≅Unit)
+                             (isoToEquiv A□0≅cofib-f)
+                             refl (funExt λ x
+                               → cong (A□0≅cofib-f .Iso.fun ∘ f□1 inst)
+                                       (sym (Iso.leftInv A□2≅B x))))
+
+    A○□≅ : Iso (A○□ inst) (Susp (typ A))
+    A○□≅ =
+      compIso
+        (pushoutIso _ _ _ _
+          (isoToEquiv A2□≅A)
+          (isoToEquiv A0□≅Unit)
+          (isoToEquiv A4□≅Unit)
+          refl refl)
+        PushoutSuspIsoSusp
+
+  Iso-cofibInr-Susp : Iso (cofib {B = cofib (fst f)} inr)
+                          (Susp (typ A))
+  Iso-cofibInr-Susp =
+    compIso (compIso (invIso A□○≅cofibInr)
+      (3x3-Iso inst)) A○□≅
+
+-- Commutative squares and pushout squares
+module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
+  private
+    ℓ* = ℓ-maxList (ℓ₀ ∷ ℓ₂ ∷ ℓ₄ ∷ ℓP ∷ [])
+
+  record  commSquare : Type (ℓ-suc ℓ*) where
+    open 3-span
+    field
+      sp : 3-span {ℓ₀} {ℓ₂} {ℓ₄}
+      P : Type ℓP
+      inlP : A0 sp → P
+      inrP : A4 sp → P
+      comm : inlP ∘ f1 sp ≡ inrP ∘ f3 sp
+
+  open commSquare
+
+  Pushout→commSquare : (sk : commSquare) → spanPushout (sp sk) → P sk
+  Pushout→commSquare sk (inl x) = inlP sk x
+  Pushout→commSquare sk (inr x) = inrP sk x
+  Pushout→commSquare sk (push a i) = comm sk i a
+
+  isPushoutSquare : commSquare → Type _
+  isPushoutSquare sk = isEquiv (Pushout→commSquare sk)
+
+  PushoutSquare : Type (ℓ-suc ℓ*)
+  PushoutSquare = Σ commSquare isPushoutSquare
+
+-- Rotations of commutative squares and pushout squares
+module _ {ℓ₀ ℓ₂ ℓ₄ ℓP : Level} where
+  open commSquare
+  open 3-span
+
+  rotateCommSquare : commSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP} → commSquare {ℓ₄} {ℓ₂} {ℓ₀} {ℓP}
+  A0 (sp (rotateCommSquare sq)) = A4 (sp sq)
+  A2 (sp (rotateCommSquare sq)) = A2 (sp sq)
+  A4 (sp (rotateCommSquare sq)) = A0 (sp sq)
+  f1 (sp (rotateCommSquare sq)) = f3 (sp sq)
+  f3 (sp (rotateCommSquare sq)) = f1 (sp sq)
+  P (rotateCommSquare sq) = P sq
+  inlP (rotateCommSquare sq) = inrP sq
+  inrP (rotateCommSquare sq) = inlP sq
+  comm (rotateCommSquare sq) = sym (comm sq)
+
+  rotatePushoutSquare : PushoutSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP}
+                     → PushoutSquare {ℓ₄} {ℓ₂} {ℓ₀} {ℓP}
+  fst (rotatePushoutSquare (sq , eq)) = rotateCommSquare sq
+  snd (rotatePushoutSquare (sq , eq)) =
+    subst isEquiv (funExt lem) (compEquiv (symPushout _ _) (_ , eq) .snd)
+    where
+    lem : (x : _) → Pushout→commSquare sq (symPushout _ _ .fst x)
+                  ≡ Pushout→commSquare (rotateCommSquare sq) x
+    lem (inl x) = refl
+    lem (inr x) = refl
+    lem (push a i) = refl
+
+
+-- Pushout pasting lemma:
+{- Given a diagram consisting of two
+commuting squares where the top square is a pushout:
+
+A2 -—f3-→ A4
+ ∣           ∣
+f1         inrP
+ ↓       ⌜  ↓
+A0 -—inlP→ P
+ |          |
+ f          h
+ ↓          ↓
+ A -—-g-—→ B
+
+The bottom square is a pushout square iff the outer rectangle is
+a pushout square.
+-}
+
+module PushoutPasteDown {ℓ₀ ℓ₂ ℓ₄ ℓP ℓA ℓB : Level}
+  (SQ : PushoutSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
+  {A : Type ℓA} {B : Type ℓB}
+  (f : 3-span.A0 (commSquare.sp (fst SQ)) → A)
+  (g : A → B) (h : commSquare.P (fst SQ) → B)
+  (com : g ∘ f ≡ h ∘ commSquare.inlP (fst SQ))
+  where
+  private
+    sq = fst SQ
+    isP = snd SQ
+    ℓ* = ℓ-maxList (ℓ₀ ∷ ℓ₂ ∷ ℓ₄ ∷ ℓP ∷ [])
+
+  open commSquare sq
+  open 3-span sp
+
+  bottomSquare : commSquare
+  3-span.A0 (commSquare.sp bottomSquare) = A
+  3-span.A2 (commSquare.sp bottomSquare) = A0
+  3-span.A4 (commSquare.sp bottomSquare) = P
+  3-span.f1 (commSquare.sp bottomSquare) = f
+  3-span.f3 (commSquare.sp bottomSquare) = inlP
+  commSquare.P bottomSquare = B
+  commSquare.inlP bottomSquare = g
+  commSquare.inrP bottomSquare = h
+  commSquare.comm bottomSquare = com
+
+  totSquare : commSquare
+  3-span.A0 (commSquare.sp totSquare) = A
+  3-span.A2 (commSquare.sp totSquare) = A2
+  3-span.A4 (commSquare.sp totSquare) = A4
+  3-span.f1 (commSquare.sp totSquare) = f ∘ f1
+  3-span.f3 (commSquare.sp totSquare) = f3
+  commSquare.P totSquare = B
+  commSquare.inlP totSquare = g
+  commSquare.inrP totSquare = h ∘ inrP
+  commSquare.comm totSquare =
+    funExt λ x → funExt⁻ com (f1 x) ∙ cong h (funExt⁻ comm x)
+
+  private
+    P' : Type _
+    P' = Pushout f1 f3
+
+    Iso-P'-P : P' ≃ P
+    Iso-P'-P = _ , isP
+
+    P'≃P = equiv→HAEquiv Iso-P'-P
+
+    B'bot = Pushout {C = P'} f inl
+
+    B'bot→BBot : B'bot → Pushout {C = P} f inlP
+    B'bot→BBot (inl x) = inl x
+    B'bot→BBot (inr x) = inr (fst Iso-P'-P x)
+    B'bot→BBot (push a i) = push a i
+
+    Bbot→B'bot : Pushout {C = P} f inlP → B'bot
+    Bbot→B'bot (inl x) = inl x
+    Bbot→B'bot (inr x) = inr (invEq Iso-P'-P x)
+    Bbot→B'bot (push a i) =
+      (push a ∙ λ i → inr (isHAEquiv.linv (P'≃P .snd) (inl a) (~ i))) i
+
+    Iso-B'bot-Bbot : Iso B'bot (Pushout {C = P} f inlP)
+    fun Iso-B'bot-Bbot = B'bot→BBot
+    inv Iso-B'bot-Bbot = Bbot→B'bot
+    rightInv Iso-B'bot-Bbot (inl x) = refl
+    rightInv Iso-B'bot-Bbot (inr x) i = inr (isHAEquiv.rinv (P'≃P .snd) x i)
+    rightInv Iso-B'bot-Bbot (push a i) j = help j i
+      where
+      help : Square
+               (cong B'bot→BBot
+                (push a ∙ λ i → inr (isHAEquiv.linv (P'≃P .snd) (inl a) (~ i))))
+               (push a)
+               refl
+               λ i → inr (isHAEquiv.rinv (P'≃P .snd) (inlP a) i)
+      help = flipSquare ((λ i j → B'bot→BBot (compPath-filler (push a)
+              (λ i → inr (isHAEquiv.linv (P'≃P .snd) (inl a) (~ i))) (~ j) i))
+           ▷ λ j i → inr (isHAEquiv.com (P'≃P .snd) (inl a) j i))
+    leftInv Iso-B'bot-Bbot (inl x) = refl
+    leftInv Iso-B'bot-Bbot (inr x) i = inr (isHAEquiv.linv (P'≃P .snd) x i)
+    leftInv Iso-B'bot-Bbot (push a i) j =
+      compPath-filler (push a)
+        (λ i → inr (isHAEquiv.linv (P'≃P .snd) (inl a) (~ i))) (~ j) i
+
+    B'tot : Type _
+    B'tot = Pushout (f ∘ f1) f3
+
+    B'bot→B'tot : B'bot → B'tot
+    B'bot→B'tot (inl x) = inl x
+    B'bot→B'tot (inr (inl x)) = inl (f x)
+    B'bot→B'tot (inr (inr x)) = inr x
+    B'bot→B'tot (inr (push a i)) = push a i
+    B'bot→B'tot (push a i) = inl (f a)
+
+    B'tot→B'bot : B'tot → B'bot
+    B'tot→B'bot (inl x) = inl x
+    B'tot→B'bot (inr x) = inr (inr x)
+    B'tot→B'bot (push a i) = (push (f1 a) ∙ λ i → inr (push a i)) i
+
+    Iso-B'bot→B'tot : Iso B'bot B'tot
+    Iso.fun Iso-B'bot→B'tot = B'bot→B'tot
+    Iso.inv Iso-B'bot→B'tot = B'tot→B'bot
+    Iso.rightInv Iso-B'bot→B'tot (inl x) = refl
+    Iso.rightInv Iso-B'bot→B'tot (inr x) = refl
+    Iso.rightInv Iso-B'bot→B'tot (push a i) j =
+       (cong-∙ B'bot→B'tot (push (f1 a)) (λ i → inr (push a i))
+      ∙ sym (lUnit _)) j i
+    Iso.leftInv Iso-B'bot→B'tot (inl x) = refl
+    Iso.leftInv Iso-B'bot→B'tot (inr (inl x)) = push x
+    Iso.leftInv Iso-B'bot→B'tot (inr (inr x)) = refl
+    Iso.leftInv Iso-B'bot→B'tot (inr (push a i)) j =
+      compPath-filler' (push (f1 a)) (λ i → inr (push a i)) (~ j) i
+    Iso.leftInv Iso-B'bot→B'tot (push a i) j = push a (i ∧ j)
+
+    main' : Iso (spanPushout (commSquare.sp bottomSquare)) B'tot
+    main' = compIso (invIso Iso-B'bot-Bbot) (Iso-B'bot→B'tot)
+
+    mainInv∘ : (x : _) → Pushout→commSquare bottomSquare (main' .inv x)
+                        ≡ Pushout→commSquare totSquare x
+    mainInv∘ (inl x) = refl
+    mainInv∘ (inr x) = refl
+    mainInv∘ (push a i) j = help j i
+      where
+      help : cong (Pushout→commSquare bottomSquare)
+                  (cong (Iso.fun Iso-B'bot-Bbot) (push (f1 a) ∙ (λ i → inr (push a i))))
+          ≡ funExt⁻ com (f1 a) ∙ cong h (funExt⁻ comm a)
+      help = cong (cong (Pushout→commSquare bottomSquare))
+                  (cong-∙ (Iso.fun Iso-B'bot-Bbot) (push (f1 a)) (λ i → inr (push a i)))
+                ∙ cong-∙ (Pushout→commSquare bottomSquare)
+                         (push (3-span.f1 (commSquare.sp sq) a))
+                         (λ i → inr (commSquare.comm sq i a))
+
+  isPushoutBottomSquare→isPushoutTotSquare :
+    isPushoutSquare bottomSquare → isPushoutSquare totSquare
+  isPushoutBottomSquare→isPushoutTotSquare eq =
+    subst isEquiv (funExt mainInv∘) (isoToEquiv main .snd)
+    where
+    main : Iso (spanPushout (commSquare.sp totSquare)) B
+    main = compIso (invIso main') (equivToIso (_ , eq))
+
+  isPushoutTotSquare→isPushoutBottomSquare :
+    isPushoutSquare totSquare → isPushoutSquare bottomSquare
+  isPushoutTotSquare→isPushoutBottomSquare eq =
+    subst isEquiv (funExt coh)
+      (snd (isoToEquiv main))
+    where
+
+    main : Iso (spanPushout (commSquare.sp bottomSquare)) B
+    main = compIso
+            (compIso (invIso Iso-B'bot-Bbot) (Iso-B'bot→B'tot))
+            (equivToIso (_ , eq))
+
+    coh : (x : spanPushout (commSquare.sp bottomSquare)) →
+          main .fun x ≡ Pushout→commSquare bottomSquare x
+    coh x = sym (secEq (_ , eq) (fun main x))
+      ∙∙ sym (mainInv∘ (invEq (_ , eq) (Iso.fun main x)))
+      ∙∙ cong (Pushout→commSquare bottomSquare) (Iso.leftInv main x)
+
+-- Pushout pasting lemma, alternative version:
+{- Given a diagram consisting of two
+commuting squares where the left square is a pushout:
+
+A2 -—f3-→ A4 -—-f--→ A
+ ∣           ∣          ∣
+f1         inrP        g
+ ↓       ⌜  ↓          ↓
+A0 -—inlP→ P -—-h--→ B
+
+The right square is a pushout square iff the outer rectangle is
+a pushout square.
+-}
+module PushoutPasteLeft {ℓ₀ ℓ₂ ℓ₄ ℓP ℓA ℓB : Level}
+  (SQ : PushoutSquare {ℓ₀} {ℓ₂} {ℓ₄} {ℓP})
+  {A : Type ℓA} {B : Type ℓB}
+  (f : 3-span.A4 (commSquare.sp (fst SQ)) → A)
+  (g : A → B) (h : commSquare.P (fst SQ) → B)
+  (com : h ∘ commSquare.inrP (fst SQ) ≡ g ∘ f)
+  where
+
+  private
+    sq = fst SQ
+    isP = snd SQ
+    ℓ* = ℓ-maxList (ℓ₀ ∷ ℓ₂ ∷ ℓ₄ ∷ ℓP ∷ [])
+
+  open commSquare sq
+  open 3-span sp
+
+  rightSquare : commSquare
+  3-span.A0 (commSquare.sp rightSquare) = P
+  3-span.A2 (commSquare.sp rightSquare) = A4
+  3-span.A4 (commSquare.sp rightSquare) = A
+  3-span.f1 (commSquare.sp rightSquare) = inrP
+  3-span.f3 (commSquare.sp rightSquare) = f
+  commSquare.P rightSquare = B
+  commSquare.inlP rightSquare = h
+  commSquare.inrP rightSquare = g
+  commSquare.comm rightSquare = com
+
+  totSquare : commSquare
+  3-span.A0 (commSquare.sp totSquare) = A0
+  3-span.A2 (commSquare.sp totSquare) = A2
+  3-span.A4 (commSquare.sp totSquare) = A
+  3-span.f1 (commSquare.sp totSquare) = f1
+  3-span.f3 (commSquare.sp totSquare) = f ∘ f3
+  commSquare.P totSquare = B
+  commSquare.inlP totSquare = h ∘ inlP
+  commSquare.inrP totSquare = g
+  commSquare.comm totSquare = funExt λ x →
+    sym (sym (funExt⁻ com (f3 x)) ∙ cong h (sym (funExt⁻ comm x)))
+
+
+  module M = PushoutPasteDown (rotatePushoutSquare SQ) f g h (sym com)
+
+  isPushoutRightSquare→isPushoutTotSquare :
+    isPushoutSquare rightSquare → isPushoutSquare totSquare
+  isPushoutRightSquare→isPushoutTotSquare e = rotatePushoutSquare (_ , help) .snd
+    where
+    help : isPushoutSquare M.totSquare
+    help = M.isPushoutBottomSquare→isPushoutTotSquare (rotatePushoutSquare (_ , e) .snd)
+
+  isPushoutTotSquare→isPushoutRightSquare :
+    isPushoutSquare totSquare → isPushoutSquare rightSquare
+  isPushoutTotSquare→isPushoutRightSquare e = rotatePushoutSquare (_ , help) .snd
+    where
+    help = M.isPushoutTotSquare→isPushoutBottomSquare (rotatePushoutSquare (_ , e) .snd)
diff --git a/Cubical/HITs/SequentialColimit/Properties.agda b/Cubical/HITs/SequentialColimit/Properties.agda
index 6f2fa6a5a5..f9cfdb8e29 100644
--- a/Cubical/HITs/SequentialColimit/Properties.agda
+++ b/Cubical/HITs/SequentialColimit/Properties.agda
@@ -17,10 +17,12 @@ open import Cubical.Foundations.Function
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Transport
 
 open import Cubical.Data.Nat hiding (elim)
 open import Cubical.Data.Sequence
 open import Cubical.Data.Fin.Inductive
+open import Cubical.Data.Sigma
 
 open import Cubical.HITs.SequentialColimit.Base
 open import Cubical.Homotopy.Connected
@@ -410,7 +412,8 @@ realiseCompSequenceMap {C = C} {E = E} g f =
                 (push {n = n} (g₁ (f₁ x))
                 ∙ cong incl (SequenceMap.comm g n (f₁ x)
                            ∙ cong g₊ (SequenceMap.comm f n x)))
-                (cong (realiseSequenceMap g) (push (f₁ x) ∙ cong incl (SequenceMap.comm f n x)))
+                (cong (realiseSequenceMap g)
+                  (push (f₁ x) ∙ cong incl (SequenceMap.comm f n x)))
     main = cong (push (SequenceMap.map g n (f₁ x)) ∙_)
                       (cong-∙ incl (SequenceMap.comm g n (f₁ x))
                                    (cong g₊ (SequenceMap.comm f n x)))
@@ -420,6 +423,34 @@ realiseCompSequenceMap {C = C} {E = E} g f =
       ∙ sym (cong-∙ (realiseSequenceMap g)
                     (push (f₁ x)) (cong incl (SequenceMap.comm f n x)))
 
+sequenceEquiv→ColimIso : {A B : Sequence ℓ}
+  → SequenceEquiv A B → Iso (SeqColim A) (SeqColim B)
+sequenceEquiv→ColimIso e = mainIso
+  where
+  main : {A : Sequence ℓ} (B : Sequence ℓ) (e : SequenceEquiv A B)
+    → section (realiseSequenceMap (fst e))
+               (realiseSequenceMap (fst (invSequenceEquiv e)))
+     × retract (realiseSequenceMap (fst e))
+               (realiseSequenceMap (fst (invSequenceEquiv e)))
+  main {A = A} = SequenceEquivJ>
+    ((λ x → (λ i → realiseIdSequenceMap {C = A} i
+                    (realiseSequenceMap (fst (invIdSequenceEquiv {A = A} i)) x))
+           ∙ funExt⁻ realiseIdSequenceMap x)
+   , λ x → (λ i → realiseSequenceMap (fst (invIdSequenceEquiv {A = A} i))
+                      (realiseIdSequenceMap {C = A} i x))
+           ∙ funExt⁻ realiseIdSequenceMap x)
+
+  mainIso : Iso _ _
+  Iso.fun mainIso = realiseSequenceMap (fst e)
+  Iso.inv mainIso = realiseSequenceMap (fst (invSequenceEquiv e))
+  Iso.rightInv mainIso = main _ e .fst
+  Iso.leftInv mainIso = main _ e .snd
+
+sequenceIso→ColimIso : {A B : Sequence ℓ}
+  → SequenceIso A B → Iso (SeqColim A) (SeqColim B)
+sequenceIso→ColimIso e =
+  sequenceEquiv→ColimIso (SequenceIso→SequenceEquiv e)
+
 converges→funId : {seq1 : Sequence ℓ} {seq2 : Sequence ℓ'}
   (n m : ℕ)
   → converges seq1 n
@@ -512,3 +543,73 @@ Iso.leftInv (Iso-FinSeqColim-Top X m) r =
   (transport (λ i → (x : isoToPath (invIso (Iso-FinSeqColim-Top X m)) i)
     → f (ua-unglue (isoToEquiv (invIso (Iso-FinSeqColim-Top X m))) i x)
      ≡ g (ua-unglue (isoToEquiv (invIso (Iso-FinSeqColim-Top X m))) i x)) h)
+
+
+-- Shifting colimits
+Iso-SeqColim→SeqColimSuc : (X : Sequence ℓ)
+  → Iso (SeqColim X) (SeqColim (ShiftSeq X))
+Iso-SeqColim→SeqColimSuc X = iso G F F→G→F G→F→G
+  where
+  F : SeqColim (ShiftSeq X) → SeqColim X
+  F (incl {n = n} x) = incl {n = suc n} x
+  F (push {n = n} x i) = push {n = suc n} x i
+
+  G : SeqColim X → SeqColim (ShiftSeq X)
+  G (incl {n = zero} x) = incl {n = zero} (map X x)
+  G (incl {n = suc n} x) = incl {n = n} x
+  G (push {n = zero} x i) = incl {n = zero} (map X x)
+  G (push {n = suc n} x i) = push {n = n} x i
+
+  F→G→F : (x : SeqColim (ShiftSeq X)) → G (F x) ≡ x
+  F→G→F (incl x) = refl
+  F→G→F (push x i) = refl
+
+  G→F→G : (x : SeqColim X) → F (G x) ≡ x
+  G→F→G (incl {n = zero} x) = sym (push {n = zero} x)
+  G→F→G (incl {n = suc n} x) = refl
+  G→F→G (push {n = zero} x i) j = push {n = zero} x (i ∨ ~ j)
+  G→F→G (push {n = suc n} x i) = refl
+
+ShiftSequence+ : (S : Sequence ℓ) (n : ℕ) → Sequence ℓ
+Sequence.obj (ShiftSequence+ S n) m = Sequence.obj S (m + n)
+Sequence.map (ShiftSequence+ S n) {n = m} = Sequence.map S
+
+ShiftSequence+Rec : (S : Sequence ℓ) (n : ℕ) → Sequence ℓ
+ShiftSequence+Rec S zero = S
+ShiftSequence+Rec S (suc n) = ShiftSeq (ShiftSequence+Rec S n)
+
+Iso-SeqColim→SeqColimShift : (S : Sequence ℓ) (n : ℕ)
+  → Iso (SeqColim S) (SeqColim (ShiftSequence+Rec S n))
+Iso-SeqColim→SeqColimShift S zero = idIso
+Iso-SeqColim→SeqColimShift S (suc n) =
+  compIso (Iso-SeqColim→SeqColimShift S n)
+          (Iso-SeqColim→SeqColimSuc _)
+
+ShiftSequenceIso : {A : Sequence ℓ} (n : ℕ)
+  → SequenceIso (ShiftSequence+Rec A n) (ShiftSequence+ A n)
+fst (ShiftSequenceIso {A = A} zero) m =
+  pathToIso λ i → Sequence.obj A (+-comm zero m i)
+fst (ShiftSequenceIso {A = A} (suc n)) m =
+  compIso (fst (ShiftSequenceIso {A = A} n) (suc m))
+          (pathToIso λ i → Sequence.obj A (+-suc m n (~ i)))
+snd (ShiftSequenceIso {A = A} zero) m a =
+  sym (substCommSlice (Sequence.obj A) (Sequence.obj A ∘ suc)
+                        (λ _ → Sequence.map A)
+                        (+-comm zero m) a)
+  ∙ λ t → subst (Sequence.obj A)
+             (lUnit (cong suc (+-comm zero m)) t)
+             (Sequence.map A a)
+snd (ShiftSequenceIso {A = A} (suc n)) m a =
+    sym (substCommSlice (Sequence.obj A) (Sequence.obj A ∘ suc)
+                        (λ _ → Sequence.map A)
+                        (λ i → (+-suc m n (~ i)))
+                        (Iso.fun (fst (ShiftSequenceIso n) (suc m)) a))
+  ∙ cong (subst (λ x → Sequence.obj A (suc x)) (sym (+-suc m n)))
+         (snd (ShiftSequenceIso {A = A} n) (suc m) a)
+
+SeqColimIso : (S : Sequence ℓ) (n : ℕ)
+  → Iso (SeqColim S) (SeqColim (ShiftSequence+ S n))
+SeqColimIso S n =
+  compIso (Iso-SeqColim→SeqColimShift S n)
+    (sequenceEquiv→ColimIso
+      (SequenceIso→SequenceEquiv (ShiftSequenceIso n)))
diff --git a/Cubical/HITs/SphereBouquet/Properties.agda b/Cubical/HITs/SphereBouquet/Properties.agda
index 8c0284f731..5c0c4bebf1 100644
--- a/Cubical/HITs/SphereBouquet/Properties.agda
+++ b/Cubical/HITs/SphereBouquet/Properties.agda
@@ -10,6 +10,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
 
 open import Cubical.Data.Bool
 open import Cubical.Data.Nat renaming (_+_ to _+ℕ_)
@@ -22,9 +23,12 @@ open import Cubical.HITs.Sn
 open import Cubical.HITs.Pushout
 open import Cubical.HITs.Susp
 open import Cubical.HITs.PropositionalTruncation as PT
+open import Cubical.HITs.Truncation as TR
 open import Cubical.HITs.Wedge
 open import Cubical.HITs.SphereBouquet.Base
 
+open import Cubical.Homotopy.Connected
+
 private
   variable
     ℓ ℓ' : Level
@@ -54,6 +58,24 @@ isConnectedSphereBouquet {n = n} {A} =
   (λ (a , s) → sphereToPropElim n {A = λ x → ∥ inr (a , x) ≡ inl tt ∥₁}
                                   (λ x → squash₁) ∣ sym (push a) ∣₁ s)
 
+isConnectedSphereBouquet' : {n : ℕ} {A : Type ℓ}
+  → isConnected (suc (suc n)) (SphereBouquet (suc n) A)
+fst (isConnectedSphereBouquet' {n = n}) = ∣ inl tt ∣
+snd (isConnectedSphereBouquet' {n = n} {A = A}) =
+  TR.elim (λ _ → isOfHLevelPath (suc (suc n))
+                   (isOfHLevelTrunc (suc (suc n))) _ _) (lem n)
+  where
+  lem : (n : ℕ) → (a : SphereBouquet (suc n) A)
+    → Path (hLevelTrunc (suc (suc n)) (SphereBouquet (suc n) A))
+            ∣ inl tt ∣ ∣ a ∣
+  lem n (inl x) = refl
+  lem n (inr (x , y)) =
+    sphereElim n {A = λ y → ∣ inl tt ∣ ≡ ∣ inr (x , y) ∣}
+      (λ _ → isOfHLevelTrunc (suc (suc n)) _ _)
+      (cong ∣_∣ₕ (push x)) y
+  lem zero (push a i) j = ∣ push a (i ∧ j) ∣ₕ
+  lem (suc n) (push a i) j = ∣ push a (i ∧ j) ∣ₕ
+
 sphereBouquetSuspIso₀ : {A : Type ℓ}
   → Iso (⋁gen A (λ a → Susp∙ (fst (S₊∙ zero))))
       (SphereBouquet 1 A)
@@ -74,6 +96,22 @@ Iso.leftInv sphereBouquetSuspIso₀ (inr (a , y)) i =
   inr (a , Iso.rightInv (IsoSucSphereSusp 0) y i)
 Iso.leftInv sphereBouquetSuspIso₀ (push a i) = refl
 
+SphereBouquet₀Iso : (n : ℕ)
+  → Iso (SphereBouquet zero (Fin n))
+         (Fin (suc n))
+Iso.fun (SphereBouquet₀Iso n) (inl x) = fzero
+Iso.fun (SphereBouquet₀Iso n) (inr ((x , p) , false)) = suc x , p
+Iso.fun (SphereBouquet₀Iso n) (inr ((x , p) , true)) = fzero
+Iso.fun (SphereBouquet₀Iso n) (push a i) = fzero
+Iso.inv (SphereBouquet₀Iso n) (zero , p) = inl tt
+Iso.inv (SphereBouquet₀Iso n) (suc x , p) = inr ((x , p) , false)
+Iso.rightInv (SphereBouquet₀Iso n) (zero , p) = refl
+Iso.rightInv (SphereBouquet₀Iso n) (suc x , p) = refl
+Iso.leftInv (SphereBouquet₀Iso n) (inl x) = refl
+Iso.leftInv (SphereBouquet₀Iso n) (inr (x , false)) = refl
+Iso.leftInv (SphereBouquet₀Iso n) (inr (x , true)) = push x
+Iso.leftInv (SphereBouquet₀Iso n) (push a i) j = push a (i ∧ j)
+
 --a sphere bouquet is the wedge sum of A n-dimensional spheres
 sphereBouquetSuspIso : {A : Type ℓ} {n : ℕ}
   → Iso (Susp (SphereBouquet n A)) (SphereBouquet (suc n) A)
diff --git a/Cubical/HITs/Wedge/Properties.agda b/Cubical/HITs/Wedge/Properties.agda
index 5073e6316d..c357e94d00 100644
--- a/Cubical/HITs/Wedge/Properties.agda
+++ b/Cubical/HITs/Wedge/Properties.agda
@@ -6,20 +6,148 @@ open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
 
 open import Cubical.Data.Sigma
 open import Cubical.Data.Unit
+open import Cubical.Data.Sum as ⊎
 
 open import Cubical.HITs.Pushout.Base
 open import Cubical.HITs.Wedge.Base
 open import Cubical.HITs.Susp
+open import Cubical.HITs.Pushout
 
 open import Cubical.Homotopy.Loopspace
 
 
 private
   variable
-    ℓ ℓ' : Level
+    ℓ ℓ' ℓ'' : Level
+
+-- commutativity
+⋁-commFun : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → A ⋁ B → B ⋁ A
+⋁-commFun (inl x) = inr x
+⋁-commFun (inr x) = inl x
+⋁-commFun (push a i) = push a (~ i)
+
+⋁-commFun² : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → (x : A ⋁ B) → ⋁-commFun (⋁-commFun x) ≡ x
+⋁-commFun² (inl x) = refl
+⋁-commFun² (inr x) = refl
+⋁-commFun² (push a i) = refl
+
+⋁-commIso : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → Iso (A ⋁ B) (B ⋁ A)
+Iso.fun ⋁-commIso = ⋁-commFun
+Iso.inv ⋁-commIso = ⋁-commFun
+Iso.rightInv ⋁-commIso = ⋁-commFun²
+Iso.leftInv ⋁-commIso = ⋁-commFun²
+
+-- cofibre of A --inl→ A ⋁ B is B
+cofibInl-⋁ : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → Iso (cofib {B = A ⋁ B} inl) (fst B)
+Iso.fun (cofibInl-⋁ {B = B}) (inl x) = pt B
+Iso.fun (cofibInl-⋁ {B = B}) (inr (inl x)) = pt B
+Iso.fun cofibInl-⋁ (inr (inr x)) = x
+Iso.fun (cofibInl-⋁ {B = B}) (inr (push a i)) = pt B
+Iso.fun (cofibInl-⋁ {B = B}) (push a i) = pt B
+Iso.inv cofibInl-⋁ x = inr (inr x)
+Iso.rightInv cofibInl-⋁ x = refl
+Iso.leftInv (cofibInl-⋁ {A = A}) (inl x) =
+  (λ i → inr (push tt (~ i))) ∙ sym (push (pt A))
+Iso.leftInv (cofibInl-⋁ {A = A}) (inr (inl x)) =
+  ((λ i → inr (push tt (~ i))) ∙ sym (push (pt A))) ∙ push x
+Iso.leftInv cofibInl-⋁ (inr (inr x)) = refl
+Iso.leftInv (cofibInl-⋁ {A = A}) (inr (push a i)) j =
+  help (λ i → inr (push tt (~ i))) (sym (push (pt A))) (~ i) j
+  where
+  help : ∀ {ℓ} {A : Type ℓ} {x y z : A} (p : x ≡ y) (q : y ≡ z)
+    → Square refl ((p ∙ q) ∙ sym q) refl p
+  help p q =
+    (λ i j → p (i ∧ j))
+    ▷ (rUnit p
+    ∙∙ cong (p ∙_) (sym (rCancel q))
+    ∙∙ assoc p q (sym q))
+Iso.leftInv (cofibInl-⋁ {A = A}) (push a i) j =
+  compPath-filler
+    ((λ i → inr (push tt (~ i))) ∙ sym (push (pt A)))
+    (push a) i j
+
+-- cofibre of B --inl→ A ⋁ B is A
+cofibInr-⋁ : {A : Pointed ℓ} {B : Pointed ℓ'}
+  → Iso (cofib {B = A ⋁ B} inr) (fst A)
+cofibInr-⋁ {A = A} {B = B} =
+  compIso (pushoutIso _ _ _ _
+            (idEquiv _)
+            (idEquiv Unit)
+            (isoToEquiv ⋁-commIso)
+            refl refl)
+          (cofibInl-⋁ {A = B} {B = A})
+
+-- A ⋁ Unit ≃ A ≃ Unit ⋁ A
+⋁-rUnitIso : {A : Pointed ℓ} → Iso (A ⋁ Unit*∙ {ℓ'}) (fst A)
+Iso.fun ⋁-rUnitIso (inl x) = x
+Iso.fun (⋁-rUnitIso {A = A}) (inr x) = pt A
+Iso.fun (⋁-rUnitIso {A = A}) (push a i) = pt A
+Iso.inv ⋁-rUnitIso = inl
+Iso.rightInv ⋁-rUnitIso x = refl
+Iso.leftInv ⋁-rUnitIso (inl x) = refl
+Iso.leftInv ⋁-rUnitIso (inr x) = push tt
+Iso.leftInv ⋁-rUnitIso (push tt i) j = push tt (i ∧ j)
+
+⋁-lUnitIso : {A : Pointed ℓ} → Iso (Unit*∙ {ℓ'} ⋁ A) (fst A)
+⋁-lUnitIso = compIso ⋁-commIso ⋁-rUnitIso
+
+-- cofiber of constant function
+module _ {A : Pointed ℓ} {B : Pointed ℓ'} where
+  cofibConst→⋁ : cofib (const∙ A B .fst) → Susp∙ (fst A) ⋁ B
+  cofibConst→⋁ (inl x) = inl north
+  cofibConst→⋁ (inr x) = inr x
+  cofibConst→⋁ (push a i) = ((λ i → inl (toSusp A a i)) ∙ push tt) i
+
+  ⋁→cofibConst : Susp∙ (fst A) ⋁ B → cofib (const∙ A B .fst)
+  ⋁→cofibConst (inl north) = inl tt
+  ⋁→cofibConst (inl south) = inr (pt B)
+  ⋁→cofibConst (inl (merid a i)) = push a i
+  ⋁→cofibConst (inr x) = inr x
+  ⋁→cofibConst (push a i) = push (pt A) i
+
+  cofibConst-⋁-Iso : Iso (cofib (const∙ A B .fst))
+                     (Susp∙ (fst A) ⋁ B)
+  Iso.fun cofibConst-⋁-Iso = cofibConst→⋁
+  Iso.inv cofibConst-⋁-Iso = ⋁→cofibConst
+  Iso.rightInv cofibConst-⋁-Iso (inl north) = refl
+  Iso.rightInv cofibConst-⋁-Iso (inl south) =
+    sym (push tt) ∙ λ i → inl (merid (pt A) i)
+  Iso.rightInv cofibConst-⋁-Iso (inl (merid a i)) j =
+    hcomp (λ k →
+      λ {(i = i0) → inl (compPath-filler (merid a) (sym (merid (pt A))) (~ j) (~ k))
+       ; (i = i1) → (sym (push tt) ∙ λ i → inl (merid (pt A) i)) j
+       ; (j = i0) → compPath-filler' (λ i → inl (toSusp A a i)) (push tt) k i
+       ; (j = i1) → inl (merid a (~ k ∨ i))})
+    (compPath-filler' (sym (push tt)) (λ i → inl (merid (pt A) i)) i j)
+  Iso.rightInv cofibConst-⋁-Iso (inr x) = refl
+  Iso.rightInv cofibConst-⋁-Iso (push tt i) j =
+      (cong (_∙ push tt) (λ i j  → inl (rCancel (merid (pt A)) i j))
+    ∙ sym (lUnit _)) j i
+  Iso.leftInv cofibConst-⋁-Iso (inl x) = refl
+  Iso.leftInv cofibConst-⋁-Iso (inr x) = refl
+  Iso.leftInv cofibConst-⋁-Iso (push a i) j = help j i
+    where
+    help : cong ⋁→cofibConst (((λ i → inl (toSusp A a i)) ∙ push tt)) ≡ push a
+    help = cong-∙ ⋁→cofibConst (λ i → inl (toSusp A a i)) (push tt)
+         ∙ cong₂ _∙_ (cong-∙ (⋁→cofibConst ∘ inl) (merid a) (sym (merid (pt A)))) refl
+         ∙ sym (assoc _ _ _)
+         ∙ cong (push a ∙_) (lCancel (push (pt A)))
+         ∙ sym (rUnit _)
+
+  cofibConst-⋁-Iso' : (f : A →∙ B) → ((x : fst A) → fst f x ≡ pt B)
+              → Iso (cofib (fst f)) ((Susp∙ (fst A) ⋁ B))
+  cofibConst-⋁-Iso' f d =
+    compIso (pushoutIso _ _ _ _
+              (idEquiv _) (idEquiv _) (idEquiv _) refl (funExt d))
+            cofibConst-⋁-Iso
 
 -- Susp (⋁ᵢ Aᵢ) ≃ ⋁ᵢ (Susp Aᵢ)
 private
@@ -165,3 +293,258 @@ Iso.leftInv (Iso-SuspBouquet-Bouquet A B) = SuspBouquet-Bouquet-cancel A B .snd
 SuspBouquet≃Bouquet : (A : Type ℓ) (B : A → Pointed ℓ')
   → Susp (⋁gen A B) ≃ ⋁gen A (λ a → Susp∙ (fst (B a)))
 SuspBouquet≃Bouquet A B = isoToEquiv (Iso-SuspBouquet-Bouquet A B)
+
+-- cofibre of f ∨→ g : A ⋁ B → C is cofibre of
+-- inr ∘ f : A → cofib g
+module _ {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+  (f : A →∙ C) (g : B →∙ C)
+  where
+  private
+    inst : 3x3-span
+    3x3-span.A00 inst = Unit
+    3x3-span.A02 inst = Unit
+    3x3-span.A04 inst = Unit
+    3x3-span.A20 inst = fst A
+    3x3-span.A22 inst = Unit
+    3x3-span.A24 inst = fst B
+    3x3-span.A40 inst = fst C
+    3x3-span.A42 inst = fst C
+    3x3-span.A44 inst = fst C
+    3x3-span.f10 inst = _
+    3x3-span.f12 inst = _
+    3x3-span.f14 inst = _
+    3x3-span.f30 inst = fst f
+    3x3-span.f32 inst = λ _ → pt C
+    3x3-span.f34 inst = fst g
+    3x3-span.f01 inst = _
+    3x3-span.f21 inst = λ _ → pt A
+    3x3-span.f41 inst = λ c → c
+    3x3-span.f03 inst = _
+    3x3-span.f23 inst = λ _ → pt B
+    3x3-span.f43 inst = λ c → c
+    3x3-span.H11 inst = λ _ → refl
+    3x3-span.H13 inst = λ _ → refl
+    3x3-span.H31 inst = λ _ → sym (snd f)
+    3x3-span.H33 inst = λ _ → sym (snd g)
+
+    open 3x3-span inst
+
+    A□2≅C : A□2 ≃ (fst C)
+    A□2≅C = isoToEquiv (PushoutAlongEquiv (idEquiv _) λ _ → pt C)
+
+    A□○≅ : Iso (Pushout {B = cofib (fst f)} {C = cofib (fst g)} inr inr) A□○
+    A□○≅ =
+      pushoutIso _ _ _ _ (invEquiv A□2≅C) (idEquiv _) (idEquiv _)
+             refl
+             refl
+
+    A0□≅ : A0□ ≃ Unit
+    A0□≅ = isoToEquiv (PushoutAlongEquiv (idEquiv _) _)
+
+    A4□≅ : A4□ ≃ fst C
+    A4□≅ = isoToEquiv (PushoutAlongEquiv (idEquiv _) _)
+
+    A○□≅ : Iso A○□ (cofib (f ∨→ g))
+    A○□≅ = pushoutIso _ _ _ _ (idEquiv _) A0□≅ A4□≅ refl
+      (funExt λ { (inl x) → refl
+                ; (inr x) → refl
+                ; (push tt i) j → help j i})
+      where
+      help : cong (fst A4□≅) (cong f3□ (push tt)) ≡ snd f ∙ sym (snd g)
+      help = cong-∙∙ (fst A4□≅) (λ i → inl (snd f i))
+                           refl (λ i → inl (snd g (~ i)))
+           ∙ doubleCompPath≡compPath _ _ _
+           ∙ cong (snd f ∙_) (sym (lUnit _))
+
+
+    cofibf-Square : commSquare
+    3-span.A0 (commSquare.sp cofibf-Square) = Unit
+    3-span.A2 (commSquare.sp cofibf-Square) = fst A
+    3-span.A4 (commSquare.sp cofibf-Square) = fst C
+    3-span.f1 (commSquare.sp cofibf-Square) = _
+    3-span.f3 (commSquare.sp cofibf-Square) = fst f
+    commSquare.P cofibf-Square = cofib (fst f)
+    commSquare.inlP cofibf-Square = λ _ → inl tt
+    commSquare.inrP cofibf-Square = inr
+    commSquare.comm cofibf-Square i x = push x i
+
+    cofibf-PSquare : PushoutSquare
+    fst cofibf-PSquare = cofibf-Square
+    snd cofibf-PSquare =
+      subst isEquiv (funExt (λ { (inl x) → refl
+                               ; (inr x) → refl
+                               ; (push a i) → refl}))
+                     (idIsEquiv _)
+
+    F : cofib (fst f)
+      → cofib {B = cofib (fst g)} (λ x → inr (fst f x))
+    F (inl x) = inl tt
+    F (inr x) = inr (inr x)
+    F (push a i) = push a i
+
+    open PushoutPasteLeft
+          cofibf-PSquare
+            {B = cofib {B = cofib (fst g)} (λ x → inr (fst f x))}
+            inr inr F refl
+
+    isPushoutRight : isPushoutSquare rightSquare
+    isPushoutRight = isPushoutTotSquare→isPushoutRightSquare
+             (subst isEquiv
+               (funExt (λ { (inl x) → refl
+                          ; (inr x) → refl
+                          ; (push a i) j → lUnit (sym (push a)) j (~ i)}))
+               (idEquiv _ .snd))
+
+  cofib∨→distrIso :
+    Iso (cofib (f ∨→ g))
+        (Pushout {B = cofib (fst f)} {C = cofib (fst g)} inr inr)
+  cofib∨→distrIso = invIso (compIso (compIso A□○≅ 3x3-Iso) A○□≅)
+
+  cofib∨→compIsoᵣ : Iso (cofib (f ∨→ g))
+                        (cofib {B = cofib (fst g)} (λ x → inr (fst f x)))
+  cofib∨→compIsoᵣ = compIso cofib∨→distrIso (equivToIso (_ , isPushoutRight))
+
+-- cofibre of f ∨→ g : A ⋁ B → C is cofibre of
+-- inr ∘ g : B → cofib f
+cofib∨→compIsoₗ :
+  {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓ''}
+  (f : A →∙ C) (g : B →∙ C)
+    → Iso (cofib (f ∨→ g))
+           (cofib {B = cofib (fst f)} (λ x → inr (fst g x)))
+cofib∨→compIsoₗ f g =
+  compIso (pushoutIso _ _ _ _ (isoToEquiv ⋁-commIso)
+            (idEquiv _) (idEquiv _)
+            refl (funExt
+            λ { (inl x) → refl
+              ; (inr x) → refl
+              ; (push a i) j → symDistr (snd g) (sym (snd f)) (~ j) i}))
+          (cofib∨→compIsoᵣ g f)
+
+-- (⋁ᵢ Aᵢ ∨ ⋁ⱼ Bᵢ) ≃ ⋁ᵢ₊ⱼ(Aᵢ + Bⱼ)
+module _ {A : Type ℓ} {B : Type ℓ'}
+  {P : A → Pointed ℓ''} {Q : B → Pointed ℓ''}
+  where
+  private
+    ⋁gen⊎→ : ⋁gen∙ A P ⋁ ⋁gen∙ B Q
+            → ⋁gen (A ⊎ B) (⊎.rec P Q)
+    ⋁gen⊎→ (inl (inl x)) = inl tt
+    ⋁gen⊎→ (inl (inr (a , p))) = inr (inl a , p)
+    ⋁gen⊎→ (inl (push a i)) = push (inl a) i
+    ⋁gen⊎→ (inr (inl x)) = inl tt
+    ⋁gen⊎→ (inr (inr (b , q))) = inr (inr b , q)
+    ⋁gen⊎→ (inr (push b i)) = push (inr b) i
+    ⋁gen⊎→ (push a i) = inl tt
+
+    ⋁gen⊎← : ⋁gen (A ⊎ B) (⊎.rec P Q)
+            → ⋁gen∙ A P ⋁ ⋁gen∙ B Q
+    ⋁gen⊎← (inl x) = inl (inl tt)
+    ⋁gen⊎← (inr (inl x , p)) = inl (inr (x , p))
+    ⋁gen⊎← (inr (inr x , p)) = inr (inr (x , p))
+    ⋁gen⊎← (push (inl x) i) = inl (push x i)
+    ⋁gen⊎← (push (inr x) i) = (push tt ∙ λ i → inr (push x i)) i
+
+  ⋁gen⊎Iso : Iso (⋁gen∙ A P ⋁ ⋁gen∙ B Q)
+                  (⋁gen (A ⊎ B) (⊎.rec P Q))
+  Iso.fun ⋁gen⊎Iso = ⋁gen⊎→
+  Iso.inv ⋁gen⊎Iso = ⋁gen⊎←
+  Iso.rightInv ⋁gen⊎Iso (inl tt) = refl
+  Iso.rightInv ⋁gen⊎Iso (inr (inl x , p)) = refl
+  Iso.rightInv ⋁gen⊎Iso (inr (inr x , p)) = refl
+  Iso.rightInv ⋁gen⊎Iso (push (inl x) i) = refl
+  Iso.rightInv ⋁gen⊎Iso (push (inr x) i) j =
+    ⋁gen⊎→ (compPath-filler' (push tt) (λ i → inr (push x i)) (~ j) i)
+  Iso.leftInv ⋁gen⊎Iso (inl (inl x)) = refl
+  Iso.leftInv ⋁gen⊎Iso (inl (inr x)) = refl
+  Iso.leftInv ⋁gen⊎Iso (inl (push a i)) = refl
+  Iso.leftInv ⋁gen⊎Iso (inr (inl x)) = push tt
+  Iso.leftInv ⋁gen⊎Iso (inr (inr x)) = refl
+  Iso.leftInv ⋁gen⊎Iso (inr (push a i)) j =
+    compPath-filler' (push tt) (λ i → inr (push a i)) (~ j) i
+  Iso.leftInv ⋁gen⊎Iso (push a i) j = push a (i ∧ j)
+
+-- f : ⋁ₐ Bₐ → C has cofibre the pushout of cofib (f ∘ inr) ← Σₐ → A
+module _ {ℓA ℓB ℓC : Level} {A : Type ℓA} {B : A → Pointed ℓB} (C : Pointed ℓC)
+         (f : (⋁gen A B , inl tt) →∙ C) where
+  private
+    open 3x3-span
+    inst : 3x3-span
+    A00 inst = A
+    A02 inst = Σ A (fst ∘ B)
+    A04 inst = Σ A (fst ∘ B)
+    A20 inst = A
+    A22 inst = A
+    A24 inst = Σ A (fst ∘ B)
+    A40 inst = Unit
+    A42 inst = Unit
+    A44 inst = fst C
+    f10 inst = idfun A
+    f12 inst = λ x → x , snd (B x)
+    f14 inst = idfun _
+    f30 inst = λ _ → tt
+    f32 inst = λ _ → tt
+    f34 inst = fst f ∘ inr
+    f01 inst = fst
+    f21 inst = idfun A
+    f41 inst = λ _ → tt
+    f03 inst = idfun _
+    f23 inst = λ x → x , snd (B x)
+    f43 inst = λ _ → pt C
+    H11 inst = λ _ → refl
+    H13 inst = λ _ → refl
+    H31 inst = λ _ → refl
+    H33 inst = λ x → sym (snd f) ∙ cong (fst f) (push x)
+
+    A0□Iso : Iso (A0□ inst) A
+    A0□Iso = compIso (equivToIso (symPushout _ _))
+                     (PushoutAlongEquiv (idEquiv _) fst)
+
+    A2□Iso : Iso (A2□ inst) (Σ A (fst ∘ B))
+    A2□Iso = PushoutAlongEquiv (idEquiv A) _
+
+    A4□Iso : Iso (A4□ inst) (fst C)
+    A4□Iso = PushoutAlongEquiv (idEquiv Unit) λ _ → pt C
+
+    A○□Iso : Iso (A○□ inst) (Pushout (fst f ∘ inr) fst)
+    A○□Iso = compIso (equivToIso (symPushout _ _))
+                     (invIso (pushoutIso _ _ _ _
+                       (isoToEquiv (invIso A2□Iso))
+                       (isoToEquiv (invIso A4□Iso))
+                       (isoToEquiv (invIso A0□Iso))
+                       refl
+                       λ i x → push x i))
+
+    A□0Iso : Iso (A□0 inst) Unit
+    A□0Iso = isContr→Iso
+      (inr tt , λ { (inl x) → sym (push x)
+                  ; (inr x) → refl
+                  ; (push a i) j → push a (i ∨ ~ j)})
+      (tt , (λ _ → refl))
+
+    A□2Iso : Iso (A□2 inst) (⋁gen A B)
+    A□2Iso = equivToIso (symPushout _ _)
+
+    A□4Iso : Iso (A□4 inst) (fst C)
+    A□4Iso = PushoutAlongEquiv (idEquiv _) _
+
+    A□○Iso : Iso (A□○ inst) (cofib (fst f))
+    A□○Iso = invIso (pushoutIso _ _ _ _
+      (isoToEquiv (invIso A□2Iso))
+      (isoToEquiv (invIso A□0Iso))
+      (isoToEquiv (invIso A□4Iso))
+      (funExt (λ { (inl x) → refl
+                  ; (inr x) → sym (push (fst x)) ∙ refl
+                  ; (push a i) j → (sym (push a) ∙ refl) (i ∧ j)}))
+      (funExt λ { (inl x) i → inr (snd f i)
+                ; (inr x) → sym (push x)
+                ; (push a i) j
+                → hcomp (λ k
+                → (λ {(i = i0) → inr (compPath-filler' (sym (snd f))
+                                        (cong (fst f) (push a)) j (~ k))
+                     ; (i = i1) → push (a , snd (B a)) (~ j)
+                     ; (j = i0) → inr (fst f (push a (~ k ∨ i)))}))
+          (push (a , snd (B a)) (~ i ∨ ~ j))}))
+
+  ⋁-cofib-Iso : Iso (Pushout (fst f ∘ inr) fst) (cofib (fst f))
+  ⋁-cofib-Iso = compIso (compIso (invIso A○□Iso)
+                                  (invIso (3x3-Iso inst)))
+                                  A□○Iso
diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda
index 842e58ac3d..922a257fe4 100644
--- a/Cubical/Homotopy/Connected.agda
+++ b/Cubical/Homotopy/Connected.agda
@@ -62,6 +62,12 @@ isConnectedSubtr {A = A} n m iscon =
   helper zero iscon = isContrUnit*
   helper (suc n) iscon = ∣ iscon .fst ∣ , (Trunc.elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ a → cong ∣_∣ (iscon .snd a))
 
+isConnectedSubtr' : ∀ {ℓ} {A : Type ℓ} (n m : HLevel)
+                → isConnected (m + n) A
+                → isConnected m A
+isConnectedSubtr' {A = A} n m iscon =
+  isConnectedSubtr m n (subst (λ k → isConnected k A) (+-comm m n) iscon)
+
 isConnectedFunSubtr : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLevel) (f : A → B)
                 → isConnectedFun (m + n) f
                 → isConnectedFun n f
diff --git a/Cubical/Relation/Nullary/Properties.agda b/Cubical/Relation/Nullary/Properties.agda
index 77535b9c88..71150a5a8e 100644
--- a/Cubical/Relation/Nullary/Properties.agda
+++ b/Cubical/Relation/Nullary/Properties.agda
@@ -17,6 +17,7 @@ open import Cubical.Functions.Fixpoint
 
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma.Base using (_×_)
+open import Cubical.Data.Sum.Base
 
 open import Cubical.Relation.Nullary.Base
 open import Cubical.HITs.PropositionalTruncation.Base
@@ -205,3 +206,8 @@ Discrete→isSet = Separated→isSet ∘ Discrete→Separated
 ≡no : ∀ {A : Type ℓ} x y → Path (Dec A) x (no y)
 ≡no (yes p) y = ⊥.rec (y p)
 ≡no (no ¬p) y i = no (isProp¬ _ ¬p y i)
+
+inhabitedFibres? : ∀ {ℓ'} {A : Type ℓ} {B : Type ℓ'}
+  (f : A → B) → Type (ℓ-max ℓ ℓ')
+inhabitedFibres? {A = A} {B = B} f =
+  (y : B) → (Σ[ x ∈ A ] f x ≡ y) ⊎ ((x : A) → ¬ f x ≡ y)