From 9e1843b98bcf410d8a8208b1d38dcabf9e97ae2b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 28 Feb 2024 14:51:28 +0100 Subject: [PATCH] remove associativity of standard pullbacks --- src/foundation/standard-pullbacks.lagda.md | 171 --------------------- 1 file changed, 171 deletions(-) diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index 54fb69560b..24ab985b00 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -271,177 +271,6 @@ triangle-map-commutative-standard-pullback : triangle-map-commutative-standard-pullback f g c = refl-htpy ``` -### Associativity of standard pullbacks - -Consider two cospans with a shared vertex - -```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 giving a definition -of the standard ternary pullback, and show that both are equivalent to it. - -**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: - [Assocaitivity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks). - -#### The standard ternary 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 - - 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)))) -``` - -#### 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) -``` - ### Pullbacks can be "folded" Given a standard pullback square