From 20569c124266f6b44edfa21fae7cae8b7c713e10 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Vojt=C4=9Bch=20=C5=A0t=C4=9Bpan=C4=8D=C3=ADk?=
 <vojtechstepancik@outlook.com>
Date: Wed, 10 Apr 2024 11:31:02 +0200
Subject: [PATCH] Shifts and unshifts of concepts around sequential colimits
 (#1070)

This PR formalizes shifts of sequential diagrams, morphisms of
sequential diagrams, cocones of sequential diagrams, homotopies of
cocones of sequential diagrams, and unshifts of the last two. This
machinery is used to show that dropping any finite number of vertices
from the beginning of a sequential diagram gives an equivalent
sequential colimit.
---
 src/synthetic-homotopy-theory.lagda.md        |   2 +
 ...cocones-under-sequential-diagrams.lagda.md |  38 +-
 ...cocones-under-sequential-diagrams.lagda.md |   2 +-
 .../dependent-sequential-diagrams.lagda.md    |   2 +-
 .../morphisms-sequential-diagrams.lagda.md    |  14 +-
 .../sequential-diagrams.lagda.md              |   2 +-
 .../shifts-sequential-diagrams.lagda.md       | 773 ++++++++++++++++++
 .../total-sequential-diagrams.lagda.md        | 117 +++
 8 files changed, 933 insertions(+), 17 deletions(-)
 create mode 100644 src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md
 create mode 100644 src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md

diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md
index 89173b31c2..d0edc20c56 100644
--- a/src/synthetic-homotopy-theory.lagda.md
+++ b/src/synthetic-homotopy-theory.lagda.md
@@ -86,6 +86,7 @@ open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
 open import synthetic-homotopy-theory.sequentially-compact-types public
+open import synthetic-homotopy-theory.shifts-sequential-diagrams public
 open import synthetic-homotopy-theory.smash-products-of-pointed-types public
 open import synthetic-homotopy-theory.spectra public
 open import synthetic-homotopy-theory.sphere-prespectrum public
@@ -95,6 +96,7 @@ open import synthetic-homotopy-theory.suspension-structures public
 open import synthetic-homotopy-theory.suspensions-of-pointed-types public
 open import synthetic-homotopy-theory.suspensions-of-types public
 open import synthetic-homotopy-theory.tangent-spheres public
+open import synthetic-homotopy-theory.total-sequential-diagrams public
 open import synthetic-homotopy-theory.triple-loop-spaces public
 open import synthetic-homotopy-theory.truncated-acyclic-maps public
 open import synthetic-homotopy-theory.truncated-acyclic-types public
diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
index 7eb8ec69fd..1da0704bf2 100644
--- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -35,10 +35,11 @@ open import synthetic-homotopy-theory.sequential-diagrams
 
 ## Idea
 
-A **cocone under a
-[sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
-`(A, a)`** with codomain `X : 𝓤` consists of a family of maps `iₙ : A n → C` and
-a family of [homotopies](foundation.homotopies.md) `Hₙ` asserting that the
+A
+{{#concept "cocone" Disambiguation="sequential diagram" Agda=cocone-sequential-diagram}}
+under a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
+`(A, a)` with codomain `X : 𝒰` consists of a family of maps `iₙ : A n → C` and a
+family of [homotopies](foundation.homotopies.md) `Hₙ` asserting that the
 triangles
 
 ```text
@@ -154,6 +155,35 @@ module _
   coherence-htpy-htpy-cocone-sequential-diagram = pr2 H
 ```
 
+### Concatenation of homotopies of cocones under a sequential diagram
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  {c c' c'' : cocone-sequential-diagram A X}
+  (H : htpy-cocone-sequential-diagram c c')
+  (K : htpy-cocone-sequential-diagram c' c'')
+  where
+
+  concat-htpy-cocone-sequential-diagram : htpy-cocone-sequential-diagram c c''
+  pr1 concat-htpy-cocone-sequential-diagram n =
+    ( htpy-htpy-cocone-sequential-diagram H n) ∙h
+    ( htpy-htpy-cocone-sequential-diagram K n)
+  pr2 concat-htpy-cocone-sequential-diagram n =
+    horizontal-pasting-coherence-square-homotopies
+      ( htpy-htpy-cocone-sequential-diagram H n)
+      ( htpy-htpy-cocone-sequential-diagram K n)
+      ( coherence-cocone-sequential-diagram c n)
+      ( coherence-cocone-sequential-diagram c' n)
+      ( coherence-cocone-sequential-diagram c'' n)
+      ( ( htpy-htpy-cocone-sequential-diagram H (succ-ℕ n)) ·r
+        ( map-sequential-diagram A n))
+      ( ( htpy-htpy-cocone-sequential-diagram K (succ-ℕ n)) ·r
+        ( map-sequential-diagram A n))
+      ( coherence-htpy-htpy-cocone-sequential-diagram H n)
+      ( coherence-htpy-htpy-cocone-sequential-diagram K n)
+```
+
 ### Postcomposing cocones under a sequential diagram with a map
 
 Given a cocone `c` with vertex `X` under `(A, a)` and a map `f : X → Y`, we may
diff --git a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md
index dcee6298d0..6711f8276f 100644
--- a/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-cocones-under-sequential-diagrams.lagda.md
@@ -41,7 +41,7 @@ open import synthetic-homotopy-theory.sequential-diagrams
 Given a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
 `(A, a)`, a
 [cocone](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md) `c`
-with vertex `X` under it, and a type family `P : X → 𝓤`, we may construct
+with vertex `X` under it, and a type family `P : X → 𝒰`, we may construct
 _dependent_ cocones on `P` over `c`.
 
 A **dependent cocone under a
diff --git a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
index 7cafe2e7ee..a4554336de 100644
--- a/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/dependent-sequential-diagrams.lagda.md
@@ -24,7 +24,7 @@ open import synthetic-homotopy-theory.sequential-diagrams
 A **dependent sequential diagram** over a
 [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) `(A, a)`
 is a [sequence](foundation.dependent-sequences.md) of families of types
-`B : (n : ℕ) → Aₙ → 𝓤` over the types in the base sequential diagram, equipped
+`B : (n : ℕ) → Aₙ → 𝒰` over the types in the base sequential diagram, equipped
 with fiberwise maps
 
 ```text
diff --git a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
index 86c6950684..47a9948110 100644
--- a/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md
@@ -71,8 +71,8 @@ module _
 
   hom-sequential-diagram : UU (l1 ⊔ l2)
   hom-sequential-diagram =
-    section-dependent-sequential-diagram A
-      ( constant-dependent-sequential-diagram A B)
+    Σ ( (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n)
+      ( naturality-hom-sequential-diagram)
 ```
 
 ### Components of morphisms of sequential diagrams
@@ -91,17 +91,11 @@ module _
 
   map-hom-sequential-diagram :
     ( n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n
-  map-hom-sequential-diagram =
-    map-section-dependent-sequential-diagram A
-      ( constant-dependent-sequential-diagram A B)
-      ( h)
+  map-hom-sequential-diagram = pr1 h
 
   naturality-map-hom-sequential-diagram :
     naturality-hom-sequential-diagram A B map-hom-sequential-diagram
-  naturality-map-hom-sequential-diagram =
-    naturality-map-section-dependent-sequential-diagram A
-      ( constant-dependent-sequential-diagram A B)
-      ( h)
+  naturality-map-hom-sequential-diagram = pr2 h
 ```
 
 ### The identity morphism of sequential diagrams
diff --git a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
index 33166e8430..34fe7194f0 100644
--- a/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
+++ b/src/synthetic-homotopy-theory/sequential-diagrams.lagda.md
@@ -18,7 +18,7 @@ open import foundation.universe-levels
 ## Idea
 
 A **sequential diagram** `(A, a)` is a [sequence](foundation.sequences.md) of
-types `A : ℕ → 𝓤` over the natural numbers, equipped with a family of maps
+types `A : ℕ → 𝒰` over the natural numbers, equipped with a family of maps
 `aₙ : Aₙ → Aₙ₊₁` for all `n`.
 
 They can be represented by diagrams
diff --git a/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md
new file mode 100644
index 0000000000..66cb304593
--- /dev/null
+++ b/src/synthetic-homotopy-theory/shifts-sequential-diagrams.lagda.md
@@ -0,0 +1,773 @@
+# Shifts of sequential diagrams
+
+```agda
+module synthetic-homotopy-theory.shifts-sequential-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-triangles-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.sections
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
+open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.sequential-colimits
+open import synthetic-homotopy-theory.sequential-diagrams
+open import synthetic-homotopy-theory.universal-property-sequential-colimits
+```
+
+</details>
+
+## Idea
+
+A
+{{#concept "shift" Disambiguation="sequential diagram" Agda=shift-sequential-diagram}}
+of a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) is a
+sequential diagram consisting of the types and maps shifted by one. It is also
+denoted `A[1]`. This shifting can be iterated for any
+[natural number](elementary-number-theory.natural-numbers.md) `k`; then the
+resulting sequential diagram is denoted `A[k]`.
+
+Similarly, a
+{{#concept "shift" Disambiguation="morphism of sequential diagrams" Agda=shift-hom-sequential-diagram}}
+of a
+[morphism of sequential diagrams](synthetic-homotopy-theory.morphisms-sequential-diagrams.md)
+is a morphism from the shifted domain into the shifted codomain. In symbols,
+given a morphism `f : A → B`, we have `f[k] : A[k] → B[k]`.
+
+We also define shifts of
+[cocones](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md) and
+[homotopies of cocones](synthetic-homotopy-theory.cocones-under-sequential-diagrams.md),
+which can additionally be unshifted.
+
+Importantly the type of cocones under a sequential diagram is
+[equivalent](foundation-core.equivalences.md) to the type of cocones under its
+shift, which implies that the
+[sequential colimit](synthetic-homotopy-theory.sequential-colimits.md) of a
+shifted sequential diagram is equivalent to the colimit of the original diagram.
+
+## Definitions
+
+_Implementation note_: the constructions are defined by first defining a shift
+by one, and then recursively shifting by one according to the argument. An
+alternative would be to shift all data using
+[addition](elementary-number-theory.addition-natural-numbers.md) on the natural
+numbers.
+
+However, addition computes only on one side, so we have a choice to make: given
+a shift `k`, do we define the `n`-th level of the shifted structure to be the
+`n+k`-th or `k+n`-th level of the original?
+
+The former runs into issues already when defining the shifted sequence, since
+`aₙ₊ₖ : Aₙ₊ₖ → A₍ₙ₊₁₎₊ₖ`, but we need a map of type `Aₙ₊ₖ → A₍ₙ₊ₖ₎₊₁`, which
+forces us to introduce a
+[transport](foundation-core.transport-along-identifications.md).
+
+On the other hand, the latter requires transport when proving anything by
+induction on `k` and doesn't satisfy the judgmental equality `A[0] ≐ A`, because
+`A₍ₖ₊₁₎₊ₙ` is not `A₍ₖ₊ₙ₎₊₁` and `A₀₊ₙ` is not `Aₙ`, and it requires more
+infrastructure for working with horizontal compositions in sequential colimit to
+be formalized in terms of addition.
+
+To contrast, defining the operations by induction does satisfy `A[0] ≐ A`, it
+computes when proving properties by induction, which is the expected primary
+use-case, and no further infrastructure is necessary.
+
+### Shifts of sequential diagrams
+
+Given a sequential diagram `A`
+
+```text
+     a₀      a₁      a₂
+ A₀ ---> A₁ ---> A₂ ---> ⋯ ,
+```
+
+we can forget the first type and map to get the diagram
+
+```text
+     a₁      a₂
+ A₁ ---> A₂ ---> ⋯ ,
+```
+
+which we call `A[1]`. Inductively, we define `A[k + 1] ≐ A[k][1]`.
+
+```agda
+module _
+  {l1 : Level} (A : sequential-diagram l1)
+  where
+
+  shift-once-sequential-diagram : sequential-diagram l1
+  pr1 shift-once-sequential-diagram n = family-sequential-diagram A (succ-ℕ n)
+  pr2 shift-once-sequential-diagram n = map-sequential-diagram A (succ-ℕ n)
+
+module _
+  {l1 : Level}
+  where
+
+  shift-sequential-diagram : ℕ → sequential-diagram l1 → sequential-diagram l1
+  shift-sequential-diagram zero-ℕ A = A
+  shift-sequential-diagram (succ-ℕ k) A =
+    shift-once-sequential-diagram (shift-sequential-diagram k A)
+```
+
+### Shifts of morphisms of sequential diagrams
+
+Given a morphism of sequential diagrams `f : A → B`
+
+```text
+        a₀      a₁
+    A₀ ---> A₁ ---> A₂ ---> ⋯
+    |       |       |
+ f₀ |       | f₁    | f₂
+    ∨       ∨       ∨
+    B₀ ---> B₁ ---> B₂ ---> ⋯ ,
+        b₀      b₁
+```
+
+we can drop the first square to get the morphism
+
+```text
+        a₁
+    A₁ ---> A₂ ---> ⋯
+    |       |
+ f₁ |       | f₂
+    ∨       ∨
+    B₁ ---> B₂ ---> ⋯ ,
+        b₁
+```
+
+which we call `f[1] : A[1] → B[1]`. Inductively, we define `f[k + 1] ≐ f[k][1]`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} (B : sequential-diagram l2)
+  (f : hom-sequential-diagram A B)
+  where
+
+  shift-once-hom-sequential-diagram :
+    hom-sequential-diagram
+      ( shift-once-sequential-diagram A)
+      ( shift-once-sequential-diagram B)
+  pr1 shift-once-hom-sequential-diagram n =
+    map-hom-sequential-diagram B f (succ-ℕ n)
+  pr2 shift-once-hom-sequential-diagram n =
+    naturality-map-hom-sequential-diagram B f (succ-ℕ n)
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} (B : sequential-diagram l2)
+  where
+
+  shift-hom-sequential-diagram :
+    (k : ℕ) →
+    hom-sequential-diagram A B →
+    hom-sequential-diagram
+      ( shift-sequential-diagram k A)
+      ( shift-sequential-diagram k B)
+  shift-hom-sequential-diagram zero-ℕ f = f
+  shift-hom-sequential-diagram (succ-ℕ k) f =
+    shift-once-hom-sequential-diagram
+      ( shift-sequential-diagram k B)
+      ( shift-hom-sequential-diagram k f)
+```
+
+### Shifts of cocones under sequential diagrams
+
+Given a cocone `c`
+
+```text
+      a₀      a₁
+  A₀ ---> A₁ ---> A₂ ---> ⋯
+   \      |      /
+    \     |     /
+  i₀ \    | i₁ / i₂
+      \   |   /
+       ∨  ∨  ∨
+          X
+```
+
+under `A`, we may forget the first inclusion and homotopy to get the cocone
+
+```text
+         a₁
+     A₁ ---> A₂ ---> ⋯
+     |      /
+     |     /
+  i₁ |    / i₂
+     |   /
+     ∨  ∨
+     X
+```
+
+under `A[1]`. We denote this cocone `c[1]`. Inductively, we define
+`c[k + 1] ≐ c[k][1]`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2} (c : cocone-sequential-diagram A X)
+  where
+
+  shift-once-cocone-sequential-diagram :
+    cocone-sequential-diagram (shift-once-sequential-diagram A) X
+  pr1 shift-once-cocone-sequential-diagram n =
+    map-cocone-sequential-diagram c (succ-ℕ n)
+  pr2 shift-once-cocone-sequential-diagram n =
+    coherence-cocone-sequential-diagram c (succ-ℕ n)
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  shift-cocone-sequential-diagram :
+    (k : ℕ) →
+    cocone-sequential-diagram A X →
+    cocone-sequential-diagram (shift-sequential-diagram k A) X
+  shift-cocone-sequential-diagram zero-ℕ c =
+    c
+  shift-cocone-sequential-diagram (succ-ℕ k) c =
+    shift-once-cocone-sequential-diagram
+      ( shift-cocone-sequential-diagram k c)
+```
+
+### Unshifts of cocones under sequential diagrams
+
+Conversely, given a cocone `c`
+
+```text
+         a₁
+     A₁ ---> A₂ ---> ⋯
+     |      /
+     |     /
+  i₁ |    / i₂
+     |   /
+     ∨  ∨
+     X
+```
+
+under `A[1]`, we may prepend a map
+
+```text
+           a₀      a₁
+       A₀ ---> A₁ ---> A₂ ---> ⋯
+        \      |      /
+         \     |     /
+  i₁ ∘ a₀ \    | i₁ / i₂
+           \   |   /
+            ∨  ∨  ∨
+               X
+```
+
+which commutes by reflexivity, giving us a cocone under `A`, which we call
+`c[-1]`.
+
+Notice that by restricting the type of `c` to be the cocones under an already
+shifted diagram, we ensure that unshifting cannot get out of bounds of the
+original diagram.
+
+Inductively, we define `c[-(k + 1)] ≐ c[-1][-k]`. One might expect that
+following the pattern of shifts, this should be `c[-k][-1]`, but recall that we
+only know how to unshift a cocone under `A[n]` by `n`; since this `c` is under
+`A[k][1]`, we first need to unshift by 1 to get `c[-1]` under `A[k]`, and only
+then we can unshift by `k` to get `c[-1][-k]` under `A`.
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1)
+  {X : UU l2}
+  (c : cocone-sequential-diagram (shift-once-sequential-diagram A) X)
+  where
+
+  unshift-once-cocone-sequential-diagram :
+    cocone-sequential-diagram A X
+  pr1 unshift-once-cocone-sequential-diagram zero-ℕ =
+    map-cocone-sequential-diagram c zero-ℕ ∘ map-sequential-diagram A zero-ℕ
+  pr1 unshift-once-cocone-sequential-diagram (succ-ℕ n) =
+    map-cocone-sequential-diagram c n
+  pr2 unshift-once-cocone-sequential-diagram zero-ℕ =
+    refl-htpy
+  pr2 unshift-once-cocone-sequential-diagram (succ-ℕ n) =
+    coherence-cocone-sequential-diagram c n
+
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1)
+  {X : UU l2}
+  where
+
+  unshift-cocone-sequential-diagram :
+    (k : ℕ) →
+    cocone-sequential-diagram (shift-sequential-diagram k A) X →
+    cocone-sequential-diagram A X
+  unshift-cocone-sequential-diagram zero-ℕ c =
+    c
+  unshift-cocone-sequential-diagram (succ-ℕ k) c =
+    unshift-cocone-sequential-diagram k
+      ( unshift-once-cocone-sequential-diagram
+        ( shift-sequential-diagram k A)
+        ( c))
+```
+
+### Shifts of homotopies of cocones under sequential diagrams
+
+Given cocones `c` and `c'` under `A`
+
+```text
+     a₀      a₁                   a₀      a₁
+ A₀ ---> A₁ ---> A₂ ---> ⋯    A₀ ---> A₁ ---> A₂ ---> ⋯
+  \      |      /              \      |      /
+   \     | i₁  /                \     | i'₁ /
+ i₀ \    |    / i₂     ~     i'₀ \    |    / i'₂
+     \   |   /                    \   |   /
+      ∨  ∨  ∨                      ∨  ∨  ∨
+         X                            X
+```
+
+and a homotopy `H : c ~ c'` between them, we can again forget the first homotopy
+of maps and coherence to get the homotopy `H[1] : c[1] ~ c'[1]`. Inductively, we
+define `H[k + 1] ≐ H[k][1]`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  {c c' : cocone-sequential-diagram A X}
+  (H : htpy-cocone-sequential-diagram c c')
+  where
+
+  shift-once-htpy-cocone-sequential-diagram :
+    htpy-cocone-sequential-diagram
+      ( shift-once-cocone-sequential-diagram c)
+      ( shift-once-cocone-sequential-diagram c')
+  pr1 shift-once-htpy-cocone-sequential-diagram n =
+    htpy-htpy-cocone-sequential-diagram H (succ-ℕ n)
+  pr2 shift-once-htpy-cocone-sequential-diagram n =
+    coherence-htpy-htpy-cocone-sequential-diagram
+      ( H)
+      ( succ-ℕ n)
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  {c c' : cocone-sequential-diagram A X}
+  where
+
+  shift-htpy-cocone-sequential-diagram :
+    (k : ℕ) →
+    htpy-cocone-sequential-diagram c c' →
+    htpy-cocone-sequential-diagram
+      ( shift-cocone-sequential-diagram k c)
+      ( shift-cocone-sequential-diagram k c')
+  shift-htpy-cocone-sequential-diagram zero-ℕ H =
+    H
+  shift-htpy-cocone-sequential-diagram (succ-ℕ k) H =
+    shift-once-htpy-cocone-sequential-diagram
+      ( shift-htpy-cocone-sequential-diagram k H)
+```
+
+### Unshifts of homotopies of cocones under sequential diagrams
+
+Similarly to unshifting cocones, we can recover the first homotopy and coherence
+to unshift a homotopy of cocones. Given two cocones `c`, `c'` under `A[1]`
+
+```text
+         a₁                     a₁
+     A₁ ---> A₂ ---> ⋯      A₁ ---> A₂ ---> ⋯
+     |      /               |      /
+     |     /                |     /
+  i₁ |    / i₂     ~    i'₁ |    / i'₂
+     |   /                  |   /
+     ∨  ∨                   ∨  ∨
+     X                      X
+```
+
+and a homotopy `H : c ~ c'`, we need to show that `i₁ ∘ a₀ ~ i'₁ ∘ a₀`. This can
+be obtained by whiskering `H₀ ·r a₀`, which makes the coherence trivial.
+
+Inductively, we define `H[-(k + 1)] ≐ H[-1][-k]`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  {c c' : cocone-sequential-diagram (shift-once-sequential-diagram A) X}
+  (H : htpy-cocone-sequential-diagram c c')
+  where
+
+  unshift-once-htpy-cocone-sequential-diagram :
+    htpy-cocone-sequential-diagram
+      ( unshift-once-cocone-sequential-diagram A c)
+      ( unshift-once-cocone-sequential-diagram A c')
+  pr1 unshift-once-htpy-cocone-sequential-diagram zero-ℕ =
+    ( htpy-htpy-cocone-sequential-diagram H zero-ℕ) ·r
+    ( map-sequential-diagram A zero-ℕ)
+  pr1 unshift-once-htpy-cocone-sequential-diagram (succ-ℕ n) =
+    htpy-htpy-cocone-sequential-diagram H n
+  pr2 unshift-once-htpy-cocone-sequential-diagram zero-ℕ =
+    inv-htpy-right-unit-htpy
+  pr2 unshift-once-htpy-cocone-sequential-diagram (succ-ℕ n) =
+    coherence-htpy-htpy-cocone-sequential-diagram H n
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1} {X : UU l2}
+  where
+
+  unshift-htpy-cocone-sequential-diagram :
+    (k : ℕ) →
+    {c c' : cocone-sequential-diagram (shift-sequential-diagram k A) X} →
+    htpy-cocone-sequential-diagram c c' →
+    htpy-cocone-sequential-diagram
+      ( unshift-cocone-sequential-diagram A k c)
+      ( unshift-cocone-sequential-diagram A k c')
+  unshift-htpy-cocone-sequential-diagram zero-ℕ H =
+    H
+  unshift-htpy-cocone-sequential-diagram (succ-ℕ k) H =
+    unshift-htpy-cocone-sequential-diagram k
+      (unshift-once-htpy-cocone-sequential-diagram H)
+```
+
+### Morphisms from sequential diagrams into their shifts
+
+The morphism is obtained by observing that the squares in the diagram
+
+```text
+        a₀      a₁
+    A₀ ---> A₁ ---> A₂ ---> ⋯
+    |       |       |
+ a₀ |       | a₁    | a₂
+    ∨       ∨       ∨
+    A₁ ---> A₂ ---> A₃ ---> ⋯
+        a₁      a₂
+```
+
+commute by reflexivity.
+
+```agda
+module _
+  {l1 : Level} (A : sequential-diagram l1)
+  where
+
+  hom-shift-once-sequential-diagram :
+    hom-sequential-diagram
+      ( A)
+      ( shift-once-sequential-diagram A)
+  pr1 hom-shift-once-sequential-diagram = map-sequential-diagram A
+  pr2 hom-shift-once-sequential-diagram n = refl-htpy
+
+module _
+  {l1 : Level} (A : sequential-diagram l1)
+  where
+
+  hom-shift-sequential-diagram :
+    (k : ℕ) →
+    hom-sequential-diagram
+      ( A)
+      ( shift-sequential-diagram k A)
+  hom-shift-sequential-diagram zero-ℕ = id-hom-sequential-diagram A
+  hom-shift-sequential-diagram (succ-ℕ k) =
+    comp-hom-sequential-diagram
+      ( A)
+      ( shift-sequential-diagram k A)
+      ( shift-sequential-diagram (succ-ℕ k) A)
+      ( hom-shift-once-sequential-diagram
+        ( shift-sequential-diagram k A))
+      ( hom-shift-sequential-diagram k)
+```
+
+## Properties
+
+### The type of cocones under a sequential diagram is equivalent to the type of cocones under its shift
+
+This is shown by proving that shifting and unshifting of cocones are mutually
+inverse operations.
+
+To show that `shift ∘ unshift ~ id` is trivial, since the first step synthesizes
+some data for the first level, which the second step promptly forgets.
+
+In the inductive step, we need to show `c[-(k + 1)][k + 1] ~ c`. The left-hand
+side computes to `c[-1][-k][k][1]`, which is homotopic to `c[-1][1]` by shifting
+the homotopy given by the inductive hypothesis, and that computes to `c`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  htpy-is-section-unshift-once-cocone-sequential-diagram :
+    (c : cocone-sequential-diagram (shift-once-sequential-diagram A) X) →
+    htpy-cocone-sequential-diagram
+      ( shift-once-cocone-sequential-diagram
+        ( unshift-once-cocone-sequential-diagram A c))
+      ( c)
+  htpy-is-section-unshift-once-cocone-sequential-diagram c =
+    refl-htpy-cocone-sequential-diagram (shift-once-sequential-diagram A) c
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  htpy-is-section-unshift-cocone-sequential-diagram :
+    (k : ℕ) →
+    (c : cocone-sequential-diagram (shift-sequential-diagram k A) X) →
+    htpy-cocone-sequential-diagram
+      ( shift-cocone-sequential-diagram k
+        ( unshift-cocone-sequential-diagram A k c))
+      ( c)
+  htpy-is-section-unshift-cocone-sequential-diagram zero-ℕ c =
+    refl-htpy-cocone-sequential-diagram A c
+  htpy-is-section-unshift-cocone-sequential-diagram (succ-ℕ k) c =
+    shift-once-htpy-cocone-sequential-diagram
+      ( htpy-is-section-unshift-cocone-sequential-diagram k
+        ( unshift-once-cocone-sequential-diagram
+          ( shift-sequential-diagram k A)
+          ( c)))
+
+  is-section-unshift-cocone-sequential-diagram :
+    (k : ℕ) →
+    is-section
+      ( shift-cocone-sequential-diagram k)
+      ( unshift-cocone-sequential-diagram A {X} k)
+  is-section-unshift-cocone-sequential-diagram k c =
+    eq-htpy-cocone-sequential-diagram
+      ( shift-sequential-diagram k A)
+      ( _)
+      ( _)
+      ( htpy-is-section-unshift-cocone-sequential-diagram k c)
+```
+
+For the other direction, we need to show that the synthesized data, namely the
+map `i₁ ∘ a₀ : A₀ → X` and the reflexive homotopy, is consistent with the
+original data `i₀ : A₀ → X` and the homotopy `H₀ : i₀ ~ i₁ ∘ a₀`. It is more
+convenient to show the inverse homotopy `id ~ unshift ∘ shift`, because `H₀`
+gives us exactly the right homotopy for the first level, so the rest of the
+coherences are also trivial.
+
+In the inductive step, we need to show
+`c ~ c[k + 1][-(k + 1)] ≐ c[k][1][-1][-k]`. This follows from the inductive
+hypothesis, which states that `c ~ c[k][-k]`, and which we compose with the
+homotopy `c[k] ~ c[k][1][-1]` unshifted by `k`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram :
+    (c : cocone-sequential-diagram A X) →
+    htpy-cocone-sequential-diagram
+      ( c)
+      ( unshift-once-cocone-sequential-diagram A
+        ( shift-once-cocone-sequential-diagram c))
+  pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
+    zero-ℕ =
+    coherence-cocone-sequential-diagram c zero-ℕ
+  pr1 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
+    (succ-ℕ n) =
+    refl-htpy
+  pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
+    zero-ℕ =
+    refl-htpy
+  pr2 (inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
+    (succ-ℕ n) =
+    right-unit-htpy
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  inv-htpy-is-retraction-unshift-cocone-sequential-diagram :
+    (k : ℕ) →
+    (c : cocone-sequential-diagram A X) →
+    htpy-cocone-sequential-diagram
+      ( c)
+      ( unshift-cocone-sequential-diagram A k
+        ( shift-cocone-sequential-diagram k c))
+  inv-htpy-is-retraction-unshift-cocone-sequential-diagram zero-ℕ c =
+    refl-htpy-cocone-sequential-diagram A c
+  inv-htpy-is-retraction-unshift-cocone-sequential-diagram (succ-ℕ k) c =
+    concat-htpy-cocone-sequential-diagram
+      ( inv-htpy-is-retraction-unshift-cocone-sequential-diagram k c)
+      ( unshift-htpy-cocone-sequential-diagram k
+        ( inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram
+          ( shift-cocone-sequential-diagram k c)))
+
+  is-retraction-unshift-cocone-sequential-diagram :
+    (k : ℕ) →
+    is-retraction
+      ( shift-cocone-sequential-diagram k)
+      ( unshift-cocone-sequential-diagram A {X} k)
+  is-retraction-unshift-cocone-sequential-diagram k c =
+    inv
+      ( eq-htpy-cocone-sequential-diagram A _ _
+        ( inv-htpy-is-retraction-unshift-cocone-sequential-diagram k c))
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2}
+  where
+
+  is-equiv-shift-cocone-sequential-diagram :
+    (k : ℕ) →
+    is-equiv (shift-cocone-sequential-diagram {X = X} k)
+  is-equiv-shift-cocone-sequential-diagram k =
+    is-equiv-is-invertible
+      ( unshift-cocone-sequential-diagram A k)
+      ( is-section-unshift-cocone-sequential-diagram k)
+      ( is-retraction-unshift-cocone-sequential-diagram k)
+
+  equiv-shift-cocone-sequential-diagram :
+    (k : ℕ) →
+    cocone-sequential-diagram A X ≃
+    cocone-sequential-diagram (shift-sequential-diagram k A) X
+  pr1 (equiv-shift-cocone-sequential-diagram k) =
+    shift-cocone-sequential-diagram k
+  pr2 (equiv-shift-cocone-sequential-diagram k) =
+    is-equiv-shift-cocone-sequential-diagram k
+```
+
+### The sequential colimit of a sequential diagram is also the sequential colimit of its shift
+
+Given a sequential colimit
+
+```text
+     a₀      a₁      a₂
+ A₀ ---> A₁ ---> A₂ ---> ⋯ --> X,
+```
+
+there is a commuting triangle
+
+```text
+              cocone-map
+      X → Y ------------> cocone A Y
+            \           /
+  cocone-map  \       /
+                ∨   ∨
+             cocone A[1] Y.
+```
+
+Inductively, we compose this triangle in the following way
+
+```text
+              cocone-map
+      X → Y ------------> cocone A Y
+            \⟍             |
+             \ ⟍           |
+              \  ⟍         |
+               \   ⟍       ∨
+                \    > cocone A[k] Y
+     cocone-map  \       /
+                  \     /
+                   \   /
+                    ∨ ∨
+             cocone A[k + 1] Y,
+```
+
+where the top triangle is the inductive hypothesis, and the bottom triangle is
+the step instantiated at `A[k]`.
+
+This gives us the commuting triangle
+
+```text
+              cocone-map
+      X → Y ------------> cocone A Y
+            \     ≃     /
+  cocone-map  \       / ≃
+                ∨   ∨
+             cocone A[k] Y,
+```
+
+where the top map is an equivalence by the universal property of the cocone on
+`X`, and the right map is an equivalence by a theorem shown above, which implies
+that the left map is an equivalence, which exactly says that `X` is the
+sequential colimit of `A[k]`.
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2} (c : cocone-sequential-diagram A X)
+  where
+
+  triangle-cocone-map-shift-once-cocone-sequential-diagram :
+    {l : Level} (Y : UU l) →
+    coherence-triangle-maps
+      ( cocone-map-sequential-diagram
+        ( shift-once-cocone-sequential-diagram c)
+        { Y = Y})
+      ( shift-once-cocone-sequential-diagram)
+      ( cocone-map-sequential-diagram c)
+  triangle-cocone-map-shift-once-cocone-sequential-diagram Y = refl-htpy
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2} (c : cocone-sequential-diagram A X)
+  where
+
+  triangle-cocone-map-shift-cocone-sequential-diagram :
+    (k : ℕ) →
+    {l : Level} (Y : UU l) →
+    coherence-triangle-maps
+      ( cocone-map-sequential-diagram
+        ( shift-cocone-sequential-diagram k c))
+      ( shift-cocone-sequential-diagram k)
+      ( cocone-map-sequential-diagram c)
+  triangle-cocone-map-shift-cocone-sequential-diagram zero-ℕ Y =
+    refl-htpy
+  triangle-cocone-map-shift-cocone-sequential-diagram (succ-ℕ k) Y =
+    ( triangle-cocone-map-shift-once-cocone-sequential-diagram
+      ( shift-cocone-sequential-diagram k c)
+      ( Y)) ∙h
+    ( ( shift-once-cocone-sequential-diagram) ·l
+      ( triangle-cocone-map-shift-cocone-sequential-diagram k Y))
+
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2} {c : cocone-sequential-diagram A X}
+  where
+
+  up-shift-cocone-sequential-diagram :
+    (k : ℕ) →
+    universal-property-sequential-colimit c →
+    universal-property-sequential-colimit (shift-cocone-sequential-diagram k c)
+  up-shift-cocone-sequential-diagram k up-c Y =
+    is-equiv-left-map-triangle
+      ( cocone-map-sequential-diagram
+        ( shift-cocone-sequential-diagram k c))
+      ( shift-cocone-sequential-diagram k)
+      ( cocone-map-sequential-diagram c)
+      ( triangle-cocone-map-shift-cocone-sequential-diagram c k Y)
+      ( up-c Y)
+      ( is-equiv-shift-cocone-sequential-diagram k)
+```
+
+We instantiate this theorem for the standard sequential colimits, giving us
+`A[k]∞ ≃ A∞`.
+
+```agda
+module _
+  {l1 : Level} (A : sequential-diagram l1)
+  where
+
+  compute-sequential-colimit-shift-sequential-diagram :
+    (k : ℕ) →
+    standard-sequential-colimit (shift-sequential-diagram k A) ≃
+    standard-sequential-colimit A
+  pr1 (compute-sequential-colimit-shift-sequential-diagram k) =
+    cogap-standard-sequential-colimit
+      ( shift-cocone-sequential-diagram
+        ( k)
+        ( cocone-standard-sequential-colimit A))
+  pr2 (compute-sequential-colimit-shift-sequential-diagram k) =
+    is-sequential-colimit-universal-property _
+      ( up-shift-cocone-sequential-diagram k up-standard-sequential-colimit)
+```
diff --git a/src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md
new file mode 100644
index 0000000000..70bd318d5a
--- /dev/null
+++ b/src/synthetic-homotopy-theory/total-sequential-diagrams.lagda.md
@@ -0,0 +1,117 @@
+# Total sequential diagrams of dependent sequential diagrams
+
+```agda
+module synthetic-homotopy-theory.total-sequential-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.dependent-pair-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
+open import synthetic-homotopy-theory.dependent-sequential-diagrams
+open import synthetic-homotopy-theory.functoriality-sequential-colimits
+open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.sequential-colimits
+open import synthetic-homotopy-theory.sequential-diagrams
+open import synthetic-homotopy-theory.universal-property-sequential-colimits
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "total diagram" Disambiguation="dependent sequential diagrams" Agda=total-sequential-diagram}}
+of a
+[dependent sequential diagram](synthetic-homotopy-theory.dependent-sequential-diagrams.md)
+`B : (A, a) → 𝒰` is the
+[sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md)
+consisting of [total spaces](foundation.dependent-pair-types.md) `Σ Aₙ Bₙ` and
+total maps.
+
+## Definitions
+
+### The total sequential diagram of a dependent sequential diagram
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : sequential-diagram l1} (B : dependent-sequential-diagram A l2)
+  where
+
+  family-total-sequential-diagram : ℕ → UU (l1 ⊔ l2)
+  family-total-sequential-diagram n =
+    Σ (family-sequential-diagram A n)
+      (family-dependent-sequential-diagram A B n)
+
+  map-total-sequential-diagram :
+    (n : ℕ) → family-total-sequential-diagram n →
+    family-total-sequential-diagram (succ-ℕ n)
+  map-total-sequential-diagram n =
+    map-Σ
+      ( family-dependent-sequential-diagram A B (succ-ℕ n))
+      ( map-sequential-diagram A n)
+      ( map-dependent-sequential-diagram A B n)
+
+  total-sequential-diagram : sequential-diagram (l1 ⊔ l2)
+  pr1 total-sequential-diagram = family-total-sequential-diagram
+  pr2 total-sequential-diagram = map-total-sequential-diagram
+```
+
+### The projection morphism onto the base of the total sequential diagram
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : sequential-diagram l1} (B : dependent-sequential-diagram A l2)
+  where
+
+  pr1-total-sequential-diagram :
+    hom-sequential-diagram
+      ( total-sequential-diagram B)
+      ( A)
+  pr1 pr1-total-sequential-diagram n = pr1
+  pr2 pr1-total-sequential-diagram n = refl-htpy
+```
+
+### The induced projection map on sequential colimits
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : sequential-diagram l1} (B : dependent-sequential-diagram A l2)
+  {X : UU l3} {c : cocone-sequential-diagram (total-sequential-diagram B) X}
+  (up-c : universal-property-sequential-colimit c)
+  {Y : UU l4} (c' : cocone-sequential-diagram A Y)
+  where
+
+  pr1-sequential-colimit-total-sequential-diagram : X → Y
+  pr1-sequential-colimit-total-sequential-diagram =
+    map-sequential-colimit-hom-sequential-diagram
+      ( up-c)
+      ( c')
+      ( pr1-total-sequential-diagram B)
+```
+
+### The induced projection map on standard sequential colimits
+
+```agda
+module _
+  {l1 l2 : Level}
+  {A : sequential-diagram l1} (B : dependent-sequential-diagram A l2)
+  where
+
+  pr1-standard-sequential-colimit-total-sequential-diagram :
+    standard-sequential-colimit (total-sequential-diagram B) →
+    standard-sequential-colimit A
+  pr1-standard-sequential-colimit-total-sequential-diagram =
+    map-hom-standard-sequential-colimit A
+      ( pr1-total-sequential-diagram B)
+```