Pullbacks
module foundation-core.pullbacks where
Imports
open import foundation.functoriality-cartesian-product-types open import foundation.identity-types open import foundation.structure-identity-principle open import foundation.type-theoretic-principle-of-choice open import foundation-core.cartesian-product-types open import foundation-core.cones-over-cospans open import foundation-core.dependent-pair-types open import foundation-core.diagonal-maps-of-types open import foundation-core.equality-cartesian-product-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.functions open import foundation-core.functoriality-dependent-pair-types open import foundation-core.functoriality-fibers-of-maps open import foundation-core.homotopies open import foundation-core.morphisms-cospans open import foundation-core.type-arithmetic-dependent-pair-types open import foundation-core.universal-property-pullbacks open import foundation-core.universe-levels
Definitions
The canonical pullback of a cospan
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where canonical-pullback : UU ((l1 ⊔ l2) ⊔ l3) canonical-pullback = Σ A (λ x → Σ B (λ y → f x ＝ g y)) module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {f : A → X} {g : B → X} where π₁ : canonical-pullback f g → A π₁ = pr1 π₂ : canonical-pullback f g → B π₂ t = pr1 (pr2 t) π₃ : (f ∘ π₁) ~ (g ∘ π₂) π₃ t = pr2 (pr2 t)
The cone at the canonical pullback
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where cone-canonical-pullback : cone f g (canonical-pullback f g) pr1 cone-canonical-pullback = π₁ pr1 (pr2 cone-canonical-pullback) = π₂ pr2 (pr2 cone-canonical-pullback) = π₃
The gap-map into the canonical pullback
The gap map of a square is the map fron the vertex of the cone into the canonical pullback.
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) where gap : cone f g C → C → canonical-pullback f g pr1 (gap c z) = vertical-map-cone f g c z pr1 (pr2 (gap c z)) = horizontal-map-cone f g c z pr2 (pr2 (gap c z)) = coherence-square-cone f g c z
The is-pullback property
The proposition is-pullback is the assertion that the gap map is an equivalence. Note that this proposition is small, whereas the universal property is a large proposition.
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) where is-pullback : cone f g C → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-pullback c = is-equiv (gap f g c)
Functoriality of canonical pullbacks
module _ {l1 l2 l3 l1' l2' l3' : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') where map-canonical-pullback : hom-cospan f' g' f g → canonical-pullback f' g' → canonical-pullback f g pr1 (map-canonical-pullback (hA , _) (a' , _)) = hA a' pr1 (pr2 (map-canonical-pullback (hA , hB , _) (a' , b' , _))) = hB b' pr2 (pr2 (map-canonical-pullback (hA , hB , hX , HA , HB) (a' , b' , p'))) = (HA a') ∙ ((ap hX p') ∙ (inv (HB b')))
Properties
Characterization of the identity type of the canonical pullback
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where Eq-canonical-pullback : (t t' : canonical-pullback f g) → UU (l1 ⊔ l2 ⊔ l3) Eq-canonical-pullback (pair a bp) t' = let b = pr1 bp p = pr2 bp a' = pr1 t' b' = pr1 (pr2 t') p' = pr2 (pr2 t') in Σ (a ＝ a') (λ α → Σ (b ＝ b') (λ β → ((ap f α) ∙ p') ＝ (p ∙ (ap g β)))) refl-Eq-canonical-pullback : (t : canonical-pullback f g) → Eq-canonical-pullback t t pr1 (refl-Eq-canonical-pullback (pair a (pair b p))) = refl pr1 (pr2 (refl-Eq-canonical-pullback (pair a (pair b p)))) = refl pr2 (pr2 (refl-Eq-canonical-pullback (pair a (pair b p)))) = inv right-unit Eq-eq-canonical-pullback : (s t : canonical-pullback f g) → s ＝ t → Eq-canonical-pullback s t Eq-eq-canonical-pullback s .s refl = refl-Eq-canonical-pullback s extensionality-canonical-pullback : (t t' : canonical-pullback f g) → (t ＝ t') ≃ Eq-canonical-pullback t t' extensionality-canonical-pullback (pair a (pair b p)) = extensionality-Σ ( λ {a'} bp' α → Σ (b ＝ pr1 bp') (λ β → (ap f α ∙ pr2 bp') ＝ (p ∙ ap g β))) ( refl) ( pair refl (inv right-unit)) ( λ x → id-equiv) ( extensionality-Σ ( λ {b'} p' β → p' ＝ (p ∙ ap g β)) ( refl) ( inv right-unit) ( λ y → id-equiv) ( λ p' → equiv-concat' p' (inv right-unit) ∘e equiv-inv p p')) map-extensionality-canonical-pullback : { s t : canonical-pullback f g} ( α : π₁ s ＝ π₁ t) (β : π₂ s ＝ π₂ t) → ( ((ap f α) ∙ π₃ t) ＝ (π₃ s ∙ (ap g β))) → s ＝ t map-extensionality-canonical-pullback {s} {t} α β γ = map-inv-equiv ( extensionality-canonical-pullback s t) ( triple α β γ)
The canonical pullback satisfies the universal property of pullbacks
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where abstract universal-property-pullback-canonical-pullback : {l : Level} → universal-property-pullback l f g (cone-canonical-pullback f g) universal-property-pullback-canonical-pullback C = is-equiv-comp ( tot (λ p → map-distributive-Π-Σ)) ( mapping-into-Σ) ( is-equiv-mapping-into-Σ) ( is-equiv-tot-is-fiberwise-equiv ( λ p → is-equiv-map-distributive-Π-Σ))
A cone is equal to the value of cone-map at its own gap map
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) where htpy-cone-up-pullback-canonical-pullback : (c : cone f g C) → htpy-cone f g (cone-map f g (cone-canonical-pullback f g) (gap f g c)) c pr1 (htpy-cone-up-pullback-canonical-pullback c) = refl-htpy pr1 (pr2 (htpy-cone-up-pullback-canonical-pullback c)) = refl-htpy pr2 (pr2 (htpy-cone-up-pullback-canonical-pullback c)) = right-unit-htpy
A cone satisfies the universal property of the pullback if and only if the gap map is an equivalence
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) where abstract is-pullback-universal-property-pullback : (c : cone f g C) → ({l : Level} → universal-property-pullback l f g c) → is-pullback f g c is-pullback-universal-property-pullback c up = is-equiv-up-pullback-up-pullback ( cone-canonical-pullback f g) ( c) ( gap f g c) ( htpy-cone-up-pullback-canonical-pullback f g c) ( universal-property-pullback-canonical-pullback f g) ( up) abstract universal-property-pullback-is-pullback : (c : cone f g C) → is-pullback f g c → {l : Level} → universal-property-pullback l f g c universal-property-pullback-is-pullback c is-pullback-c = up-pullback-up-pullback-is-equiv ( cone-canonical-pullback f g) ( c) ( gap f g c) ( htpy-cone-up-pullback-canonical-pullback f g c) ( is-pullback-c) ( universal-property-pullback-canonical-pullback f g)
The pullback of a Σ-type
module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (f : A → B) (Q : B → UU l3) where canonical-pullback-Σ : UU (l1 ⊔ l3) canonical-pullback-Σ = Σ A (λ x → Q (f x)) cone-canonical-pullback-Σ : cone f (pr1 {B = Q}) canonical-pullback-Σ pr1 cone-canonical-pullback-Σ = pr1 pr1 (pr2 cone-canonical-pullback-Σ) = map-Σ-map-base f Q pr2 (pr2 cone-canonical-pullback-Σ) = refl-htpy inv-gap-cone-canonical-pullback-Σ : canonical-pullback f (pr1 {B = Q}) → canonical-pullback-Σ pr1 (inv-gap-cone-canonical-pullback-Σ (pair x (pair (pair .(f x) q) refl))) = x pr2 (inv-gap-cone-canonical-pullback-Σ (pair x (pair (pair .(f x) q) refl))) = q abstract issec-inv-gap-cone-canonical-pullback-Σ : ( ( gap f (pr1 {B = Q}) cone-canonical-pullback-Σ) ∘ ( inv-gap-cone-canonical-pullback-Σ)) ~ id issec-inv-gap-cone-canonical-pullback-Σ (pair x (pair (pair .(f x) q) refl)) = refl abstract isretr-inv-gap-cone-canonical-pullback-Σ : ( ( inv-gap-cone-canonical-pullback-Σ) ∘ ( gap f (pr1 {B = Q}) cone-canonical-pullback-Σ)) ~ id isretr-inv-gap-cone-canonical-pullback-Σ (pair x q) = refl abstract is-pullback-cone-canonical-pullback-Σ : is-pullback f (pr1 {B = Q}) cone-canonical-pullback-Σ is-pullback-cone-canonical-pullback-Σ = is-equiv-has-inverse inv-gap-cone-canonical-pullback-Σ issec-inv-gap-cone-canonical-pullback-Σ isretr-inv-gap-cone-canonical-pullback-Σ compute-canonical-pullback-Σ : canonical-pullback-Σ ≃ canonical-pullback f (pr1 {B = Q}) pr1 compute-canonical-pullback-Σ = gap f pr1 cone-canonical-pullback-Σ pr2 compute-canonical-pullback-Σ = is-pullback-cone-canonical-pullback-Σ
Pullbacks are symmetric
map-commutative-canonical-pullback : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → canonical-pullback f g → canonical-pullback g f pr1 (map-commutative-canonical-pullback f g x) = π₂ x pr1 (pr2 (map-commutative-canonical-pullback f g x)) = π₁ x pr2 (pr2 (map-commutative-canonical-pullback f g x)) = inv (π₃ x) inv-inv-map-commutative-canonical-pullback : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → ( map-commutative-canonical-pullback f g ∘ map-commutative-canonical-pullback g f) ~ id inv-inv-map-commutative-canonical-pullback f g x = eq-pair-Σ refl (eq-pair-Σ refl (inv-inv (π₃ x))) abstract is-equiv-map-commutative-canonical-pullback : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → is-equiv (map-commutative-canonical-pullback f g) is-equiv-map-commutative-canonical-pullback f g = is-equiv-has-inverse ( map-commutative-canonical-pullback g f) ( inv-inv-map-commutative-canonical-pullback f g) ( inv-inv-map-commutative-canonical-pullback g f) commutative-canonical-pullback : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → canonical-pullback f g ≃ canonical-pullback g f pr1 (commutative-canonical-pullback f g) = map-commutative-canonical-pullback f g pr2 (commutative-canonical-pullback f g) = is-equiv-map-commutative-canonical-pullback f g triangle-map-commutative-canonical-pullback : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → ( gap g f (swap-cone f g c)) ~ ( ( map-commutative-canonical-pullback f g) ∘ ( gap f g c)) triangle-map-commutative-canonical-pullback f g (pair p (pair q H)) x = refl abstract is-pullback-swap-cone : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c → is-pullback g f (swap-cone f g c) is-pullback-swap-cone f g c is-pb-c = is-equiv-comp-htpy ( gap g f (swap-cone f g c)) ( map-commutative-canonical-pullback f g) ( gap f g c) ( triangle-map-commutative-canonical-pullback f g c) ( is-pb-c) ( is-equiv-map-commutative-canonical-pullback f g) abstract is-pullback-swap-cone' : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → is-pullback g f (swap-cone f g c) → is-pullback f g c is-pullback-swap-cone' f g c is-pb-c' = is-equiv-right-factor-htpy ( gap g f (swap-cone f g c)) ( map-commutative-canonical-pullback f g) ( gap f g c) ( triangle-map-commutative-canonical-pullback f g c) ( is-equiv-map-commutative-canonical-pullback f g) ( is-pb-c')
Pullbacks can be "folded"
fold-cone : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) → cone f g C → cone (map-prod f g) (diagonal X) C pr1 (pr1 (fold-cone f g c) z) = vertical-map-cone f g c z pr2 (pr1 (fold-cone f g c) z) = horizontal-map-cone f g c z pr1 (pr2 (fold-cone f g c)) = g ∘ horizontal-map-cone f g c pr2 (pr2 (fold-cone f g c)) z = eq-pair (coherence-square-cone f g c z) refl map-fold-cone : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) → (g : B → X) → canonical-pullback f g → canonical-pullback (map-prod f g) (diagonal X) pr1 (pr1 (map-fold-cone f g x)) = π₁ x pr2 (pr1 (map-fold-cone f g x)) = π₂ x pr1 (pr2 (map-fold-cone f g x)) = g (π₂ x) pr2 (pr2 (map-fold-cone f g x)) = eq-pair (π₃ x) refl inv-map-fold-cone : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) → (g : B → X) → canonical-pullback (map-prod f g) (diagonal X) → canonical-pullback f g inv-map-fold-cone f g (pair (pair a b) (pair x α)) = triple a b ((ap pr1 α) ∙ (inv (ap pr2 α))) abstract issec-inv-map-fold-cone : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → ((map-fold-cone f g) ∘ (inv-map-fold-cone f g)) ~ id issec-inv-map-fold-cone {A = A} {B} {X} f g (pair (pair a b) (pair x α)) = map-extensionality-canonical-pullback ( map-prod f g) ( diagonal X) refl ( ap pr2 α) ( ( ( ( inv (issec-pair-eq α)) ∙ ( ap ( λ t → (eq-pair t (ap pr2 α))) ( ( ( inv right-unit) ∙ ( inv (ap (concat (ap pr1 α) x) (left-inv (ap pr2 α))))) ∙ ( inv (assoc (ap pr1 α) (inv (ap pr2 α)) (ap pr2 α)))))) ∙ ( eq-pair-concat ( (ap pr1 α) ∙ (inv (ap pr2 α))) ( ap pr2 α) ( refl) ( ap pr2 α))) ∙ ( ap ( concat ( eq-pair ((ap pr1 α) ∙ (inv (ap pr2 α))) refl) ( pair x x)) ( inv (ap-diagonal (ap pr2 α))))) abstract isretr-inv-map-fold-cone : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → ((inv-map-fold-cone f g) ∘ (map-fold-cone f g)) ~ id isretr-inv-map-fold-cone { A = A} { B = B} { X = X} f g (pair a (pair b p)) = map-extensionality-canonical-pullback {A = A} {B = B} {X = X} f g refl refl ( inv ( ( ap ( concat' (f a) refl) ( ( ( ap ( λ t → t ∙ ( inv ( ap pr2 (eq-pair { s = pair (f a) (g b)} { pair (g b) (g b)} p refl)))) ( ap-pr1-eq-pair p refl)) ∙ ( ap (λ t → p ∙ (inv t)) (ap-pr2-eq-pair p refl))) ∙ ( right-unit))) ∙ ( right-unit))) abstract is-equiv-map-fold-cone : {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) → is-equiv (map-fold-cone f g) is-equiv-map-fold-cone f g = is-equiv-has-inverse ( inv-map-fold-cone f g) ( issec-inv-map-fold-cone f g) ( isretr-inv-map-fold-cone f g) triangle-map-fold-cone : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → ( gap (map-prod f g) (diagonal X) (fold-cone f g c)) ~ ( (map-fold-cone f g) ∘ (gap f g c)) triangle-map-fold-cone f g (pair p (pair q H)) z = refl abstract is-pullback-fold-cone-is-pullback : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → is-pullback f g c → is-pullback (map-prod f g) (diagonal X) (fold-cone f g c) is-pullback-fold-cone-is-pullback f g c is-pb-c = is-equiv-comp-htpy ( gap (map-prod f g) (diagonal _) (fold-cone f g c)) ( map-fold-cone f g) ( gap f g c) ( triangle-map-fold-cone f g c) ( is-pb-c) ( is-equiv-map-fold-cone f g) abstract is-pullback-is-pullback-fold-cone : {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} (f : A → X) (g : B → X) (c : cone f g C) → is-pullback (map-prod f g) (diagonal X) (fold-cone f g c) → is-pullback f g c is-pullback-is-pullback-fold-cone f g c is-pb-fold = is-equiv-right-factor-htpy ( gap (map-prod f g) (diagonal _) (fold-cone f g c)) ( map-fold-cone f g) ( gap f g c) ( triangle-map-fold-cone f g c) ( is-equiv-map-fold-cone f g) ( is-pb-fold)
Products of pullbacks are pullbacks
prod-cone : {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') → cone f g C → cone f' g' C' → cone (map-prod f f') (map-prod g g') (C × C') pr1 (prod-cone f g f' g' (p , q , H) (p' , q' , H')) = map-prod p p' pr1 (pr2 (prod-cone f g f' g' (p , q , H) (p' , q' , H'))) = map-prod q q' pr2 (pr2 (prod-cone f g f' g' (p , q , H) (p' , q' , H'))) = ( inv-htpy (map-prod-comp p p' f f')) ∙h ( ( htpy-map-prod H H') ∙h ( map-prod-comp q q' g g')) map-prod-cone : {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') → (canonical-pullback f g) × (canonical-pullback f' g') → canonical-pullback (map-prod f f') (map-prod g g') map-prod-cone {A' = A'} {B'} f g f' g' = ( tot ( λ t → ( tot (λ s → eq-pair')) ∘ ( map-interchange-Σ-Σ (λ y p y' → Id (f' (pr2 t)) (g' y'))))) ∘ ( map-interchange-Σ-Σ (λ x t x' → Σ _ (λ y' → Id (f' x') (g' y')))) triangle-map-prod-cone : {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) (c : cone f g C) (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') → (gap (map-prod f f') (map-prod g g') (prod-cone f g f' g' c c')) ~ ((map-prod-cone f g f' g') ∘ (map-prod (gap f g c) (gap f' g' c'))) triangle-map-prod-cone {B' = B'} f g (pair p (pair q H)) f' g' (pair p' (pair q' H')) (pair z z') = eq-pair-Σ refl (eq-pair-Σ refl right-unit) abstract is-equiv-map-prod-cone : {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') → is-equiv (map-prod-cone f g f' g') is-equiv-map-prod-cone f g f' g' = 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' → Id (f' (pr2 t)) (g' y'))) ( is-equiv-map-interchange-Σ-Σ _) ( is-equiv-tot-is-fiberwise-equiv ( λ s → is-equiv-comp ( eq-pair') ( id) ( is-equiv-id) ( is-equiv-eq-pair ( map-prod f f' t) ( map-prod g g' s)))))) abstract is-pullback-prod-is-pullback-pair : {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) (c : cone f g C) (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') → is-pullback f g c → is-pullback f' g' c' → is-pullback ( map-prod f f') (map-prod g g') (prod-cone f g f' g' c c') is-pullback-prod-is-pullback-pair f g c f' g' c' is-pb-c is-pb-c' = is-equiv-comp-htpy ( gap (map-prod f f') (map-prod g g') (prod-cone f g f' g' c c')) ( map-prod-cone f g f' g') ( map-prod (gap f g c) (gap f' g' c')) ( triangle-map-prod-cone f g c f' g' c') ( is-equiv-map-prod _ _ is-pb-c is-pb-c') ( is-equiv-map-prod-cone f g f' g') abstract is-pullback-left-factor-is-pullback-prod : {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) (c : cone f g C) (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') → is-pullback ( map-prod f f') ( map-prod g g') ( prod-cone f g f' g' c c') → canonical-pullback f' g' → is-pullback f g c is-pullback-left-factor-is-pullback-prod f g c f' g' c' is-pb-cc' t = is-equiv-left-factor-is-equiv-map-prod (gap f g c) (gap f' g' c') t ( is-equiv-right-factor-htpy ( gap ( map-prod f f') ( map-prod g g') ( prod-cone f g f' g' c c')) ( map-prod-cone f g f' g') ( map-prod (gap f g c) (gap f' g' c')) ( triangle-map-prod-cone f g c f' g' c') ( is-equiv-map-prod-cone f g f' g') ( is-pb-cc')) abstract is-pullback-right-factor-is-pullback-prod : {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) (c : cone f g C) (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') → is-pullback ( map-prod f f') ( map-prod g g') ( prod-cone f g f' g' c c') → canonical-pullback f g → is-pullback f' g' c' is-pullback-right-factor-is-pullback-prod f g c f' g' c' is-pb-cc' t = is-equiv-right-factor-is-equiv-map-prod (gap f g c) (gap f' g' c') t ( is-equiv-right-factor-htpy ( gap ( map-prod f f') ( map-prod g g') ( prod-cone f g f' g' c c')) ( map-prod-cone f g f' g') ( map-prod (gap f g c) (gap f' g' c')) ( triangle-map-prod-cone f g c f' g' c') ( is-equiv-map-prod-cone 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
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {P : A → UU l3} (Q : B → UU l4) (f : A → B) (g : (x : A) → (P x) → (Q (f x))) where cone-map-Σ : cone f (pr1 {B = Q}) (Σ A P) pr1 cone-map-Σ = pr1 pr1 (pr2 cone-map-Σ) = map-Σ Q f g pr2 (pr2 cone-map-Σ) = refl-htpy abstract is-pullback-is-fiberwise-equiv : is-fiberwise-equiv g → is-pullback f (pr1 {B = Q}) cone-map-Σ is-pullback-is-fiberwise-equiv is-equiv-g = is-equiv-comp ( gap f pr1 (cone-canonical-pullback-Σ f Q)) ( tot g) ( is-equiv-tot-is-fiberwise-equiv is-equiv-g) ( is-pullback-cone-canonical-pullback-Σ f Q) abstract universal-property-pullback-is-fiberwise-equiv : is-fiberwise-equiv g → {l : Level} → universal-property-pullback l f (pr1 {B = Q}) cone-map-Σ universal-property-pullback-is-fiberwise-equiv is-equiv-g = universal-property-pullback-is-pullback f pr1 cone-map-Σ ( is-pullback-is-fiberwise-equiv is-equiv-g) abstract is-fiberwise-equiv-is-pullback : is-pullback f (pr1 {B = Q}) cone-map-Σ → is-fiberwise-equiv g is-fiberwise-equiv-is-pullback is-pullback-cone-map-Σ = is-fiberwise-equiv-is-equiv-tot ( is-equiv-right-factor ( gap f pr1 (cone-canonical-pullback-Σ f Q)) ( tot g) ( is-pullback-cone-canonical-pullback-Σ f Q) ( is-pullback-cone-map-Σ)) abstract is-fiberwise-equiv-universal-property-pullback : ( {l : Level} → universal-property-pullback l f (pr1 {B = Q}) cone-map-Σ) → is-fiberwise-equiv g is-fiberwise-equiv-universal-property-pullback up = is-fiberwise-equiv-is-pullback ( is-pullback-universal-property-pullback f pr1 cone-map-Σ up)
A cone is a pullback if and only if it induces a family of equivalences between the fibers of the vertical maps
module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (f : A → X) (g : B → X) (c : cone f g C) where square-tot-map-fib-cone : ( (gap f g c) ∘ (map-equiv-total-fib (pr1 c))) ~ ( (tot (λ a → tot (λ b → inv))) ∘ (tot (map-fib-cone f g c))) square-tot-map-fib-cone (pair .((vertical-map-cone f g c) x) (pair x refl)) = eq-pair-Σ refl ( eq-pair-Σ refl ( inv ( ( ap inv right-unit) ∙ ( inv-inv (coherence-square-cone f g c x))))) abstract is-fiberwise-equiv-map-fib-cone-is-pullback : is-pullback f g c → is-fiberwise-equiv (map-fib-cone f g c) is-fiberwise-equiv-map-fib-cone-is-pullback pb = is-fiberwise-equiv-is-equiv-tot ( is-equiv-top-is-equiv-bottom-square ( map-equiv-total-fib (vertical-map-cone f g c)) ( tot (λ x → tot (λ y → inv))) ( tot (map-fib-cone f g c)) ( gap f g c) ( square-tot-map-fib-cone) ( is-equiv-map-equiv-total-fib (vertical-map-cone f g c)) ( is-equiv-tot-is-fiberwise-equiv ( λ x → is-equiv-tot-is-fiberwise-equiv ( λ y → is-equiv-inv (g y) (f x)))) ( pb)) abstract is-pullback-is-fiberwise-equiv-map-fib-cone : is-fiberwise-equiv (map-fib-cone f g c) → is-pullback f g c is-pullback-is-fiberwise-equiv-map-fib-cone is-equiv-fsq = is-equiv-bottom-is-equiv-top-square ( map-equiv-total-fib (vertical-map-cone f g c)) ( tot (λ x → tot (λ y → inv))) ( tot (map-fib-cone f g c)) ( gap f g c) ( square-tot-map-fib-cone) ( is-equiv-map-equiv-total-fib (vertical-map-cone f g c)) ( is-equiv-tot-is-fiberwise-equiv ( λ x → is-equiv-tot-is-fiberwise-equiv ( λ y → is-equiv-inv (g y) (f x)))) ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq)
The horizontal pullback pasting property
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6} (i : X → Y) (j : Y → Z) (h : C → Z) where abstract is-pullback-rectangle-is-pullback-left-square : (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) → is-pullback j h c → is-pullback i (vertical-map-cone j h c) d → is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) is-pullback-rectangle-is-pullback-left-square c d is-pb-c is-pb-d = is-pullback-is-fiberwise-equiv-map-fib-cone (j ∘ i) h ( pasting-horizontal-cone i j h c d) ( λ x → is-equiv-comp-htpy ( map-fib-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x) ( map-fib-cone j h c (i x)) ( map-fib-cone i (vertical-map-cone j h c) d x) ( map-fib-pasting-horizontal-cone i j h c d x) ( is-fiberwise-equiv-map-fib-cone-is-pullback i ( vertical-map-cone j h c) ( d) ( is-pb-d) ( x)) ( is-fiberwise-equiv-map-fib-cone-is-pullback j h c is-pb-c (i x))) abstract is-pullback-left-square-is-pullback-rectangle : (c : cone j h B) (d : cone i (vertical-map-cone j h c) A) → is-pullback j h c → is-pullback (j ∘ i) h (pasting-horizontal-cone i j h c d) → is-pullback i (vertical-map-cone j h c) d is-pullback-left-square-is-pullback-rectangle c d is-pb-c is-pb-rect = is-pullback-is-fiberwise-equiv-map-fib-cone i ( vertical-map-cone j h c) ( d) ( λ x → is-equiv-right-factor-htpy ( map-fib-cone (j ∘ i) h (pasting-horizontal-cone i j h c d) x) ( map-fib-cone j h c (i x)) ( map-fib-cone i (vertical-map-cone j h c) d x) ( map-fib-pasting-horizontal-cone i j h c d x) ( is-fiberwise-equiv-map-fib-cone-is-pullback j h c is-pb-c (i x)) ( is-fiberwise-equiv-map-fib-cone-is-pullback (j ∘ i) h ( pasting-horizontal-cone i j h c d) is-pb-rect x))
The vertical pullback pasting property
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} {Y : UU l5} {Z : UU l6} (f : C → Z) (g : Y → Z) (h : X → Y) where abstract is-pullback-top-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-is-fiberwise-equiv-map-fib-cone ( horizontal-map-cone f g c) ( h) ( d) ( λ x → is-fiberwise-equiv-is-equiv-map-Σ ( λ t → fib h (pr1 t)) ( map-fib-cone f g c (vertical-map-cone f g c x)) ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t)) ( is-fiberwise-equiv-map-fib-cone-is-pullback f g c is-pb-c ( vertical-map-cone f g c x)) ( is-equiv-top-is-equiv-bottom-square ( inv-map-compute-fib-comp ( vertical-map-cone f g c) ( vertical-map-cone (horizontal-map-cone f g c) h d) ( vertical-map-cone f g c x)) ( inv-map-compute-fib-comp g h (f (vertical-map-cone f g c x))) ( map-Σ ( λ t → fib h (pr1 t)) ( map-fib-cone f g c (vertical-map-cone f g c x)) ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t))) ( map-fib-cone f ( g ∘ h) ( pasting-vertical-cone f g h c d) ( vertical-map-cone f g c x)) ( map-fib-pasting-vertical-cone f g h c d ( vertical-map-cone f g c x)) ( is-equiv-inv-map-compute-fib-comp ( vertical-map-cone f g c) ( vertical-map-cone (horizontal-map-cone f g c) h d) ( vertical-map-cone f g c x)) ( is-equiv-inv-map-compute-fib-comp g h ( f (vertical-map-cone f g c x))) ( is-fiberwise-equiv-map-fib-cone-is-pullback f ( g ∘ h) ( pasting-vertical-cone f g h c d) ( is-pb-dc) ( vertical-map-cone f g c x))) ( pair x refl)) abstract is-pullback-rectangle-is-pullback-top : (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-is-fiberwise-equiv-map-fib-cone f (g ∘ h) ( pasting-vertical-cone f g h c d) ( λ x → is-equiv-bottom-is-equiv-top-square ( inv-map-compute-fib-comp ( vertical-map-cone f g c) ( vertical-map-cone (horizontal-map-cone f g c) h d) ( x)) ( inv-map-compute-fib-comp g h (f x)) ( map-Σ ( λ t → fib h (pr1 t)) ( map-fib-cone f g c x) ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t))) ( map-fib-cone f (g ∘ h) (pasting-vertical-cone f g h c d) x) ( map-fib-pasting-vertical-cone f g h c d x) ( is-equiv-inv-map-compute-fib-comp ( vertical-map-cone f g c) ( vertical-map-cone (horizontal-map-cone f g c) h d) ( x)) ( is-equiv-inv-map-compute-fib-comp g h (f x)) ( is-equiv-map-Σ ( λ t → fib h (pr1 t)) ( map-fib-cone f g c x) ( λ t → map-fib-cone (horizontal-map-cone f g c) h d (pr1 t)) ( is-fiberwise-equiv-map-fib-cone-is-pullback f g c is-pb-c x) ( λ t → is-fiberwise-equiv-map-fib-cone-is-pullback (horizontal-map-cone f g c) h d is-pb-d (pr1 t))))