From 88591165f79f2944c3e8b33ac60dd9c47d4bf314 Mon Sep 17 00:00:00 2001
From: VojtechStep <vojtechstepancik@outlook.com>
Date: Fri, 8 Dec 2023 22:52:35 +0100
Subject: [PATCH] Refactor functoriality of sequential colimits

---
 ...functoriality-sequential-colimits.lagda.md | 758 ++++++++++++------
 1 file changed, 506 insertions(+), 252 deletions(-)

diff --git a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
index 1bca6b7e9a4..8a704baefba 100644
--- a/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
+++ b/src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md
@@ -21,6 +21,7 @@ open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.retractions
 open import foundation.retracts-of-types
+open import foundation.sections
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies
 
@@ -37,23 +38,38 @@ open import synthetic-homotopy-theory.universal-property-sequential-colimits
 
 ## Idea
 
-Taking the
-[sequential colimit](synthetic-homotopy-theory.sequential-colimits.md) of a
-[sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) is a
-functorial action `(A, a) ↦ A∞`.
+Given two
+[sequential diagrams](synthetic-homotopy-theory.sequential-diagrams.md) `(A, a)`
+and `(B, b)`, their
+[sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md)
+`X` and `Y`, and a
+[morphism](synthetic-homotopy-theory.morphisms-sequential-diagrams.md)
+`f : (A, a) → (B, b)`, we get an induced map `f∞ : X → Y`, as in the following
+diagram:
 
-In other words, a
-[morphism of sequential diagrams](synthetic-homotopy-theory.morphisms-sequential-diagrams.md)
-`f : (A, a) → (B, b)` induces a map `f∞ : A∞ → B∞` between the
-[standard sequential colimits](synthetic-homotopy-theory.sequential-colimits.md)
-of the diagrams, and this action preserves the identity morphism and morphism
-composition.
+```text
+        a₀      a₁      a₂
+    A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X
+    |       |       |              |
+ f₀ |       | f₁    | f₂           | f∞
+    V       V       V              V
+    B₀ ---> B₁ ---> B₂ ---> ⋯ ---> Y
+        b₀      b₁      b₂             .
+```
+
+The identity morphism is taken to the identity function, `id∞ ~ id`, and
+composition of morphisms is taken to composition of functions,
+`(g ∘ f)∞ ~ g∞ ∘ f∞`.
 
-Furthermore, an
-[equivalence of sequential diagrams](synthetic-homotopy-theory.equivalences-sequential-diagrams.md)
-`e : (A, a) ≃ (B, b)` induces an equivalence `e∞ : A∞ ≃ B∞`.
+A corollary of these facts is that taking the
+[standard sequential colimit](synthetic-homotopy-theory.sequential-colimits.md)
+is a functorial action `(A, a) ↦ A∞`.
 
-The development in this file is a formalization of Lemma 3.5 in Sequential
+Additionally, an
+[equivalence of sequentual diagrams](synthetic-homotopy-theory.equivalences-sequential-diagrams)
+induces an [equivalence](foundation.equivalences.md) of their colimits.
+
+The development in this file is a generalization of Lemma 3.5 from Sequential
 Colimits in Homotopy Type Theory.
 
 ## Properties
@@ -72,24 +88,24 @@ module _
     comp-hom-sequential-diagram A B (constant-sequential-diagram X) c f
 ```
 
-### A morphism of sequential diagrams induces a map of standard sequential colimits
+### A morphism of sequential diagrams induces a map of sequential colimits
 
 The induced map
 
 ```text
         a₀      a₁      a₂
-    A₀ ---> A₁ ---> A₂ ---> ⋯ ---> A∞
+    A₀ ---> A₁ ---> A₂ ---> ⋯ ---> X
     |       |       |              |
  f₀ |       | f₁    | f₂           | f∞
     V       V       V              V
-    B₀ ---> B₁ ---> B₂ ---> ⋯ ---> B∞
+    B₀ ---> B₁ ---> B₂ ---> ⋯ ---> Y
         b₀      b₁      b₂
 ```
 
 then induces a
 [cocone](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md) under
-`(A, a)` with codomain `B∞`, which is homotopic to the standard cocone under
-`(B, b)` precomposed by `f`.
+`(A, a)` with codomain `Y`, which is homotopic to the cocone under `(B, b)`
+precomposed by `f`.
 
 This homotopy of cocones provides
 [vertical commuting prisms of maps](foundation.commuting-prisms-of-maps.md),
@@ -99,21 +115,431 @@ This homotopy of cocones provides
          ^ | \
        /   |   \
      /     |fₙ₊₁ V
-    Aₙ ---------> A∞
+    Aₙ ---------> X
     |      |      |
     |      V      |
  fₙ |     Bₙ₊₁    | f∞
     |    ^   \    |
     |  /       \  |
     V/           VV
-    Bₙ ---------> B∞ ,
+    Bₙ ---------> Y ,
 ```
 
 where the [triangles](foundation-core.commuting-triangles-of-maps.md) are
-coherences of the cocones of the standard sequential colimits, the back left
+coherences of the cocones of the sequential colimits, the back left
 [square](foundation-core.commuting-triangles-of-maps.md) is coherence of `f`,
 and the front and back right squares are provided by uniqueness of `f∞`.
 
+```agda
+module _
+  { l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  { X : UU l3} {c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  { Y : UU l4} (c' : cocone-sequential-diagram B Y)
+  ( f : hom-sequential-diagram A B)
+  where
+
+  map-sequential-colimit-hom-sequential-diagram : X → Y
+  map-sequential-colimit-hom-sequential-diagram =
+    map-universal-property-sequential-colimit up-c
+      ( map-cocone-hom-sequential-diagram f c')
+
+  htpy-cocone-map-sequential-colimit-hom-sequential-diagram :
+    htpy-cocone-sequential-diagram
+      ( cocone-map-sequential-diagram c
+        ( map-sequential-colimit-hom-sequential-diagram))
+      ( map-cocone-hom-sequential-diagram f c')
+  htpy-cocone-map-sequential-colimit-hom-sequential-diagram =
+    htpy-cocone-universal-property-sequential-colimit up-c
+      ( map-cocone-hom-sequential-diagram f c')
+
+  htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram :
+    ( n : ℕ) →
+    coherence-square-maps
+      ( map-hom-sequential-diagram B f n)
+      ( map-cocone-sequential-diagram c n)
+      ( map-cocone-sequential-diagram c' n)
+      ( map-sequential-colimit-hom-sequential-diagram)
+  htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram =
+    htpy-htpy-cocone-sequential-diagram
+      ( htpy-cocone-map-sequential-colimit-hom-sequential-diagram)
+
+  coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram :
+    ( n : ℕ) →
+    coherence-square-homotopies
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n)
+      ( ( map-sequential-colimit-hom-sequential-diagram) ·l
+        ( coherence-triangle-cocone-sequential-diagram c n))
+      ( coherence-triangle-cocone-sequential-diagram
+        ( map-cocone-hom-sequential-diagram f c')
+        ( n))
+      ( ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+          ( succ-ℕ n)) ·r
+        ( map-sequential-diagram A n))
+  coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram =
+    coherence-htpy-htpy-cocone-sequential-diagram
+      htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+
+  prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram :
+    ( n : ℕ) →
+    vertical-coherence-prism-maps
+      ( map-cocone-sequential-diagram c n)
+      ( map-cocone-sequential-diagram c (succ-ℕ n))
+      ( map-sequential-diagram A n)
+      ( map-cocone-sequential-diagram c' n)
+      ( map-cocone-sequential-diagram c' (succ-ℕ n))
+      ( map-sequential-diagram B n)
+      ( map-hom-sequential-diagram B f n)
+      ( map-hom-sequential-diagram B f (succ-ℕ n))
+      ( map-sequential-colimit-hom-sequential-diagram)
+      ( coherence-triangle-cocone-sequential-diagram c n)
+      ( inv-htpy
+        ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n))
+      ( inv-htpy
+        ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+          ( succ-ℕ n)))
+      ( naturality-map-hom-sequential-diagram B f n)
+      ( coherence-triangle-cocone-sequential-diagram c' n)
+  prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n =
+    rotate-vertical-coherence-prism-maps
+      ( map-cocone-sequential-diagram c n)
+      ( map-cocone-sequential-diagram c (succ-ℕ n))
+      ( map-sequential-diagram A n)
+      ( map-cocone-sequential-diagram c' n)
+      ( map-cocone-sequential-diagram c' (succ-ℕ n))
+      ( map-sequential-diagram B n)
+      ( map-hom-sequential-diagram B f n)
+      ( map-hom-sequential-diagram B f (succ-ℕ n))
+      ( map-sequential-colimit-hom-sequential-diagram)
+      ( coherence-triangle-cocone-sequential-diagram c n)
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram n)
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+        ( succ-ℕ n))
+      ( naturality-map-hom-sequential-diagram B f n)
+      ( coherence-triangle-cocone-sequential-diagram c' n)
+      ( inv-htpy
+        ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+          ( n)))
+```
+
+### Homotopies between morphisms of sequential diagrams induce homotopies of maps between sequential colimits
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  { X : UU l3} {c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  { Y : UU l4} (c' : cocone-sequential-diagram B Y)
+  { f g : hom-sequential-diagram A B} (H : htpy-hom-sequential-diagram B f g)
+  where
+
+  htpy-map-sequential-colimit-htpy-hom-sequential-diagram :
+    map-sequential-colimit-hom-sequential-diagram up-c c' f ~
+    map-sequential-colimit-hom-sequential-diagram up-c c' g
+  htpy-map-sequential-colimit-htpy-hom-sequential-diagram =
+    htpy-eq
+      ( ap
+        ( map-sequential-colimit-hom-sequential-diagram up-c c')
+        ( eq-htpy-sequential-diagram _ _ f g H))
+```
+
+### The identity morphism induces the identity map
+
+```agda
+module _
+  { l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  { c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  where
+
+  htpy-preserves-id-map-sequential-colimit-hom-sequential-diagram :
+    htpy-out-of-sequential-colimit c
+      ( map-sequential-colimit-hom-sequential-diagram up-c c
+        ( id-hom-sequential-diagram A))
+      ( id)
+  pr1 htpy-preserves-id-map-sequential-colimit-hom-sequential-diagram =
+    htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c
+      ( id-hom-sequential-diagram A)
+  pr2 htpy-preserves-id-map-sequential-colimit-hom-sequential-diagram n =
+    ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c
+      ( id-hom-sequential-diagram A)
+      ( n)) ∙h
+    ( ap-concat-htpy _
+      ( ( right-unit-htpy) ∙h
+        ( inv-htpy
+          ( left-unit-law-left-whisk-htpy
+            ( coherence-triangle-cocone-sequential-diagram c n)))))
+
+  preserves-id-map-sequential-colimit-hom-sequential-diagram :
+    ( map-sequential-colimit-hom-sequential-diagram up-c c
+      ( id-hom-sequential-diagram A)) ~
+    ( id)
+  preserves-id-map-sequential-colimit-hom-sequential-diagram =
+    htpy-htpy-out-of-sequential-colimit up-c
+      ( htpy-preserves-id-map-sequential-colimit-hom-sequential-diagram)
+```
+
+### Composition of morphisms induces composition of functions
+
+```agda
+module _
+  { l1 l2 l3 l4 l5 l6 : Level}
+  { A : sequential-diagram l1} {B : sequential-diagram l2}
+  { C : sequential-diagram l3}
+  { X : UU l4} {c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  { Y : UU l5} {c' : cocone-sequential-diagram B Y}
+  ( up-c' : universal-property-sequential-colimit c')
+  { Z : UU l6} (c'' : cocone-sequential-diagram C Z)
+  ( g : hom-sequential-diagram B C) (f : hom-sequential-diagram A B)
+  where
+
+  htpy-preserves-comp-map-sequential-colimit-hom-sequential-diagram :
+    htpy-out-of-sequential-colimit c
+      ( map-sequential-colimit-hom-sequential-diagram up-c c''
+        ( comp-hom-sequential-diagram A B C g f))
+      ( ( map-sequential-colimit-hom-sequential-diagram up-c' c'' g) ∘
+        ( map-sequential-colimit-hom-sequential-diagram up-c c' f))
+  pr1 htpy-preserves-comp-map-sequential-colimit-hom-sequential-diagram n =
+    ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c''
+      ( comp-hom-sequential-diagram A B C g f)
+      ( n)) ∙h
+    pasting-vertical-coherence-square-maps
+      ( map-cocone-sequential-diagram c n)
+      ( map-hom-sequential-diagram B f n)
+      ( map-sequential-colimit-hom-sequential-diagram up-c c' f)
+      ( map-cocone-sequential-diagram c' n)
+      ( map-hom-sequential-diagram C g n)
+      ( map-sequential-colimit-hom-sequential-diagram up-c' c'' g)
+      ( map-cocone-sequential-diagram c'' n)
+      ( inv-htpy
+        ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c'
+          ( f)
+          ( n)))
+      ( inv-htpy
+        ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c'
+          ( c'')
+          ( g)
+          ( n)))
+  pr2 htpy-preserves-comp-map-sequential-colimit-hom-sequential-diagram n =
+    ( right-whisk-square-htpy
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c''
+        ( comp-hom-sequential-diagram A B C g f)
+        ( n))
+      ( ( map-sequential-colimit-hom-sequential-diagram up-c c''
+          ( comp-hom-sequential-diagram A B C g f)) ·l
+        ( coherence-triangle-cocone-sequential-diagram c n))
+      ( _)
+      ( coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c
+        ( c'')
+        ( comp-hom-sequential-diagram A B C g f)
+        ( n))) ∙h
+    ( ap-concat-htpy
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c''
+        ( comp-hom-sequential-diagram A B C g f)
+        ( n))
+      ( ( assoc-htpy
+          ( ( coherence-triangle-cocone-sequential-diagram c'' n) ·r
+            ( ( map-hom-sequential-diagram C g n) ∘
+              ( map-hom-sequential-diagram B f n)))
+          ( map-cocone-sequential-diagram c'' (succ-ℕ n) ·l _)
+          ( _)) ∙h
+        ( pasting-vertical-coherence-prism-maps
+          ( map-cocone-sequential-diagram c n)
+          ( map-cocone-sequential-diagram c (succ-ℕ n))
+          ( map-sequential-diagram A n)
+          ( map-cocone-sequential-diagram c' n)
+          ( map-cocone-sequential-diagram c' (succ-ℕ n))
+          ( map-sequential-diagram B n)
+          ( map-hom-sequential-diagram B f n)
+          ( map-hom-sequential-diagram B f (succ-ℕ n))
+          ( map-sequential-colimit-hom-sequential-diagram up-c c' f)
+          ( map-cocone-sequential-diagram c'' n)
+          ( map-cocone-sequential-diagram c'' (succ-ℕ n))
+          ( map-sequential-diagram C n)
+          ( map-hom-sequential-diagram C g n)
+          ( map-hom-sequential-diagram C g (succ-ℕ n))
+          ( map-sequential-colimit-hom-sequential-diagram up-c' c'' g)
+          ( coherence-triangle-cocone-sequential-diagram c n)
+          ( inv-htpy
+            ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+              ( up-c)
+              ( c')
+              ( f)
+              ( n)))
+          ( inv-htpy
+            ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+              ( up-c)
+              ( c')
+              ( f)
+              ( succ-ℕ n)))
+          ( naturality-map-hom-sequential-diagram B f n)
+          ( coherence-triangle-cocone-sequential-diagram c' n)
+          ( inv-htpy
+            ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+              ( up-c')
+              ( c'')
+              ( g)
+              ( n)))
+          ( inv-htpy
+            ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+              ( up-c')
+              ( c'')
+              ( g)
+              ( succ-ℕ n)))
+          ( naturality-map-hom-sequential-diagram C g n)
+          ( coherence-triangle-cocone-sequential-diagram c'' n)
+          ( prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c
+            ( c')
+            ( f)
+            ( n))
+          ( prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+            ( up-c')
+            ( c'')
+            ( g)
+            ( n))))) ∙h
+    ( inv-htpy-assoc-htpy
+      ( htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram up-c c''
+        ( comp-hom-sequential-diagram A B C g f)
+        ( n))
+      ( _)
+      ( ( ( map-sequential-colimit-hom-sequential-diagram up-c' c'' g) ∘
+          ( map-sequential-colimit-hom-sequential-diagram up-c c' f)) ·l
+        ( coherence-triangle-cocone-sequential-diagram c n)))
+
+  preserves-comp-map-sequential-colimit-hom-sequential-diagram :
+    ( map-sequential-colimit-hom-sequential-diagram up-c c''
+      ( comp-hom-sequential-diagram A B C g f)) ~
+    ( ( map-sequential-colimit-hom-sequential-diagram up-c' c'' g) ∘
+      ( map-sequential-colimit-hom-sequential-diagram up-c c' f))
+  preserves-comp-map-sequential-colimit-hom-sequential-diagram =
+    htpy-htpy-out-of-sequential-colimit up-c
+      ( htpy-preserves-comp-map-sequential-colimit-hom-sequential-diagram)
+```
+
+### A retract of sequential diagrams induces a retract of sequential colimits
+
+Additionally, the underlying map of the retraction is definitionally equal to
+the map induced by the retraction of sequential diagrams.
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  { X : UU l3} {c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  { Y : UU l4} {c' : cocone-sequential-diagram B Y}
+  ( up-c' : universal-property-sequential-colimit c')
+  ( R : A retract-of-sequential-diagram B)
+  where
+
+  map-inclusion-sequential-colimit-retract-sequential-diagram : X → Y
+  map-inclusion-sequential-colimit-retract-sequential-diagram =
+    map-sequential-colimit-hom-sequential-diagram up-c c'
+      ( inclusion-retract-sequential-diagram A B R)
+
+  map-sequential-colimit-retract-sequential-diagram : Y → X
+  map-sequential-colimit-retract-sequential-diagram =
+    map-sequential-colimit-hom-sequential-diagram up-c' c
+      ( hom-retraction-retract-sequential-diagram A B R)
+
+  abstract
+    is-retraction-map-sequential-colimit-retract-sequential-diagram :
+      is-retraction
+        ( map-inclusion-sequential-colimit-retract-sequential-diagram)
+        ( map-sequential-colimit-retract-sequential-diagram)
+    is-retraction-map-sequential-colimit-retract-sequential-diagram =
+      ( inv-htpy
+        ( preserves-comp-map-sequential-colimit-hom-sequential-diagram up-c
+          ( up-c')
+          ( c)
+          ( hom-retraction-retract-sequential-diagram A B R)
+          ( inclusion-retract-sequential-diagram A B R))) ∙h
+      ( htpy-map-sequential-colimit-htpy-hom-sequential-diagram up-c c
+        ( is-retraction-hom-retraction-retract-sequential-diagram A B R)) ∙h
+      ( preserves-id-map-sequential-colimit-hom-sequential-diagram up-c)
+
+  retraction-sequential-colimit-retract-sequential-diagram :
+    retraction map-inclusion-sequential-colimit-retract-sequential-diagram
+  pr1 retraction-sequential-colimit-retract-sequential-diagram =
+    map-sequential-colimit-retract-sequential-diagram
+  pr2 retraction-sequential-colimit-retract-sequential-diagram =
+    is-retraction-map-sequential-colimit-retract-sequential-diagram
+
+  retract-sequential-colimit-retract-sequential-diagram :
+    X retract-of Y
+  pr1 retract-sequential-colimit-retract-sequential-diagram =
+    map-inclusion-sequential-colimit-retract-sequential-diagram
+  pr2 retract-sequential-colimit-retract-sequential-diagram =
+    retraction-sequential-colimit-retract-sequential-diagram
+```
+
+### An equivalence of sequential diagrams induces an equivalence of sequential colimits
+
+Additionally, the underlying map of the inverse equivalence is definitionally
+equal to the map induced by the inverse of the equivalence of sequential
+diagrams, i.e. `(e∞)⁻¹ = (e⁻¹)∞`.
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  { X : UU l3} {c : cocone-sequential-diagram A X}
+  ( up-c : universal-property-sequential-colimit c)
+  { Y : UU l4} {c' : cocone-sequential-diagram B Y}
+  ( up-c' : universal-property-sequential-colimit c')
+  ( e : equiv-sequential-diagram A B)
+  where
+
+  map-equiv-sequential-colimit-equiv-sequential-diagram : X → Y
+  map-equiv-sequential-colimit-equiv-sequential-diagram =
+    map-sequential-colimit-hom-sequential-diagram up-c c'
+      ( hom-equiv-sequential-diagram B e)
+
+  map-inv-equiv-sequential-colimit-equiv-sequential-diagram : Y → X
+  map-inv-equiv-sequential-colimit-equiv-sequential-diagram =
+    map-sequential-colimit-hom-sequential-diagram up-c' c
+      ( hom-inv-equiv-sequential-diagram B e)
+
+  abstract
+    is-section-map-inv-equiv-sequential-colimit-equiv-sequential-diagram :
+      is-section
+        ( map-equiv-sequential-colimit-equiv-sequential-diagram)
+        ( map-inv-equiv-sequential-colimit-equiv-sequential-diagram)
+    is-section-map-inv-equiv-sequential-colimit-equiv-sequential-diagram =
+      ( inv-htpy
+        ( preserves-comp-map-sequential-colimit-hom-sequential-diagram up-c'
+          ( up-c)
+          ( c')
+          ( hom-equiv-sequential-diagram B e)
+          ( hom-inv-equiv-sequential-diagram B e))) ∙h
+      ( htpy-map-sequential-colimit-htpy-hom-sequential-diagram up-c' c'
+        ( is-section-inv-equiv-sequential-diagram _ e)) ∙h
+      ( preserves-id-map-sequential-colimit-hom-sequential-diagram up-c')
+
+    is-retraction-map-inv-equiv-sequential-colimit-equiv-sequential-diagram :
+      is-retraction
+        ( map-equiv-sequential-colimit-equiv-sequential-diagram)
+        ( map-inv-equiv-sequential-colimit-equiv-sequential-diagram)
+    is-retraction-map-inv-equiv-sequential-colimit-equiv-sequential-diagram =
+      is-retraction-map-sequential-colimit-retract-sequential-diagram up-c up-c'
+        ( retract-equiv-sequential-diagram e)
+
+  is-equiv-map-equiv-sequential-colimit-equiv-sequential-diagram :
+    is-equiv map-equiv-sequential-colimit-equiv-sequential-diagram
+  is-equiv-map-equiv-sequential-colimit-equiv-sequential-diagram =
+    is-equiv-is-invertible
+      ( map-inv-equiv-sequential-colimit-equiv-sequential-diagram)
+      ( is-section-map-inv-equiv-sequential-colimit-equiv-sequential-diagram)
+      ( is-retraction-map-inv-equiv-sequential-colimit-equiv-sequential-diagram)
+
+  equiv-sequential-colimit-equiv-sequential-diagram : X ≃ Y
+  pr1 equiv-sequential-colimit-equiv-sequential-diagram =
+    map-equiv-sequential-colimit-equiv-sequential-diagram
+  pr2 equiv-sequential-colimit-equiv-sequential-diagram =
+    is-equiv-map-equiv-sequential-colimit-equiv-sequential-diagram
+```
+
+### A morphism of sequential diagrams induces a map of standard sequential colimits
+
 ```agda
 module _
   { l1 l2 : Level} {A : sequential-diagram l1} (B : sequential-diagram l2)
@@ -123,23 +549,23 @@ module _
   map-hom-standard-sequential-colimit :
     standard-sequential-colimit A → standard-sequential-colimit B
   map-hom-standard-sequential-colimit =
-    cogap-standard-sequential-colimit
-      ( map-cocone-hom-sequential-diagram f
-        ( cocone-standard-sequential-colimit B))
+    map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit B)
+      ( f)
 
   htpy-cocone-map-hom-standard-sequential-colimit :
-    htpy-cocone-sequential-diagram A
-      ( cocone-map-sequential-diagram A
+    htpy-cocone-sequential-diagram
+      ( cocone-map-sequential-diagram
         ( cocone-standard-sequential-colimit A)
         ( map-hom-standard-sequential-colimit))
       ( map-cocone-hom-sequential-diagram f
         ( cocone-standard-sequential-colimit B))
   htpy-cocone-map-hom-standard-sequential-colimit =
-    htpy-cocone-universal-property-sequential-colimit A
-      ( cocone-standard-sequential-colimit A)
+    htpy-cocone-map-sequential-colimit-hom-sequential-diagram
       ( up-standard-sequential-colimit)
-      ( map-cocone-hom-sequential-diagram f
-        ( cocone-standard-sequential-colimit B))
+      ( cocone-standard-sequential-colimit B)
+      ( f)
 
   htpy-htpy-cocone-map-hom-standard-sequential-colimit :
     ( n : ℕ) →
@@ -149,8 +575,10 @@ module _
       ( map-cocone-standard-sequential-colimit n)
       ( map-hom-standard-sequential-colimit)
   htpy-htpy-cocone-map-hom-standard-sequential-colimit =
-    htpy-htpy-cocone-sequential-diagram A
-      ( htpy-cocone-map-hom-standard-sequential-colimit)
+    htpy-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit B)
+      ( f)
 
   coherence-htpy-cocone-map-hom-standard-sequential-colimit :
     ( n : ℕ) →
@@ -158,15 +586,17 @@ module _
       ( htpy-htpy-cocone-map-hom-standard-sequential-colimit n)
       ( ( map-hom-standard-sequential-colimit) ·l
         ( coherence-triangle-cocone-standard-sequential-colimit n))
-      ( coherence-triangle-cocone-sequential-diagram A
+      ( coherence-triangle-cocone-sequential-diagram
           ( map-cocone-hom-sequential-diagram f
             ( cocone-standard-sequential-colimit B))
           ( n))
       ( ( htpy-htpy-cocone-map-hom-standard-sequential-colimit (succ-ℕ n)) ·r
         ( map-sequential-diagram A n))
   coherence-htpy-cocone-map-hom-standard-sequential-colimit =
-    coherence-htpy-htpy-cocone-sequential-diagram A
-      ( htpy-cocone-map-hom-standard-sequential-colimit)
+    coherence-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit B)
+      ( f)
 
   prism-htpy-cocone-map-hom-standard-sequential-colimit :
     ( n : ℕ) →
@@ -186,23 +616,11 @@ module _
         ( htpy-htpy-cocone-map-hom-standard-sequential-colimit (succ-ℕ n)))
       ( naturality-map-hom-sequential-diagram B f n)
       ( coherence-triangle-cocone-standard-sequential-colimit n)
-  prism-htpy-cocone-map-hom-standard-sequential-colimit n =
-    rotate-vertical-coherence-prism-maps
-      ( map-cocone-standard-sequential-colimit n)
-      ( map-cocone-standard-sequential-colimit (succ-ℕ n))
-      ( map-sequential-diagram A n)
-      ( map-cocone-standard-sequential-colimit n)
-      ( map-cocone-standard-sequential-colimit (succ-ℕ n))
-      ( map-sequential-diagram B n)
-      ( map-hom-sequential-diagram B f n)
-      ( map-hom-sequential-diagram B f (succ-ℕ n))
-      ( map-hom-standard-sequential-colimit)
-      ( coherence-triangle-cocone-standard-sequential-colimit n)
-      ( htpy-htpy-cocone-map-hom-standard-sequential-colimit n)
-      ( htpy-htpy-cocone-map-hom-standard-sequential-colimit (succ-ℕ n))
-      ( naturality-map-hom-sequential-diagram B f n)
-      ( coherence-triangle-cocone-standard-sequential-colimit n)
-      ( inv-htpy (coherence-htpy-cocone-map-hom-standard-sequential-colimit n))
+  prism-htpy-cocone-map-hom-standard-sequential-colimit =
+    prism-htpy-cocone-map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit B)
+      ( f)
 ```
 
 ### Homotopies between morphisms of sequential diagrams induce homotopies of maps of standard sequential colimits
@@ -217,10 +635,10 @@ module _
     map-hom-standard-sequential-colimit B f ~
     map-hom-standard-sequential-colimit B g
   htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram =
-    htpy-eq
-      ( ap
-        ( map-hom-standard-sequential-colimit B)
-        ( eq-htpy-sequential-diagram A B f g H))
+    htpy-map-sequential-colimit-htpy-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit B)
+      ( H)
 ```
 
 ### The identity morphism induces the identity map
@@ -232,30 +650,13 @@ module _
   { l1 : Level} {A : sequential-diagram l1}
   where
 
-  htpy-preserves-id-map-hom-standard-sequential-colimit :
-    htpy-out-of-standard-sequential-colimit A
-      ( map-hom-standard-sequential-colimit A
-        ( id-hom-sequential-diagram A))
-      ( id)
-  pr1 htpy-preserves-id-map-hom-standard-sequential-colimit =
-    htpy-htpy-cocone-map-hom-standard-sequential-colimit A
-      ( id-hom-sequential-diagram A)
-  pr2 htpy-preserves-id-map-hom-standard-sequential-colimit n =
-    ( coherence-htpy-cocone-map-hom-standard-sequential-colimit A
-      ( id-hom-sequential-diagram A) n) ∙h
-    ( ap-concat-htpy _
-      ( ( right-unit-htpy) ∙h
-        ( inv-htpy
-          ( left-unit-law-left-whisk-htpy
-            ( coherence-triangle-cocone-standard-sequential-colimit n)))))
-
   preserves-id-map-hom-standard-sequential-colimit :
-    map-hom-standard-sequential-colimit A
-      ( id-hom-sequential-diagram A) ~
-    id
+    ( map-hom-standard-sequential-colimit A
+      ( id-hom-sequential-diagram A)) ~
+    ( id)
   preserves-id-map-hom-standard-sequential-colimit =
-    htpy-htpy-out-of-standard-sequential-colimit A
-      ( htpy-preserves-id-map-hom-standard-sequential-colimit)
+    preserves-id-map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
 ```
 
 ### Forming standard sequential colimits preserves composition of morphisms of sequential diagrams
@@ -269,112 +670,18 @@ module _
   ( g : hom-sequential-diagram B C) (f : hom-sequential-diagram A B)
   where
 
-  htpy-preserves-comp-map-hom-standard-sequential-colimit :
-    htpy-out-of-standard-sequential-colimit A
-      ( map-hom-standard-sequential-colimit C
-        ( comp-hom-sequential-diagram A B C g f))
-      ( ( map-hom-standard-sequential-colimit C g) ∘
-        ( map-hom-standard-sequential-colimit B f))
-  pr1 htpy-preserves-comp-map-hom-standard-sequential-colimit n =
-    ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C
-      ( comp-hom-sequential-diagram A B C g f) n) ∙h
-    ( pasting-vertical-coherence-square-maps
-      ( map-cocone-standard-sequential-colimit n)
-      ( map-hom-sequential-diagram B f n)
-      ( map-hom-standard-sequential-colimit B f)
-      ( map-cocone-standard-sequential-colimit n)
-      ( map-hom-sequential-diagram C g n)
-      ( map-hom-standard-sequential-colimit C g)
-      ( map-cocone-standard-sequential-colimit n)
-      ( inv-htpy
-        ( htpy-htpy-cocone-map-hom-standard-sequential-colimit B f n))
-      ( inv-htpy
-        ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C g n)))
-  pr2 htpy-preserves-comp-map-hom-standard-sequential-colimit n =
-    ( inv-htpy-assoc-htpy
-      ( ( map-hom-standard-sequential-colimit C
-          ( comp-hom-sequential-diagram A B C g f)) ·l
-        ( coherence-triangle-cocone-standard-sequential-colimit n))
-      ( ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C
-          ( comp-hom-sequential-diagram A B C g f)
-          ( succ-ℕ n)) ·r
-        ( map-sequential-diagram A n))
-      ( _)) ∙h
-    ( ap-concat-htpy' _
-      ( coherence-htpy-cocone-map-hom-standard-sequential-colimit C
-        ( comp-hom-sequential-diagram A B C g f)
-        ( n)) ∙h
-    ( assoc-htpy
-      ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C
-        ( comp-hom-sequential-diagram A B C g f)
-        ( n))
-      ( coherence-triangle-cocone-sequential-diagram A
-        ( map-cocone-hom-sequential-diagram
-          ( comp-hom-sequential-diagram A B C g f)
-          ( cocone-standard-sequential-colimit C))
-        ( n))
-      ( _)) ∙h
-    ( ap-concat-htpy
-      ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C
-        ( comp-hom-sequential-diagram A B C g f)
-        ( n))
-      ( ( assoc-htpy
-          ( ( coherence-triangle-cocone-standard-sequential-colimit n) ·r
-            ( ( map-hom-sequential-diagram C g n) ∘
-              ( map-hom-sequential-diagram B f n)))
-          ( map-cocone-standard-sequential-colimit (succ-ℕ n) ·l _)
-          ( _)) ∙h
-        ( pasting-vertical-coherence-prism-maps
-          ( map-cocone-standard-sequential-colimit n)
-          ( map-cocone-standard-sequential-colimit (succ-ℕ n))
-          ( map-sequential-diagram A n)
-          ( map-cocone-standard-sequential-colimit n)
-          ( map-cocone-standard-sequential-colimit (succ-ℕ n))
-          ( map-sequential-diagram B n)
-          ( map-hom-sequential-diagram B f n)
-          ( map-hom-sequential-diagram B f (succ-ℕ n))
-          ( map-hom-standard-sequential-colimit B f)
-          ( map-cocone-standard-sequential-colimit n)
-          ( map-cocone-standard-sequential-colimit (succ-ℕ n))
-          ( map-sequential-diagram C n)
-          ( map-hom-sequential-diagram C g n)
-          ( map-hom-sequential-diagram C g (succ-ℕ n))
-          ( map-hom-standard-sequential-colimit C g)
-          ( coherence-triangle-cocone-standard-sequential-colimit n)
-          ( inv-htpy
-            ( htpy-htpy-cocone-map-hom-standard-sequential-colimit B f n))
-          ( inv-htpy
-            ( htpy-htpy-cocone-map-hom-standard-sequential-colimit B f
-              ( succ-ℕ n)))
-          ( naturality-map-hom-sequential-diagram B f n)
-          ( coherence-triangle-cocone-standard-sequential-colimit n)
-          ( inv-htpy
-            ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C g n))
-          ( inv-htpy
-            ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C g
-              ( succ-ℕ n)))
-          ( naturality-map-hom-sequential-diagram C g n)
-          ( coherence-triangle-cocone-standard-sequential-colimit n)
-          ( prism-htpy-cocone-map-hom-standard-sequential-colimit B f n)
-          ( prism-htpy-cocone-map-hom-standard-sequential-colimit C g
-            ( n))))) ∙h
-    ( inv-htpy-assoc-htpy
-      ( htpy-htpy-cocone-map-hom-standard-sequential-colimit C
-        ( comp-hom-sequential-diagram A B C g f)
-        ( n))
-      ( _)
-      ( ( ( map-hom-standard-sequential-colimit C g) ∘
-          ( map-hom-standard-sequential-colimit B f)) ·l
-        ( coherence-triangle-cocone-standard-sequential-colimit n))))
-
   preserves-comp-map-hom-standard-sequential-colimit :
     ( map-hom-standard-sequential-colimit C
       ( comp-hom-sequential-diagram A B C g f)) ~
     ( ( map-hom-standard-sequential-colimit C g) ∘
       ( map-hom-standard-sequential-colimit B f))
   preserves-comp-map-hom-standard-sequential-colimit =
-    htpy-htpy-out-of-standard-sequential-colimit A
-      htpy-preserves-comp-map-hom-standard-sequential-colimit
+    preserves-comp-map-sequential-colimit-hom-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( up-standard-sequential-colimit)
+      ( cocone-standard-sequential-colimit C)
+      ( g)
+      ( f)
 ```
 
 ### An equivalence of sequential diagrams induces an equivalence of standard sequential colimits
@@ -392,56 +699,26 @@ module _
   map-equiv-standard-sequential-colimit :
     standard-sequential-colimit A → standard-sequential-colimit B
   map-equiv-standard-sequential-colimit =
-    map-hom-standard-sequential-colimit B
-      ( hom-equiv-sequential-diagram B e)
+    map-equiv-sequential-colimit-equiv-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( up-standard-sequential-colimit)
+      ( e)
 
-  inv-map-equiv-standard-sequential-colimit :
+  map-inv-equiv-standard-sequential-colimit :
     standard-sequential-colimit B → standard-sequential-colimit A
-  inv-map-equiv-standard-sequential-colimit =
-    map-hom-standard-sequential-colimit A
-      ( hom-inv-equiv-sequential-diagram B e)
-
-  abstract
-    is-section-inv-map-equiv-standard-sequential-colimit :
-      ( ( map-equiv-standard-sequential-colimit) ∘
-        ( inv-map-equiv-standard-sequential-colimit)) ~
-      ( id)
-    is-section-inv-map-equiv-standard-sequential-colimit =
-      ( inv-htpy
-        ( preserves-comp-map-hom-standard-sequential-colimit
-          ( hom-equiv-sequential-diagram B e)
-          ( hom-inv-equiv-sequential-diagram B e))) ∙h
-      ( htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram
-        ( is-section-inv-equiv-sequential-diagram B e)) ∙h
-      ( preserves-id-map-hom-standard-sequential-colimit)
-
-    is-retraction-inv-map-equiv-standard-sequential-colimit :
-      ( ( inv-map-equiv-standard-sequential-colimit) ∘
-        ( map-equiv-standard-sequential-colimit)) ~
-      ( id)
-    is-retraction-inv-map-equiv-standard-sequential-colimit =
-      ( inv-htpy
-        ( preserves-comp-map-hom-standard-sequential-colimit
-          ( hom-inv-equiv-sequential-diagram B e)
-          ( hom-equiv-sequential-diagram B e))) ∙h
-      ( htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram
-        ( is-retraction-inv-equiv-sequential-diagram B e)) ∙h
-      ( preserves-id-map-hom-standard-sequential-colimit)
-
-  is-equiv-map-hom-standard-sequential-colimit :
-    is-equiv map-equiv-standard-sequential-colimit
-  is-equiv-map-hom-standard-sequential-colimit =
-    is-equiv-is-invertible
-      ( inv-map-equiv-standard-sequential-colimit)
-      ( is-section-inv-map-equiv-standard-sequential-colimit)
-      ( is-retraction-inv-map-equiv-standard-sequential-colimit)
+  map-inv-equiv-standard-sequential-colimit =
+    map-inv-equiv-sequential-colimit-equiv-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( up-standard-sequential-colimit)
+      ( e)
 
   equiv-equiv-standard-sequential-colimit :
     standard-sequential-colimit A ≃ standard-sequential-colimit B
-  pr1 equiv-equiv-standard-sequential-colimit =
-    map-hom-standard-sequential-colimit B (hom-equiv-sequential-diagram B e)
-  pr2 equiv-equiv-standard-sequential-colimit =
-    is-equiv-map-hom-standard-sequential-colimit
+  equiv-equiv-standard-sequential-colimit =
+    equiv-sequential-colimit-equiv-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( up-standard-sequential-colimit)
+      ( e)
 ```
 
 ### A retract of sequential diagrams induces a retract of standard sequential colimits
@@ -467,36 +744,13 @@ module _
     map-hom-standard-sequential-colimit A
       ( hom-retraction-retract-sequential-diagram A B R)
 
-  abstract
-    is-retraction-map-hom-retraction-retract-standard-sequential-colimit :
-      is-retraction
-        ( map-inclusion-retract-standard-sequential-colimit)
-        ( map-hom-retraction-retract-standard-sequential-colimit)
-    is-retraction-map-hom-retraction-retract-standard-sequential-colimit =
-      ( inv-htpy
-        ( preserves-comp-map-hom-standard-sequential-colimit
-          ( hom-retraction-retract-sequential-diagram A B R)
-          ( inclusion-retract-sequential-diagram A B R))) ∙h
-      ( htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram
-        ( is-retraction-hom-retraction-retract-sequential-diagram A B R)) ∙h
-      ( preserves-id-map-hom-standard-sequential-colimit)
-
-  retraction-retract-standard-sequential-colimit :
-    retraction
-      ( map-hom-standard-sequential-colimit B
-        ( inclusion-retract-sequential-diagram A B R))
-  pr1 retraction-retract-standard-sequential-colimit =
-    map-hom-retraction-retract-standard-sequential-colimit
-  pr2 retraction-retract-standard-sequential-colimit =
-    is-retraction-map-hom-retraction-retract-standard-sequential-colimit
-
   retract-retract-standard-sequential-colimit :
     (standard-sequential-colimit A) retract-of (standard-sequential-colimit B)
-  pr1 retract-retract-standard-sequential-colimit =
-    map-hom-standard-sequential-colimit B
-      ( inclusion-retract-sequential-diagram A B R)
-  pr2 retract-retract-standard-sequential-colimit =
-    retraction-retract-standard-sequential-colimit
+  retract-retract-standard-sequential-colimit =
+    retract-sequential-colimit-retract-sequential-diagram
+      ( up-standard-sequential-colimit)
+      ( up-standard-sequential-colimit)
+      ( R)
 ```
 
 ## References