Flattening lemma for equifibered dependent span diagrams

references.bib

@@ -631,6 +631,15 @@ @phdthesis{Qui16
   langid   = {english}
 }
 
+@online{Rezk10HomotopyToposes,
+  title   = {Toposes and homotopy toposes},
+  author  = {Rezk, Charles},
+  year    = {2010},
+  month   = {01},
+  url     = {https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf},
+  version = {0.15}
+}
+
 @book{Rie17,
   title     = {Category {{Theory}} in {{Context}}},
   author    = {Riehl, Emily},

src/foundation-core/fibers-of-maps.lagda.md

@@ -52,6 +52,13 @@ module _
 
   compute-value-inclusion-fiber : (y : fiber f b) → f (inclusion-fiber y) ＝ b
   compute-value-inclusion-fiber = pr2
+
+  inclusion-fiber' : fiber' f b → A
+  inclusion-fiber' = pr1
+
+  compute-value-inclusion-fiber' :
+    (y : fiber' f b) → b ＝ f (inclusion-fiber' y)
+  compute-value-inclusion-fiber' = pr2
 ```
 
 ## Properties
@@ -280,9 +287,7 @@ module _
   triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t))
 
   map-inv-equiv-total-fiber : A → Σ B (fiber f)
-  pr1 (map-inv-equiv-total-fiber x) = f x
-  pr1 (pr2 (map-inv-equiv-total-fiber x)) = x
-  pr2 (pr2 (map-inv-equiv-total-fiber x)) = refl
+  map-inv-equiv-total-fiber x = (f x , x , refl)
 
   is-retraction-map-inv-equiv-total-fiber :
     is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber
@@ -316,6 +321,51 @@ module _
   pr2 inv-equiv-total-fiber = is-equiv-map-inv-equiv-total-fiber
 ```
 
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  map-equiv-total-fiber' : Σ B (fiber' f) → A
+  map-equiv-total-fiber' t = pr1 (pr2 t)
+
+  triangle-map-equiv-total-fiber' : pr1 ~ f ∘ map-equiv-total-fiber'
+  triangle-map-equiv-total-fiber' t = pr2 (pr2 t)
+
+  map-inv-equiv-total-fiber' : A → Σ B (fiber' f)
+  map-inv-equiv-total-fiber' x = (f x , x , refl)
+
+  is-retraction-map-inv-equiv-total-fiber' :
+    is-retraction map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-retraction-map-inv-equiv-total-fiber' (.(f x) , x , refl) = refl
+
+  is-section-map-inv-equiv-total-fiber' :
+    is-section map-equiv-total-fiber' map-inv-equiv-total-fiber'
+  is-section-map-inv-equiv-total-fiber' x = refl
+
+  is-equiv-map-equiv-total-fiber' : is-equiv map-equiv-total-fiber'
+  is-equiv-map-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+
+  is-equiv-map-inv-equiv-total-fiber' : is-equiv map-inv-equiv-total-fiber'
+  is-equiv-map-inv-equiv-total-fiber' =
+    is-equiv-is-invertible
+      map-equiv-total-fiber'
+      is-retraction-map-inv-equiv-total-fiber'
+      is-section-map-inv-equiv-total-fiber'
+
+  equiv-total-fiber' : Σ B (fiber' f) ≃ A
+  pr1 equiv-total-fiber' = map-equiv-total-fiber'
+  pr2 equiv-total-fiber' = is-equiv-map-equiv-total-fiber'
+
+  inv-equiv-total-fiber' : A ≃ Σ B (fiber' f)
+  pr1 inv-equiv-total-fiber' = map-inv-equiv-total-fiber'
+  pr2 inv-equiv-total-fiber' = is-equiv-map-inv-equiv-total-fiber'
+```
+
 ### Fibers of compositions
 
 ```agda

src/foundation-core/pullbacks.lagda.md

@@ -309,6 +309,86 @@ the vertical maps is a family of equivalences
               f
 ```
 
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
+  (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  triangle-tot-map-fiber-vertical-map-cone' :
+    tot (map-fiber-vertical-map-cone' f g c) ~
+    gap f g c ∘ map-equiv-total-fiber' (vertical-map-cone f g c)
+  triangle-tot-map-fiber-vertical-map-cone'
+    (.(vertical-map-cone f g c x) , x , refl) = refl
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb =
+      is-fiberwise-equiv-is-equiv-tot
+        ( is-equiv-left-map-triangle
+          ( tot (map-fiber-vertical-map-cone' f g c))
+          ( gap f g c)
+          ( map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( triangle-tot-map-fiber-vertical-map-cone')
+          ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+          ( pb))
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x)
+
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' :
+      is-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-is-pullback' pb =
+    equiv-tot (fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb)
+
+  abstract
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' :
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) →
+      is-pullback f g c
+    is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' is-equiv-fsq =
+      is-equiv-right-map-triangle
+        ( tot (map-fiber-vertical-map-cone' f g c))
+        ( gap f g c)
+        ( map-equiv-total-fiber' (vertical-map-cone f g c))
+        ( triangle-tot-map-fiber-vertical-map-cone')
+        ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+        ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c))
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback'
+        ( is-pullback-universal-property-pullback f g c up)
+
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c → (x : A) →
+      fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x)
+  fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+    pb x =
+    ( map-fiber-vertical-map-cone' f g c x ,
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb)
+        ( x))
+
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' :
+      universal-property-pullback f g c →
+      Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f)
+  equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' pb =
+    equiv-tot
+      ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback'
+        ( pb))
+```
+
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
@@ -356,6 +436,15 @@ module _
           ( λ x →
             is-equiv-tot-is-fiberwise-equiv (λ y → is-equiv-inv (g y) (f x))))
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
+
+  abstract
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback :
+      universal-property-pullback f g c →
+      is-fiberwise-equiv (map-fiber-vertical-map-cone f g c)
+    is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback
+      up =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback
+        ( is-pullback-universal-property-pullback f g c up)
 ```
 
 ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps

src/foundation/equivalences-arrows.lagda.md

@@ -87,8 +87,7 @@ module _
     coherence-hom-arrow f g (map-equiv i) (map-equiv j)
 
   equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
-  equiv-arrow =
-    Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
+  equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i))
 
   module _
     (e : equiv-arrow)
@@ -100,6 +99,9 @@ module _
     map-domain-equiv-arrow : A → X
     map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow
 
+    map-inv-domain-equiv-arrow : X → A
+    map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow
+
     is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow
     is-equiv-map-domain-equiv-arrow =
       is-equiv-map-equiv equiv-domain-equiv-arrow
@@ -110,6 +112,9 @@ module _
     map-codomain-equiv-arrow : B → Y
     map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow
 
+    map-inv-codomain-equiv-arrow : Y → B
+    map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow
+
     is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow
     is-equiv-map-codomain-equiv-arrow =
       is-equiv-map-equiv equiv-codomain-equiv-arrow

src/foundation/fibers-of-maps.lagda.md

@@ -141,6 +141,45 @@ module _
     {y y' : B} (p : y ＝ y') (u : fiber f y) →
     tot (λ x → concat' _ p) u ＝ tr (fiber f) p u
   compute-tr-fiber refl u = ap (pair _) right-unit
+
+  inv-compute-tr-fiber :
+    {y y' : B} (p : y ＝ y') (u : fiber f y) →
+    tr (fiber f) p u ＝ tot (λ x → concat' _ p) u
+  inv-compute-tr-fiber p u = inv (compute-tr-fiber p u)
+
+  compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tot (λ x q → inv p ∙ q) u ＝ tr (fiber' f) p u
+  compute-tr-fiber' refl u = refl
+
+  inv-compute-tr-fiber' :
+    {y y' : B} (p : y ＝ y') (u : fiber' f y) →
+    tr (fiber' f) p u ＝ tot (λ x q → inv p ∙ q) u
+  inv-compute-tr-fiber' p u = inv (compute-tr-fiber' p u)
+```
+
+### Transport in fibers along the fiber
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
+  where
+
+  compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → (pr1 u , refl) ＝ tr (fiber f) (inv (pr2 u)) u
+  compute-tr-self-fiber (._ , refl) = refl
+
+  inv-compute-tr-self-fiber :
+    {y : B} (u : fiber f y) → tr (fiber f) (inv (pr2 u)) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber u = inv (compute-tr-self-fiber u)
+
+  compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → (pr1 u , refl) ＝ tr (fiber' f) (pr2 u) u
+  compute-tr-self-fiber' (._ , refl) = refl
+
+  inv-compute-tr-self-fiber' :
+    {y : B} (u : fiber' f y) → tr (fiber' f) (pr2 u) u ＝ (pr1 u , refl)
+  inv-compute-tr-self-fiber' u = inv (compute-tr-self-fiber' u)
 ```
 
 ## Table of files about fibers of maps

src/foundation/functoriality-fibers-of-maps.lagda.md

@@ -103,6 +103,41 @@ module _
   pr1 hom-arrow-fiber = map-domain-hom-arrow-fiber
   pr1 (pr2 hom-arrow-fiber) = map-codomain-hom-arrow-fiber
   pr2 (pr2 hom-arrow-fiber) = coh-hom-arrow-fiber
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (f : A → B) (g : X → Y) (α : hom-arrow f g) (b : B)
+  where
+
+  map-domain-hom-arrow-fiber' :
+    fiber' f b → fiber' g (map-codomain-hom-arrow f g α b)
+  map-domain-hom-arrow-fiber' =
+    map-Σ _
+      ( map-domain-hom-arrow f g α)
+      ( λ a p → ap (map-codomain-hom-arrow f g α) p ∙ coh-hom-arrow f g α a)
+
+  map-fiber' :
+    fiber' f b → fiber' g (map-codomain-hom-arrow f g α b)
+  map-fiber' = map-domain-hom-arrow-fiber'
+
+  map-codomain-hom-arrow-fiber' : A → X
+  map-codomain-hom-arrow-fiber' = map-domain-hom-arrow f g α
+
+  coh-hom-arrow-fiber' :
+    coherence-square-maps
+      ( map-domain-hom-arrow-fiber')
+      ( inclusion-fiber' f)
+      ( inclusion-fiber' g)
+      ( map-domain-hom-arrow f g α)
+  coh-hom-arrow-fiber' = refl-htpy
+
+  hom-arrow-fiber' :
+    hom-arrow
+      ( inclusion-fiber' f {b})
+      ( inclusion-fiber' g {map-codomain-hom-arrow f g α b})
+  pr1 hom-arrow-fiber' = map-domain-hom-arrow-fiber'
+  pr1 (pr2 hom-arrow-fiber') = map-codomain-hom-arrow-fiber'
+  pr2 (pr2 hom-arrow-fiber') = coh-hom-arrow-fiber'
 ```
 
 ### Any cone induces a family of maps between the fibers of the vertical maps
@@ -121,6 +156,15 @@ module _
       ( g)
       ( hom-arrow-cone f g c)
       ( a)
+
+  map-fiber-vertical-map-cone' :
+    fiber' (vertical-map-cone f g c) a → fiber' g (f a)
+  map-fiber-vertical-map-cone' =
+    map-domain-hom-arrow-fiber'
+      ( vertical-map-cone f g c)
+      ( g)
+      ( hom-arrow-cone f g c)
+      ( a)
 ```
 
 ### Any cone induces a family of maps between the fibers of the vertical maps
@@ -139,6 +183,15 @@ module _
       ( f)
       ( hom-arrow-cone' f g c)
       ( b)
+
+  map-fiber-horizontal-map-cone' :
+    fiber' (horizontal-map-cone f g c) b → fiber' f (g b)
+  map-fiber-horizontal-map-cone' =
+    map-domain-hom-arrow-fiber'
+      ( horizontal-map-cone f g c)
+      ( f)
+      ( hom-arrow-cone' f g c)
+      ( b)
 ```
 
 ### For any `f : A → B` and any identification `p : b ＝ b'` in `B`, we obtain a morphism of arrows between the fiber inclusion at `b` to the fiber inclusion at `b'`