Characterizing the fibers of cogap as a pushout of fibers (#887)

Co-authored-by: Fredrik Bakke <[email protected]>
Co-authored-by: Vojtěch Štěpančík <[email protected]>

src/synthetic-homotopy-theory/pushouts.lagda.md

@@ -7,17 +7,20 @@ module synthetic-homotopy-theory.pushouts where
 <details><summary>Imports</summary>
 
 ```agda
-open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-maps
 open import foundation.dependent-pair-types
 open import foundation.equivalences
+open import foundation.fibers-of-maps
 open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.26-descent
 open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.dependent-universal-property-pushouts
+open import synthetic-homotopy-theory.flattening-lemma-pushouts
 open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
@@ -207,3 +210,196 @@ module _
       ( up-pushout f g)
       ( c)
 ```
+
+### Fibers of the cogap map
+
+We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map
+as a pushout of fibers. This is an application of the
+[flattening lemma for pushouts](synthetic-homotopy-theory.flattening-lemma-pushouts.md).
+
+Given a pushout square with a
+[cocone](synthetic-homotopy-theory.cocones-under-spans.md)
+
+```text
+       g
+   S ----> B
+   |       | \
+ f |    inr|  \  n
+   v    ⌜  v   \
+   A ----> ∙    \
+    \ inl   \   |
+  m  \  cogap\  |
+      \       \ v
+       \-----> X
+```
+
+we have, for every `x : X`, a pushout square of fibers:
+
+```text
+    fiber (m ∘ f) x ---> fiber (cogap ∘ inr) x
+           |                       |
+           |                       |
+           v                    ⌜  v
+ fiber (cogap ∘ inl) x ----> fiber cogap x
+```
+
+```agda
+module _
+  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  ( f : S → A) (g : S → B)
+  { X : UU l4} (c : cocone f g X) (x : X)
+  where
+
+  equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span :
+    fiber (horizontal-map-cocone f g c ∘ f) x ≃
+    fiber (cogap f g c ∘ inl-pushout f g ∘ f) x
+  equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span =
+    equiv-tot (λ s → equiv-concat (compute-inl-cogap f g c (f s)) x)
+
+  equiv-fiber-horizontal-map-cocone-cogap-inl :
+    fiber (horizontal-map-cocone f g c) x ≃
+    fiber (cogap f g c ∘ inl-pushout f g) x
+  equiv-fiber-horizontal-map-cocone-cogap-inl =
+    equiv-tot (λ a → equiv-concat (compute-inl-cogap f g c a) x)
+
+  equiv-fiber-vertical-map-cocone-cogap-inr :
+    fiber (vertical-map-cocone f g c) x ≃
+    fiber (cogap f g c ∘ inr-pushout f g) x
+  equiv-fiber-vertical-map-cocone-cogap-inr =
+    equiv-tot (λ b → equiv-concat (compute-inr-cogap f g c b) x)
+
+  horizontal-map-span-cogap-fiber :
+    fiber (horizontal-map-cocone f g c ∘ f) x →
+    fiber (horizontal-map-cocone f g c) x
+  horizontal-map-span-cogap-fiber =
+    map-Σ-map-base f (λ a → horizontal-map-cocone f g c a ＝ x)
+```
+
+Since our pushout square of fibers has `fiber (m ∘ f) x` as its top-left corner
+and not `fiber (n ∘ g) x`, things are "left-biased". For this reason, the
+following map is constructed as a composition which makes a later coherence
+square commute (almost) trivially.
+
+```agda
+  vertical-map-span-cogap-fiber :
+    fiber (horizontal-map-cocone f g c ∘ f) x →
+    fiber (vertical-map-cocone f g c) x
+  vertical-map-span-cogap-fiber =
+    ( map-inv-equiv equiv-fiber-vertical-map-cocone-cogap-inr) ∘
+    ( horizontal-map-span-flattening-pushout
+      ( λ y → (cogap f g c y) ＝ x) f g (cocone-pushout f g)) ∘
+    ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span)
+
+  statement-universal-property-pushout-cogap-fiber : UUω
+  statement-universal-property-pushout-cogap-fiber =
+    { l : Level} →
+    Σ ( cocone
+        ( horizontal-map-span-cogap-fiber)
+        ( vertical-map-span-cogap-fiber)
+        ( fiber (cogap f g c) x))
+      ( universal-property-pushout l
+        ( horizontal-map-span-cogap-fiber)
+        ( vertical-map-span-cogap-fiber))
+
+  universal-property-pushout-cogap-fiber :
+    statement-universal-property-pushout-cogap-fiber
+  universal-property-pushout-cogap-fiber =
+    universal-property-pushout-extension-by-equivalences
+      ( vertical-map-span-flattening-pushout
+        ( λ y → cogap f g c y ＝ x)
+        ( f)
+        ( g)
+        ( cocone-pushout f g))
+      ( horizontal-map-span-flattening-pushout
+        ( λ y → cogap f g c y ＝ x)
+        ( f)
+        ( g)
+        ( cocone-pushout f g))
+      ( horizontal-map-span-cogap-fiber)
+      ( vertical-map-span-cogap-fiber)
+      ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl)
+      ( map-equiv equiv-fiber-vertical-map-cocone-cogap-inr)
+      ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span)
+      ( cocone-flattening-pushout
+        ( λ y → cogap f g c y ＝ x)
+        ( f)
+        ( g)
+        ( cocone-pushout f g))
+      ( flattening-lemma-pushout
+        ( λ y → cogap f g c y ＝ x)
+        ( f)
+        ( g)
+        ( cocone-pushout f g)
+        ( dependent-up-pushout f g))
+      ( refl-htpy)
+      ( λ _ →
+        inv
+          ( is-section-map-inv-equiv
+            ( equiv-fiber-vertical-map-cocone-cogap-inr)
+            ( _)))
+      ( is-equiv-map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl)
+      ( is-equiv-map-equiv equiv-fiber-vertical-map-cocone-cogap-inr)
+      ( is-equiv-map-equiv
+        ( equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span))
+```
+
+We record the following auxiliary lemma which says that if we have types `T`,
+`F` and `G` such that `T ≃ fiber (m ∘ f) x`, `F ≃ fiber (cogap ∘ inl) x` and
+`G ≃ fiber (cogap ∘ inr) x`, together with suitable maps `u : T → F` and
+`v : T → G`, then we get a pushout square:
+
+```text
+          v
+   T ----------> G
+   |             |
+ u |             |
+   v          ⌜  v
+   F ----> fiber cogap x
+```
+
+Thus, this lemma is useful in case we have convenient descriptions of the
+fibers.
+
+```agda
+  module _
+    { l5 l6 l7 : Level} (T : UU l5) (F : UU l6) (G : UU l7)
+    ( i : F ≃ fiber (horizontal-map-cocone f g c) x)
+    ( j : G ≃ fiber (vertical-map-cocone f g c) x)
+    ( k : T ≃ fiber (horizontal-map-cocone f g c ∘ f) x)
+    ( u : T → F)
+    ( v : T → G)
+    ( coh-l :
+      coherence-square-maps
+        ( map-equiv k)
+        ( u)
+        ( horizontal-map-span-cogap-fiber)
+        ( map-equiv i))
+    ( coh-r :
+      coherence-square-maps
+        ( v)
+        ( map-equiv k)
+        ( map-equiv j)
+        ( vertical-map-span-cogap-fiber))
+    where
+
+    universal-property-pushout-cogap-fiber-up-to-equiv :
+      { l : Level} →
+      ( Σ ( cocone u v (fiber (cogap f g c) x))
+          ( λ c → universal-property-pushout l u v c))
+    universal-property-pushout-cogap-fiber-up-to-equiv {l} =
+      universal-property-pushout-extension-by-equivalences
+        ( horizontal-map-span-cogap-fiber)
+        ( vertical-map-span-cogap-fiber)
+        ( u)
+        ( v)
+        ( map-equiv i)
+        ( map-equiv j)
+        ( map-equiv k)
+        ( pr1 ( universal-property-pushout-cogap-fiber {l}))
+        ( pr2 universal-property-pushout-cogap-fiber)
+        ( coh-l)
+        ( coh-r)
+        ( is-equiv-map-equiv i)
+        ( is-equiv-map-equiv j)
+        ( is-equiv-map-equiv k)
+```

src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md

@@ -592,6 +592,14 @@ module _
       ( c)
       ( universal-property-pushout-is-equiv' f' i (j , f , coh) ie je)
       ( up-c)
+
+  universal-property-pushout-left-extension-by-equivalences :
+    {l : Level} → is-equiv i → is-equiv j →
+    Σ (cocone f' (g ∘ i) X) (universal-property-pushout l f' (g ∘ i))
+  pr1 (universal-property-pushout-left-extension-by-equivalences ie je) =
+    cocone-comp-horizontal' f' i g f j c coh
+  pr2 (universal-property-pushout-left-extension-by-equivalences ie je) =
+    universal-property-pushout-left-extended-by-equivalences ie je
 ```
 
 #### The vertical pushout pasting lemma
@@ -752,9 +760,10 @@ module _
 
 #### Extending pushouts by equivalences at the top
 
-If we have a pushout square on the right, equivalences S' ≃ S and B' ≃ B, and a
-map g' : S' → B' making the top square commute, then the vertical rectangle is
-again a pushout. This is a special case of the vertical pushout pasting lemma.
+If we have a pushout square on the right, equivalences `S' ≃ S` and `B' ≃ B`,
+and a map `g' : S' → B'` making the top square commute, then the vertical
+rectangle is again a pushout. This is a special case of the vertical pushout
+pasting lemma.
 
 ```text
            g'
@@ -793,11 +802,19 @@ module _
       ( c)
       ( universal-property-pushout-is-equiv i g' (g , j , coh) ie je)
       ( up-c)
+
+  universal-property-pushout-top-extension-by-equivalences :
+    {l : Level} → is-equiv i → is-equiv j →
+    Σ (cocone (f ∘ i) g' X) (universal-property-pushout l (f ∘ i) g')
+  pr1 (universal-property-pushout-top-extension-by-equivalences ie je) =
+    cocone-comp-vertical' i g' j g f c coh
+  pr2 (universal-property-pushout-top-extension-by-equivalences ie je) =
+    universal-property-pushout-top-extended-by-equivalences ie je
 ```
 
 ### Extending pushouts by equivalences of cocones
 
-Given a commutative diagram where i, j and k are equivalences,
+Given a commutative diagram where `i`, `j` and `k` are equivalences,
 
 ```text
           g'
@@ -824,7 +841,7 @@ the induced square is a pushout.
 
 This combines both special cases of the pushout pasting lemmas for equivalences.
 
-Notice that the triple (i.j.k) is really an equivalence of spans. Thus, this
+Notice that the triple `(i,j,k)` is really an equivalence of spans. Thus, this
 result can be phrased as: the pushout is invariant under equivalence of spans.
 
 ```agda
@@ -840,15 +857,12 @@ module _
   ( coh-r : coherence-square-maps g' k j g)
   where
 
-  universal-property-pushout-extended-by-equivalences :
-    is-equiv i → is-equiv j → is-equiv k →
-    {l : Level} →
-    universal-property-pushout l
+  universal-property-pushout-extension-by-equivalences :
+    {l : Level} → is-equiv i → is-equiv j → is-equiv k →
+    Σ (cocone f' g' X) (λ d → universal-property-pushout l f' g' d)
+  universal-property-pushout-extension-by-equivalences ie je ke =
+    universal-property-pushout-top-extension-by-equivalences
       ( f')
-      ( g')
-      ( comp-cocone-hom-span f g f' g' i j k c coh-l coh-r)
-  universal-property-pushout-extended-by-equivalences ie je ke =
-    universal-property-pushout-top-extended-by-equivalences f'
       ( g ∘ k)
       ( id)
       ( j)
@@ -864,6 +878,16 @@ module _
       ( coh-r)
       ( is-equiv-id)
       ( je)
+
+  universal-property-pushout-extended-by-equivalences :
+    is-equiv i → is-equiv j → is-equiv k →
+    {l : Level} →
+    universal-property-pushout l
+      ( f')
+      ( g')
+      ( comp-cocone-hom-span f g f' g' i j k c coh-l coh-r)
+  universal-property-pushout-extended-by-equivalences ie je ke =
+    pr2 (universal-property-pushout-extension-by-equivalences ie je ke)
 ```
 
 ### In a commuting cube where the vertical maps are equivalences, the bottom square is a pushout if and only if the top square is a pushout