# Shifts of sequential diagrams

Content created by Vojtěch Štěpančík.

Created on 2024-04-10.

module synthetic-homotopy-theory.shifts-sequential-diagrams where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.commuting-triangles-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.homotopy-algebra
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 foundation.whiskering-homotopies-concatenation

open import synthetic-homotopy-theory.cocones-under-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


## Idea

A shift of a sequential diagram 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 k; then the resulting sequential diagram is denoted A[k].

Similarly, a shift of a morphism of sequential diagrams 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 and homotopies of cocones, which can additionally be unshifted.

Importantly the type of cocones under a sequential diagram is equivalent to the type of cocones under its shift, which implies that the sequential colimit 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 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.

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

     a₀      a₁      a₂
A₀ ---> A₁ ---> A₂ ---> ⋯ ,


we can forget the first type and map to get the diagram

     a₁      a₂
A₁ ---> A₂ ---> ⋯ ,


which we call A[1]. Inductively, we define A[k + 1] ≐ A[k][1].

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

        a₀      a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
|       |       |
f₀ |       | f₁    | f₂
∨       ∨       ∨
B₀ ---> B₁ ---> B₂ ---> ⋯ ,
b₀      b₁


we can drop the first square to get the morphism

        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].

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

      a₀      a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
\      |      /
\     |     /
i₀ \    | i₁ / i₂
\   |   /
∨  ∨  ∨
X


under A, we may forget the first inclusion and homotopy to get the cocone

         a₁
A₁ ---> A₂ ---> ⋯
|      /
|     /
i₁ |    / i₂
|   /
∨  ∨
X


under A[1]. We denote this cocone c[1]. Inductively, we define c[k + 1] ≐ c[k][1].

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

         a₁
A₁ ---> A₂ ---> ⋯
|      /
|     /
i₁ |    / i₂
|   /
∨  ∨
X


under A[1], we may prepend a map

           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.

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

     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].

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]

         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].

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

        a₀      a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
|       |       |
a₀ |       | a₁    | a₂
∨       ∨       ∨
A₁ ---> A₂ ---> A₃ ---> ⋯
a₁      a₂


commute by reflexivity.

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.

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.

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

     a₀      a₁      a₂
A₀ ---> A₁ ---> A₂ ---> ⋯ --> X,


there is a commuting triangle

              cocone-map
X → Y ------------> cocone A Y
\           /
cocone-map  \       /
∨   ∨
cocone A[1] Y.


Inductively, we compose this triangle in the following way

              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

              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].

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∞.

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)


### Unshifting cocones under sequential diagrams is homotopic to precomposing them with shift inclusion morphisms

Given a cocone c

         a₁
A₁ ---> A₂ ---> ⋯
|      /
|     /
i₁ |    / i₂
|   /
∨  ∨
X


under A[1], we have two way of turning it into a cocone under A --- we can unshift it, which gives the cocone

           a₀      a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
\      |      /
\     |     /
i₁ ∘ a₀ \    | i₁ / i₂
\   |   /
∨  ∨  ∨
X ,


or we can prepend the inclusion morphism hom-shift-sequential-diagram : A → A[1] to get

         a₀
A₀ ---> A₁ ---> ⋯
|       |
a₀ |       | a₁
∨   a₁  ∨
A₁ ---> A₂ ---> ⋯
|      /
|     /
i₁ |    / i₂
|   /
∨  ∨
X .


We show that these two cocones are homotopic.

module _
{l1 l2 : Level} {A : sequential-diagram l1}
{X : UU l2}
(c : cocone-sequential-diagram (shift-once-sequential-diagram A) X)
where

htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram :
htpy-cocone-sequential-diagram
( unshift-once-cocone-sequential-diagram A c)
( map-cocone-hom-sequential-diagram
( hom-shift-once-sequential-diagram A)
( c))
pr1 htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram
zero-ℕ = refl-htpy
pr1 htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram
(succ-ℕ n) = coherence-cocone-sequential-diagram c n
pr2 htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram
zero-ℕ = inv-htpy-right-unit-htpy
pr2 htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram
(succ-ℕ n) =
left-whisker-concat-htpy
( coherence-cocone-sequential-diagram c n)
( inv-htpy-right-unit-htpy)


As a corollary, taking a cocone c under A, shifting it and prepending the shift inclusion morphism results in a cocone homotopic to c, i.e.,

         a₀      a₁
A₀ ---> A₁ ---> A₂ ---> ⋯
|       |       |                     a₀      a₁
a₀ |       | a₁    | a₂              A₀ ---> A₁ ---> A₂ ---> ⋯
∨   a₁  ∨   a₂  ∨                  \      |      /
A₁ ---> A₂ ---> A₃ ---> ⋯    ~      \     | i₁  /
\      |      /                  i₀ \    |    / i₂
\     |     /                       \   |   /
i₁ \    | i₂ / i₃                      ∨  ∨  ∨
\   |   /                             X .
∨  ∨  ∨
X


Proof: We first use the above lemma, which says that the left cocone is homotopic to c[1][-1], and then we use the fact that unshifting is a retraction.

module _
{l1 l2 : Level} {A : sequential-diagram l1}
{X : UU l2} (c : cocone-sequential-diagram A X)
where

inv-compute-map-cocone-hom-shift-sequential-diagram :
htpy-cocone-sequential-diagram
( c)
( map-cocone-hom-sequential-diagram
( hom-shift-once-sequential-diagram A)
( shift-once-cocone-sequential-diagram c))
inv-compute-map-cocone-hom-shift-sequential-diagram =
concat-htpy-cocone-sequential-diagram
( inv-htpy-is-retraction-unshift-once-cocone-sequential-diagram c)
( htpy-cocone-unshift-cocone-map-cocone-hom-shift-sequential-diagram
( shift-once-cocone-sequential-diagram c))

compute-map-cocone-hom-shift-sequential-diagram :
htpy-cocone-sequential-diagram
( map-cocone-hom-sequential-diagram
( hom-shift-once-sequential-diagram A)
( shift-once-cocone-sequential-diagram c))
( c)
compute-map-cocone-hom-shift-sequential-diagram =
inv-htpy-cocone-sequential-diagram
( inv-compute-map-cocone-hom-shift-sequential-diagram)


### Inclusion morphisms of shifting sequential diagrams induce the identity map on sequential colimits

Given a sequential diagram (A, a) with a colimit X, then we know that for every natural number k

• X is also a sequential colimit of A[k] and
• there is a morphism A → A[k], inducing a map between colimits.

Together they give a map X → X, which we show here to be the identity map.

Proof: By induction on k; for the base case, observe that A → A[0] is the identity morphism, which gets sent to the identity map by functoriality of sequential colimits.

For the inductive case, observe that the inclusion morphism A → A[k + 1] is defined as the composition A → A[k] → A[k + 1], so by functoriality the induced map is the composition of the maps induced by A → A[k] and A[k] → A[k + 1]. The first induced map is the identity map by the inductive hypothesis. The second induced map is defined to be the map obtained by the universal property of X as a colimit of A[k] from the cocone c[k + 1] precomposed by the inclusion A[k] → A[k + 1]. We have seen above that this precomposition results in a cocone homotopic to c[k], so the map induced by A[k] → A[k + 1] is homotopic to the one induced by c[k]. But c[k] is the cocone of the sequential colimit of A[k], so it also induces the identity map.

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

compute-map-colimit-hom-shift-once-sequential-diagram :
map-sequential-colimit-hom-sequential-diagram
( up-c)
( shift-once-cocone-sequential-diagram c)
( hom-shift-once-sequential-diagram A) ~
id
compute-map-colimit-hom-shift-once-sequential-diagram =
( htpy-map-universal-property-htpy-cocone-sequential-diagram
( up-c)
( compute-map-cocone-hom-shift-sequential-diagram c)) ∙h
( compute-map-universal-property-sequential-colimit-id up-c)

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

compute-map-colimit-hom-shift-sequential-diagram :
(k : ℕ) →
map-sequential-colimit-hom-sequential-diagram
( up-c)
( shift-cocone-sequential-diagram k c)
( hom-shift-sequential-diagram A k) ~
id
compute-map-colimit-hom-shift-sequential-diagram zero-ℕ =
preserves-id-map-sequential-colimit-hom-sequential-diagram up-c
compute-map-colimit-hom-shift-sequential-diagram (succ-ℕ k) =
( preserves-comp-map-sequential-colimit-hom-sequential-diagram
( up-c)
( up-shift-cocone-sequential-diagram k up-c)
( shift-cocone-sequential-diagram (succ-ℕ k) c)
( hom-shift-once-sequential-diagram (shift-sequential-diagram k A))
( hom-shift-sequential-diagram A k)) ∙h
( horizontal-concat-htpy
( compute-map-colimit-hom-shift-once-sequential-diagram
( up-shift-cocone-sequential-diagram k up-c))
( compute-map-colimit-hom-shift-sequential-diagram k))