Shifts and unshifts of concepts around sequential colimits

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

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

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

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

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

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