From b4683ee5a97c7f925caae3a8449a30b1487021e4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 27 Feb 2024 15:48:51 +0100 Subject: [PATCH] `postcomposition-pullbacks` --- src/foundation.lagda.md | 1 + .../functoriality-function-types.lagda.md | 13 -- .../postcomposition-pullbacks.lagda.md | 185 ++++++++++++++++++ src/foundation/pullbacks.lagda.md | 65 ------ src/foundation/standard-pullbacks.lagda.md | 58 ------ .../universal-property-pullbacks.lagda.md | 52 ----- .../orthogonal-maps.lagda.md | 1 + 7 files changed, 187 insertions(+), 188 deletions(-) create mode 100644 src/foundation/postcomposition-pullbacks.lagda.md diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index b825958648..9902f6a670 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -275,6 +275,7 @@ open import foundation.pi-decompositions-subuniverse public open import foundation.pointed-torsorial-type-families public open import foundation.postcomposition-dependent-functions public open import foundation.postcomposition-functions public +open import foundation.postcomposition-pullbacks public open import foundation.powersets public open import foundation.precomposition-dependent-functions public open import foundation.precomposition-functions public diff --git a/src/foundation/functoriality-function-types.lagda.md b/src/foundation/functoriality-function-types.lagda.md index 98ca040496..b2d8dfe958 100644 --- a/src/foundation/functoriality-function-types.lagda.md +++ b/src/foundation/functoriality-function-types.lagda.md @@ -117,19 +117,6 @@ pr1 (emb-postcomp f A) = postcomp A (map-emb f) pr2 (emb-postcomp f A) = is-emb-postcomp-is-emb (map-emb f) (is-emb-map-emb f) A ``` -### Postcomposition cones - -```agda -postcomp-cone : - {l1 l2 l3 l4 l5 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5) - (f : A → X) (g : B → X) (c : cone f g C) → - cone (postcomp T f) (postcomp T g) (T → C) -pr1 (postcomp-cone T f g c) h = vertical-map-cone f g c ∘ h -pr1 (pr2 (postcomp-cone T f g c)) h = horizontal-map-cone f g c ∘ h -pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h) -``` - ## See also - Functorial properties of dependent function types are recorded in diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md new file mode 100644 index 0000000000..54c8c86c06 --- /dev/null +++ b/src/foundation/postcomposition-pullbacks.lagda.md @@ -0,0 +1,185 @@ +# Postcomposition of pullbacks + +```agda +module foundation.postcomposition-pullbacks where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.cones-over-cospan-diagrams +open import foundation.coproduct-types +open import foundation.dependent-pair-types +open import foundation.equality-coproduct-types +open import foundation.function-extensionality +open import foundation.functoriality-coproduct-types +open import foundation.functoriality-function-types +open import foundation.identity-types +open import foundation.universe-levels +open import foundation.whiskering-homotopies-composition + +open import foundation-core.equality-dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies +open import foundation-core.postcomposition-functions +open import foundation-core.pullbacks +open import foundation-core.retractions +open import foundation-core.sections +open import foundation-core.standard-pullbacks +open import foundation-core.universal-property-pullbacks +``` + +
+ +## Idea + +Given a [pullback](foundation-core.pullbacks.md) square + +```text + f' + C -------> B + | ⌟ | + g'| | g + ∨ ∨ + A -------> X + f +``` + +then the exponentiated square given by +[postcomposition](foundation-core.postcomposition-functions.md) + +```text + f' ∘ - + (T → C) ---------> (T → B) + | | + g' ∘ - | | g ∘ - + | | + ∨ ∨ + (T → A) ---------> (T → X) + f ∘ - +``` + +is a pullback square for any type `T`. + +## Definitions + +### Postcomposition cones + +```agda +postcomp-cone : + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} (T : UU l5) + (f : A → X) (g : B → X) (c : cone f g C) → + cone (postcomp T f) (postcomp T g) (T → C) +pr1 (postcomp-cone T f g c) h = vertical-map-cone f g c ∘ h +pr1 (pr2 (postcomp-cone T f g c)) h = horizontal-map-cone f g c ∘ h +pr2 (pr2 (postcomp-cone T f g c)) h = eq-htpy (coherence-square-cone f g c ·r h) +``` + +## Properties + +### Standard pullbacks are closed under postcomposition exponentiation + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) + (T : UU l4) + where + + map-postcomp-cone-standard-pullback : + standard-pullback (postcomp T f) (postcomp T g) → cone f g T + map-postcomp-cone-standard-pullback = tot (λ _ → tot (λ _ → htpy-eq)) + + abstract + is-equiv-map-postcomp-cone-standard-pullback : + is-equiv map-postcomp-cone-standard-pullback + is-equiv-map-postcomp-cone-standard-pullback = + is-equiv-tot-is-fiberwise-equiv + ( λ p → is-equiv-tot-is-fiberwise-equiv (λ q → funext (f ∘ p) (g ∘ q))) +``` + +### The precomposition action on cones computes as the gap map of a postcomposition cone + +```agda +triangle-map-postcomp-cone-standard-pullback : + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} + (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) → + cone-map f g c {T} ~ + map-postcomp-cone-standard-pullback f g T ∘ + gap (postcomp T f) (postcomp T g) (postcomp-cone T f g c) +triangle-map-postcomp-cone-standard-pullback T f g c h = + eq-pair-eq-fiber + ( eq-pair-eq-fiber + ( inv (is-section-eq-htpy (coherence-square-cone f g c ·r h)))) +``` + +### Pullbacks are closed under postcomposition exponentiation + +```agda +abstract + is-pullback-postcomp-is-pullback : + {l1 l2 l3 l4 l5 : 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 → + (T : UU l5) → + is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c) + is-pullback-postcomp-is-pullback f g c is-pb-c T = + is-equiv-top-map-triangle + ( cone-map f g c) + ( map-postcomp-cone-standard-pullback f g T) + ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) + ( triangle-map-postcomp-cone-standard-pullback T f g c) + ( is-equiv-map-postcomp-cone-standard-pullback f g T) + ( universal-property-pullback-is-pullback f g c is-pb-c T) + +abstract + is-pullback-is-pullback-postcomp : + {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) → + ( {l5 : Level} (T : UU l5) → + is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) → + is-pullback f g c + is-pullback-is-pullback-postcomp f g c is-pb-postcomp = + is-pullback-universal-property-pullback f g c + ( λ T → + is-equiv-left-map-triangle + ( cone-map f g c) + ( map-postcomp-cone-standard-pullback f g T) + ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) + ( triangle-map-postcomp-cone-standard-pullback T f g c) + ( is-pb-postcomp T) + ( is-equiv-map-postcomp-cone-standard-pullback f g T)) +``` + +### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} + (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) + where + + universal-property-pullback-postcomp : + universal-property-pullback f g c → + universal-property-pullback + ( postcomp T f) + ( postcomp T g) + ( postcomp-cone T f g c) + universal-property-pullback-postcomp H = + universal-property-pullback-is-pullback + ( postcomp T f) + ( postcomp T g) + ( postcomp-cone T f g c) + ( is-pullback-postcomp-is-pullback f g c + ( is-pullback-universal-property-pullback f g c H) + ( T)) +``` + +## Table of files about pullbacks + +The following table lists files that are about pullbacks as a general concept. + +{{#include tables/pullbacks.md}} diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index 2fb7fdc448..62849a0af0 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -86,71 +86,6 @@ module _ pr2 (is-pullback-Prop c) = is-prop-is-pullback c ``` -### Pullbacks are closed under exponentiation - -Given a pullback square - -```text - f' - C ---------> B - | ⌟ | - g'| | g - | | - v v - A ---------> X - f -``` - -then the exponentiated square given by postcomposition - -```text - f' ∘ - - (S → C) ---------> (S → B) - | | - g' ∘ - | | g ∘ - - | | - v v - (S → A) ---------> (S → X) - f ∘ - -``` - -is a pullback square for any type `S`. - -```agda -abstract - is-pullback-postcomp-is-pullback : - {l1 l2 l3 l4 l5 : 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 → - (T : UU l5) → - is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c) - is-pullback-postcomp-is-pullback f g c is-pb-c T = - is-equiv-top-map-triangle - ( cone-map f g c) - ( map-postcomp-cone-standard-pullback f g T) - ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) - ( triangle-map-postcomp-cone-standard-pullback T f g c) - ( is-equiv-map-postcomp-cone-standard-pullback f g T) - ( universal-property-pullback-is-pullback f g c is-pb-c T) - -abstract - is-pullback-is-pullback-postcomp : - {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) → - ( {l5 : Level} (T : UU l5) → - is-pullback (postcomp T f) (postcomp T g) (postcomp-cone T f g c)) → - is-pullback f g c - is-pullback-is-pullback-postcomp f g c is-pb-postcomp = - is-pullback-universal-property-pullback f g c - ( λ T → - is-equiv-left-map-triangle - ( cone-map f g c) - ( map-postcomp-cone-standard-pullback f g T) - ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) - ( triangle-map-postcomp-cone-standard-pullback T f g c) - ( is-pb-postcomp T) - ( is-equiv-map-postcomp-cone-standard-pullback f g T)) -``` - ### Identity types can be presented as pullbacks Identity types fit into pullback squares diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index d24dac2eee..f599b411b2 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -69,64 +69,6 @@ the canonical projections. ## Properties -### Standard pullbacks are closed under exponentiation - -Given a pullback square - -```text - f' - C ---------> B - | ⌟ | - g'| | g - | | - v v - A ---------> X - f -``` - -then the exponentiated square given by postcomposition - -```text - f' ∘ - - (S → C) ---------> (S → B) - | | - g' ∘ - | | g ∘ - - | | - v v - (S → A) ---------> (S → X) - f ∘ - -``` - -is a pullback square for any type `S`. - -```agda -map-postcomp-cone-standard-pullback : - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) - (T : UU l4) → standard-pullback (postcomp T f) (postcomp T g) → cone f g T -map-postcomp-cone-standard-pullback f g T = tot (λ _ → tot (λ _ → htpy-eq)) - -abstract - is-equiv-map-postcomp-cone-standard-pullback : - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) - (T : UU l4) → is-equiv (map-postcomp-cone-standard-pullback f g T) - is-equiv-map-postcomp-cone-standard-pullback f g T = - is-equiv-tot-is-fiberwise-equiv - ( λ p → is-equiv-tot-is-fiberwise-equiv (λ q → funext (f ∘ p) (g ∘ q))) - -triangle-map-postcomp-cone-standard-pullback : - {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} - (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) → - cone-map f g c {T} ~ - map-postcomp-cone-standard-pullback f g T ∘ - gap (postcomp T f) (postcomp T g) (postcomp-cone T f g c) -triangle-map-postcomp-cone-standard-pullback T f g c h = - eq-pair-eq-fiber - ( eq-pair-eq-fiber - ( inv (is-section-eq-htpy (coherence-square-cone f g c ·r h)))) -``` - ### The equivalence on standard pullbacks induced by parallel cospans ```agda diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index e2d9f1769c..787884c48c 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -243,58 +243,6 @@ module _ is-pullback-universal-property-pullback (f i) (g i) (c i) (H i))) ``` -### Pullbacks are closed under exponentiation - -Given a pullback square - -```text - f' - C ---------> B - | ⌟ | - g'| | g - | | - v v - A ---------> X - f -``` - -then the exponentiated square given by postcomposition - -```text - f' ∘ - - (S → C) ---------> (S → B) - | | - g' ∘ - | | g ∘ - - | | - v v - (S → A) ---------> (S → X) - f ∘ - -``` - -is a pullback square for any type `S`. - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4} - (T : UU l5) (f : A → X) (g : B → X) (c : cone f g C) - where - - universal-property-pullback-postcomp : - universal-property-pullback f g c → - universal-property-pullback - ( postcomp T f) - ( postcomp T g) - ( postcomp-cone T f g c) - universal-property-pullback-postcomp H = - universal-property-pullback-is-pullback - ( postcomp T f) - ( postcomp T g) - ( postcomp-cone T f g c) - ( is-pullback-postcomp-is-pullback f g c - ( is-pullback-universal-property-pullback f g c H) - ( T)) -``` - ## Table of files about pullbacks The following table lists files that are about pullbacks as a general concept. diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index ba9f041642..037e3d4401 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -26,6 +26,7 @@ open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.morphisms-arrows open import foundation.postcomposition-functions +open import foundation.postcomposition-pullbacks open import foundation.precomposition-functions open import foundation.products-pullbacks open import foundation.propositions