dependent-products-pullbacks

src/foundation.lagda.md

@@ -106,6 +106,7 @@ open import foundation.dependent-homotopies public
 open import foundation.dependent-identifications public
 open import foundation.dependent-inverse-sequential-diagrams public
 open import foundation.dependent-pair-types public
+open import foundation.dependent-products-pullbacks public
 open import foundation.dependent-sequences public
 open import foundation.dependent-telescopes public
 open import foundation.dependent-universal-property-equivalences public

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

@@ -0,0 +1,199 @@
+# Dependent products of pullbacks
+
+```agda
+module foundation.dependent-products-pullbacks where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cones-over-cospan-diagrams
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.equality-coproduct-types
+open import foundation.function-extensionality
+open import foundation.functoriality-coproduct-types
+open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-function-types
+open import foundation.identity-types
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.equality-dependent-pair-types
+open import foundation-core.equivalences
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.postcomposition-functions
+open import foundation-core.pullbacks
+open import foundation-core.retractions
+open import foundation-core.sections
+open import foundation-core.standard-pullbacks
+open import foundation-core.universal-property-pullbacks
+```
+
+</details>
+
+## Idea
+
+Given a family of pullback squares, their dependent product is again a pullback
+square.
+
+## Definitions
+
+### Dependent products of cones
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
+  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
+  (c : (i : I) → cone (f i) (g i) (C i))
+  where
+
+  cone-Π : cone (map-Π f) (map-Π g) ((i : I) → C i)
+  pr1 cone-Π = map-Π (λ i → pr1 (c i))
+  pr1 (pr2 cone-Π) = map-Π (λ i → pr1 (pr2 (c i)))
+  pr2 (pr2 cone-Π) = htpy-map-Π (λ i → pr2 (pr2 (c i)))
+```
+
+## Properties
+
+### Computing the standard pullback of a dependent product
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
+  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
+  where
+
+  map-standard-pullback-Π :
+    standard-pullback (map-Π f) (map-Π g) →
+    (i : I) → standard-pullback (f i) (g i)
+  pr1 (map-standard-pullback-Π (α , β , γ) i) = α i
+  pr1 (pr2 (map-standard-pullback-Π (α , β , γ) i)) = β i
+  pr2 (pr2 (map-standard-pullback-Π (α , β , γ) i)) = htpy-eq γ i
+
+  map-inv-standard-pullback-Π :
+    ((i : I) → standard-pullback (f i) (g i)) →
+    standard-pullback (map-Π f) (map-Π g)
+  pr1 (map-inv-standard-pullback-Π h) i = pr1 (h i)
+  pr1 (pr2 (map-inv-standard-pullback-Π h)) i = pr1 (pr2 (h i))
+  pr2 (pr2 (map-inv-standard-pullback-Π h)) = eq-htpy (λ i → pr2 (pr2 (h i)))
+
+  abstract
+    is-section-map-inv-standard-pullback-Π :
+      is-section (map-standard-pullback-Π) (map-inv-standard-pullback-Π)
+    is-section-map-inv-standard-pullback-Π h =
+      eq-htpy
+        ( λ i →
+          map-extensionality-standard-pullback (f i) (g i) refl refl
+            ( inv
+              ( ( right-unit) ∙
+                ( htpy-eq (is-section-eq-htpy (λ i → pr2 (pr2 (h i)))) i))))
+
+  abstract
+    is-retraction-map-inv-standard-pullback-Π :
+      is-retraction (map-standard-pullback-Π) (map-inv-standard-pullback-Π)
+    is-retraction-map-inv-standard-pullback-Π (α , β , γ) =
+      map-extensionality-standard-pullback
+        ( map-Π f)
+        ( map-Π g)
+        ( refl)
+        ( refl)
+        ( inv (right-unit ∙ is-retraction-eq-htpy γ))
+
+  abstract
+    is-equiv-map-standard-pullback-Π :
+      is-equiv (map-standard-pullback-Π)
+    is-equiv-map-standard-pullback-Π =
+      is-equiv-is-invertible
+        ( map-inv-standard-pullback-Π)
+        ( is-section-map-inv-standard-pullback-Π)
+        ( is-retraction-map-inv-standard-pullback-Π)
+
+  compute-standard-pullback-Π :
+    ( standard-pullback (map-Π f) (map-Π g)) ≃
+    ( (i : I) → standard-pullback (f i) (g i))
+  compute-standard-pullback-Π =
+    map-standard-pullback-Π , is-equiv-map-standard-pullback-Π
+```
+
+### A dependent product of gap maps computes as the gap map of the dependent product
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
+  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
+  (c : (i : I) → cone (f i) (g i) (C i))
+  where
+
+  triangle-map-standard-pullback-Π :
+    map-Π (λ i → gap (f i) (g i) (c i)) ~
+    map-standard-pullback-Π f g ∘ gap (map-Π f) (map-Π g) (cone-Π f g c)
+  triangle-map-standard-pullback-Π h =
+    eq-htpy
+      ( λ i →
+        map-extensionality-standard-pullback
+          ( f i)
+          ( g i)
+          ( refl)
+          ( refl)
+          ( htpy-eq (is-section-eq-htpy _) i ∙ inv right-unit))
+```
+
+### Dependent products of pullbacks are pullbacks
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
+  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
+  (c : (i : I) → cone (f i) (g i) (C i))
+  where
+
+  abstract
+    is-pullback-Π :
+      ((i : I) → is-pullback (f i) (g i) (c i)) →
+      is-pullback (map-Π f) (map-Π g) (cone-Π f g c)
+    is-pullback-Π is-pb-c =
+      is-equiv-top-map-triangle
+        ( map-Π (λ i → gap (f i) (g i) (c i)))
+        ( map-standard-pullback-Π f g)
+        ( gap (map-Π f) (map-Π g) (cone-Π f g c))
+        ( triangle-map-standard-pullback-Π f g c)
+        ( is-equiv-map-standard-pullback-Π f g)
+        ( is-equiv-map-Π-is-fiberwise-equiv is-pb-c)
+```
+
+### Cones satisfying the universal property of pullbacks are closed under dependent products
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
+  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4}
+  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
+  {C : I → UU l5} (c : (i : I) → cone (f i) (g i) (C i))
+  where
+
+  universal-property-pullback-Π :
+    ((i : I) → universal-property-pullback (f i) (g i) (c i)) →
+    universal-property-pullback (map-Π f) (map-Π g) (cone-Π f g c)
+  universal-property-pullback-Π H =
+    universal-property-pullback-is-pullback
+      ( map-Π f)
+      ( map-Π g)
+      ( cone-Π f g c)
+      ( is-pullback-Π f g c
+        ( λ i →
+          is-pullback-universal-property-pullback (f i) (g i) (c i) (H i)))
+```
+
+## Table of files about pullbacks
+
+The following table lists files that are about pullbacks as a general concept.
+
+{{#include tables/pullbacks.md}}

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

@@ -289,22 +289,6 @@ pr1 (automorphism-Π e f) = map-automorphism-Π e f
 pr2 (automorphism-Π e f) = is-equiv-map-automorphism-Π e f
 ```
 
-### Dependent products of cones
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
-  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
-  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
-  (c : (i : I) → cone (f i) (g i) (C i))
-  where
-
-  cone-Π : cone (map-Π f) (map-Π g) ((i : I) → C i)
-  pr1 cone-Π = map-Π (λ i → pr1 (c i))
-  pr1 (pr2 cone-Π) = map-Π (λ i → pr1 (pr2 (c i)))
-  pr2 (pr2 cone-Π) = htpy-map-Π (λ i → pr2 (pr2 (c i)))
-```
-
 ## See also
 
 - Arithmetical laws involving dependent function types are recorded in

src/foundation/postcomposition-pullbacks.lagda.md

@@ -81,7 +81,7 @@ pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h
 
 ## Properties
 
-### Standard pullbacks are closed under postcomposition exponentiation
+### The standard pullback computes of a postcomposition exponential computes as the type of cones
 
 ```agda
 module _
@@ -90,28 +90,34 @@ module _
   (T : UU l4)
   where
 
-  map-postcomp-cone-standard-pullback :
+  map-standard-pullback-postcomp :
     standard-pullback (postcomp T f) (postcomp T g) → cone f g T
-  map-postcomp-cone-standard-pullback = tot (λ _ → tot (λ _ → htpy-eq))
+  map-standard-pullback-postcomp = tot (λ _ → tot (λ _ → htpy-eq))
 
   abstract
-    is-equiv-map-postcomp-cone-standard-pullback :
-      is-equiv map-postcomp-cone-standard-pullback
-    is-equiv-map-postcomp-cone-standard-pullback =
+    is-equiv-map-standard-pullback-postcomp :
+      is-equiv map-standard-pullback-postcomp
+    is-equiv-map-standard-pullback-postcomp =
       is-equiv-tot-is-fiberwise-equiv
         ( λ p → is-equiv-tot-is-fiberwise-equiv (λ q → funext (f ∘ p) (g ∘ q)))
+
+  compute-standard-pullback-postcomp :
+    standard-pullback (postcomp T f) (postcomp T g) ≃ cone f g T
+  compute-standard-pullback-postcomp =
+    ( map-standard-pullback-postcomp ,
+      is-equiv-map-standard-pullback-postcomp)
 ```
 
 ### The precomposition action on cones computes as the gap map of a postcomposition cone
 
 ```agda
-triangle-map-postcomp-cone-standard-pullback :
+triangle-map-standard-pullback-postcomp :
   {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
   (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) →
   cone-map f g c {T} ~
-  map-postcomp-cone-standard-pullback f g T ∘
+  map-standard-pullback-postcomp f g T ∘
   gap (postcomp T f) (postcomp T g) (postcomp-cone T f g c)
-triangle-map-postcomp-cone-standard-pullback T f g c h =
+triangle-map-standard-pullback-postcomp T f g c h =
   eq-pair-eq-fiber
     ( eq-pair-eq-fiber
       ( inv (is-section-eq-htpy (coherence-square-cone f g c ·r h))))
@@ -129,10 +135,10 @@ abstract
   is-pullback-postcomp-is-pullback f g c is-pb-c T =
     is-equiv-top-map-triangle
       ( cone-map f g c)
-      ( map-postcomp-cone-standard-pullback f g T)
+      ( map-standard-pullback-postcomp f g T)
       ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-      ( triangle-map-postcomp-cone-standard-pullback T f g c)
-      ( is-equiv-map-postcomp-cone-standard-pullback f g T)
+      ( triangle-map-standard-pullback-postcomp T f g c)
+      ( is-equiv-map-standard-pullback-postcomp f g T)
       ( universal-property-pullback-is-pullback f g c is-pb-c T)
 
 abstract
@@ -147,11 +153,11 @@ abstract
       ( λ T →
         is-equiv-left-map-triangle
           ( cone-map f g c)
-          ( map-postcomp-cone-standard-pullback f g T)
+          ( map-standard-pullback-postcomp f g T)
           ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c))
-          ( triangle-map-postcomp-cone-standard-pullback T f g c)
+          ( triangle-map-standard-pullback-postcomp T f g c)
           ( is-pb-postcomp T)
-          ( is-equiv-map-postcomp-cone-standard-pullback f g T))
+          ( is-equiv-map-standard-pullback-postcomp f g T))
 ```
 
 ### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation

src/foundation/products-pullbacks.lagda.md

@@ -65,7 +65,7 @@ module _
 
 ## Properties
 
-### Products of standard pullbacks are pullbacks
+### Computing the standard pullback of a product
 
 ```agda
 module _

src/foundation/pullbacks.lagda.md

@@ -218,46 +218,6 @@ module _
         ( is-equiv-map-equiv-standard-pullback-htpy Hf Hg)
 ```
 
-### Dependent products of pullbacks are pullbacks
-
-Given a family of pullback squares, their dependent product is again a pullback
-square.
-
-```agda
-module _
-  {l1 l2 l3 l4 l5 : Level} {I : UU l1}
-  {A : I → UU l2} {B : I → UU l3} {X : I → UU l4} {C : I → UU l5}
-  (f : (i : I) → A i → X i) (g : (i : I) → B i → X i)
-  (c : (i : I) → cone (f i) (g i) (C i))
-  where
-
-  triangle-map-standard-pullback-Π :
-    map-Π (λ i → gap (f i) (g i) (c i)) ~
-    map-standard-pullback-Π f g ∘ gap (map-Π f) (map-Π g) (cone-Π f g c)
-  triangle-map-standard-pullback-Π h =
-    eq-htpy
-      ( λ i →
-        map-extensionality-standard-pullback
-          ( f i)
-          ( g i)
-          ( refl)
-          ( refl)
-          ( htpy-eq (is-section-eq-htpy _) i ∙ inv right-unit))
-
-  abstract
-    is-pullback-Π :
-      ((i : I) → is-pullback (f i) (g i) (c i)) →
-      is-pullback (map-Π f) (map-Π g) (cone-Π f g c)
-    is-pullback-Π is-pb-c =
-      is-equiv-top-map-triangle
-        ( map-Π (λ i → gap (f i) (g i) (c i)))
-        ( map-standard-pullback-Π f g)
-        ( gap (map-Π f) (map-Π g) (cone-Π f g c))
-        ( triangle-map-standard-pullback-Π)
-        ( is-equiv-map-standard-pullback-Π f g)
-        ( is-equiv-map-Π-is-fiberwise-equiv is-pb-c)
-```
-
 ### Coproducts of pullbacks are pullbacks
 
 ```agda