Associativity of pullbacks (#1054)

Proves $(A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C)$ for standard and non-standard pullbacks.
UniMath · Mar 9, 2024 · fdc36fc · fdc36fc
1 parent 27e36c6
commit fdc36fc
Show file tree

Hide file tree

Showing 6 changed files with 305 additions and 12 deletions.
diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md
@@ -384,12 +384,12 @@ module _
   where
 
   abstract
-    is-pullback-top-is-pullback-rectangle :
+    is-pullback-top-square-is-pullback-rectangle :
       (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
       is-pullback f g c →
       is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d) →
       is-pullback (horizontal-map-cone f g c) h d
-    is-pullback-top-is-pullback-rectangle c d is-pb-c is-pb-dc =
+    is-pullback-top-square-is-pullback-rectangle c d is-pb-c is-pb-dc =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
         ( horizontal-map-cone f g c)
         ( h)
@@ -442,12 +442,12 @@ module _
             ( x , refl))
 
   abstract
-    is-pullback-rectangle-is-pullback-top :
+    is-pullback-rectangle-is-pullback-top-square :
       (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) →
       is-pullback f g c →
       is-pullback (horizontal-map-cone f g c) h d →
       is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d)
-    is-pullback-rectangle-is-pullback-top c d is-pb-c is-pb-d =
+    is-pullback-rectangle-is-pullback-top-square c d is-pb-c is-pb-d =
       is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone
         ( f)
         ( g ∘ h)
@@ -502,6 +502,101 @@ module _
                   ( pr1 t))))
 ```
 
+### Pullbacks are associative
+
+Consider two cospans with a shared vertex `B`:
+
+```text
+      f       g       h       i
+  A ----> X <---- B ----> Y <---- C,
+```
+
+and with pullback cones `α` and `β` respectively. Moreover, consider a cone `γ`
+over the pullbacks as in the following diagram
+
+```text
+  ∙ ------------> ∙ ------------> C
+  |               | ⌟             |
+  |       γ       |       β       | i
+  ∨               ∨               ∨
+  ∙ ------------> B ------------> Y
+  | ⌟             |       h
+  |       α       | g
+  ∨               ∨
+  A ------------> X.
+          f
+```
+
+Then the pasting `γ □ α` is a pullback if and only if `γ` is if and only if the
+pasting `γ □ β` is. And, in particular, we have the equivalence
+
+\[ (A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C). \]
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  {S : UU l6} {T : UU l7} {U : UU l8}
+  (α : cone f g S) (β : cone h i T)
+  (γ : cone (horizontal-map-cone f g α) (vertical-map-cone h i β) U)
+  (is-pullback-α : is-pullback f g α)
+  (is-pullback-β : is-pullback h i β)
+  where
+
+  is-pullback-associative :
+    is-pullback
+      ( f)
+      ( g ∘ vertical-map-cone h i β)
+      ( pasting-vertical-cone f g (vertical-map-cone h i β) α γ) →
+    is-pullback
+      ( h ∘ horizontal-map-cone f g α)
+      ( i)
+      ( pasting-horizontal-cone (horizontal-map-cone f g α) h i β γ)
+  is-pullback-associative H =
+    is-pullback-rectangle-is-pullback-left-square
+      ( horizontal-map-cone f g α)
+      ( h)
+      ( i)
+      ( β)
+      ( γ)
+      ( is-pullback-β)
+      ( is-pullback-top-square-is-pullback-rectangle
+        ( f)
+        ( g)
+        ( vertical-map-cone h i β)
+        ( α)
+        ( γ)
+        ( is-pullback-α)
+        ( H))
+
+  is-pullback-inv-associative :
+    is-pullback
+      ( h ∘ horizontal-map-cone f g α)
+      ( i)
+      ( pasting-horizontal-cone (horizontal-map-cone f g α) h i β γ) →
+    is-pullback
+      ( f)
+      ( g ∘ vertical-map-cone h i β)
+      ( pasting-vertical-cone f g (vertical-map-cone h i β) α γ)
+  is-pullback-inv-associative H =
+    is-pullback-rectangle-is-pullback-top-square
+        ( f)
+        ( g)
+        ( vertical-map-cone h i β)
+        ( α)
+        ( γ)
+        ( is-pullback-α)
+        ( is-pullback-left-square-is-pullback-rectangle
+          ( horizontal-map-cone f g α)
+          ( h)
+          ( i)
+          ( β)
+          ( γ)
+          ( is-pullback-β)
+          ( H))
+```
+
 ### Pullbacks can be "folded"
 
 Given a pullback square

diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md
@@ -240,7 +240,7 @@ module _
     is-pullback h' k' (f' , g' , top)
   is-pullback-top-is-pullback-bottom-cube-is-equiv
     is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-bottom =
-    is-pullback-top-is-pullback-rectangle h hD k'
+    is-pullback-top-square-is-pullback-rectangle h hD k'
       ( hB , h' , front-left)
       ( f' , g' , top)
       ( is-pullback-is-equiv-vertical-maps h hD
@@ -262,7 +262,7 @@ module _
             ( ap-concat-htpy'
               ( (front-left ·r f') ∙h (hD ·l top))
               ( inv-htpy-right-unit-htpy {H = h ·l back-left}))))
-        ( is-pullback-rectangle-is-pullback-top h k hC
+        ( is-pullback-rectangle-is-pullback-top-square h k hC
           ( f , g , bottom)
           ( hA , g' , back-right)
           ( is-pb-bottom)

diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md
@@ -129,6 +129,36 @@ module _
   pr2 (pr2 (gap c z)) = coherence-square-cone f g c z
 ```
 
+#### The standard ternary pullback
+
+Given two cospans with a shared vertex `B`:
+
+```text
+      f       g       h       i
+  A ----> X <---- B ----> Y <---- C,
+```
+
+we call the standard limit of the diagram the
+{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}.
+It is defined as the sum
+
+```text
+  standard-ternary-pullback f g h i :=
+    Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)).
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
+  standard-ternary-pullback =
+    Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c))))
+```
+
 ## Properties
 
 ### Characterization of the identity type of the standard pullback
@@ -271,6 +301,174 @@ triangle-map-commutative-standard-pullback :
 triangle-map-commutative-standard-pullback f g c = refl-htpy
 ```
 
+### Standard pullbacks are associative
+
+Consider two cospans with a shared vertex `B`:
+
+```text
+      f       g       h       i
+  A ----> X <---- B ----> Y <---- C,
+```
+
+then we can construct their limit using standard pullbacks in two equivalent
+ways. We can construct it by first forming the standard pullback of `f` and `g`,
+and then forming the standard pullback of the resulting `h ∘ f'` and `i`
+
+```text
+  (A ×_X B) ×_Y C ---------------------> C
+         | ⌟                             |
+         |                               | i
+         ∨                               ∨
+      A ×_X B ---------> B ------------> Y
+         | ⌟     f'      |       h
+         |               | g
+         ∨               ∨
+         A ------------> X,
+                 f
+```
+
+or we can first form the pullback of `h` and `i`, and then form the pullback of
+`f` and the resulting `g ∘ i'`:
+
+```text
+  A ×_X (B ×_Y C) --> B ×_Y C ---------> C
+         | ⌟             | ⌟             |
+         |               | i'            | i
+         |               ∨               ∨
+         |               B ------------> Y
+         |               |       h
+         |               | g
+         ∨               ∨
+         A ------------> X.
+                 f
+```
+
+We show that both of these constructions are equivalent by showing they are
+equivalent to the standard ternary pullback.
+
+**Note:** Associativity with respect to ternary cospans
+
+```text
+              B
+              |
+              | g
+              ∨
+    A ------> X <------ C
+         f         h
+```
+
+is a special case of what we consider here that is recovered by using
+
+```text
+      f       g       g       h
+  A ----> X <---- B ----> X <---- C.
+```
+
+- See also the following relevant stack exchange question:
+  [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks).
+
+#### Computing the left associated iterated standard pullback
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  map-left-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
+    standard-ternary-pullback f g h i
+  map-left-associative-standard-pullback ((a , b , p) , c , q) =
+    ( a , b , c , p , q)
+
+  map-inv-left-associative-standard-pullback :
+    standard-ternary-pullback f g h i →
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  map-inv-left-associative-standard-pullback (a , b , c , p , q) =
+    ( ( a , b , p) , c , q)
+
+  is-equiv-map-left-associative-standard-pullback :
+    is-equiv map-left-associative-standard-pullback
+  is-equiv-map-left-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-inv-left-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  compute-left-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
+    standard-ternary-pullback f g h i
+  compute-left-associative-standard-pullback =
+    ( map-left-associative-standard-pullback ,
+      is-equiv-map-left-associative-standard-pullback)
+```
+
+#### Computing the right associated iterated dependent pullback
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  map-right-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
+    standard-ternary-pullback f g h i
+  map-right-associative-standard-pullback (a , (b , c , p) , q) =
+    ( a , b , c , q , p)
+
+  map-inv-right-associative-standard-pullback :
+    standard-ternary-pullback f g h i →
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  map-inv-right-associative-standard-pullback (a , b , c , p , q) =
+    ( a , (b , c , q) , p)
+
+  is-equiv-map-right-associative-standard-pullback :
+    is-equiv map-right-associative-standard-pullback
+  is-equiv-map-right-associative-standard-pullback =
+    is-equiv-is-invertible
+      ( map-inv-right-associative-standard-pullback)
+      ( refl-htpy)
+      ( refl-htpy)
+
+  compute-right-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃
+    standard-ternary-pullback f g h i
+  compute-right-associative-standard-pullback =
+    ( map-right-associative-standard-pullback ,
+      is-equiv-map-right-associative-standard-pullback)
+```
+
+#### Standard pullbacks are associative
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5}
+  (f : A → X) (g : B → X) (h : B → Y) (i : C → Y)
+  where
+
+  associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  associative-standard-pullback =
+    ( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e
+    ( compute-left-associative-standard-pullback f g h i)
+
+  map-associative-standard-pullback :
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i →
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i})
+  map-associative-standard-pullback = map-equiv associative-standard-pullback
+
+  map-inv-associative-standard-pullback :
+    standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) →
+    standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i
+  map-inv-associative-standard-pullback =
+    map-inv-equiv associative-standard-pullback
+```
+
 ### Pullbacks can be "folded"
 
 Given a standard pullback square

diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md
@@ -189,7 +189,7 @@ module _
         ( horizontal-map-cone f g c)
         ( h)
         ( d)
-        ( is-pullback-top-is-pullback-rectangle f g h c d
+        ( is-pullback-top-square-is-pullback-rectangle f g h c d
           ( is-pullback-universal-property-pullback f g c up-pb-c)
           ( is-pullback-universal-property-pullback f (g ∘ h)
             ( pasting-vertical-cone f g h c d)
@@ -207,7 +207,7 @@ module _
         ( f)
         ( g ∘ h)
         ( pasting-vertical-cone f g h c d)
-        ( is-pullback-rectangle-is-pullback-top f g h c d
+        ( is-pullback-rectangle-is-pullback-top-square f g h c d
           ( is-pullback-universal-property-pullback f g c up-pb-c)
           ( is-pullback-universal-property-pullback
             ( horizontal-map-cone f g c)

diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md
@@ -420,7 +420,7 @@ module _
     is-orthogonal-pullback-condition f g →
     is-orthogonal-pullback-condition f (h ∘ g)
   is-orthogonal-pullback-condition-right-comp =
-    is-pullback-rectangle-is-pullback-top
+    is-pullback-rectangle-is-pullback-top-square
       ( precomp f Z)
       ( postcomp A h)
       ( postcomp A g)
@@ -452,7 +452,7 @@ module _
     is-orthogonal-pullback-condition f (h ∘ g) →
     is-orthogonal-pullback-condition f g
   is-orthogonal-pullback-condition-right-right-factor =
-    is-pullback-top-is-pullback-rectangle
+    is-pullback-top-square-is-pullback-rectangle
       ( precomp f Z)
       ( postcomp A h)
       ( postcomp A g)