Shifts and unshifts

UniMath · Mar 14, 2024 · 8e55f95 · 8e55f95
1 parent 165dcb3
commit 8e55f95
Show file tree

Hide file tree

Showing 3 changed files with 606 additions and 193 deletions.
diff --git a/src/papers/SDR20.lagda.md b/src/papers/SDR20.lagda.md
@@ -64,18 +64,18 @@ import synthetic-homotopy-theory.functoriality-sequential-colimits using
 Lemma 3.6: Dropping a head of a sequential diagram preserves the sequential
 colimit.
 
-TODO: the actual equivalence
-
 ```agda
 import synthetic-homotopy-theory.shifts-sequential-diagrams using
-  ( up-cocone-shift-sequential-diagram)
+  ( up-cocone-shift-sequential-diagram ;
+    compute-sequential-colimit-shift-sequential-diagram) -- apply to 1
 ```
 
 Lemma 3.7: Dropping finitely many objects from the head of a sequential diagram
 preserves the sequential colimit.
 
 ```agda
--- TODO
+import synthetic-homotopy-theory.shifts-sequential-diagrams using
+  ( compute-sequential-colimit-shift-sequential-diagram)
 ```
 
 Liftings?

diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md
@@ -154,6 +154,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