Horizontal fiber condition for pullbacks

src/foundation-core/pullbacks.lagda.md

@@ -13,6 +13,7 @@ open import foundation.dependent-pair-types
 open import foundation.functoriality-cartesian-product-types
 open import foundation.functoriality-fibers-of-maps
 open import foundation.identity-types
+open import foundation.morphisms-arrows
 open import foundation.standard-pullbacks
 open import foundation.universe-levels
 
@@ -283,14 +284,30 @@ abstract
 
 ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the vertical maps
 
+A cone is a pullback if and only if the induced family of maps on fibers between
+the vertical maps is a family of equivalences
+
+```text
+  fiber i a --> fiber g (f a)
+      |               |
+      |               |
+      ∨               ∨
+      C ------------> B
+      |               |
+    i |               | g
+      ∨               ∨
+  a ∈ A ------------> X.
+              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
 
   square-tot-map-fiber-vertical-map-cone :
-    gap f g c ∘ map-equiv-total-fiber (pr1 c) ~
+    gap f g c ∘ map-equiv-total-fiber (vertical-map-cone f g c) ~
     tot (λ _ → tot (λ _ → inv)) ∘ tot (map-fiber-vertical-map-cone f g c)
   square-tot-map-fiber-vertical-map-cone
     (.(vertical-map-cone f g c x) , x , refl) =
@@ -332,6 +349,73 @@ module _
         ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
 ```
 
+### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps
+
+A cone is a pullback if and only if the induced family of maps on fibers between
+the horizontal maps is a family of equivalences
+
+```text
+                            j
+      fiber j b ----> C --------> B ∋ b
+          |           |           |
+          |           |           | g
+          ∨           ∨           ∨
+    fiber f (g b) --> A --------> X.
+                            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
+
+  square-tot-map-fiber-horizontal-map-cone :
+    ( gap g f (swap-cone f g c) ∘
+      map-equiv-total-fiber (horizontal-map-cone f g c)) ~
+    ( tot (λ _ → tot (λ _ → inv)) ∘
+      tot (map-fiber-horizontal-map-cone f g c))
+  square-tot-map-fiber-horizontal-map-cone
+    (.(horizontal-map-cone f g c x) , x , refl) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( ap
+          ( inv)
+          ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x)))))
+
+  square-tot-map-fiber-horizontal-map-cone' :
+    ( ( λ x →
+        ( horizontal-map-cone f g c x ,
+          vertical-map-cone f g c x ,
+          coherence-square-cone f g c x)) ∘
+      map-equiv-total-fiber (horizontal-map-cone f g c)) ~
+    tot (map-fiber-horizontal-map-cone f g c)
+  square-tot-map-fiber-horizontal-map-cone'
+    (.(horizontal-map-cone f g c x) , x , refl) =
+    eq-pair-eq-fiber
+      ( eq-pair-eq-fiber
+        ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x))))
+
+  abstract
+    is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback :
+      is-pullback f g c →
+      is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c)
+    is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback pb =
+      is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback g f
+        ( swap-cone f g c)
+        ( is-pullback-swap-cone f g c pb)
+
+  abstract
+    is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone :
+      is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c) →
+      is-pullback f g c
+    is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone is-equiv-fsq =
+      is-pullback-swap-cone' f g c
+        ( is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone g f
+          ( swap-cone f g c)
+          ( is-equiv-fsq))
+```
+
 ### The horizontal pullback pasting property
 
 Given a diagram as follows where the right-hand square is a pullback

src/foundation/cartesian-morphisms-arrows.lagda.md

@@ -831,7 +831,7 @@ module _
 
 ### Lifting cartesian morphisms along lifts of the codomain
 
-Suppose given a cospan of morphisms of arrows
+Suppose given a cospan diagram of arrows
 
 ```text
     A ------> C <------ B

src/foundation/dependent-sums-pullbacks.lagda.md

@@ -102,7 +102,7 @@ Given a map `f : A → B` with a family of maps over it
 
 ```text
          map-Σ f g
-  Σ A P ----------> Σ B Q
+  Σ A P ---------> Σ B Q
     |                |
     |                |
     ∨                ∨

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

@@ -123,6 +123,24 @@ module _
       ( a)
 ```
 
+### Any cone induces a family of maps between the fibers of the vertical maps
+
+```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) (b : B)
+  where
+
+  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'`
 
 ```agda