UF.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.YonedaA 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 = pushoutWe 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) = MFrom 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.