Flattening lemma for sequential colimits (#972)

Resolves #869

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

@@ -8,8 +8,10 @@ module foundation.commuting-triangles-of-identifications where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.path-algebra
 open import foundation.universe-levels
 
+open import foundation-core.equivalences
 open import foundation-core.function-types
 open import foundation-core.homotopies
 open import foundation-core.identity-types
@@ -47,3 +49,153 @@ module _
     (left : x ＝ z) (right : y ＝ z) (top : x ＝ y) → UU l
   coherence-triangle-identifications' left right top = (top ∙ right) ＝ left
 ```
+
+## Properties
+
+### Whiskering of triangles of identifications
+
+Given a commuting triangle of identifications
+
+```text
+       top
+    x ----- y
+     \     /
+ left \   / right
+       \ /
+        z     ,
+```
+
+we may consider three ways of attaching new identifications to it: prepending
+`p : u ＝ x` to the left, which gives us a commuting triangle
+
+```text
+         p ∙ top
+        u ----- y
+         \     /
+ p ∙ left \   / right
+           \ /
+            z     ,
+```
+
+or appending an identification `p : z ＝ u` to the right, which gives
+
+```text
+           top
+        u ----- y
+         \     /
+ left ∙ p \   / right ∙ p
+           \ /
+            z     ,
+```
+
+or splicing an identification `p : y ＝ u` and its inverse into the middle, to
+get
+
+```text
+     top ∙ p
+    u ----- y
+     \     /
+ left \   / p⁻¹ ∙ right
+       \ /
+        z     ,
+```
+
+which isn't formalized yet.
+
+Because concatenation of identifications is an equivalence, it follows that all
+of these transformations are equivalences.
+
+These lemmas are useful in proofs involving path algebra, because taking
+`equiv-right-whisk-triangle-identicications` as an example, it provides us with
+two maps: the forward direction states `(p ＝ q ∙ r) → (p ∙ s ＝ q ∙ (r ∙ s))`,
+which allows one to append an identification without needing to reassociate on
+the right, and the backwards direction conversely allows one to cancel out an
+identification in parentheses.
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z u : A}
+  (left : x ＝ z) (top : x ＝ y) {right : y ＝ z} (p : z ＝ u)
+  where
+
+  equiv-right-whisk-triangle-identifications :
+    ( coherence-triangle-identifications left right top) ≃
+    ( coherence-triangle-identifications (left ∙ p) (right ∙ p) top)
+  equiv-right-whisk-triangle-identifications =
+    ( equiv-concat-assoc' (left ∙ p) top right p) ∘e
+    ( equiv-identification-right-whisk p)
+
+  right-whisk-triangle-identifications :
+    coherence-triangle-identifications left right top →
+    coherence-triangle-identifications (left ∙ p) (right ∙ p) top
+  right-whisk-triangle-identifications =
+    map-equiv equiv-right-whisk-triangle-identifications
+
+  right-unwhisk-triangle-identifications :
+    coherence-triangle-identifications (left ∙ p) (right ∙ p) top →
+    coherence-triangle-identifications left right top
+  right-unwhisk-triangle-identifications =
+    map-inv-equiv equiv-right-whisk-triangle-identifications
+
+  equiv-right-whisk-triangle-identifications' :
+    ( coherence-triangle-identifications' left right top) ≃
+    ( coherence-triangle-identifications' (left ∙ p) (right ∙ p) top)
+  equiv-right-whisk-triangle-identifications' =
+    ( equiv-concat-assoc top right p (left ∙ p)) ∘e
+    ( equiv-identification-right-whisk p)
+
+  right-whisk-triangle-identifications' :
+    coherence-triangle-identifications' left right top →
+    coherence-triangle-identifications' (left ∙ p) (right ∙ p) top
+  right-whisk-triangle-identifications' =
+    map-equiv equiv-right-whisk-triangle-identifications'
+
+  right-unwhisk-triangle-identifications' :
+    coherence-triangle-identifications' (left ∙ p) (right ∙ p) top →
+    coherence-triangle-identifications' left right top
+  right-unwhisk-triangle-identifications' =
+    map-inv-equiv equiv-right-whisk-triangle-identifications'
+
+module _
+  {l : Level} {A : UU l} {x y z u : A}
+  (p : u ＝ x) {left : x ＝ z} {right : y ＝ z} {top : x ＝ y}
+  where
+
+  equiv-left-whisk-triangle-identifications :
+    ( coherence-triangle-identifications left right top) ≃
+    ( coherence-triangle-identifications (p ∙ left) right (p ∙ top))
+  equiv-left-whisk-triangle-identifications =
+    ( inv-equiv (equiv-concat-assoc' (p ∙ left) p top right)) ∘e
+    ( equiv-identification-left-whisk p)
+
+  left-whisk-triangle-identifications :
+    coherence-triangle-identifications left right top →
+    coherence-triangle-identifications (p ∙ left) right (p ∙ top)
+  left-whisk-triangle-identifications =
+    map-equiv equiv-left-whisk-triangle-identifications
+
+  left-unwhisk-triangle-identifications :
+    coherence-triangle-identifications (p ∙ left) right (p ∙ top) →
+    coherence-triangle-identifications left right top
+  left-unwhisk-triangle-identifications =
+    map-inv-equiv equiv-left-whisk-triangle-identifications
+
+  equiv-left-whisk-triangle-identifications' :
+    ( coherence-triangle-identifications' left right top) ≃
+    ( coherence-triangle-identifications' (p ∙ left) right (p ∙ top))
+  equiv-left-whisk-triangle-identifications' =
+    ( inv-equiv (equiv-concat-assoc p top right (p ∙ left))) ∘e
+    ( equiv-identification-left-whisk p)
+
+  left-whisk-triangle-identifications' :
+    coherence-triangle-identifications' left right top →
+    coherence-triangle-identifications' (p ∙ left) right (p ∙ top)
+  left-whisk-triangle-identifications' =
+    map-equiv equiv-left-whisk-triangle-identifications'
+
+  left-unwhisk-triangle-identifications' :
+    coherence-triangle-identifications' (p ∙ left) right (p ∙ top) →
+    coherence-triangle-identifications' left right top
+  left-unwhisk-triangle-identifications' =
+    map-inv-equiv equiv-left-whisk-triangle-identifications'
+```

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

@@ -19,6 +19,7 @@ open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universe-levels
 
 open import foundation-core.commuting-squares-of-maps
+open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.dependent-identifications
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
@@ -375,6 +376,24 @@ module _
   coherence-square-maps-map-Σ-map-base H (a , p) = eq-pair-Σ (H a) refl
 ```
 
+#### `map-Σ-map-base` preserves commuting triangles of maps
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} (S : X → UU l4)
+  (left : A → X) (right : B → X) (top : A → B)
+  where
+
+  coherence-triangle-maps-map-Σ-map-base :
+    (H : coherence-triangle-maps left right top) →
+    coherence-triangle-maps
+      ( map-Σ-map-base left S)
+      ( map-Σ-map-base right S)
+      ( map-Σ (S ∘ right) top (λ a → tr S (H a)))
+  coherence-triangle-maps-map-Σ-map-base H (a , _) = eq-pair-Σ (H a) refl
+```
+
 ### The action of `map-Σ-map-base` on identifications of the form `eq-pair-Σ` is given by the action on the base
 
 ```agda

src/foundation/morphisms-arrows.lagda.md

@@ -10,9 +10,11 @@ module foundation.morphisms-arrows where
 open import foundation.action-on-identifications-functions
 open import foundation.commuting-squares-of-homotopies
 open import foundation.commuting-squares-of-identifications
+open import foundation.commuting-triangles-of-identifications
 open import foundation.dependent-pair-types
 open import foundation.fundamental-theorem-of-identity-types
 open import foundation.homotopy-induction
+open import foundation.path-algebra
 open import foundation.structure-identity-principle
 open import foundation.universe-levels
 
@@ -163,7 +165,7 @@ module _
     coh-comp-hom-arrow
 ```
 
-### Homotopies of morphsims of arrows
+### Homotopies of morphisms of arrows
 
 A **homotopy of morphisms of arrows** from `(i , j , H)` to `(i' , j' , H')` is
 a triple `(I , J , K)` consisting of homotopies `I : i ~ i'` and `J : j ~ j'`
@@ -377,60 +379,36 @@ module _
       ( htpy-domain-left-whisker-htpy-hom-arrow)
       ( htpy-codomain-left-whisker-htpy-hom-arrow)
   coh-left-whisker-htpy-hom-arrow a =
-    ( inv
-      ( ap
-        ( concat _ _)
-        ( ap-comp h
-          ( map-domain-hom-arrow g h γ)
-          ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
-    ( assoc
+    ( left-whisk-triangle-identifications'
       ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g α a))
+      ( ( ap
+          ( coh-hom-arrow g h γ (map-domain-hom-arrow f g α a) ∙_)
+          ( inv
+            ( ap-comp h
+              ( map-domain-hom-arrow g h γ)
+              ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
+        ( nat-htpy
+          ( coh-hom-arrow g h γ)
+          ( htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
+    ( right-whisk-square-identification
       ( ap
-        ( h ∘ map-domain-hom-arrow g h γ)
-        ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-    ( ap
-      ( concat
-        ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-        ( h _))
-      ( nat-htpy
-        ( coh-hom-arrow g h γ)
-        ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-    ( inv
-      ( assoc
-        ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-        ( ap
-          ( map-codomain-hom-arrow g h γ ∘ g)
-          ( htpy-domain-htpy-hom-arrow f g α β H a))
-        ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))) ∙
-    ( ap
-      ( concat' _ (coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))
+        ( map-codomain-hom-arrow g h γ)
+        ( htpy-codomain-htpy-hom-arrow f g α β H (f a)))
+      ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
+      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a))
       ( ( ap
-          ( concat
-            ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a))
-            ( _))
+          ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g α a) ∙_)
           ( ap-comp
             ( map-codomain-hom-arrow g h γ)
             ( g)
             ( htpy-domain-htpy-hom-arrow f g α β H a))) ∙
-        ( ( inv
-            ( ap-concat
-              ( map-codomain-hom-arrow g h γ)
-              ( coh-hom-arrow f g α a)
-              ( ap g (htpy-domain-htpy-hom-arrow f g α β H a)))) ∙
-          ( ap
-            ( ap (map-codomain-hom-arrow g h γ))
-            ( coh-htpy-hom-arrow f g α β H a)) ∙
-          ( ap-concat
-            ( map-codomain-hom-arrow g h γ)
-            ( htpy-codomain-htpy-hom-arrow f g α β H (f a))
-            ( coh-hom-arrow f g β a))))) ∙
-    ( assoc
-      ( ap
-        ( map-codomain-hom-arrow g h γ)
-        ( htpy-codomain-htpy-hom-arrow f g α β H (f a)))
-      ( ap (map-codomain-hom-arrow g h γ) (coh-hom-arrow f g β a))
-      ( coh-hom-arrow g h γ (map-domain-hom-arrow f g β a)))
+        ( coherence-square-identifications-ap
+          ( map-codomain-hom-arrow g h γ)
+          ( htpy-codomain-htpy-hom-arrow f g α β H (f a))
+          ( coh-hom-arrow f g α a)
+          ( coh-hom-arrow f g β a)
+          ( ap g (htpy-domain-htpy-hom-arrow f g α β H a))
+          ( coh-htpy-hom-arrow f g α β H a))))
 
   left-whisker-htpy-hom-arrow :
     htpy-hom-arrow f h

src/foundation/type-arithmetic-dependent-pair-types.lagda.md

@@ -201,13 +201,17 @@ module _
   pr1 associative-Σ = map-associative-Σ
   pr2 associative-Σ = is-equiv-map-associative-Σ
 
+  abstract
+    is-equiv-map-inv-associative-Σ : is-equiv map-inv-associative-Σ
+    is-equiv-map-inv-associative-Σ =
+      is-equiv-is-invertible
+        map-associative-Σ
+        is-retraction-map-inv-associative-Σ
+        is-section-map-inv-associative-Σ
+
   inv-associative-Σ : Σ A (λ x → Σ (B x) (λ y → C (x , y))) ≃ Σ (Σ A B) C
   pr1 inv-associative-Σ = map-inv-associative-Σ
-  pr2 inv-associative-Σ =
-    is-equiv-is-invertible
-      map-associative-Σ
-      is-retraction-map-inv-associative-Σ
-      is-section-map-inv-associative-Σ
+  pr2 inv-associative-Σ = is-equiv-map-inv-associative-Σ
 ```
 
 ### Associativity, second formulation

src/synthetic-homotopy-theory.lagda.md

@@ -48,6 +48,7 @@ open import synthetic-homotopy-theory.eckmann-hilton-argument public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams 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
 open import synthetic-homotopy-theory.free-loops public
 open import synthetic-homotopy-theory.functoriality-loop-spaces public
 open import synthetic-homotopy-theory.functoriality-sequential-colimits public

src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md

@@ -31,7 +31,7 @@ open import synthetic-homotopy-theory.universal-property-pushouts
 
 ## Idea
 
-The **flattening lemma** for
+The {{#concept "flattening lemma" Disambiguation="coequalizers"}} for
 [coequalizers](synthetic-homotopy-theory.coequalizers.md) states that
 coequalizers commute with
 [dependent pair types](foundation.dependent-pair-types.md). More precisely,
@@ -171,26 +171,18 @@ module _
             ( vertical-map-span-cocone-cofork f g)
             ( horizontal-map-span-cocone-cofork f g)
             ( cocone-codiagonal-cofork f g e))
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) → refl)
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) → refl)
+          ( ind-Σ (ind-coprod _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
+          ( ind-Σ (ind-coprod _ (ev-pair refl-htpy) (ev-pair refl-htpy)))
           ( refl-htpy)
           ( refl-htpy)
           ( coherence-square-cocone-cofork
             ( bottom-map-cofork-flattening-lemma-coequalizer f g P e)
             ( top-map-cofork-flattening-lemma-coequalizer f g P e)
             ( cofork-flattening-lemma-coequalizer f g P e))
-          ( λ where
-            (inl a , t) → refl
-            (inr a , t) →
-              ( ap-id
-                ( eq-pair-Σ
-                  ( coherence-cofork f g e a)
-                  ( refl))) ∙
-              ( inv right-unit))
+          ( ind-Σ
+            ( ind-coprod _
+              ( ev-pair refl-htpy)
+              ( ev-pair (λ t → ap-id _ ∙ inv right-unit))))
           ( is-equiv-map-equiv
             ( right-distributive-Σ-coprod A A
               ( ( P) ∘