Flattening lemma for descent data for sequential colimits

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

src/foundation/functoriality-dependent-pair-types.lagda.md

@@ -301,6 +301,33 @@ module _
   coherence-square-maps-map-Σ-map-base H (a , p) = eq-pair-Σ (H a) refl
 ```
 
+### Commuting triangles of maps on total spaces
+
+#### Functoriality of `Σ` preserves commuting triangles of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 : Level}
+  {A : UU l1} {P : A → UU l2}
+  {B : UU l3} {Q : B → UU l4}
+  {C : UU l5} (R : C → UU l6)
+  {left' : A → C} {right' : B → C} {top' : A → B}
+  (left : (a : A) → P a → R (left' a))
+  (right : (b : B) → Q b → R (right' b))
+  (top : (a : A) → P a → Q (top' a))
+  where
+
+  coherence-triangle-maps-Σ :
+    {H' : coherence-triangle-maps left' right' top'} →
+    ( (a : A) (p : P a) →
+      dependent-identification R (H' a) (left _ p) (right _ (top _ p))) →
+    coherence-triangle-maps
+      ( map-Σ R left' left)
+      ( map-Σ R right' right)
+      ( map-Σ Q top' top)
+  coherence-triangle-maps-Σ {H'} H (a , p) = eq-pair-Σ (H' a) (H a p)
+```
+
 #### `map-Σ-map-base` preserves commuting triangles of maps
 
 ```agda

src/synthetic-homotopy-theory.lagda.md

@@ -53,6 +53,7 @@ open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-se
 open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
+open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
 open import synthetic-homotopy-theory.flattening-lemma-sequential-colimits public
@@ -104,6 +105,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-cocones-families-sequential-diagrams 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

src/synthetic-homotopy-theory/families-descent-data-sequential-colimits.lagda.md

@@ -0,0 +1,205 @@
+# Families with descent data for sequential colimits
+
+```agda
+module synthetic-homotopy-theory.families-descent-data-sequential-colimits where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equivalences
+open import foundation.transport-along-identifications
+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.descent-data-sequential-colimits
+open import synthetic-homotopy-theory.sequential-diagrams
+```
+
+</details>
+
+## Idea
+
+As shown in
+[`descent-property-sequential-colimits`](synthetic-homotopy-theory.descent-property-sequential-colimits.md),
+the type of type families over
+[sequential colimits](synthetic-homotopy-theory.universal-property-sequential-colimits.md)
+is [equivalent](foundation-core.equivalences.md) to
+[descent data](synthetic-homotopy-theory.descent-data-sequential-colimits.md).
+
+Sometimes it is useful to consider tripes `(P, B, e)` where `P : X → 𝒰` is a
+type family, `B` is descent data, and `e` is an equivalence between `B` and the
+descent data induced by `P`. The type of such pairs `(B, e)` is
+[contractible](foundation-core.contractible-types.md), so the type of these
+triples is equivalent to the type of type families over `X`, but it may be more
+ergonomic to characterize descent data of a particular type family, and then
+have theorems know about this characterization, rather than transporting along
+such a characterization after the fact.
+
+## Definitions
+
+### Families over a cocone equipped with corresponding descent data for sequential colimits
+
+```agda
+module _
+  {l1 l2 : Level} {A : sequential-diagram l1}
+  {X : UU l2} (c : cocone-sequential-diagram A X)
+  where
+
+  family-with-descent-data-sequential-colimit :
+    (l3 : Level) → UU (l1 ⊔ l2 ⊔ lsuc l3)
+  family-with-descent-data-sequential-colimit l3 =
+    Σ ( X → UU l3)
+      ( λ P →
+        Σ ( descent-data-sequential-colimit A l3)
+          ( λ B →
+            equiv-descent-data-sequential-colimit
+              ( B)
+              ( descent-data-family-cocone-sequential-diagram c P)))
+```
+
+### Components of a family with corresponding descent data for sequential colimits
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : sequential-diagram l1}
+  {X : UU l2} {c : cocone-sequential-diagram A X}
+  (P : family-with-descent-data-sequential-colimit c l3)
+  where
+
+  family-cocone-family-with-descent-data-sequential-colimit : X → UU l3
+  family-cocone-family-with-descent-data-sequential-colimit = pr1 P
+
+  descent-data-family-with-descent-data-sequential-colimit :
+    descent-data-sequential-colimit A l3
+  descent-data-family-with-descent-data-sequential-colimit = pr1 (pr2 P)
+
+  family-family-with-descent-data-sequential-colimit :
+    (n : ℕ) → family-sequential-diagram A n → UU l3
+  family-family-with-descent-data-sequential-colimit =
+    family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+
+  equiv-family-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-family-with-descent-data-sequential-colimit n a ≃
+    family-family-with-descent-data-sequential-colimit
+      ( succ-ℕ n)
+      ( map-sequential-diagram A n a)
+  equiv-family-family-with-descent-data-sequential-colimit =
+    equiv-family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+
+  map-family-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-family-with-descent-data-sequential-colimit n a →
+    family-family-with-descent-data-sequential-colimit
+      ( succ-ℕ n)
+      ( map-sequential-diagram A n a)
+  map-family-family-with-descent-data-sequential-colimit =
+    map-family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+
+  is-equiv-map-family-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    is-equiv (map-family-family-with-descent-data-sequential-colimit n a)
+  is-equiv-map-family-family-with-descent-data-sequential-colimit =
+    is-equiv-map-family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+
+  dependent-sequential-diagram-family-with-descent-data-sequential-colimit :
+    dependent-sequential-diagram A l3
+  dependent-sequential-diagram-family-with-descent-data-sequential-colimit =
+    dependent-sequential-diagram-descent-data
+      ( descent-data-family-with-descent-data-sequential-colimit)
+
+  equiv-descent-data-family-with-descent-data-sequential-colimit :
+    equiv-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( descent-data-family-cocone-sequential-diagram c
+        ( family-cocone-family-with-descent-data-sequential-colimit))
+  equiv-descent-data-family-with-descent-data-sequential-colimit = pr2 (pr2 P)
+
+  equiv-equiv-descent-data-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( n)
+      ( a) ≃
+    family-cocone-family-with-descent-data-sequential-colimit
+      ( map-cocone-sequential-diagram c n a)
+  equiv-equiv-descent-data-family-with-descent-data-sequential-colimit =
+    equiv-equiv-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( descent-data-family-cocone-sequential-diagram c
+        ( family-cocone-family-with-descent-data-sequential-colimit))
+      ( equiv-descent-data-family-with-descent-data-sequential-colimit)
+
+  map-equiv-descent-data-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    family-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( n)
+      ( a) →
+    family-cocone-family-with-descent-data-sequential-colimit
+      ( map-cocone-sequential-diagram c n a)
+  map-equiv-descent-data-family-with-descent-data-sequential-colimit =
+    map-equiv-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( descent-data-family-cocone-sequential-diagram c
+        ( family-cocone-family-with-descent-data-sequential-colimit))
+      ( equiv-descent-data-family-with-descent-data-sequential-colimit)
+
+  is-equiv-map-equiv-descent-data-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    is-equiv
+      ( map-equiv-descent-data-family-with-descent-data-sequential-colimit n a)
+  is-equiv-map-equiv-descent-data-family-with-descent-data-sequential-colimit =
+    is-equiv-map-equiv-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( descent-data-family-cocone-sequential-diagram c
+        ( family-cocone-family-with-descent-data-sequential-colimit))
+      ( equiv-descent-data-family-with-descent-data-sequential-colimit)
+
+  coherence-square-equiv-descent-data-family-with-descent-data-sequential-colimit :
+    (n : ℕ) (a : family-sequential-diagram A n) →
+    coherence-square-maps
+      ( map-equiv-descent-data-family-with-descent-data-sequential-colimit n a)
+      ( map-family-family-with-descent-data-sequential-colimit n a)
+      ( tr
+        ( family-cocone-family-with-descent-data-sequential-colimit)
+        ( coherence-cocone-sequential-diagram c n a))
+      ( map-equiv-descent-data-family-with-descent-data-sequential-colimit
+        ( succ-ℕ n)
+        ( map-sequential-diagram A n a))
+  coherence-square-equiv-descent-data-family-with-descent-data-sequential-colimit =
+    coh-equiv-descent-data-sequential-colimit
+      ( descent-data-family-with-descent-data-sequential-colimit)
+      ( descent-data-family-cocone-sequential-diagram c
+        ( family-cocone-family-with-descent-data-sequential-colimit))
+      ( equiv-descent-data-family-with-descent-data-sequential-colimit)
+```
+
+### A type family equipped with its induced descent data for sequential colimits
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : sequential-diagram l1}
+  {X : UU l2} (c : cocone-sequential-diagram A X)
+  (P : X → UU l3)
+  where
+
+  family-with-descent-data-family-cocone-sequential-diagram :
+    family-with-descent-data-sequential-colimit c l3
+  pr1 family-with-descent-data-family-cocone-sequential-diagram = P
+  pr1 (pr2 family-with-descent-data-family-cocone-sequential-diagram) =
+    descent-data-family-cocone-sequential-diagram c P
+  pr2 (pr2 family-with-descent-data-family-cocone-sequential-diagram) =
+    id-equiv-descent-data-sequential-colimit
+      ( descent-data-family-cocone-sequential-diagram c P)
+```