products-pullbacks

UniMath · Feb 27, 2024 · e26a445 · e26a445
1 parent d12d696
commit e26a445
Show file tree

Hide file tree

Showing 8 changed files with 279 additions and 175 deletions.
diff --git a/src/foundation-core/contractible-types.lagda.md b/src/foundation-core/contractible-types.lagda.md
@@ -18,8 +18,8 @@ open import foundation.universe-levels
 open import foundation-core.cartesian-product-types
 open import foundation-core.equality-dependent-pair-types
 open import foundation-core.equivalences
-open import foundation-core.identity-types
 open import foundation-core.homotopies
+open import foundation-core.identity-types
 open import foundation-core.transport-along-identifications
 ```
 

diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
@@ -162,95 +162,6 @@ abstract
       ( is-equiv-map-commutative-standard-pullback f g)
 ```
 
-### Products of pullbacks are pullbacks
-
-```agda
-module _
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
-  (f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
-  where
-
-  triangle-map-product-cone-standard-pullback :
-    (c : cone f g C) (c' : cone f' g' C') →
-    ( gap (map-product f f') (map-product g g') (product-cone f g f' g' c c')) ~
-    ( ( map-product-cone-standard-pullback f g f' g') ∘
-      ( map-product (gap f g c) (gap f' g' c')))
-  triangle-map-product-cone-standard-pullback c c' = refl-htpy
-
-  abstract
-    is-pullback-product-is-pullback :
-      (c : cone f g C) (c' : cone f' g' C') →
-      is-pullback f g c →
-      is-pullback f' g' c' →
-      is-pullback
-        ( map-product f f')
-        ( map-product g g')
-        ( product-cone f g f' g' c c')
-    is-pullback-product-is-pullback c c' is-pb-c is-pb-c' =
-      is-equiv-left-map-triangle
-        ( gap
-          ( map-product f f')
-          ( map-product g g')
-          ( product-cone f g f' g' c c'))
-        ( map-product-cone-standard-pullback f g f' g')
-        ( map-product (gap f g c) (gap f' g' c'))
-        ( triangle-map-product-cone-standard-pullback c c')
-        ( is-equiv-map-product (gap f g c) (gap f' g' c') is-pb-c is-pb-c')
-        ( is-equiv-map-product-cone-standard-pullback f g f' g')
-
-  abstract
-    is-pullback-left-factor-is-pullback-product :
-      (c : cone f g C) (c' : cone f' g' C') →
-      is-pullback
-        ( map-product f f')
-        ( map-product g g')
-        ( product-cone f g f' g' c c') →
-      standard-pullback f' g' →
-      is-pullback f g c
-    is-pullback-left-factor-is-pullback-product c c' is-pb-cc' t =
-      is-equiv-left-factor-is-equiv-map-product
-        ( gap f g c)
-        ( gap f' g' c')
-        ( t)
-        ( is-equiv-top-map-triangle
-          ( gap
-            ( map-product f f')
-            ( map-product g g')
-            ( product-cone f g f' g' c c'))
-        ( map-product-cone-standard-pullback f g f' g')
-          ( map-product (gap f g c) (gap f' g' c'))
-          ( triangle-map-product-cone-standard-pullback c c')
-          ( is-equiv-map-product-cone-standard-pullback f g f' g')
-          ( is-pb-cc'))
-
-  abstract
-    is-pullback-right-factor-is-pullback-product :
-      (c : cone f g C) (c' : cone f' g' C') →
-      is-pullback
-        ( map-product f f')
-        ( map-product g g')
-        ( product-cone f g f' g' c c') →
-      standard-pullback f g →
-      is-pullback f' g' c'
-    is-pullback-right-factor-is-pullback-product c c' is-pb-cc' t =
-      is-equiv-right-factor-is-equiv-map-product
-        ( gap f g c)
-        ( gap f' g' c')
-        ( t)
-        ( is-equiv-top-map-triangle
-          ( gap
-            ( map-product f f')
-            ( map-product g g')
-            ( product-cone f g f' g' c c'))
-          ( map-product-cone-standard-pullback f g f' g')
-          ( map-product (gap f g c) (gap f' g' c'))
-          ( triangle-map-product-cone-standard-pullback c c')
-          ( is-equiv-map-product-cone-standard-pullback f g f' g')
-          ( is-pb-cc'))
-```
-
 ### A family of maps over a base map induces a pullback square if and only if it is a family of equivalences
 
 Given a map `f : A → B` with a family of maps over it

diff --git a/src/foundation-core/standard-pullbacks.lagda.md b/src/foundation-core/standard-pullbacks.lagda.md
@@ -457,45 +457,6 @@ module _
   triangle-map-fold-cone-standard-pullback c = refl-htpy
 ```
 
-### Products of standard pullbacks are pullbacks
-
-```agda
-module _
-  {l1 l2 l3 l1' l2' l3' : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3}
-  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
-  (f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
-  where
-
-  map-product-cone-standard-pullback :
-    (standard-pullback f g) × (standard-pullback f' g') →
-    standard-pullback (map-product f f') (map-product g g')
-  map-product-cone-standard-pullback =
-    ( tot
-      ( λ t →
-        ( tot (λ s → eq-pair')) ∘
-        ( map-interchange-Σ-Σ (λ y p y' → f' (pr2 t) ＝ g' y')))) ∘
-    ( map-interchange-Σ-Σ (λ x t x' → Σ B' (λ y' → f' x' ＝ g' y')))
-
-  abstract
-    is-equiv-map-product-cone-standard-pullback :
-      is-equiv map-product-cone-standard-pullback
-    is-equiv-map-product-cone-standard-pullback =
-      is-equiv-comp
-        ( tot (λ t → tot (λ s → eq-pair') ∘ map-interchange-Σ-Σ _))
-        ( map-interchange-Σ-Σ _)
-        ( is-equiv-map-interchange-Σ-Σ _)
-        ( is-equiv-tot-is-fiberwise-equiv
-          ( λ t →
-            is-equiv-comp
-              ( tot (λ s → eq-pair'))
-              ( map-interchange-Σ-Σ (λ y p y' → f' (pr2 t) ＝ g' y'))
-              ( is-equiv-map-interchange-Σ-Σ _)
-              ( is-equiv-tot-is-fiberwise-equiv
-                ( λ s →
-                  is-equiv-eq-pair (map-product f f' t) (map-product g g' s)))))
-```
-
 ## Table of files about pullbacks
 
 The following table lists files that are about pullbacks as a general concept.

diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
@@ -290,6 +290,7 @@ open import foundation.product-decompositions-subuniverse public
 open import foundation.products-binary-relations public
 open import foundation.products-equivalence-relations public
 open import foundation.products-of-tuples-of-types public
+open import foundation.products-pullbacks public
 open import foundation.products-unordered-pairs-of-types public
 open import foundation.products-unordered-tuples-of-types public
 open import foundation.projective-types public

diff --git a/src/foundation/functoriality-cartesian-product-types.lagda.md b/src/foundation/functoriality-cartesian-product-types.lagda.md
@@ -254,24 +254,6 @@ module _
             ( is-contr-map-is-equiv is-equiv-fg (c , y))))
 ```
 
-### Product cones
-
-```agda
-module _
-  {l1 l2 l3 l4 l1' l2' l3' l4' : Level}
-  {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
-  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
-  (f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
-  where
-
-  product-cone :
-    cone f g C → cone f' g' C' →
-    cone (map-product f f') (map-product g g') (C × C')
-  pr1 (product-cone (p , q , H) (p' , q' , H')) = map-product p p'
-  pr1 (pr2 (product-cone (p , q , H) (p' , q' , H'))) = map-product q q'
-  pr2 (pr2 (product-cone (p , q , H) (p' , q' , H'))) = htpy-map-product H H'
-```
-
 ## See also
 
 - Arithmetical laws involving cartesian product types are recorded in