SequentialColimits

Ian Ray, 21st Jun 2025.

We develop sequential colimits in HoTT/UF. This formalization follows Section 26
of Introduction to Homotopy Type Theory by Egbert Rijke (HoTTEST summer school
version:
https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/HoTT/hott-intro.pdf).


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

open import UF.FunExt

module UF.SequentialColimits (fe : Fun-Ext) where

open import MLTT.Spartan
open import UF.Base
open import UF.CoconesofSpans fe
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.PropIndexedPiSigma
open import UF.Pushouts fe
open import UF.Subsingletons
open import UF.Yoneda


A diagram of the following form

          a₀      a₁      a₂
     A₀ ----> A₁ ----> A₂ ----> ...

is a type sequence. We can give a formal specification as follows.


type-sequence : (𝓤 : Universe) → (𝓤 ⁺) ̇
type-sequence 𝓤 = Σ A ꞉ (ℕ → 𝓤 ̇) , ((n : ℕ) → A n → A (succ n))


A sequential cocone on a type sequence consists of a sequence of maps to a
specified type

          a₀      a₁      a₂
     A₀ ----> A₁ ----> A₂ ----> ...
      \       |        /
       \      |       /
    b₀  \     | b₁   / b₂ ...
         \    |     /
          \   |    /
           v  v   v
              B

such that every triangle commutes. Formally we can define this as
follows.


sequential-cocone : {𝓤 𝓥 : Universe}
                  → type-sequence 𝓤
                  → 𝓥 ̇
                  → 𝓤 ⊔ 𝓥 ̇ 
sequential-cocone (A , a) B
 = Σ b ꞉ ((n : ℕ) → A n → B) , ((n : ℕ) → b n ∼ b (succ n) ∘ a n)


We now characterize the identity type of sequential cocones.


module _ (𝓐@(A , a) : type-sequence 𝓤)
         (B : 𝓥 ̇)
       where

 sequential-cocone-identity : sequential-cocone 𝓐 B
                            → sequential-cocone 𝓐 B
                            → 𝓤 ⊔ 𝓥 ̇
 sequential-cocone-identity (s , S) (r , R)
  = Σ H ꞉ ((n : ℕ) → s n ∼ r n) ,
    ((n : ℕ) → ∼-trans (S n) (H (succ n) ∘ a n) ∼ ∼-trans (H n) (R n))

 id-to-sequential-cocone-family : (𝓑 𝓑' : sequential-cocone 𝓐 B)
                                → 𝓑 ＝ 𝓑'
                                → sequential-cocone-identity 𝓑 𝓑'
 id-to-sequential-cocone-family 𝓑 𝓑 refl
  = ((λ - → ∼-refl) , λ - → λ -' → refl-left-neutral ⁻¹)

 sequential-cocone-identity-is-identity-system
  : (𝓑 : sequential-cocone 𝓐 B)
  → is-contr (Σ 𝓑' ꞉ (sequential-cocone 𝓐 B) , sequential-cocone-identity 𝓑 𝓑')
 sequential-cocone-identity-is-identity-system (b , G)
  = equiv-to-singleton e 𝟙-is-singleton
  where
   e : (Σ 𝓑' ꞉ (sequential-cocone 𝓐 B) , sequential-cocone-identity (b , G) 𝓑')
     ≃ 𝟙 {𝓤 ⊔ 𝓥}
   e = (Σ 𝓑' ꞉ (sequential-cocone 𝓐 B) , sequential-cocone-identity (b , G) 𝓑')
                                                                        ≃⟨ I ⟩
       (Σ b' ꞉ ((n : ℕ) → A n → B) ,
        Σ G' ꞉ ((n : ℕ) → b' n ∼ b' (succ n) ∘ a n) ,
         Σ H ꞉ ((n : ℕ) → b n ∼ b' n) ,
          ((n : ℕ) → ∼-trans (G n) (H (succ n) ∘ a n) ∼ ∼-trans (H n) (G' n)))
                                                                        ≃⟨ II ⟩
       (Σ b' ꞉ ((n : ℕ) → A n → B) ,
        Σ H ꞉ ((n : ℕ) → b n ∼ b' n) ,
         Σ G' ꞉ ((n : ℕ) → b' n ∼ b' (succ n) ∘ a n) ,
          ((n : ℕ) → ∼-trans (G n) (H (succ n) ∘ a n) ∼ ∼-trans (H n) (G' n)))
                                                                        ≃⟨ III ⟩
       (Σ G' ꞉ ((n : ℕ) → b n ∼ b (succ n) ∘ a n) ,
        ((n : ℕ) → G n ∼ G' n))
                                                                        ≃⟨ IV ⟩
       𝟙                                                                ■
    where
     I = Σ-assoc
     II = Σ-cong (λ - → Σ-flip)
     III = (Σ b' ꞉ ((n : ℕ) → A n → B) ,
            Σ H ꞉ ((n : ℕ) → b n ∼ b' n) ,
             Σ G' ꞉ ((n : ℕ) → b' n ∼ b' (succ n) ∘ a n) ,
              ((n : ℕ) → ∼-trans (G n) (H (succ n) ∘ a n)
                       ∼ ∼-trans (H n) (G' n)))
                                                                       ≃⟨ V ⟩
           (Σ (b' , H) ꞉ (Σ b' ꞉ ((n : ℕ) → A n → B) , ((n : ℕ) → b n ∼ b' n)) ,
            (Σ G' ꞉ ((n : ℕ) → b' n ∼ b' (succ n) ∘ a n) ,
              ((n : ℕ) → ∼-trans (G n) (H (succ n) ∘ a n)
                       ∼ ∼-trans (H n) (G' n))))
                                                                       ≃⟨ VII ⟩
           (Σ G' ꞉ ((n : ℕ) → b n ∼ b (succ n) ∘ a n) ,
            ((n : ℕ) → ∼-trans (G n) ∼-refl ∼ ∼-trans ∼-refl (G' n)))
                                                                       ≃⟨ VIII ⟩
           (Σ G' ꞉ ((n : ℕ) → b n ∼ b (succ n) ∘ a n) , ((n : ℕ) → G n ∼ G' n))
                                                                       ■
      where
       V = ≃-sym Σ-assoc
       VI = (Σ b' ꞉ ((n : ℕ) → A n → B) , ((n : ℕ) → b n ∼ b' n)) ≃⟨ Σ-cong IX ⟩
            (Σ b' ꞉ ((n : ℕ) → A n → B) , b ＝ b')                ≃⟨ X ⟩
            𝟙                                                     ■
        where
         IX : (b' : (n : ℕ) → A n → B)
            → ((n : ℕ) → b n ∼ b' n) ≃ (b ＝ b')
         IX b' = ((n : ℕ) → b n ∼ b' n)
                                         ≃⟨ Π-cong fe fe
                                             (λ n → ≃-sym
                                              (≃-funext fe (b n) (b' n))) ⟩
                 ((n : ℕ) → b n ＝ b' n)
                                         ≃⟨ ≃-sym (≃-funext fe b b') ⟩
                 (b ＝ b')               ■
         X = singleton-≃-𝟙 {𝓤 ⊔ 𝓥} {𝓥} (singleton-types-are-singletons b)
       VII = prop-indexed-sum (b , (λ n → ∼-refl)) (equiv-to-prop VI 𝟙-is-prop)
       VIII = Σ-cong (λ G' → Π-cong fe fe
               (λ n → Π-cong fe fe
                (λ x → ＝-cong (G n x) (∼-trans (λ - → refl) (G' n) x)
                 refl refl-left-neutral)))
     IV = (Σ G' ꞉ ((n : ℕ) → b n ∼ b (succ n) ∘ a n) , ((n : ℕ) → G n ∼ G' n))
                                                                        ≃⟨ VI ⟩
          (Σ G' ꞉ ((n : ℕ) → b n ∼ b (succ n) ∘ a n) , G ＝ G')
                                                                        ≃⟨ VII ⟩
          𝟙                                                             ■
      where
       V : (G' : ((n : ℕ) → b n ∼ b (succ n) ∘ a n))
         → ((n : ℕ) → G n ∼ G' n) ≃ (G ＝ G')
       V G' = ((n : ℕ) → G n ∼ G' n)
                                      ≃⟨ Π-cong fe fe
                                          (λ n → ≃-sym
                                           (≃-funext fe (G n) (G' n))) ⟩
              ((n : ℕ) → G n ＝ G' n)
                                      ≃⟨ ≃-sym (≃-funext fe G G') ⟩
              (G ＝ G')               ■
       VI = Σ-cong V
       VII = singleton-≃-𝟙 (singleton-types-are-singletons G)

 sequential-cocone-identity-characterization
  : (𝓑 𝓑' : sequential-cocone 𝓐 B)
  → (𝓑 ＝ 𝓑') ≃ (sequential-cocone-identity 𝓑 𝓑')
 sequential-cocone-identity-characterization 𝓑 𝓑' =
  (id-to-sequential-cocone-family 𝓑 𝓑' ,
    Yoneda-Theorem-forth 𝓑 (id-to-sequential-cocone-family 𝓑)
     (sequential-cocone-identity-is-identity-system 𝓑) 𝓑')

 sequential-cocone-family-to-id : (𝓑 𝓑' : sequential-cocone 𝓐 B)
                                → (sequential-cocone-identity 𝓑 𝓑')
                                → 𝓑 ＝ 𝓑'
 sequential-cocone-family-to-id 𝓑 𝓑'
  = ⌜ sequential-cocone-identity-characterization 𝓑 𝓑' ⌝⁻¹


Given a sequential cocone over X and a map X → Y there is a canonical assignment
to a sequential cocone over Y.


module _ (𝓐 : type-sequence 𝓤)
         (X : 𝓥 ̇) (Y : 𝓣 ̇)
       where

 canonical-map-to-sequential-cocone : sequential-cocone 𝓐 X
                                    → (X → Y)
                                    → sequential-cocone 𝓐 Y
 canonical-map-to-sequential-cocone (h , H) u =
  ((λ n → u ∘ h n) , λ n → ∼-ap-∘ u (H n))


A sequential cocone over X is universal if the above map is an equivalence for
any Y. Such a sequential cocone is said to be the sequential colimit of a type
sequence.


 Sequential-Colimit-Universal-Property : (𝓧 : sequential-cocone 𝓐 X)
                                       → 𝓤 ⊔ 𝓥 ⊔ 𝓣 ̇
 Sequential-Colimit-Universal-Property 𝓧 =
  is-equiv (canonical-map-to-sequential-cocone 𝓧)


We now give a construction of the sequential colimit in terms of the pushout.
This construction follows 26.2 in Introduction to Homotopy Type Theory
(link above).

The sequential colimit A∞ can be constructed as the pushout of the following
diagram

                     [id , σ]
          Σ A + Σ A ------------> Σ A
              |                    |
   [id , id]  |                    | inrr
              |                    |
             Σ A ----------------> A∞
                       inll

where σ (n , x) = (n + 1 , a n x).


module _ (𝓐@(A , a) : type-sequence 𝓤)
         (X : 𝓣 ̇)
       where

 σ : Σ A → Σ A
 σ (n , x) = (succ n , a n x)

 f : Σ A + Σ A → Σ A
 f = cases id id

 g : Σ A + Σ A → Σ A
 g = cases id σ

 private
  index : Σ A → ℕ
  index = pr₁

  element-at : ((n , x) : Σ A) → A n
  element-at = pr₂

 module _ (push-ex : pushout-exists f g)
           where

  open pushout-exists push-ex

  sequential-colimit : 𝓤 ̇
  sequential-colimit = pushout


We provide the sequential cocone structure for the sequential colimit. 


  ι : (n : ℕ) → A n → sequential-colimit
  ι n x = inrr (n , x)

  seq-colim-homotopy : (n : ℕ) → ι n ∼ ι (succ n) ∘ a n
  seq-colim-homotopy n x = glue (inl (n , x)) ⁻¹ ∙ glue (inr (n , x))

  sequential-colimit-is-cocone : sequential-cocone 𝓐 sequential-colimit
  sequential-colimit-is-cocone = (ι , seq-colim-homotopy)


We will quickly provide names and a technical lemma that will prove useful
later.


  ap-on-glue : (u : sequential-colimit → X)
             → ((n , x) : Σ A)
             → ap u (seq-colim-homotopy n x)
             ＝ ap u (glue (inl (n , x))) ⁻¹ ∙ ap u (glue (inr (n , x)))
  ap-on-glue u (n , x)
   = ap u (seq-colim-homotopy n x)                             ＝⟨ I ⟩
     ap u (glue (inl (n , x)) ⁻¹) ∙ ap u (glue (inr (n , x)))  ＝⟨ II ⟩
     ap u (glue (inl (n , x))) ⁻¹ ∙ ap u (glue (inr (n , x)))  ∎
   where
    I = ap-∙ u (glue (inl (n , x)) ⁻¹) (glue (inr (n , x)))
    II = ap (_∙ ap u (glue (inr (n , x)))) (ap-sym u (glue (inl (n , x)))) ⁻¹


We show that cocones over the above pushout diagram are equivalent to sequential
cocones over the above type sequence. 


  gluing-from-sequential-cocone
   : ((b , H) : sequential-cocone 𝓐 X)
   → (c : Σ A + Σ A)
   → b (index (f c)) (element-at (f c)) ＝ b (index (g c)) (element-at (g c))
  gluing-from-sequential-cocone (b , H) (inl -) = refl
  gluing-from-sequential-cocone (b , H) (inr (n , x)) = H n x

  pushout-cocone-to-seq-cocone : cocone f g X → sequential-cocone 𝓐 X
  pushout-cocone-to-seq-cocone (i , j , H) = (curry j , I)
   where
    I : (n : ℕ) → (curry j n) ∼ (λ - → j (succ n , a n -))
    I n x = H (inl (n , x)) ⁻¹ ∙ H (inr (n , x))

  seq-cocone-to-pushout-cocone : sequential-cocone 𝓐 X → cocone f g X
  seq-cocone-to-pushout-cocone (b , H)
   = (uncurry b , uncurry b , gluing-from-sequential-cocone (b , H))

  pushout-cocone-to-seq-cocone-is-retraction
   : pushout-cocone-to-seq-cocone ∘ seq-cocone-to-pushout-cocone ∼ id
  pushout-cocone-to-seq-cocone-is-retraction (b , H)
   = sequential-cocone-family-to-id 𝓐 X
      (pushout-cocone-to-seq-cocone (seq-cocone-to-pushout-cocone (b , H)))
      (b , H) ((λ n → λ x → refl) , (λ n → λ x → refl))

  pushout-cocone-to-seq-cocone-is-section
   : seq-cocone-to-pushout-cocone ∘ pushout-cocone-to-seq-cocone ∼ id
  pushout-cocone-to-seq-cocone-is-section (i , j , H)
   = inverse-cocone-map f g X
      (seq-cocone-to-pushout-cocone (pushout-cocone-to-seq-cocone (i , j , H)))
      (i , j , H) ((λ (n , x) → H (inl (n , x)) ⁻¹) , ∼-refl , I)
   where
    I : (z : Σ A + Σ A)
      → H (inl (index (f z) , element-at (f z))) ⁻¹ ∙ H z
      ＝ gluing-from-sequential-cocone
         (curry j , λ n → λ x → H (inl (n , x)) ⁻¹ ∙ H (inr (n , x))) z
    I (inl -) = left-inverse (H (inl -))
    I (inr -) = refl

  pushout-to-seq-cocone-is-equiv : is-equiv pushout-cocone-to-seq-cocone
  pushout-to-seq-cocone-is-equiv
   = qinvs-are-equivs pushout-cocone-to-seq-cocone
      (seq-cocone-to-pushout-cocone ,
       pushout-cocone-to-seq-cocone-is-section ,
        pushout-cocone-to-seq-cocone-is-retraction)


Additionally, we show that the canonical map to sequential cocones factors
through the canonical map to pushout cocones and the above map that translates
between them.


  canonical-maps-commute
   : canonical-map-to-sequential-cocone 𝓐 sequential-colimit X
      sequential-colimit-is-cocone
   ∼ pushout-cocone-to-seq-cocone
    ∘ canonical-map-to-cocone sequential-colimit f g pushout-cocone X
  canonical-maps-commute u
   = sequential-cocone-family-to-id 𝓐 X
      (canonical-map-to-sequential-cocone 𝓐 sequential-colimit X
       sequential-colimit-is-cocone u)
      (pushout-cocone-to-seq-cocone
       (canonical-map-to-cocone sequential-colimit f g
        pushout-cocone X u))
      (I , II)
    where
     I : (n : ℕ) → u ∘ ι n ∼ curry (u ∘ inrr) n
     I n x = refl
     II : (n : ℕ) (x : A n)
        → ap u (seq-colim-homotopy n x)
        ＝ refl ∙ (ap u (glue (inl (n , x))) ⁻¹ ∙ ap u (glue (inr (n , x))))
     II n x
      = ap u (seq-colim-homotopy n x)                                 ＝⟨ III ⟩
      ap u (glue (inl (n , x)) ⁻¹) ∙ ap u (glue (inr (n , x)))        ＝⟨ IV ⟩
        ap u (glue (inl (n , x))) ⁻¹ ∙ ap u (glue (inr (n , x)))      ＝⟨ V ⟩
        refl ∙ (ap u (glue (inl (n , x))) ⁻¹ ∙ ap u (glue (inr (n , x)))) ∎
      where
       III = ap-∙ u (glue (inl (n , x)) ⁻¹) (glue (inr (n , x)))
       IV = ap (_∙ ap u (glue (inr (n , x)))) (ap-sym u (glue (inl (n , x))) ⁻¹)
       V = refl-left-neutral ⁻¹


Using the above results we prove that the pushout constructed above satisfies
the universal property of the sequential colimit.


  sequential-colimit-universal-property
   : Sequential-Colimit-Universal-Property 𝓐 sequential-colimit X
      sequential-colimit-is-cocone  
  sequential-colimit-universal-property
   = transport is-equiv (dfunext fe (∼-sym canonical-maps-commute))
      (∘-is-equiv pushout-universal-property pushout-to-seq-cocone-is-equiv)


We unpack some useful results from the from the universal property.


  module _ (𝓧@(h , H) : sequential-cocone 𝓐 X)
         where

   canonical-map-seq-cocone-fiber-contr
    : is-contr (fiber (canonical-map-to-sequential-cocone 𝓐 sequential-colimit X
                        sequential-colimit-is-cocone) 𝓧)
   canonical-map-seq-cocone-fiber-contr
    = equivs-are-vv-equivs
       (canonical-map-to-sequential-cocone 𝓐 sequential-colimit X
        sequential-colimit-is-cocone) sequential-colimit-universal-property 𝓧

   canonical-map-seq-cocone-fiber-contr'
    : is-contr (Σ u ꞉ (sequential-colimit → X) ,
       sequential-cocone-identity 𝓐 X
        ((λ n → u ∘ ι n) , λ n → ∼-ap-∘ u (seq-colim-homotopy n)) 𝓧)
   canonical-map-seq-cocone-fiber-contr' =
    equiv-to-singleton'
     (Σ-cong (λ - → sequential-cocone-identity-characterization 𝓐 X
      ((λ n → - ∘ ι n) , λ n → ∼-ap-∘ - (seq-colim-homotopy n)) 𝓧))
       (canonical-map-seq-cocone-fiber-contr)

   sequential-colimit-unique-map
    : Σ u ꞉ (sequential-colimit → X) ,
       sequential-cocone-identity 𝓐 X
        ((λ n → u ∘ ι n) , λ n → ∼-ap-∘ u (seq-colim-homotopy n)) 𝓧
    → sequential-colimit → X
   sequential-colimit-unique-map (u , _ , _) = u

   sequential-colimit-homotopy
    : (z : Σ u ꞉ (sequential-colimit → X) ,
       sequential-cocone-identity 𝓐 X
        ((λ n → u ∘ ι n) , λ n → ∼-ap-∘ u (seq-colim-homotopy n)) 𝓧)
    → (n : ℕ) → sequential-colimit-unique-map z ∘ ι n ∼ h n
   sequential-colimit-homotopy (_ , G , _) = G

   sequential-colimit-glue
    : ((u , G , M) : Σ u ꞉ (sequential-colimit → X) ,
       sequential-cocone-identity 𝓐 X
        ((λ n → u ∘ ι n) , λ n → ∼-ap-∘ u (seq-colim-homotopy n)) 𝓧)
    → (n : ℕ)
    → ∼-trans (∼-ap-∘ u (seq-colim-homotopy n)) (λ x → G (succ n) (a n x))
    ∼ ∼-trans (G n) (H n)
   sequential-colimit-glue (_ , _ , M) = M


From the universal property we derive the recursion principle and computation
rules for sequential colimits.


  sequential-colimit-recursion : sequential-cocone 𝓐 X
                               → sequential-colimit → X
  sequential-colimit-recursion 𝓧
   = sequential-colimit-unique-map 𝓧
      (center (canonical-map-seq-cocone-fiber-contr' 𝓧))

  sequential-colimit-recursion-computation
   : ((h , H) : sequential-cocone 𝓐 X)
   → (n : ℕ)
   → (x : A n)
   → sequential-colimit-recursion (h , H) (ι n x) ＝ h n x
  sequential-colimit-recursion-computation 𝓧
   = sequential-colimit-homotopy 𝓧
      (center (canonical-map-seq-cocone-fiber-contr' 𝓧))

  sequential-colimit-recursion-glue
   : ((h , H) : sequential-cocone 𝓐 X)
   → (n : ℕ)
   → (x : A n)
   → ap (sequential-colimit-recursion (h , H)) (seq-colim-homotopy n x)
     ∙ sequential-colimit-recursion-computation (h , H) (succ n) (a n x)
   ＝ sequential-colimit-recursion-computation (h , H) n x ∙ H n x
  sequential-colimit-recursion-glue 𝓧
   = sequential-colimit-glue 𝓧
      (center (canonical-map-seq-cocone-fiber-contr' 𝓧))


Finally, we prove the uniqueness principle for sequential colimits.


  sequential-colimit-uniqueness
   : (u u' : sequential-colimit → X)
   → (G : (n : ℕ) → u ∘ (ι n) ∼ u' ∘ (ι n))
   → (M : (n : ℕ) (x : A n) → ap u (seq-colim-homotopy n x) ∙ G (succ n) (a n x)
   ＝ G n x ∙ ap u' (seq-colim-homotopy n x))
   → u ∼ u'
  sequential-colimit-uniqueness u u' G M = pushout-uniqueness u u' I II III
   where
    I : (z : Σ A) → u (inll z) ＝ u' (inll z)
    I (n , x)
     = ap u (glue (inl (n , x))) ∙ G n x ∙ ap u' (glue (inl (n , x))) ⁻¹
    II : (z : Σ A) → u (inrr z) ＝ u' (inrr z)
    II (n , x) = G n x
    III : (c : Σ A + Σ A)
        → ap u (glue c) ∙ II (g c) ＝ I (f c) ∙ ap u' (glue c)
    III (inl (n , x)) = p ∙ G n x                 ＝⟨ IV ⟩
                        p ∙ G n x ∙ (p' ⁻¹ ∙ p')  ＝⟨ V ⟩
                        I (n , x) ∙ p'            ∎
     where
      p = ap u (glue (inl (n , x)))
      p' = ap u' (glue (inl (n , x)))
      IV = ap (p ∙ G n x ∙_) (sym-is-inverse p')
      V = ∙assoc (p ∙ G n x) (p' ⁻¹) p' ⁻¹
    III (inr (n , x)) =
     q ∙ G (succ n) (a n x)                                    ＝⟨ IV ⟩
     (p ∙ p ⁻¹) ∙ (q ∙ G (succ n) (a n x))                     ＝⟨ V ⟩
     p ∙ (p ⁻¹ ∙ (q ∙ G (succ n) (a n x)))                     ＝⟨ VI ⟩
     p ∙ (p ⁻¹ ∙ q ∙ G (succ n) (a n x))                       ＝⟨ VII ⟩
     p ∙ (ap u (seq-colim-homotopy n x) ∙ G (succ n) (a n x))  ＝⟨ VIII ⟩
     p ∙ (G n x ∙ ap u' (seq-colim-homotopy n x))              ＝⟨ IX ⟩
     p ∙ G n x ∙ ap u' (seq-colim-homotopy n x)                ＝⟨ X' ⟩
     I (n , x) ∙ q'                                            ∎
     where
      p = ap u (glue (inl (n , x)))
      q = ap u (glue (inr (n , x)))
      p' = ap u' (glue (inl (n , x)))
      q' = ap u' (glue (inr (n , x)))
      IV = refl-left-neutral ⁻¹ ∙ ap (_∙ (q ∙ G (succ n) (a n x)))
                                     (sym-is-inverse' p)
      V = ∙assoc p (p ⁻¹) (q ∙ G (succ n) (a n x))
      VI = ap (p ∙_) (∙assoc (p ⁻¹) q (G (succ n) (a n x)) ⁻¹)
      VII = ap (p ∙_) (ap (_∙ G (succ n) (a n x)) (ap-on-glue u (n , x) ⁻¹))
      VIII = ap (p ∙_) (M n x)
      IX = ∙assoc p (G n x) (ap u' (seq-colim-homotopy n x)) ⁻¹
      X' = ap (p ∙ G n x ∙_ ) (ap-on-glue u' (n , x))
           ∙ (∙assoc (p ∙ G n x) (p' ⁻¹) q') ⁻¹


TODO. Derive the dependent universal property and induction principle for
sequential colimits.