Descent data for sequential colimits and its version of the flattenin…

…g lemma (#1109)

Sorry, this is bigger than I anticipated...

This PR
- defines morphisms and equivalences between dependent sequential
diagrams
- defines morphisms and equivalences of cocones under morphisms and
equivalences of sequential diagrams
- defines equifibered sequential diagrams
- defines descent data for sequential colimits
- shows the descent property of sequential colimits
- proves a version of the flattening lemma expressed with families with
associated descent data
- collects various helpers for converting between sequential stuff and
coequalizer stuff into one file
- adds some auxiliary infrastructure along the way

I took care to properly separate the work into commits, so it might be
more digestible to review it commit by commit.

This is progress towards #1080

src/foundation-core/commuting-prisms-of-maps.lagda.md

@@ -7,8 +7,12 @@ module foundation-core.commuting-prisms-of-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
+open import foundation.commuting-pentagons-of-identifications
+open import foundation.identity-types
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
+open import foundation.whiskering-identifications-concatenation
 
 open import foundation-core.commuting-squares-of-maps
 open import foundation-core.commuting-triangles-of-maps
@@ -249,6 +253,46 @@ module _
             ( (hC ·l top) ∙h (inv-right ·r h ∙h (g' ·l inv-left)))
             ( H))))
 
+  module _
+    ( top : coherence-triangle-maps f g h)
+    ( inv-front : coherence-square-maps f hA hC f')
+    ( inv-right : coherence-square-maps g hB hC g')
+    ( inv-left : coherence-square-maps h hA hB h')
+    ( bottom : coherence-triangle-maps f' g' h')
+    where
+
+    vertical-coherence-prism-inv-squares-maps-vertical-coherence-prism-maps :
+      vertical-coherence-prism-maps f g h f' g' h' hA hB hC
+        ( top)
+        ( inv-front)
+        ( inv-right)
+        ( inv-left)
+        ( bottom) →
+      vertical-coherence-prism-inv-squares-maps f g h f' g' h' hA hB hC
+        ( top)
+        ( inv-htpy inv-front)
+        ( inv-htpy inv-right)
+        ( inv-htpy inv-left)
+        ( bottom)
+    vertical-coherence-prism-inv-squares-maps-vertical-coherence-prism-maps
+      H a =
+      ( reflect-top-left-coherence-pentagon-identifications
+        ( bottom (hA a))
+        ( inv-front a)
+        ( ap g' (inv-left a))
+        ( ap hC (top a))
+        ( inv-right (h a))
+        ( inv
+          ( ( assoc (bottom (hA a)) (ap g' (inv-left a)) (inv-right (h a))) ∙
+            ( H a)))) ∙
+      ( left-whisker-concat
+        ( ap hC (top a) ∙ inv (inv-right (h a)))
+        ( inv (ap-inv g' (inv-left a)))) ∙
+      ( assoc
+        ( ap hC (top a))
+        ( inv (inv-right (h a)))
+        ( ap g' (inv (inv-left a))))
+
   module _
     ( inv-top : coherence-triangle-maps' f g h)
     ( inv-front : coherence-square-maps' f hA hC f')

src/foundation/commuting-pentagons-of-identifications.lagda.md

@@ -7,6 +7,7 @@ module foundation.commuting-pentagons-of-identifications where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.universe-levels
 
 open import foundation-core.identity-types
@@ -19,14 +20,14 @@ open import foundation-core.identity-types
 A pentagon of [identifications](foundation-core.identity-types.md)
 
 ```text
-             top
-           x --- y
-top-left  /       \ top-right
-         /         \
-        z           w
-          \       /
-bottom-left \   / bottom-right
-              v
+               top
+             x --- y
+   top-left /       \ top-right
+           /         \
+          z           w
+            \       /
+  bottom-left \   / bottom-right
+                v
 ```
 
 is said to **commute** if there is an identification
@@ -37,7 +38,9 @@ is said to **commute** if there is an identification
 
 Such an identification is called a **coherence** of the pentagon.
 
-## Definition
+## Definitions
+
+### Commuting pentagons of identifications
 
 ```agda
 module _
@@ -52,3 +55,139 @@ module _
     top top-left top-right bottom-left bottom-right =
     top-left ∙ bottom-left ＝ (top ∙ top-right) ∙ bottom-right
 ```
+
+### Reflections of commuting pentagons of identifications
+
+A pentagon may be reflected along an axis connecting an edge with its opposing
+vertex. For example, we may reflect a pentagon
+
+```text
+               top
+             x --- y
+   top-left /       \ top-right
+           /         \
+          z           w
+            \       /
+  bottom-left \   / bottom-right
+                v
+```
+
+along the axis connecting `top` and `v` to get
+
+```text
+               top⁻¹
+              y --- x
+   top-right /       \ top-left
+            /         \
+           w           z
+             \       /
+  bottom-right \   / bottom-left
+                 v .
+```
+
+The reflections are named after the edge which the axis passes through, so the
+above example is `reflect-top-coherence-pentagon-identifications`.
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z w v : A}
+  where
+
+  reflect-top-coherence-pentagon-identifications :
+    (top : x ＝ y)
+    (top-left : x ＝ z) (top-right : y ＝ w)
+    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
+    coherence-pentagon-identifications
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( bottom-left)
+      ( bottom-right) →
+    coherence-pentagon-identifications
+      ( inv top)
+      ( top-right)
+      ( top-left)
+      ( bottom-right)
+      ( bottom-left)
+  reflect-top-coherence-pentagon-identifications
+    refl top-left top-right bottom-left bottom-right H = inv H
+
+  reflect-top-left-coherence-pentagon-identifications :
+    (top : x ＝ y)
+    (top-left : x ＝ z) (top-right : y ＝ w)
+    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
+    coherence-pentagon-identifications
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( bottom-left)
+      ( bottom-right) →
+    coherence-pentagon-identifications
+      ( bottom-left)
+      ( inv top-left)
+      ( inv bottom-right)
+      ( top)
+      ( inv top-right)
+  reflect-top-left-coherence-pentagon-identifications
+    refl refl refl bottom-left refl H =
+    inv (right-unit ∙ right-unit ∙ H)
+
+  reflect-top-right-coherence-pentagon-identifications :
+    (top : x ＝ y)
+    (top-left : x ＝ z) (top-right : y ＝ w)
+    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
+    coherence-pentagon-identifications
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( bottom-left)
+      ( bottom-right) →
+    coherence-pentagon-identifications
+      ( inv bottom-right)
+      ( inv bottom-left)
+      ( inv top-right)
+      ( inv top-left)
+      ( inv top)
+  reflect-top-right-coherence-pentagon-identifications
+    refl top-left refl refl refl H =
+    ap inv (inv right-unit ∙ H)
+
+  reflect-bottom-left-coherence-pentagon-identifications :
+    (top : x ＝ y)
+    (top-left : x ＝ z) (top-right : y ＝ w)
+    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
+    coherence-pentagon-identifications
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( bottom-left)
+      ( bottom-right) →
+    coherence-pentagon-identifications
+      ( inv top-right)
+      ( bottom-right)
+      ( inv top)
+      ( inv bottom-left)
+      ( top-left)
+  reflect-bottom-left-coherence-pentagon-identifications
+    refl refl refl refl bottom-right H = right-unit ∙ inv H
+
+  reflect-bottom-right-coherence-pentagon-identifications :
+    (top : x ＝ y)
+    (top-left : x ＝ z) (top-right : y ＝ w)
+    (bottom-left : z ＝ v) (bottom-right : w ＝ v) →
+    coherence-pentagon-identifications
+      ( top)
+      ( top-left)
+      ( top-right)
+      ( bottom-left)
+      ( bottom-right) →
+    coherence-pentagon-identifications
+      ( bottom-left)
+      ( inv top-left)
+      ( inv bottom-right)
+      ( top)
+      ( inv top-right)
+  reflect-bottom-right-coherence-pentagon-identifications
+    refl refl refl bottom-left refl H =
+    inv (right-unit ∙ right-unit ∙ H)
+```

src/foundation/commuting-triangles-of-identifications.lagda.md

@@ -455,21 +455,6 @@ module _
   compute-refl-top-map-coherence-triangle-identifications p = refl
 ```
 
-### The action of functions on commuting triangles of identifications
-
-```agda
-module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
-  {x y z : A} (left : x ＝ z) (right : y ＝ z) (top : x ＝ y)
-  where
-
-  action-function-coherence-triangle-identifications :
-    coherence-triangle-identifications left right top →
-    coherence-triangle-identifications (ap f left) (ap f right) (ap f top)
-  action-function-coherence-triangle-identifications s =
-    ap (ap f) s ∙ ap-concat f top right
-```
-
 ### Inverting one side of a commuting triangle of identifications
 
 ```agda
@@ -588,6 +573,21 @@ module _
         ( t))
 ```
 
+### Inverting all sides of a commuting triangle of identifications
+
+```agda
+module _
+  {l1 : Level} {A : UU l1} {x y z : A}
+  where
+
+  inv-coherence-triangle-identifications :
+    (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) →
+    coherence-triangle-identifications left right top →
+    coherence-triangle-identifications (inv left) (inv top) (inv right)
+  inv-coherence-triangle-identifications .(top ∙ right) right top refl =
+    distributive-inv-concat top right
+```
+
 ### Concatenating identifications on edges with coherences of commuting triangles of identifications
 
 ```agda