From 8fa9db7580b6b33ea64e4956490626fcba612a3f Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 28 Feb 2024 13:57:08 +0100 Subject: [PATCH] associativity of standard pullbacks --- src/foundation/standard-pullbacks.lagda.md | 163 ++++++++++++++++++++- 1 file changed, 161 insertions(+), 2 deletions(-) diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index 4d73beac89..a54c15dd18 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -20,6 +20,7 @@ open import foundation-core.commuting-squares-of-maps open import foundation-core.diagonal-maps-of-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences +open import foundation-core.cartesian-product-types open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies @@ -270,6 +271,161 @@ triangle-map-commutative-standard-pullback : triangle-map-commutative-standard-pullback f g c = refl-htpy ``` +### Associativity of standard pullbacks with respect to ternary cospans + +Given a ternary cospan on a type `X` + +```text + B + | + | g + ∨ + A ------> X <------ C + f h +``` + +There are two ways to construct the limit using iterated standard pullbacks. +Namely, we may first form the standard pullback of `f` and `g` + +```text + f' + A ×_X B ---> B + | ⌟ | + g' | | g + ∨ ∨ + A ------> X <------ C + f h +``` + +and then form the standard pullback of `g ∘ f'` and `h` + +```text + + A ×_X B <- (A ×_X B) ×_X C + / | ⌞ | + g' / | g ∘ f' | + ∨ ∨ ∨ + A ------> X <---------- C. + f h +``` + +Or, we may do it the other way around by first forming the standard pullback of +`g` and `h` and then forming the standard pullback of `f` and the resulting +`g ∘ h'` + +```text + A ×_X (B ×_X C) -> B ×_X C + | ⌟ | \ + | g ∘ h' | \ g' + ∨ ∨ ∨ + A ----------> X <------ C. + f h +``` + +We show that these two constructions are equivalent by considering the standard +ternary pullback, and showing that they are both equivalent to this. + +#### The standard ternary pullback + +```agda +module _ + {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} + (f : A → X) (g : B → X) (h : C → X) + where + + standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + standard-ternary-pullback = + Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (g b ＝ h c)))) +``` + +#### Computing the left associated iterated standard pullback + +```agda +module _ + {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} + (f : A → X) (g : B → X) (h : C → X) + where + + map-left-associative-standard-pullback : + standard-pullback (g ∘ horizontal-map-standard-pullback {f = f} {g = g}) h → + standard-ternary-pullback f g h + 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 → + standard-pullback (g ∘ horizontal-map-standard-pullback {f = f} {g = g}) h + 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 (g ∘ horizontal-map-standard-pullback {f = f} {g = g}) h ≃ + standard-ternary-pullback f g h + compute-left-associative-standard-pullback = + ( map-left-associative-standard-pullback , + is-equiv-map-left-associative-standard-pullback) +``` + +#### Computing the right associated iterated standard pullback + +```agda +module _ + {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} + (f : A → X) (g : B → X) (h : C → X) + where + + map-right-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = g} {g = h}) → + standard-ternary-pullback f g h + 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 → + standard-pullback f (g ∘ vertical-map-standard-pullback {f = g} {g = h}) + 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 = g} {g = h}) ≃ + standard-ternary-pullback f g h + compute-right-associative-standard-pullback = + ( map-right-associative-standard-pullback , + is-equiv-map-right-associative-standard-pullback) +``` + +#### Standard pullbacks are associative with respect to ternary cospans + +```agda +module _ + {l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3} {C : UU l4} + (f : A → X) (g : B → X) (h : C → X) + where + + associative-standard-pullback : + standard-pullback (g ∘ horizontal-map-standard-pullback {f = f} {g = g}) h ≃ + standard-pullback f (g ∘ vertical-map-standard-pullback {f = g} {g = h}) + associative-standard-pullback = + ( inv-equiv (compute-right-associative-standard-pullback f g h)) ∘e + ( compute-left-associative-standard-pullback f g h) +``` + ### Pullbacks can be "folded" Given a standard pullback square @@ -388,6 +544,11 @@ module _ ( is-section-map-inv-fold-cone-standard-pullback) ( is-retraction-map-inv-fold-cone-standard-pullback) + compute-fold-standard-pullback : + standard-pullback f g ≃ standard-pullback (map-product f g) (diagonal X) + compute-fold-standard-pullback = + map-fold-cone-standard-pullback , is-equiv-map-fold-cone-standard-pullback + triangle-map-fold-cone-standard-pullback : {l4 : Level} {C : UU l4} (c : cone f g C) → gap (map-product f g) (diagonal X) (fold-cone c) ~ @@ -395,8 +556,6 @@ module _ triangle-map-fold-cone-standard-pullback c = refl-htpy ``` -## Properties - ### The equivalence on standard pullbacks induced by parallel cospans ```agda