From 17b217300058bfcdf1d7b2f8df76f49bb9923aed Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 12 Mar 2025 14:07:01 +0000 Subject: [PATCH 01/10] `anodyne-maps` --- src/foundation-core/fibers-of-maps.lagda.md | 56 +++- src/foundation-core/pullbacks.lagda.md | 89 ++++++ src/foundation/equivalences-arrows.lagda.md | 9 +- src/foundation/fibers-of-maps.lagda.md | 39 +++ .../functoriality-fibers-of-maps.lagda.md | 53 ++++ src/foundation/morphisms-arrows.lagda.md | 38 +-- .../postcomposition-pullbacks.lagda.md | 68 +++-- ...ype-arithmetic-standard-pullbacks.lagda.md | 6 +- src/orthogonal-factorization-systems.lagda.md | 2 + .../anodyne-maps.lagda.md | 172 ++++++++++++ .../maps-local-at-maps.lagda.md | 13 + .../orthogonal-maps.lagda.md | 259 +++++++++++++++-- .../weakly-anodyne-maps.lagda.md | 89 ++++++ .../cocartesian-morphisms-arrows.lagda.md | 44 +++ ...a-equivalence-types-over-pushouts.lagda.md | 25 +- ...data-function-types-over-pushouts.lagda.md | 28 +- ...data-identity-types-over-pushouts.lagda.md | 4 +- .../descent-data-pushouts.lagda.md | 170 ++++++++++- .../descent-property-pushouts.lagda.md | 12 +- ...quivalences-descent-data-pushouts.lagda.md | 265 ++++++++++++++++-- .../families-descent-data-pushouts.lagda.md | 30 +- .../flattening-lemma-coequalizers.lagda.md | 31 +- .../flattening-lemma-pushouts.lagda.md | 37 ++- ...ity-systems-descent-data-pushouts.lagda.md | 41 +-- .../morphisms-descent-data-pushouts.lagda.md | 40 +-- .../pushouts.lagda.md | 22 ++ .../sections-descent-data-pushouts.lagda.md | 28 +- .../universal-property-coequalizers.lagda.md | 19 +- .../universal-property-pushouts.lagda.md | 71 +++++ 29 files changed, 1479 insertions(+), 281 deletions(-) create mode 100644 src/orthogonal-factorization-systems/anodyne-maps.lagda.md create mode 100644 src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md index 12a441cd2d..0376de9e04 100644 --- a/src/foundation-core/fibers-of-maps.lagda.md +++ b/src/foundation-core/fibers-of-maps.lagda.md @@ -52,6 +52,13 @@ module _ compute-value-inclusion-fiber : (y : fiber f b) → f (inclusion-fiber y) ＝ b compute-value-inclusion-fiber = pr2 + + inclusion-fiber' : fiber' f b → A + inclusion-fiber' = pr1 + + compute-value-inclusion-fiber' : + (y : fiber' f b) → b ＝ f (inclusion-fiber' y) + compute-value-inclusion-fiber' = pr2 ``` ## Properties @@ -280,9 +287,7 @@ module _ triangle-map-equiv-total-fiber t = inv (pr2 (pr2 t)) map-inv-equiv-total-fiber : A → Σ B (fiber f) - pr1 (map-inv-equiv-total-fiber x) = f x - pr1 (pr2 (map-inv-equiv-total-fiber x)) = x - pr2 (pr2 (map-inv-equiv-total-fiber x)) = refl + map-inv-equiv-total-fiber x = (f x , x , refl) is-retraction-map-inv-equiv-total-fiber : is-retraction map-equiv-total-fiber map-inv-equiv-total-fiber @@ -316,6 +321,51 @@ module _ pr2 inv-equiv-total-fiber = is-equiv-map-inv-equiv-total-fiber ``` +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + map-equiv-total-fiber' : Σ B (fiber' f) → A + map-equiv-total-fiber' t = pr1 (pr2 t) + + triangle-map-equiv-total-fiber' : pr1 ~ f ∘ map-equiv-total-fiber' + triangle-map-equiv-total-fiber' t = pr2 (pr2 t) + + map-inv-equiv-total-fiber' : A → Σ B (fiber' f) + map-inv-equiv-total-fiber' x = (f x , x , refl) + + is-retraction-map-inv-equiv-total-fiber' : + is-retraction map-equiv-total-fiber' map-inv-equiv-total-fiber' + is-retraction-map-inv-equiv-total-fiber' (.(f x) , x , refl) = refl + + is-section-map-inv-equiv-total-fiber' : + is-section map-equiv-total-fiber' map-inv-equiv-total-fiber' + is-section-map-inv-equiv-total-fiber' x = refl + + is-equiv-map-equiv-total-fiber' : is-equiv map-equiv-total-fiber' + is-equiv-map-equiv-total-fiber' = + is-equiv-is-invertible + map-inv-equiv-total-fiber' + is-section-map-inv-equiv-total-fiber' + is-retraction-map-inv-equiv-total-fiber' + + is-equiv-map-inv-equiv-total-fiber' : is-equiv map-inv-equiv-total-fiber' + is-equiv-map-inv-equiv-total-fiber' = + is-equiv-is-invertible + map-equiv-total-fiber' + is-retraction-map-inv-equiv-total-fiber' + is-section-map-inv-equiv-total-fiber' + + equiv-total-fiber' : Σ B (fiber' f) ≃ A + pr1 equiv-total-fiber' = map-equiv-total-fiber' + pr2 equiv-total-fiber' = is-equiv-map-equiv-total-fiber' + + inv-equiv-total-fiber' : A ≃ Σ B (fiber' f) + pr1 inv-equiv-total-fiber' = map-inv-equiv-total-fiber' + pr2 inv-equiv-total-fiber' = is-equiv-map-inv-equiv-total-fiber' +``` + ### Fibers of compositions ```agda diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index 332e6e96e2..0170c208fc 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -309,6 +309,86 @@ the vertical maps is a family of equivalences f ``` +```agda +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 + + triangle-tot-map-fiber-vertical-map-cone' : + tot (map-fiber-vertical-map-cone' f g c) ~ + gap f g c ∘ map-equiv-total-fiber' (vertical-map-cone f g c) + triangle-tot-map-fiber-vertical-map-cone' + (.(vertical-map-cone f g c x) , x , refl) = refl + + abstract + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' : + is-pullback f g c → + is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb = + is-fiberwise-equiv-is-equiv-tot + ( is-equiv-left-map-triangle + ( tot (map-fiber-vertical-map-cone' f g c)) + ( gap f g c) + ( map-equiv-total-fiber' (vertical-map-cone f g c)) + ( triangle-tot-map-fiber-vertical-map-cone') + ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c)) + ( pb)) + + fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' : + is-pullback f g c → (x : A) → + fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x) + fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x = + ( map-fiber-vertical-map-cone' f g c x , + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb x) + + equiv-tot-map-fiber-vertical-map-cone-is-pullback' : + is-pullback f g c → + Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f) + equiv-tot-map-fiber-vertical-map-cone-is-pullback' pb = + equiv-tot (fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' pb) + + abstract + is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' : + is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) → + is-pullback f g c + is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone' is-equiv-fsq = + is-equiv-right-map-triangle + ( tot (map-fiber-vertical-map-cone' f g c)) + ( gap f g c) + ( map-equiv-total-fiber' (vertical-map-cone f g c)) + ( triangle-tot-map-fiber-vertical-map-cone') + ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq) + ( is-equiv-map-equiv-total-fiber' (vertical-map-cone f g c)) + + abstract + is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' : + universal-property-pullback f g c → + is-fiberwise-equiv (map-fiber-vertical-map-cone' f g c) + is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + up = + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback' + ( is-pullback-universal-property-pullback f g c up) + + fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' : + universal-property-pullback f g c → (x : A) → + fiber' (vertical-map-cone f g c) x ≃ fiber' g (f x) + fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + pb x = + ( map-fiber-vertical-map-cone' f g c x , + is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + ( pb) + ( x)) + + equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' : + universal-property-pullback f g c → + Σ A (fiber' (vertical-map-cone f g c)) ≃ Σ A (fiber' g ∘ f) + equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' pb = + equiv-tot + ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + ( pb)) +``` + ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} @@ -356,6 +436,15 @@ module _ ( λ x → is-equiv-tot-is-fiberwise-equiv (λ y → is-equiv-inv (g y) (f x)))) ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq) + + abstract + is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback : + universal-property-pullback f g c → + is-fiberwise-equiv (map-fiber-vertical-map-cone f g c) + is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback + up = + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback + ( is-pullback-universal-property-pullback f g c up) ``` ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps diff --git a/src/foundation/equivalences-arrows.lagda.md b/src/foundation/equivalences-arrows.lagda.md index 23e82b5948..de15f1eb08 100644 --- a/src/foundation/equivalences-arrows.lagda.md +++ b/src/foundation/equivalences-arrows.lagda.md @@ -87,8 +87,7 @@ module _ coherence-hom-arrow f g (map-equiv i) (map-equiv j) equiv-arrow : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - equiv-arrow = - Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i)) + equiv-arrow = Σ (A ≃ X) (λ i → Σ (B ≃ Y) (coherence-equiv-arrow i)) module _ (e : equiv-arrow) @@ -100,6 +99,9 @@ module _ map-domain-equiv-arrow : A → X map-domain-equiv-arrow = map-equiv equiv-domain-equiv-arrow + map-inv-domain-equiv-arrow : X → A + map-inv-domain-equiv-arrow = map-inv-equiv equiv-domain-equiv-arrow + is-equiv-map-domain-equiv-arrow : is-equiv map-domain-equiv-arrow is-equiv-map-domain-equiv-arrow = is-equiv-map-equiv equiv-domain-equiv-arrow @@ -110,6 +112,9 @@ module _ map-codomain-equiv-arrow : B → Y map-codomain-equiv-arrow = map-equiv equiv-codomain-equiv-arrow + map-inv-codomain-equiv-arrow : Y → B + map-inv-codomain-equiv-arrow = map-inv-equiv equiv-codomain-equiv-arrow + is-equiv-map-codomain-equiv-arrow : is-equiv map-codomain-equiv-arrow is-equiv-map-codomain-equiv-arrow = is-equiv-map-equiv equiv-codomain-equiv-arrow diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md index 01e4a3f77b..c6205c190d 100644 --- a/src/foundation/fibers-of-maps.lagda.md +++ b/src/foundation/fibers-of-maps.lagda.md @@ -141,6 +141,45 @@ module _ {y y' : B} (p : y ＝ y') (u : fiber f y) → tot (λ x → concat' _ p) u ＝ tr (fiber f) p u compute-tr-fiber refl u = ap (pair _) right-unit + + inv-compute-tr-fiber : + {y y' : B} (p : y ＝ y') (u : fiber f y) → + tr (fiber f) p u ＝ tot (λ x → concat' _ p) u + inv-compute-tr-fiber p u = inv (compute-tr-fiber p u) + + compute-tr-fiber' : + {y y' : B} (p : y ＝ y') (u : fiber' f y) → + tot (λ x q → inv p ∙ q) u ＝ tr (fiber' f) p u + compute-tr-fiber' refl u = refl + + inv-compute-tr-fiber' : + {y y' : B} (p : y ＝ y') (u : fiber' f y) → + tr (fiber' f) p u ＝ tot (λ x q → inv p ∙ q) u + inv-compute-tr-fiber' p u = inv (compute-tr-fiber' p u) +``` + +### Transport in fibers along the fiber + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) + where + + compute-tr-self-fiber : + {y : B} (u : fiber f y) → (pr1 u , refl) ＝ tr (fiber f) (inv (pr2 u)) u + compute-tr-self-fiber (._ , refl) = refl + + inv-compute-tr-self-fiber : + {y : B} (u : fiber f y) → tr (fiber f) (inv (pr2 u)) u ＝ (pr1 u , refl) + inv-compute-tr-self-fiber u = inv (compute-tr-self-fiber u) + + compute-tr-self-fiber' : + {y : B} (u : fiber' f y) → (pr1 u , refl) ＝ tr (fiber' f) (pr2 u) u + compute-tr-self-fiber' (._ , refl) = refl + + inv-compute-tr-self-fiber' : + {y : B} (u : fiber' f y) → tr (fiber' f) (pr2 u) u ＝ (pr1 u , refl) + inv-compute-tr-self-fiber' u = inv (compute-tr-self-fiber' u) ``` ## Table of files about fibers of maps diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index 5beb6de9e9..b27b46aa09 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -103,6 +103,41 @@ module _ pr1 hom-arrow-fiber = map-domain-hom-arrow-fiber pr1 (pr2 hom-arrow-fiber) = map-codomain-hom-arrow-fiber pr2 (pr2 hom-arrow-fiber) = coh-hom-arrow-fiber + +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (α : hom-arrow f g) (b : B) + where + + map-domain-hom-arrow-fiber' : + fiber' f b → fiber' g (map-codomain-hom-arrow f g α b) + map-domain-hom-arrow-fiber' = + map-Σ _ + ( map-domain-hom-arrow f g α) + ( λ a p → ap (map-codomain-hom-arrow f g α) p ∙ coh-hom-arrow f g α a) + + map-fiber' : + fiber' f b → fiber' g (map-codomain-hom-arrow f g α b) + map-fiber' = map-domain-hom-arrow-fiber' + + map-codomain-hom-arrow-fiber' : A → X + map-codomain-hom-arrow-fiber' = map-domain-hom-arrow f g α + + coh-hom-arrow-fiber' : + coherence-square-maps + ( map-domain-hom-arrow-fiber') + ( inclusion-fiber' f) + ( inclusion-fiber' g) + ( map-domain-hom-arrow f g α) + coh-hom-arrow-fiber' = refl-htpy + + hom-arrow-fiber' : + hom-arrow + ( inclusion-fiber' f {b}) + ( inclusion-fiber' g {map-codomain-hom-arrow f g α b}) + pr1 hom-arrow-fiber' = map-domain-hom-arrow-fiber' + pr1 (pr2 hom-arrow-fiber') = map-codomain-hom-arrow-fiber' + pr2 (pr2 hom-arrow-fiber') = coh-hom-arrow-fiber' ``` ### Any cone induces a family of maps between the fibers of the vertical maps @@ -121,6 +156,15 @@ module _ ( g) ( hom-arrow-cone f g c) ( a) + + map-fiber-vertical-map-cone' : + fiber' (vertical-map-cone f g c) a → fiber' g (f a) + map-fiber-vertical-map-cone' = + map-domain-hom-arrow-fiber' + ( vertical-map-cone f g c) + ( g) + ( hom-arrow-cone f g c) + ( a) ``` ### Any cone induces a family of maps between the fibers of the vertical maps @@ -139,6 +183,15 @@ module _ ( f) ( hom-arrow-cone' f g c) ( b) + + map-fiber-horizontal-map-cone' : + fiber' (horizontal-map-cone f g c) b → fiber' f (g b) + map-fiber-horizontal-map-cone' = + map-domain-hom-arrow-fiber' + ( horizontal-map-cone f g c) + ( f) + ( hom-arrow-cone' f g c) + ( b) ``` ### For any `f : A → B` and any identification `p : b ＝ b'` in `B`, we obtain a morphism of arrows between the fiber inclusion at `b` to the fiber inclusion at `b'` diff --git a/src/foundation/morphisms-arrows.lagda.md b/src/foundation/morphisms-arrows.lagda.md index b80513a416..7abfa99887 100644 --- a/src/foundation/morphisms-arrows.lagda.md +++ b/src/foundation/morphisms-arrows.lagda.md @@ -10,6 +10,8 @@ module foundation.morphisms-arrows where open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.function-extensionality +open import foundation.postcomposition-functions +open import foundation.precomposition-functions open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -19,8 +21,6 @@ open import foundation-core.functoriality-dependent-function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types -open import foundation-core.postcomposition-functions -open import foundation-core.precomposition-functions ``` @@ -309,19 +309,25 @@ A morphism of arrows `α : f → g` gives a morphism of precomposition arrows ```agda module _ - {l1 l2 l3 l4 : Level} + {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} (f : A → B) (g : X → Y) (α : hom-arrow f g) + (S : UU l) where - precomp-hom-arrow : - {l : Level} (S : UU l) → hom-arrow (precomp g S) (precomp f S) - pr1 (precomp-hom-arrow S) = - precomp (map-codomain-hom-arrow f g α) S - pr1 (pr2 (precomp-hom-arrow S)) = - precomp (map-domain-hom-arrow f g α) S - pr2 (pr2 (precomp-hom-arrow S)) h = - inv (eq-htpy (h ·l coh-hom-arrow f g α)) + transpose-precomp-hom-arrow : + hom-arrow + ( precomp (map-codomain-hom-arrow f g α) S) + ( precomp (map-domain-hom-arrow f g α) S) + transpose-precomp-hom-arrow = + ( precomp g S , precomp f S , htpy-precomp (coh-hom-arrow f g α) S) + + precomp-hom-arrow : hom-arrow (precomp g S) (precomp f S) + precomp-hom-arrow = + transpose-hom-arrow + ( precomp (map-codomain-hom-arrow f g α) S) + ( precomp (map-domain-hom-arrow f g α) S) + ( transpose-precomp-hom-arrow) ``` ### Morphisms of arrows give morphisms of postcomposition arrows @@ -338,12 +344,10 @@ module _ postcomp-hom-arrow : {l : Level} (S : UU l) → hom-arrow (postcomp S f) (postcomp S g) - pr1 (postcomp-hom-arrow S) = - postcomp S (map-domain-hom-arrow f g α) - pr1 (pr2 (postcomp-hom-arrow S)) = - postcomp S (map-codomain-hom-arrow f g α) - pr2 (pr2 (postcomp-hom-arrow S)) h = - eq-htpy (coh-hom-arrow f g α ·r h) + postcomp-hom-arrow S = + ( postcomp S (map-domain-hom-arrow f g α) , + postcomp S (map-codomain-hom-arrow f g α) , + htpy-postcomp S (coh-hom-arrow f g α)) ``` ## See also diff --git a/src/foundation/postcomposition-pullbacks.lagda.md b/src/foundation/postcomposition-pullbacks.lagda.md index b24c28bb74..f5f0528db2 100644 --- a/src/foundation/postcomposition-pullbacks.lagda.md +++ b/src/foundation/postcomposition-pullbacks.lagda.md @@ -11,6 +11,7 @@ open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.identity-types +open import foundation.postcomposition-functions open import foundation.standard-pullbacks open import foundation.universe-levels open import foundation.whiskering-homotopies-composition @@ -21,7 +22,6 @@ 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.universal-property-pullbacks ``` @@ -68,9 +68,10 @@ postcomp-cone : {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) +postcomp-cone T f g c = + ( postcomp T (vertical-map-cone f g c) , + postcomp T (horizontal-map-cone f g c) , + htpy-postcomp T (coherence-square-cone f g c)) ``` ## Properties @@ -121,38 +122,33 @@ triangle-map-standard-pullback-postcomp T f g c 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-standard-pullback-postcomp f g T) - ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) - ( triangle-map-standard-pullback-postcomp T f g c) - ( is-equiv-map-standard-pullback-postcomp 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-standard-pullback-postcomp f g T) - ( gap (f ∘_) (g ∘_) (postcomp-cone T f g c)) - ( triangle-map-standard-pullback-postcomp T f g c) - ( is-pb-postcomp T) - ( is-equiv-map-standard-pullback-postcomp f g T)) +module _ + {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) + where + + abstract + is-pullback-postcomp-is-pullback : + 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 is-pb-c T = + is-equiv-top-map-triangle _ _ _ + ( triangle-map-standard-pullback-postcomp T f g c) + ( is-equiv-map-standard-pullback-postcomp f g T) + ( universal-property-pullback-is-pullback f g c is-pb-c T) + + abstract + is-pullback-is-pullback-postcomp : + ( {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 is-pb-postcomp = + is-pullback-universal-property-pullback f g c + ( λ T → + is-equiv-left-map-triangle _ _ _ + ( triangle-map-standard-pullback-postcomp T f g c) + ( is-pb-postcomp T) + ( is-equiv-map-standard-pullback-postcomp f g T)) ``` ### Cones satisfying the universal property of pullbacks are closed under postcomposition exponentiation diff --git a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md index 09335074fa..73a755edc1 100644 --- a/src/foundation/type-arithmetic-standard-pullbacks.lagda.md +++ b/src/foundation/type-arithmetic-standard-pullbacks.lagda.md @@ -243,7 +243,9 @@ module _ ### Unit laws for standard pullbacks -Pulling back along the identity map +Pulling back along the identity map is the identity operation. + +#### Left unit law for standard pullbacks ```agda module _ @@ -302,7 +304,7 @@ module _ ### Unit laws for standard pullbacks -Pulling back along the identity map is the identity operation. +#### Right unit law for standard pullbacks ```agda module _ diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index a167d57d4a..e2a8bf7286 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -9,6 +9,7 @@ ```agda module orthogonal-factorization-systems where +open import orthogonal-factorization-systems.anodyne-maps public open import orthogonal-factorization-systems.cd-structures public open import orthogonal-factorization-systems.cellular-maps public open import orthogonal-factorization-systems.closed-modalities public @@ -71,6 +72,7 @@ open import orthogonal-factorization-systems.types-local-at-maps public open import orthogonal-factorization-systems.types-separated-at-maps public open import orthogonal-factorization-systems.uniquely-eliminating-modalities public open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public +open import orthogonal-factorization-systems.weakly-anodyne-maps public open import orthogonal-factorization-systems.wide-function-classes public open import orthogonal-factorization-systems.wide-global-function-classes public open import orthogonal-factorization-systems.zero-modality public diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md new file mode 100644 index 0000000000..9a53d0201b --- /dev/null +++ b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md @@ -0,0 +1,172 @@ +# Anodyne maps + +```agda +module orthogonal-factorization-systems.anodyne-maps where +``` + +
Imports + +```agda +open import foundation.equivalences-arrows +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.universe-levels + +open import orthogonal-factorization-systems.orthogonal-maps + +open import synthetic-homotopy-theory.cocartesian-morphisms-arrows +``` + +
+ +## Idea + +A map $j : C → D$ is said to be +{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne}} with +respect to a map $f : A → B$, or **$f$-anodyne**, if every map that is +orthogonal to $f$ is also orthogonal to $j$. + +## Definitions + +### The predicate of being anodyne with respect to a map + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) (j : C → D) + where + + is-anodyne-Level : + (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6) + is-anodyne-Level l5 l6 = + {X : UU l5} {Y : UU l6} (g : X → Y) → is-orthogonal f g → is-orthogonal j g + + is-anodyne : UUω + is-anodyne = {l5 l6 : Level} → is-anodyne-Level l5 l6 +``` + +## Properties + +### Anodyne maps are closed under homotopies + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) {j i : C → D} + where + + is-anodyne-htpy : j ~ i → is-anodyne f j → is-anodyne f i + is-anodyne-htpy K J g H = is-orthogonal-htpy-left j g K (J g H) +``` + +### Anodyne maps are closed under equivalences of maps + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6} + (f : A → B) {j : C → D} {j' : C' → D'} + where + + is-anodyne-equiv-arrow : equiv-arrow j j' → is-anodyne f j → is-anodyne f j' + is-anodyne-equiv-arrow α J g H = is-orthogonal-left-equiv-arrow α g (J g H) +``` + +### Anodyne maps are closed under retracts of maps + +> This remains to be formalized. + +### Anodyne maps compose + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} + (f : A → B) (j : C → D) (i : D → E) + where + + is-anodyne-comp : is-anodyne f j → is-anodyne f i → is-anodyne f (i ∘ j) + is-anodyne-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H) +``` + +### Cancellation property for anodyne maps + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} + (f : A → B) (j : C → D) (i : D → E) + where + + is-anodyne-left-factor : + is-anodyne f j → is-anodyne f (i ∘ j) → is-anodyne f i + is-anodyne-left-factor J IJ g H = + is-orthogonal-left-left-factor j i g (J g H) (IJ g H) +``` + +### Anodyne maps are closed under dependent sums + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {A : UU l1} {B : UU l2} {I : UU l3} {C : I → UU l4} {D : I → UU l5} + (f : A → B) (j : (i : I) → C i → D i) + where + + is-anodyne-tot : ((i : I) → is-anodyne f (j i)) → is-anodyne f (tot j) + is-anodyne-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H) +``` + +### Anodyne maps are closed under products + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + (f : A → B) (j : C → D) (i : E → F) + where + + is-anodyne-map-product : + is-anodyne f j → is-anodyne f i → is-anodyne f (map-product j i) + is-anodyne-map-product J I g H = + is-orthogonal-left-product j i g (J g H) (I g H) +``` + +### Anodyne maps are closed under coproducts + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + (f : A → B) (j : C → D) (i : E → F) + where + + is-anodyne-map-coproduct : + is-anodyne f j → is-anodyne f i → is-anodyne f (map-coproduct j i) + is-anodyne-map-coproduct J I g H = + is-orthogonal-left-coproduct j i g (J g H) (I g H) +``` + +### Anodyne maps are closed under cobase change + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + (f : A → B) (j : C → D) (i : E → F) + where + + is-anodyne-cobase-change : + cocartesian-hom-arrow j i → is-anodyne f j → is-anodyne f i + is-anodyne-cobase-change α J g H = + is-orthogonal-left-cobase-change j i g α (J g H) +``` + +### Anodyne maps are closed under pushout-products + +> This remains to be formalized. diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index ac69503101..921e0c45d7 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -147,6 +147,19 @@ module _ ( G (map-codomain-inclusion-retract-map g' g R d)) ``` +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} + {f : A → B} {g : C → D} {f' : E → F} + where + + is-local-retract-map' : + is-local-map f g → f' retract-of-map f → is-local-map f' g + is-local-retract-map' F R d = + is-local-retract-map-is-local f' f R (fiber g d) (F d) +``` + ## See also - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md) diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index ec37ad84de..8a3d9bdcfe 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -29,6 +29,7 @@ open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.homotopies +open import foundation.identity-types open import foundation.morphisms-arrows open import foundation.postcomposition-functions open import foundation.postcomposition-pullbacks @@ -37,6 +38,7 @@ open import foundation.precomposition-functions open import foundation.products-pullbacks open import foundation.propositions open import foundation.pullbacks +open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-function-types open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type @@ -51,6 +53,10 @@ open import foundation.whiskering-homotopies-composition open import orthogonal-factorization-systems.lifting-structures-on-squares open import orthogonal-factorization-systems.pullback-hom open import orthogonal-factorization-systems.types-local-at-maps + +open import synthetic-homotopy-theory.cocartesian-morphisms-arrows +open import synthetic-homotopy-theory.pullback-property-pushouts +open import synthetic-homotopy-theory.pushouts ``` @@ -426,19 +432,40 @@ module _ ( ( commutative-htpy-postcomp-htpy-precomp F G) ∙h ( inv-htpy-right-unit-htpy))) - is-orthogonal-pullback-condition-htpy-left : - {f' : A → B} → f ~ f' → - is-orthogonal-pullback-condition f g → - is-orthogonal-pullback-condition f' g - is-orthogonal-pullback-condition-htpy-left F = - is-orthogonal-pullback-condition-htpy F refl-htpy - - is-orthogonal-pullback-condition-htpy-right : - {g' : X → Y} → g ~ g' → - is-orthogonal-pullback-condition f g → - is-orthogonal-pullback-condition f g' - is-orthogonal-pullback-condition-htpy-right = - is-orthogonal-pullback-condition-htpy refl-htpy + abstract + is-orthogonal-pullback-condition-htpy-left : + {f' : A → B} → f ~ f' → + is-orthogonal-pullback-condition f g → + is-orthogonal-pullback-condition f' g + is-orthogonal-pullback-condition-htpy-left F = + is-orthogonal-pullback-condition-htpy F refl-htpy + + abstract + is-orthogonal-pullback-condition-htpy-right : + {g' : X → Y} → g ~ g' → + is-orthogonal-pullback-condition f g → + is-orthogonal-pullback-condition f g' + is-orthogonal-pullback-condition-htpy-right = + is-orthogonal-pullback-condition-htpy refl-htpy + + abstract + is-orthogonal-htpy : + {f' : A → B} {g' : X → Y} → f ~ f' → g ~ g' → + is-orthogonal f g → is-orthogonal f' g' + is-orthogonal-htpy {f'} {g'} F G H = + is-orthogonal-is-orthogonal-pullback-condition f' g' + ( is-orthogonal-pullback-condition-htpy F G + ( is-orthogonal-pullback-condition-is-orthogonal f g H)) + + abstract + is-orthogonal-htpy-left : + {f' : A → B} → f ~ f' → is-orthogonal f g → is-orthogonal f' g + is-orthogonal-htpy-left F = is-orthogonal-htpy F refl-htpy + + abstract + is-orthogonal-htpy-right : + {g' : X → Y} → g ~ g' → is-orthogonal f g → is-orthogonal f g' + is-orthogonal-htpy-right = is-orthogonal-htpy refl-htpy ``` ### Equivalences are orthogonal to every map @@ -698,6 +725,70 @@ module _ ( is-orthogonal-pullback-condition-is-orthogonal (h ∘ f) g HF)) ``` +### Orthogonality is preserved by equivalences of maps + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6} + {f : A → B} {f' : A' → B'} + where + + abstract + is-orthogonal-left-equiv-arrow : + equiv-arrow f f' → (g : X → Y) → is-orthogonal f g → is-orthogonal f' g + is-orthogonal-left-equiv-arrow α g F = + is-orthogonal-htpy-left + ( map-codomain-equiv-arrow f f' α ∘ + f ∘ + map-inv-domain-equiv-arrow f f' α) + ( g) + ( ( coh-equiv-arrow f f' α ·r map-inv-domain-equiv-arrow f f' α) ∙h + ( f' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow f f' α))) + ( is-orthogonal-left-comp + ( f ∘ map-inv-domain-equiv-arrow f f' α) + ( map-codomain-equiv-arrow f f' α) + ( g) + ( is-orthogonal-left-comp + ( map-inv-domain-equiv-arrow f f' α) + ( f) + ( g) + ( is-orthogonal-equiv-left (equiv-domain-inv-equiv-arrow f f' α) g) + ( F)) + ( is-orthogonal-equiv-left (equiv-codomain-equiv-arrow f f' α) g)) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6} + (f : A → B) {g : X → Y} {g' : X' → Y'} + where + + abstract + is-orthogonal-right-equiv-arrow : + equiv-arrow g g' → is-orthogonal f g → is-orthogonal f g' + is-orthogonal-right-equiv-arrow α G = + is-orthogonal-htpy-right + ( f) + ( map-codomain-equiv-arrow g g' α ∘ + g ∘ + map-inv-domain-equiv-arrow g g' α) + ( ( coh-equiv-arrow g g' α ·r map-inv-domain-equiv-arrow g g' α) ∙h + ( g' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow g g' α))) + ( is-orthogonal-right-comp + ( f) + ( g ∘ map-inv-domain-equiv-arrow g g' α) + ( map-codomain-equiv-arrow g g' α) + ( is-orthogonal-equiv-right f (equiv-codomain-equiv-arrow g g' α)) + ( is-orthogonal-right-comp + ( f) + ( map-inv-domain-equiv-arrow g g' α) + ( g) + ( G) + ( is-orthogonal-equiv-right + ( f) + ( equiv-domain-inv-equiv-arrow g g' α)))) +``` + ### Right orthogonality is preserved by dependent products If `f ⊥ gᵢ`, for each `i : I`, then `f ⊥ (map-Π g)`. @@ -912,10 +1003,10 @@ module _ (f : (i : I) → A i → B i) (g : X → Y) where - is-orthogonal-pullback-condition-left-Σ : + is-orthogonal-pullback-condition-left-tot : ((i : I) → is-orthogonal-pullback-condition (f i) g) → is-orthogonal-pullback-condition (tot f) g - is-orthogonal-pullback-condition-left-Σ F = + is-orthogonal-pullback-condition-left-tot F = is-pullback-top-is-pullback-bottom-cube-is-equiv ( map-Π (λ i → postcomp (B i) g)) ( map-Π (λ i → precomp (f i) X)) @@ -951,14 +1042,56 @@ module _ ( λ i → cone-pullback-hom (f i) g) ( F)) - is-orthogonal-left-Σ : + is-orthogonal-left-tot : ((i : I) → is-orthogonal (f i) g) → is-orthogonal (tot f) g - is-orthogonal-left-Σ F = + is-orthogonal-left-tot F = is-orthogonal-is-orthogonal-pullback-condition (tot f) g - ( is-orthogonal-pullback-condition-left-Σ + ( is-orthogonal-pullback-condition-left-tot ( λ i → is-orthogonal-pullback-condition-is-orthogonal (f i) g (F i))) ``` +### Left orthogonality is preserved by products + +If `f ⊥ g` and `f' ⊥ g`, then `(f × f') ⊥ g`. + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) + where + + is-orthogonal-left-map-right-product : + {l5 : Level} (C : UU l5) → + is-orthogonal f g → is-orthogonal (map-product (id' C) f) g + is-orthogonal-left-map-right-product C F = + is-orthogonal-left-tot (λ _ → f) g (λ _ → F) + + is-orthogonal-left-map-left-product : + {l5 : Level} (C : UU l5) → + is-orthogonal f g → is-orthogonal (map-product f (id' C)) g + is-orthogonal-left-map-left-product C F = + is-orthogonal-left-equiv-arrow + ( commutative-product , commutative-product , refl-htpy) + ( g) + ( is-orthogonal-left-map-right-product C F) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6} + (f : A → B) (f' : A' → B') (g : X → Y) + where + + is-orthogonal-left-product : + is-orthogonal f g → is-orthogonal f' g → is-orthogonal (map-product f f') g + is-orthogonal-left-product F F' = + is-orthogonal-left-comp + ( map-product f id) + ( map-product id f') + ( g) + ( is-orthogonal-left-map-left-product f g A' F) + ( is-orthogonal-left-map-right-product f' g B F') +``` + ### Left orthogonality is preserved by coproducts If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`. @@ -966,7 +1099,7 @@ If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`. **Proof:** We need to show that the square ```text - - ∘ (f + f') + - ∘ (f + f') ((B + B') → X) ---------------> ((A + A') → X) | | | | @@ -1114,6 +1247,94 @@ module _ ( is-orthogonal-pullback-condition-is-orthogonal f g G)) ``` +### Left orthogonality is preserved under cobase change + +Given a pushout square + +```text + A ------> A' + | | + f'| | f' + ∨ ⌜ ∨ + B ------> B', +``` + +if `f ⊥ g`, then `f' ⊥ g`. + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {A' : UU l5} {B' : UU l6} + (f : A → B) (f' : A' → B') (g : X → Y) (α : cocartesian-hom-arrow f f') + where + + abstract + is-orthogonal-pullback-condition-left-cobase-change : + is-orthogonal-pullback-condition f g → + is-orthogonal-pullback-condition f' g + is-orthogonal-pullback-condition-left-cobase-change F = + is-pullback-swap-cone + ( postcomp A' g) + ( precomp f' Y) + ( precomp f' X , postcomp B' g , refl-htpy) + ( is-pullback-back-left-is-pullback-back-right-cube + ( refl-htpy) + ( refl-htpy) + ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) X)) + ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) Y)) + ( refl-htpy) + ( refl-htpy) + ( right-unit-htpy ∙h + ( inv ·l + commutative-postcomp-htpy-precomp g + ( coh-cocartesian-hom-arrow f f' α)) ∙h + ( inv-htpy + ( left-whisker-inv-htpy + ( postcomp A g) + ( htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))) ∙h + ( inv-htpy-right-unit-htpy)) + ( is-pullback-swap-cone + ( precomp f Y) + ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y) + ( cone-hom-arrow + ( precomp (map-codomain-cocartesian-hom-arrow f f' α) Y) + ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y) + ( transpose-precomp-hom-arrow f f' + ( hom-arrow-cocartesian-hom-arrow f f' α) + ( Y))) + ( pullback-property-pushout-is-pushout + ( f) + ( map-domain-cocartesian-hom-arrow f f' α) + ( cocone-cocartesian-hom-arrow f f' α) + ( is-cocartesian-cocartesian-hom-arrow f f' α) + ( Y))) + ( is-pullback-swap-cone + ( precomp f Y) + ( postcomp A g) + ( cone-pullback-hom f g) + ( F)) + ( is-pullback-swap-cone + ( precomp f X) + ( precomp (map-domain-cocartesian-hom-arrow f f' α) X) + ( cone-hom-arrow + ( precomp (map-codomain-cocartesian-hom-arrow f f' α) X) + ( precomp (map-domain-cocartesian-hom-arrow f f' α) X) + ( transpose-precomp-hom-arrow f f' + ( hom-arrow-cocartesian-hom-arrow f f' α) + ( X))) + ( pullback-property-pushout-is-pushout f + ( map-domain-cocartesian-hom-arrow f f' α) + ( cocone-cocartesian-hom-arrow f f' α) + ( is-cocartesian-cocartesian-hom-arrow f f' α) X))) + + is-orthogonal-left-cobase-change : + is-orthogonal f g → is-orthogonal f' g + is-orthogonal-left-cobase-change F = + is-orthogonal-is-orthogonal-pullback-condition f' g + ( is-orthogonal-pullback-condition-left-cobase-change + ( is-orthogonal-pullback-condition-is-orthogonal f g F)) +``` + ### A type is `f`-local if and only if its terminal map is `f`-orthogonal **Proof (forward direction):** If the terminal map is right orthogonal to `f`, diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md new file mode 100644 index 0000000000..c057f9195d --- /dev/null +++ b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md @@ -0,0 +1,89 @@ +# Weakly anodyne maps + +```agda +module orthogonal-factorization-systems.weakly-anodyne-maps where +``` + +
Imports + +```agda +open import foundation.equivalences-arrows +open import foundation.fibers-of-maps +open import foundation.function-types +open import foundation.functoriality-cartesian-product-types +open import foundation.functoriality-coproduct-types +open import foundation.functoriality-dependent-pair-types +open import foundation.homotopies +open import foundation.retracts-of-maps +open import foundation.unit-type +open import foundation.universe-levels + +open import orthogonal-factorization-systems.anodyne-maps +open import orthogonal-factorization-systems.maps-local-at-maps +open import orthogonal-factorization-systems.orthogonal-maps +open import orthogonal-factorization-systems.types-local-at-maps + +open import synthetic-homotopy-theory.cocartesian-morphisms-arrows +``` + +
+ +## Idea + +A map $j : C → D$ is said to be +{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne}} +with respect to a map $f : A → B$, or **weakly $f$-anodyne**, if every map that +is local at $f$ is also local at $j$. + +## Definitions + +### The predicate of being weakly anodyne with respect to a map + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) (j : C → D) + where + + is-weakly-anodyne-Level : + (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6) + is-weakly-anodyne-Level l5 l6 = + {X : UU l5} {Y : UU l6} (g : X → Y) → is-local-map f g → is-local-map j g + + is-weakly-anodyne : UUω + is-weakly-anodyne = {l5 l6 : Level} → is-weakly-anodyne-Level l5 l6 +``` + +## Properties + +### Anodyne maps are weakly anodyne + +```agda +module _ + {l1 l2 l3 l4 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) {j : C → D} + where + + is-weakly-anodyne-is-anodyne : is-anodyne f j → is-weakly-anodyne f j + is-weakly-anodyne-is-anodyne J g G x = + is-local-is-orthogonal-terminal-map j + ( J ( terminal-map (fiber g x)) + ( is-orthogonal-terminal-map-is-local f (G x))) +``` + +### Weakly anodyne maps are closed under retracts of maps + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6} + (f : A → B) {j : C → D} {j' : C' → D'} + where + + is-weakly-anodyne-retract-map : + retract-map j j' → is-weakly-anodyne f j → is-weakly-anodyne f j' + is-weakly-anodyne-retract-map α J g G x = + is-local-retract-map-is-local j' j α (fiber g x) (J g G x) +``` diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md index 9e34713e9c..e1188a0d13 100644 --- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md +++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md @@ -7,13 +7,17 @@ module synthetic-homotopy-theory.cocartesian-morphisms-arrows where
Imports ```agda +open import foundation.cartesian-morphisms-arrows open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.morphisms-arrows +open import foundation.precomposition-functions open import foundation.propositions +open import foundation.pullbacks open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.pullback-property-pushouts open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.universal-property-pushouts ``` @@ -121,6 +125,46 @@ module _ ( is-cocartesian-cocartesian-hom-arrow) ``` +### The cartesian morphism on precomposition maps + +```agda +module _ + {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} + (f : A → B) (g : X → Y) (α : cocartesian-hom-arrow f g) (S : UU l) + where + + precomp-cocartesian-hom-arrow : hom-arrow (precomp g S) (precomp f S) + precomp-cocartesian-hom-arrow = + precomp-hom-arrow f g (hom-arrow-cocartesian-hom-arrow f g α) S + + is-cartesian-precomp-cocartesian-hom-arrow : + is-cartesian-hom-arrow + ( precomp g S) + ( precomp f S) + ( precomp-cocartesian-hom-arrow) + is-cartesian-precomp-cocartesian-hom-arrow = + is-pullback-swap-cone + ( precomp f S) + ( precomp (map-domain-cocartesian-hom-arrow f g α) S) + ( cone-hom-arrow + ( precomp (map-codomain-cocartesian-hom-arrow f g α) S) + ( precomp (map-domain-cocartesian-hom-arrow f g α) S) + ( transpose-precomp-hom-arrow f g + ( hom-arrow-cocartesian-hom-arrow f g α) + ( S))) + ( pullback-property-pushout-is-pushout + ( f) + ( map-domain-cocartesian-hom-arrow f g α) + ( cocone-cocartesian-hom-arrow f g α) + ( is-cocartesian-cocartesian-hom-arrow f g α) S) + + precomp-cartesian-hom-arrow-cocartesian-hom-arrow : + cartesian-hom-arrow (precomp g S) (precomp f S) + precomp-cartesian-hom-arrow-cocartesian-hom-arrow = + ( precomp-cocartesian-hom-arrow , + is-cartesian-precomp-cocartesian-hom-arrow) +``` + ## See also - [Cartesian morphisms of arrows](foundation.cartesian-morphisms-arrows.md) for diff --git a/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md index 7095433e23..ebea5fa249 100644 --- a/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-equivalence-types-over-pushouts.lagda.md @@ -60,18 +60,19 @@ for [pushouts](synthetic-homotopy-theory.pushouts.md) `P ≈ (PA, PB, PS)` and ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) where - family-cocone-equivalence-type-pushout : X → UU (l5 ⊔ l6) + family-cocone-equivalence-type-pushout : X → UU (l7 ⊔ l10) family-cocone-equivalence-type-pushout x = family-cocone-family-with-descent-data-pushout P x ≃ family-cocone-family-with-descent-data-pushout R x - descent-data-equivalence-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6) + descent-data-equivalence-type-pushout : + descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9) pr1 descent-data-equivalence-type-pushout a = left-family-family-with-descent-data-pushout P a ≃ left-family-family-with-descent-data-pushout R a @@ -169,7 +170,7 @@ module _ coherence-equiv-descent-data-equivalence-type-pushout family-with-descent-data-equivalence-type-pushout : - family-with-descent-data-pushout c (l5 ⊔ l6) + family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10) pr1 family-with-descent-data-equivalence-type-pushout = family-cocone-equivalence-type-pushout pr1 (pr2 family-with-descent-data-equivalence-type-pushout) = @@ -184,10 +185,10 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) where equiv-section-descent-data-equivalence-type-pushout : @@ -288,11 +289,11 @@ by inverting the inverted equivalences. ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) (e : equiv-descent-data-pushout ( descent-data-family-with-descent-data-pushout P) diff --git a/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md index ac284b320a..122a5609cf 100644 --- a/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-function-types-over-pushouts.lagda.md @@ -102,18 +102,19 @@ which we can massage into a coherence of the morphism as ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) where - family-cocone-function-type-pushout : X → UU (l5 ⊔ l6) + family-cocone-function-type-pushout : X → UU (l7 ⊔ l10) family-cocone-function-type-pushout x = family-cocone-family-with-descent-data-pushout P x → family-cocone-family-with-descent-data-pushout R x - descent-data-function-type-pushout : descent-data-pushout 𝒮 (l5 ⊔ l6) + descent-data-function-type-pushout : + descent-data-pushout 𝒮 (l5 ⊔ l8) (l6 ⊔ l9) pr1 descent-data-function-type-pushout a = left-family-family-with-descent-data-pushout P a → left-family-family-with-descent-data-pushout R a @@ -208,7 +209,7 @@ module _ coherence-equiv-descent-data-function-type-pushout family-with-descent-data-function-type-pushout : - family-with-descent-data-pushout c (l5 ⊔ l6) + family-with-descent-data-pushout c (l5 ⊔ l8) (l6 ⊔ l9) (l7 ⊔ l10) pr1 family-with-descent-data-function-type-pushout = family-cocone-function-type-pushout pr1 (pr2 family-with-descent-data-function-type-pushout) = @@ -223,10 +224,10 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) where hom-section-descent-data-function-type-pushout : @@ -250,8 +251,7 @@ module _ abstract is-equiv-hom-section-descent-data-function-type-pushout : - is-equiv - ( hom-section-descent-data-function-type-pushout) + is-equiv hom-section-descent-data-function-type-pushout is-equiv-hom-section-descent-data-function-type-pushout = is-equiv-tot-is-fiberwise-equiv ( λ tA → @@ -326,11 +326,11 @@ by inverting the inverted equivalences. ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 l8 l9 l10 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : family-with-descent-data-pushout c l5) - (R : family-with-descent-data-pushout c l6) + (P : family-with-descent-data-pushout c l5 l6 l7) + (R : family-with-descent-data-pushout c l8 l9 l10) (m : hom-descent-data-pushout ( descent-data-family-with-descent-data-pushout P) diff --git a/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md index 6244d587ce..89d5e10cc6 100644 --- a/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-identity-types-over-pushouts.lagda.md @@ -66,7 +66,7 @@ module _ family-cocone-identity-type-pushout : X → UU l4 family-cocone-identity-type-pushout x = x₀ ＝ x - descent-data-identity-type-pushout : descent-data-pushout 𝒮 l4 + descent-data-identity-type-pushout : descent-data-pushout 𝒮 l4 l4 pr1 descent-data-identity-type-pushout a = x₀ ＝ horizontal-map-cocone _ _ c a pr1 (pr2 descent-data-identity-type-pushout) b = @@ -85,7 +85,7 @@ module _ tr-Id-right (coherence-square-cocone _ _ c s) family-with-descent-data-identity-type-pushout : - family-with-descent-data-pushout c l4 + family-with-descent-data-pushout c l4 l4 l4 pr1 family-with-descent-data-identity-type-pushout = family-cocone-identity-type-pushout pr1 (pr2 family-with-descent-data-identity-type-pushout) = diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md index 020d2dcefb..5df9f42d62 100644 --- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md @@ -7,6 +7,7 @@ module synthetic-homotopy-theory.descent-data-pushouts where
Imports ```agda +open import foundation.cartesian-product-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types @@ -69,11 +70,11 @@ module _ {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) where - descent-data-pushout : (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4) - descent-data-pushout l = - Σ ( domain-span-diagram 𝒮 → UU l) + descent-data-pushout : (l4 l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5) + descent-data-pushout l4 l5 = + Σ ( domain-span-diagram 𝒮 → UU l4) ( λ PA → - Σ ( codomain-span-diagram 𝒮 → UU l) + Σ ( codomain-span-diagram 𝒮 → UU l5) ( λ PB → (s : spanning-type-span-diagram 𝒮) → PA (left-map-span-diagram 𝒮 s) ≃ PB (right-map-span-diagram 𝒮 s))) @@ -83,14 +84,14 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where left-family-descent-data-pushout : domain-span-diagram 𝒮 → UU l4 left-family-descent-data-pushout = pr1 P - right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l4 + right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5 right-family-descent-data-pushout = pr1 (pr2 P) equiv-family-descent-data-pushout : @@ -113,6 +114,140 @@ module _ is-equiv-map-equiv (equiv-family-descent-data-pushout s) ``` +### Symmetric descent data for pushouts + +We give another equivalent definition of descent data for pushouts, that records +an additional type family `PS` over the spanning type `S` and equivalences +`PS s ≃ PA (f s)` and `PS s ≃ PB (g s)` for all `s`. + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + symmetric-descent-data-pushout : + (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6) + symmetric-descent-data-pushout l4 l5 l6 = + Σ ( domain-span-diagram 𝒮 → UU l4) + ( λ PA → + Σ ( codomain-span-diagram 𝒮 → UU l5) + ( λ PB → + Σ ( spanning-type-span-diagram 𝒮 → UU l6) + ( λ PS → + ( (s : spanning-type-span-diagram 𝒮) → + PS s ≃ PA (left-map-span-diagram 𝒮 s)) × + ( (s : spanning-type-span-diagram 𝒮) → + PS s ≃ PB (right-map-span-diagram 𝒮 s))))) +``` + +### Components of symmetric descent data for pushouts + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6) + where + + left-family-symmetric-descent-data-pushout : domain-span-diagram 𝒮 → UU l4 + left-family-symmetric-descent-data-pushout = pr1 P + + right-family-symmetric-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5 + right-family-symmetric-descent-data-pushout = pr1 (pr2 P) + + spanning-type-family-symmetric-descent-data-pushout : + spanning-type-span-diagram 𝒮 → UU l6 + spanning-type-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 P)) + + equiv-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout s ≃ + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) + equiv-left-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 (pr2 P))) + + equiv-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout s ≃ + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) + equiv-right-family-symmetric-descent-data-pushout = pr2 (pr2 (pr2 (pr2 P))) + + map-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout s → + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) + map-left-family-symmetric-descent-data-pushout = + map-equiv ∘ equiv-left-family-symmetric-descent-data-pushout + + map-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout s → + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) + map-right-family-symmetric-descent-data-pushout = + map-equiv ∘ equiv-right-family-symmetric-descent-data-pushout + + map-inv-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) → + spanning-type-family-symmetric-descent-data-pushout s + map-inv-left-family-symmetric-descent-data-pushout = + map-inv-equiv ∘ equiv-left-family-symmetric-descent-data-pushout + + map-inv-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) → + spanning-type-family-symmetric-descent-data-pushout s + map-inv-right-family-symmetric-descent-data-pushout = + map-inv-equiv ∘ equiv-right-family-symmetric-descent-data-pushout + + is-equiv-map-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + is-equiv (map-left-family-symmetric-descent-data-pushout s) + is-equiv-map-left-family-symmetric-descent-data-pushout s = + is-equiv-map-equiv (equiv-left-family-symmetric-descent-data-pushout s) + + is-equiv-map-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + is-equiv (map-right-family-symmetric-descent-data-pushout s) + is-equiv-map-right-family-symmetric-descent-data-pushout s = + is-equiv-map-equiv (equiv-right-family-symmetric-descent-data-pushout s) + + equiv-left-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃ + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) + equiv-left-right-family-symmetric-descent-data-pushout s = + equiv-right-family-symmetric-descent-data-pushout s ∘e + inv-equiv (equiv-left-family-symmetric-descent-data-pushout s) + + map-left-right-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) → + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) + map-left-right-family-symmetric-descent-data-pushout = + map-equiv ∘ equiv-left-right-family-symmetric-descent-data-pushout + + equiv-right-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) ≃ + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) + equiv-right-left-family-symmetric-descent-data-pushout s = + equiv-left-family-symmetric-descent-data-pushout s ∘e + inv-equiv (equiv-right-family-symmetric-descent-data-pushout s) + + map-right-left-family-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) → + left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) + map-right-left-family-symmetric-descent-data-pushout = + map-equiv ∘ equiv-right-left-family-symmetric-descent-data-pushout + + descent-data-pushout-symmetric-descent-data-pushout : + descent-data-pushout 𝒮 l4 l5 + descent-data-pushout-symmetric-descent-data-pushout = + ( left-family-symmetric-descent-data-pushout , + right-family-symmetric-descent-data-pushout , + equiv-left-right-family-symmetric-descent-data-pushout) +``` + ### Descent data induced by families over cocones Given a [cocone](synthetic-homotopy-theory.cocones-under-spans.md) @@ -140,11 +275,18 @@ module _ where descent-data-family-cocone-span-diagram : - {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 - pr1 (descent-data-family-cocone-span-diagram P) = - P ∘ horizontal-map-cocone _ _ c - pr1 (pr2 (descent-data-family-cocone-span-diagram P)) = - P ∘ vertical-map-cocone _ _ c - pr2 (pr2 (descent-data-family-cocone-span-diagram P)) s = - equiv-tr P (coherence-square-cocone _ _ c s) + {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 l5 + descent-data-family-cocone-span-diagram P = + ( P ∘ horizontal-map-cocone _ _ c) , + ( P ∘ vertical-map-cocone _ _ c) , + ( equiv-tr P ∘ coherence-square-cocone _ _ c) + + symmetric-descent-data-family-cocone-span-diagram : + {l5 : Level} → (X → UU l5) → symmetric-descent-data-pushout 𝒮 l5 l5 l5 + symmetric-descent-data-family-cocone-span-diagram P = + ( P ∘ horizontal-map-cocone _ _ c) , + ( P ∘ vertical-map-cocone _ _ c) , + ( P ∘ horizontal-map-cocone _ _ c ∘ left-map-span-diagram 𝒮) , + ( λ _ → id-equiv) , + ( equiv-tr P ∘ coherence-square-cocone _ _ c) ``` diff --git a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md index 6d1f56638f..5d8b09bc77 100644 --- a/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-property-pushouts.lagda.md @@ -120,18 +120,16 @@ module _ equiv-descent-data-cocone-span-diagram-UU : (l4 : Level) → cocone-span-diagram 𝒮 (UU l4) ≃ - descent-data-pushout 𝒮 l4 + descent-data-pushout 𝒮 l4 l4 equiv-descent-data-cocone-span-diagram-UU _ = equiv-tot ( λ PA → - equiv-tot - ( λ PB → - ( equiv-Π-equiv-family (λ s → equiv-univalence)))) + equiv-tot (λ PB → (equiv-Π-equiv-family (λ s → equiv-univalence)))) descent-data-cocone-span-diagram-UU : {l4 : Level} → cocone-span-diagram 𝒮 (UU l4) → - descent-data-pushout 𝒮 l4 + descent-data-pushout 𝒮 l4 l4 descent-data-cocone-span-diagram-UU {l4} = map-equiv (equiv-descent-data-cocone-span-diagram-UU l4) @@ -176,7 +174,7 @@ module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : descent-data-pushout 𝒮 l5) + (P : descent-data-pushout 𝒮 l5 l5) where abstract @@ -293,7 +291,7 @@ module _ map-equiv (compute-inv-right-family-cocone-descent-data-pushout b) family-with-descent-data-pushout-descent-data-pushout : - family-with-descent-data-pushout c l5 + family-with-descent-data-pushout c l5 l5 l5 pr1 family-with-descent-data-pushout-descent-data-pushout = family-cocone-descent-data-pushout pr1 (pr2 family-with-descent-data-pushout-descent-data-pushout) = diff --git a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md index a95a4a12a1..2b126bbbb2 100644 --- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md @@ -7,6 +7,7 @@ module synthetic-homotopy-theory.equivalences-descent-data-pushouts where
Imports ```agda +open import foundation.cartesian-product-types open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types @@ -76,12 +77,13 @@ the proofs of `is-equiv` of their gluing maps. ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} + {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) where - equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + equiv-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) equiv-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a ≃ @@ -164,20 +166,224 @@ module _ coherence-equiv-descent-data-pushout = pr2 (pr2 e) hom-equiv-descent-data-pushout : hom-descent-data-pushout P Q - pr1 hom-equiv-descent-data-pushout = - left-map-equiv-descent-data-pushout - pr1 (pr2 hom-equiv-descent-data-pushout) = - right-map-equiv-descent-data-pushout - pr2 (pr2 hom-equiv-descent-data-pushout) = - coherence-equiv-descent-data-pushout + hom-equiv-descent-data-pushout = + ( left-map-equiv-descent-data-pushout , + right-map-equiv-descent-data-pushout , + coherence-equiv-descent-data-pushout) +``` + +### Equivalences of symmetric descent data for pushouts + +Note that the descent data arguments cannot be inferred when calling +`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer +the proofs of `is-equiv` of their gluing maps. + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} + {𝒮 : span-diagram l1 l2 l3} + (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6) + (Q : symmetric-descent-data-pushout 𝒮 l7 l8 l9) + where + + equiv-symmetric-descent-data-pushout : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9) + equiv-symmetric-descent-data-pushout = + Σ ( (a : domain-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout P a ≃ + left-family-symmetric-descent-data-pushout Q a) + ( λ eA → + Σ ( (b : codomain-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout P b ≃ + right-family-symmetric-descent-data-pushout Q b) + ( λ eB → + Σ ( (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout P s ≃ + spanning-type-family-symmetric-descent-data-pushout Q s) + ( λ eS → + ( (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( map-equiv (eS s)) + ( map-left-family-symmetric-descent-data-pushout P s) + ( map-left-family-symmetric-descent-data-pushout Q s) + ( map-equiv (eA (left-map-span-diagram 𝒮 s)))) × + ( (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( map-equiv (eS s)) + ( map-right-family-symmetric-descent-data-pushout P s) + ( map-right-family-symmetric-descent-data-pushout Q s) + ( map-equiv (eB (right-map-span-diagram 𝒮 s))))))) + + module _ + (e : equiv-symmetric-descent-data-pushout) + where + + left-equiv-equiv-symmetric-descent-data-pushout : + (a : domain-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout P a ≃ + left-family-symmetric-descent-data-pushout Q a + left-equiv-equiv-symmetric-descent-data-pushout = pr1 e + + left-map-equiv-symmetric-descent-data-pushout : + (a : domain-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout P a → + left-family-symmetric-descent-data-pushout Q a + left-map-equiv-symmetric-descent-data-pushout a = + map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) + + is-equiv-left-map-equiv-symmetric-descent-data-pushout : + (a : domain-span-diagram 𝒮) → + is-equiv (left-map-equiv-symmetric-descent-data-pushout a) + is-equiv-left-map-equiv-symmetric-descent-data-pushout a = + is-equiv-map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) + + inv-left-map-equiv-symmetric-descent-data-pushout : + (a : domain-span-diagram 𝒮) → + left-family-symmetric-descent-data-pushout Q a → + left-family-symmetric-descent-data-pushout P a + inv-left-map-equiv-symmetric-descent-data-pushout a = + map-inv-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) + + right-equiv-equiv-symmetric-descent-data-pushout : + (b : codomain-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout P b ≃ + right-family-symmetric-descent-data-pushout Q b + right-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 e) + + right-map-equiv-symmetric-descent-data-pushout : + (b : codomain-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout P b → + right-family-symmetric-descent-data-pushout Q b + right-map-equiv-symmetric-descent-data-pushout b = + map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) + + is-equiv-right-map-equiv-symmetric-descent-data-pushout : + (b : codomain-span-diagram 𝒮) → + is-equiv (right-map-equiv-symmetric-descent-data-pushout b) + is-equiv-right-map-equiv-symmetric-descent-data-pushout b = + is-equiv-map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) + + inv-right-map-equiv-symmetric-descent-data-pushout : + (b : codomain-span-diagram 𝒮) → + right-family-symmetric-descent-data-pushout Q b → + right-family-symmetric-descent-data-pushout P b + inv-right-map-equiv-symmetric-descent-data-pushout b = + map-inv-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) + + spanning-type-equiv-equiv-symmetric-descent-data-pushout : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout P b ≃ + spanning-type-family-symmetric-descent-data-pushout Q b + spanning-type-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 (pr2 e)) + + spanning-type-map-equiv-symmetric-descent-data-pushout : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout P b → + spanning-type-family-symmetric-descent-data-pushout Q b + spanning-type-map-equiv-symmetric-descent-data-pushout b = + map-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b) + + is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout : + (b : spanning-type-span-diagram 𝒮) → + is-equiv (spanning-type-map-equiv-symmetric-descent-data-pushout b) + is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout b = + is-equiv-map-equiv + ( spanning-type-equiv-equiv-symmetric-descent-data-pushout b) + + inv-spanning-type-map-equiv-symmetric-descent-data-pushout : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-symmetric-descent-data-pushout Q b → + spanning-type-family-symmetric-descent-data-pushout P b + inv-spanning-type-map-equiv-symmetric-descent-data-pushout b = + map-inv-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b) + + coherence-left-equiv-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( map-left-family-symmetric-descent-data-pushout P s) + ( map-left-family-symmetric-descent-data-pushout Q s) + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + coherence-left-equiv-symmetric-descent-data-pushout = + pr1 (pr2 (pr2 (pr2 e))) + + coherence-right-equiv-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( map-right-family-symmetric-descent-data-pushout P s) + ( map-right-family-symmetric-descent-data-pushout Q s) + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + coherence-right-equiv-symmetric-descent-data-pushout = + pr2 (pr2 (pr2 (pr2 e))) + + coherence-left-right-equiv-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + ( map-left-right-family-symmetric-descent-data-pushout P s) + ( map-left-right-family-symmetric-descent-data-pushout Q s) + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + coherence-left-right-equiv-symmetric-descent-data-pushout s = + pasting-vertical-coherence-square-maps + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + ( map-inv-left-family-symmetric-descent-data-pushout P s) + ( map-inv-left-family-symmetric-descent-data-pushout Q s) + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( map-right-family-symmetric-descent-data-pushout P s) + ( map-right-family-symmetric-descent-data-pushout Q s) + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + (vertical-inv-equiv-coherence-square-maps + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( equiv-left-family-symmetric-descent-data-pushout P s) + ( equiv-left-family-symmetric-descent-data-pushout Q s) + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + ( coherence-left-equiv-symmetric-descent-data-pushout s)) + ( coherence-right-equiv-symmetric-descent-data-pushout s) + + coherence-right-left-equiv-symmetric-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + ( map-right-left-family-symmetric-descent-data-pushout P s) + ( map-right-left-family-symmetric-descent-data-pushout Q s) + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + coherence-right-left-equiv-symmetric-descent-data-pushout s = + pasting-vertical-coherence-square-maps + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + ( map-inv-right-family-symmetric-descent-data-pushout P s) + ( map-inv-right-family-symmetric-descent-data-pushout Q s) + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( map-left-family-symmetric-descent-data-pushout P s) + ( map-left-family-symmetric-descent-data-pushout Q s) + ( left-map-equiv-symmetric-descent-data-pushout + ( left-map-span-diagram 𝒮 s)) + (vertical-inv-equiv-coherence-square-maps + ( spanning-type-map-equiv-symmetric-descent-data-pushout s) + ( equiv-right-family-symmetric-descent-data-pushout P s) + ( equiv-right-family-symmetric-descent-data-pushout Q s) + ( right-map-equiv-symmetric-descent-data-pushout + ( right-map-span-diagram 𝒮 s)) + ( coherence-right-equiv-symmetric-descent-data-pushout s)) + ( coherence-left-equiv-symmetric-descent-data-pushout s) ``` ### The identity equivalence of descent data for pushouts ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where id-equiv-descent-data-pushout : equiv-descent-data-pushout P P @@ -211,9 +417,9 @@ and mirroring the coherence squares vertically to get ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) where inv-equiv-descent-data-pushout : @@ -236,13 +442,14 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) where htpy-equiv-descent-data-pushout : - (e f : equiv-descent-data-pushout P Q) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + (e f : equiv-descent-data-pushout P Q) → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) htpy-equiv-descent-data-pushout e f = htpy-hom-descent-data-pushout P Q ( hom-equiv-descent-data-pushout P Q e) @@ -255,18 +462,18 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where equiv-eq-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4) → + (Q : descent-data-pushout 𝒮 l4 l5) → P ＝ Q → equiv-descent-data-pushout P Q equiv-eq-descent-data-pushout .P refl = id-equiv-descent-data-pushout P abstract is-torsorial-equiv-descent-data-pushout : - is-torsorial (equiv-descent-data-pushout {l5 = l4} P) + is-torsorial (equiv-descent-data-pushout {l6 = l4} {l7 = l5} P) is-torsorial-equiv-descent-data-pushout = is-torsorial-Eq-structure ( is-torsorial-Eq-Π @@ -281,7 +488,7 @@ module _ is-torsorial-htpy-equiv (equiv-family-descent-data-pushout P s)))) is-equiv-equiv-eq-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4) → + (Q : descent-data-pushout 𝒮 l4 l5) → is-equiv (equiv-eq-descent-data-pushout Q) is-equiv-equiv-eq-descent-data-pushout = fundamental-theorem-id @@ -289,7 +496,7 @@ module _ ( equiv-eq-descent-data-pushout) extensionality-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4) → + (Q : descent-data-pushout 𝒮 l4 l5) → (P ＝ Q) ≃ equiv-descent-data-pushout P Q pr1 (extensionality-descent-data-pushout Q) = equiv-eq-descent-data-pushout Q @@ -297,7 +504,7 @@ module _ is-equiv-equiv-eq-descent-data-pushout Q eq-equiv-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4) → + (Q : descent-data-pushout 𝒮 l4 l5) → equiv-descent-data-pushout P Q → P ＝ Q eq-equiv-descent-data-pushout Q = map-inv-equiv (extensionality-descent-data-pushout Q) @@ -307,9 +514,9 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - {P : descent-data-pushout 𝒮 l4} - {Q : descent-data-pushout 𝒮 l5} + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + {P : descent-data-pushout 𝒮 l4 l5} + {Q : descent-data-pushout 𝒮 l6 l7} (e : equiv-descent-data-pushout P Q) where diff --git a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md index 0a68a9200c..62d678d3b2 100644 --- a/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/families-descent-data-pushouts.lagda.md @@ -50,11 +50,11 @@ module _ where family-with-descent-data-pushout : - (l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5) - family-with-descent-data-pushout l5 = - Σ ( X → UU l5) + (l5 l6 l7 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6 ⊔ lsuc l7) + family-with-descent-data-pushout l5 l6 l7 = + Σ ( X → UU l7) ( λ P → - Σ ( descent-data-pushout 𝒮 l5) + Σ ( descent-data-pushout 𝒮 l5 l6) ( λ Q → equiv-descent-data-pushout ( descent-data-family-cocone-span-diagram c P) @@ -65,15 +65,15 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) + (P : family-with-descent-data-pushout c l5 l6 l7) where - family-cocone-family-with-descent-data-pushout : X → UU l5 + family-cocone-family-with-descent-data-pushout : X → UU l7 family-cocone-family-with-descent-data-pushout = pr1 P - descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5 + descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5 l6 descent-data-family-with-descent-data-pushout = pr1 (pr2 P) left-family-family-with-descent-data-pushout : @@ -83,7 +83,7 @@ module _ ( descent-data-family-with-descent-data-pushout) right-family-family-with-descent-data-pushout : - codomain-span-diagram 𝒮 → UU l5 + codomain-span-diagram 𝒮 → UU l6 right-family-family-with-descent-data-pushout = right-family-descent-data-pushout ( descent-data-family-with-descent-data-pushout) @@ -224,8 +224,7 @@ module _ ( family-cocone-family-with-descent-data-pushout) ( coherence-square-cocone _ _ c s)) ( map-family-family-with-descent-data-pushout s) - ( right-map-family-with-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) + ( right-map-family-with-descent-data-pushout (right-map-span-diagram 𝒮 s)) coherence-family-with-descent-data-pushout = coherence-equiv-descent-data-pushout ( descent-data-family-cocone-span-diagram c @@ -243,12 +242,11 @@ module _ where family-with-descent-data-pushout-family-cocone : - {l5 : Level} (P : X → UU l5) → - family-with-descent-data-pushout c l5 - pr1 (family-with-descent-data-pushout-family-cocone P) = P + {l : Level} (P : X → UU l) → family-with-descent-data-pushout c l l l + pr1 (family-with-descent-data-pushout-family-cocone P) = + P pr1 (pr2 (family-with-descent-data-pushout-family-cocone P)) = descent-data-family-cocone-span-diagram c P pr2 (pr2 (family-with-descent-data-pushout-family-cocone P)) = - id-equiv-descent-data-pushout - ( descent-data-family-cocone-span-diagram c P) + id-equiv-descent-data-pushout (descent-data-family-cocone-span-diagram c P) ``` diff --git a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md index 552c91b146..abddcc385a 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-coequalizers.lagda.md @@ -137,7 +137,7 @@ module _ universal-property-coequalizer-universal-property-pushout ( double-arrow-flattening-lemma-coequalizer a P e) ( cofork-flattening-lemma-coequalizer a P e) - ( universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv + ( universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv ( vertical-map-span-cocone-cofork ( double-arrow-flattening-lemma-coequalizer a P e)) ( horizontal-map-span-cocone-cofork @@ -166,16 +166,15 @@ module _ ( vertical-map-span-cocone-cofork a) ( horizontal-map-span-cocone-cofork a) ( cocone-codiagonal-cofork a e)) - ( map-equiv - ( right-distributive-Σ-coproduct - ( domain-double-arrow a) - ( domain-double-arrow a) - ( ( P) ∘ - ( horizontal-map-cocone-cofork a e) ∘ - ( vertical-map-span-cocone-cofork a)))) - ( id) - ( id) - ( id) + ( right-distributive-Σ-coproduct + ( domain-double-arrow a) + ( domain-double-arrow a) + ( ( P) ∘ + ( horizontal-map-cocone-cofork a e) ∘ + ( vertical-map-span-cocone-cofork a))) + ( id-equiv) + ( id-equiv) + ( id-equiv) ( coherence-square-cocone-flattening-pushout P ( vertical-map-span-cocone-cofork a) ( horizontal-map-span-cocone-cofork a) @@ -191,16 +190,6 @@ module _ ( ind-coproduct _ ( ev-pair refl-htpy) ( ev-pair (λ t → ap-id _ ∙ inv right-unit)))) - ( is-equiv-map-equiv - ( right-distributive-Σ-coproduct - ( domain-double-arrow a) - ( domain-double-arrow a) - ( ( P) ∘ - ( horizontal-map-cocone-cofork a e) ∘ - ( vertical-map-span-cocone-cofork a)))) - ( is-equiv-id) - ( is-equiv-id) - ( is-equiv-id) ( flattening-lemma-pushout P ( vertical-map-span-cocone-cofork a) ( horizontal-map-span-cocone-cofork a) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index a5842aaa89..829dc84267 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -154,8 +154,8 @@ data for the pushout. ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where vertical-map-span-flattening-descent-data-pushout : @@ -178,17 +178,18 @@ module _ ( λ s → map-equiv (pr2 (pr2 P) s)) span-diagram-flattening-descent-data-pushout : - span-diagram (l1 ⊔ l4) (l2 ⊔ l4) (l3 ⊔ l4) + span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l4) span-diagram-flattening-descent-data-pushout = make-span-diagram ( vertical-map-span-flattening-descent-data-pushout) ( horizontal-map-span-flattening-descent-data-pushout) module _ - { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} + { l1 l2 l3 l4 l5 l6 l7 : Level} + {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} ( f : S → A) (g : S → B) (c : cocone f g X) - ( P : descent-data-pushout (make-span-diagram f g) l5) - ( Q : X → UU l5) + ( P : descent-data-pushout (make-span-diagram f g) l5 l6) + ( Q : X → UU l7) ( e : equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q)) where @@ -354,10 +355,11 @@ descent data. ```agda module _ - { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} + { l1 l2 l3 l4 l5 l6 l7 : Level} + { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} ( f : S → A) (g : S → B) (c : cocone f g X) - ( P : descent-data-pushout (make-span-diagram f g) l5) - ( Q : X → UU l5) + ( P : descent-data-pushout (make-span-diagram f g) l5 l6) + ( Q : X → UU l7) ( e : equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q)) where @@ -408,7 +410,7 @@ module _ flattening-lemma-descent-data-pushout : flattening-lemma-descent-data-pushout-statement f g c P Q e flattening-lemma-descent-data-pushout up-c = - universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv + universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv ( vertical-map-span-flattening-pushout Q f g c) ( horizontal-map-span-flattening-pushout Q f g c) ( horizontal-map-cocone-flattening-pushout Q f g c) @@ -417,10 +419,10 @@ module _ ( horizontal-map-span-flattening-descent-data-pushout P) ( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e) ( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e) - ( tot (λ s → map-equiv (pr1 e (f s)))) - ( tot (λ a → map-equiv (pr1 e a))) - ( tot (λ b → map-equiv (pr1 (pr2 e) b))) - ( id) + ( equiv-tot (pr1 e ∘ f)) + ( equiv-tot (pr1 e)) + ( equiv-tot (pr1 (pr2 e))) + ( id-equiv) ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e) ( refl-htpy) ( htpy-map-Σ @@ -433,12 +435,5 @@ module _ ( refl-htpy) ( coherence-square-cocone-flattening-pushout Q f g c) ( coherence-cube-flattening-lemma-descent-data-pushout) - ( is-equiv-tot-is-fiberwise-equiv - ( λ s → is-equiv-map-equiv (pr1 e (f s)))) - ( is-equiv-tot-is-fiberwise-equiv - ( λ a → is-equiv-map-equiv (pr1 e a))) - ( is-equiv-tot-is-fiberwise-equiv - ( λ b → is-equiv-map-equiv (pr1 (pr2 e) b))) - ( is-equiv-id) ( flattening-lemma-pushout Q f g c up-c) ``` diff --git a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md index ed4ca2232d..c10b3c533a 100644 --- a/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/identity-systems-descent-data-pushouts.lagda.md @@ -156,15 +156,16 @@ section of `(RΣA, RΣB, RΣS)`, respectively. ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮} + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮} (p₀ : left-family-descent-data-pushout P a₀) where ev-refl-section-descent-data-pushout : - {l5 : Level} + {l6 l7 : Level} (R : - descent-data-pushout (span-diagram-flattening-descent-data-pushout P) l5) + descent-data-pushout + ( span-diagram-flattening-descent-data-pushout P) l6 l7) (t : section-descent-data-pushout R) → left-family-descent-data-pushout R (a₀ , p₀) ev-refl-section-descent-data-pushout R t = @@ -175,18 +176,17 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮} + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) {a₀ : domain-span-diagram 𝒮} (p₀ : left-family-descent-data-pushout P a₀) where is-identity-system-descent-data-pushout : UUω is-identity-system-descent-data-pushout = - {l5 : Level} + {l : Level} (R : descent-data-pushout - ( span-diagram-flattening-descent-data-pushout P) - ( l5)) → + ( span-diagram-flattening-descent-data-pushout P) l l) → section (ev-refl-section-descent-data-pushout P p₀ R) ``` @@ -232,9 +232,9 @@ section if and only if the right map has a section. ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) + (P : family-with-descent-data-pushout c l5 l6 l7) {a₀ : domain-span-diagram 𝒮} (p₀ : left-family-family-with-descent-data-pushout P a₀) where @@ -252,7 +252,7 @@ module _ ( inv-equiv-descent-data-family-with-descent-data-pushout P) square-ev-refl-section-descent-data-pushout : - {l5 : Level} + {l5 l6 l7 : Level} (R : family-with-descent-data-pushout ( cocone-flattening-descent-data-pushout _ _ c @@ -260,7 +260,7 @@ module _ ( family-cocone-family-with-descent-data-pushout P) ( inv-equiv-descent-data-pushout _ _ ( equiv-descent-data-family-with-descent-data-pushout P))) - ( l5)) → + l5 l6 l7) → coherence-square-maps ( section-descent-data-section-family-cocone-span-diagram R ∘ ind-Σ) ( ev-refl-identity-system @@ -307,7 +307,7 @@ right map has a section, hence the left map has a section. ( up-c))))) ( id-system-P (descent-data-family-with-descent-data-pushout fam-R)) where - fam-R : family-with-descent-data-pushout cocone-flattening l + fam-R : family-with-descent-data-pushout cocone-flattening l l l fam-R = family-with-descent-data-pushout-family-cocone ( cocone-flattening) @@ -340,7 +340,7 @@ assumption, so the right map has a section. ( section-map-equiv ( left-equiv-family-with-descent-data-pushout fam-R (a₀ , p₀)))) where - fam-R : family-with-descent-data-pushout cocone-flattening l + fam-R : family-with-descent-data-pushout cocone-flattening l l l fam-R = family-with-descent-data-pushout-descent-data-pushout ( flattening-lemma-descent-data-pushout _ _ c @@ -404,7 +404,7 @@ module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮} + (P : descent-data-pushout 𝒮 l5 l5) {a₀ : domain-span-diagram 𝒮} (p₀ : left-family-descent-data-pushout P a₀) (id-system-P : is-identity-system-descent-data-pushout P p₀) where @@ -446,7 +446,7 @@ module _ ( up-c) ( id-system-P)))) where - fam-P : family-with-descent-data-pushout c l5 + fam-P : family-with-descent-data-pushout c l5 l5 l5 fam-P = family-with-descent-data-pushout-descent-data-pushout up-c P p₀' : family-cocone-family-with-descent-data-pushout @@ -481,18 +481,19 @@ module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮} + (P : descent-data-pushout 𝒮 l5 l5) {a₀ : domain-span-diagram 𝒮} (p₀ : left-family-descent-data-pushout P a₀) where abstract is-identity-system-descent-data-pushout-ind-singleton : (H : - {l6 : Level} + {l7 : Level} (R : descent-data-pushout ( span-diagram-flattening-descent-data-pushout P) - ( l6)) + l7 + l7) (r₀ : left-family-descent-data-pushout R (a₀ , p₀)) → section-descent-data-pushout R) → is-identity-system-descent-data-pushout P p₀ diff --git a/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md index 27f747d90f..317bf3a29e 100644 --- a/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/morphisms-descent-data-pushouts.lagda.md @@ -121,12 +121,12 @@ proofs of `is-equiv` of their gluing maps. ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) where - hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) hom-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a → @@ -173,8 +173,8 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where id-hom-descent-data-pushout : hom-descent-data-pushout P P @@ -187,10 +187,10 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) - (R : descent-data-pushout 𝒮 l6) + {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) + (R : descent-data-pushout 𝒮 l8 l9) (g : hom-descent-data-pushout Q R) (f : hom-descent-data-pushout P Q) where @@ -223,13 +223,13 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) (f g : hom-descent-data-pushout P Q) where - htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) htpy-hom-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-map-hom-descent-data-pushout P Q f a ~ @@ -253,9 +253,9 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) (f : hom-descent-data-pushout P Q) where @@ -271,9 +271,9 @@ module _ ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) - (Q : descent-data-pushout 𝒮 l5) + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) (f : hom-descent-data-pushout P Q) where diff --git a/src/synthetic-homotopy-theory/pushouts.lagda.md b/src/synthetic-homotopy-theory/pushouts.lagda.md index 1b5112681f..2141345004 100644 --- a/src/synthetic-homotopy-theory/pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/pushouts.lagda.md @@ -33,6 +33,7 @@ open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.flattening-lemma-pushouts open import synthetic-homotopy-theory.induction-principle-pushouts +open import synthetic-homotopy-theory.pullback-property-pushouts open import synthetic-homotopy-theory.universal-property-pushouts ``` @@ -459,6 +460,27 @@ module _ ( up-pushout f g) ``` +### Pushout cocones satisfy the pullback property of the pushout + +```agda +module _ + {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} + (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) + where + + pullback-property-pushout-is-pushout : + is-pushout f g c → pullback-property-pushout f g c + pullback-property-pushout-is-pushout po = + pullback-property-pushout-universal-property-pushout f g c + ( universal-property-pushout-is-pushout f g c po) + + is-pushout-pullback-property-pushout : + pullback-property-pushout f g c → is-pushout f g c + is-pushout-pullback-property-pushout pb = + is-pushout-universal-property-pushout f g c + ( universal-property-pushout-pullback-property-pushout f g c pb) +``` + ### Fibers of the cogap map We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map diff --git a/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md index 583235db13..7b668de571 100644 --- a/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/sections-descent-data-pushouts.lagda.md @@ -107,11 +107,11 @@ homotopies between them. ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) where - section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) section-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a) ( λ tA → @@ -147,12 +147,12 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) (r t : section-descent-data-pushout P) where - htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + htpy-section-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) htpy-section-descent-data-pushout = Σ ( left-map-section-descent-data-pushout P r ~ left-map-section-descent-data-pushout P t) @@ -174,8 +174,8 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) (r : section-descent-data-pushout P) where @@ -192,8 +192,8 @@ module _ ```agda module _ - {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4) + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) (r : section-descent-data-pushout P) where @@ -281,9 +281,9 @@ equivalence. It follows that the left map is an equivalence ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} - (P : family-with-descent-data-pushout c l5) + (P : family-with-descent-data-pushout c l5 l6 l7) where section-descent-data-section-family-cocone-span-diagram : @@ -381,10 +381,10 @@ homotopies of sections of `(PA, PB, PS)`. ```agda module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} {c : cocone-span-diagram 𝒮 X} (up-c : universal-property-pushout _ _ c) - (P : family-with-descent-data-pushout c l5) + (P : family-with-descent-data-pushout c l5 l6 l7) (t : section-descent-data-pushout ( descent-data-family-with-descent-data-pushout P)) diff --git a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md index 14abaccfc2..31d4fe2ff3 100644 --- a/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-coequalizers.lagda.md @@ -195,7 +195,7 @@ module _ universal-property-coequalizer a c universal-property-coequalizer-equiv-cofork-equiv-double-arrow up-c' = universal-property-coequalizer-universal-property-pushout a c - ( universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv + ( universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv ( vertical-map-span-cocone-cofork a') ( horizontal-map-span-cocone-cofork a') ( horizontal-map-cocone-cofork a' c') @@ -204,11 +204,12 @@ module _ ( horizontal-map-span-cocone-cofork a) ( horizontal-map-cocone-cofork a c) ( vertical-map-cocone-cofork a c) - ( spanning-map-hom-span-diagram-cofork-hom-double-arrow a a' - ( hom-equiv-double-arrow a a' e)) - ( domain-map-equiv-double-arrow a a' e) - ( codomain-map-equiv-double-arrow a a' e) - ( map-equiv-cofork-equiv-double-arrow c c' e e') + ( equiv-coproduct + ( domain-equiv-equiv-double-arrow a a' e) + ( domain-equiv-equiv-double-arrow a a' e)) + ( domain-equiv-equiv-double-arrow a a' e) + (codomain-equiv-equiv-double-arrow a a' e) + ( equiv-equiv-cofork-equiv-double-arrow c c' e e') ( coherence-square-cocone-cofork a c) ( inv-htpy ( left-square-hom-span-diagram-cofork-hom-double-arrow a a' @@ -264,12 +265,6 @@ module _ ( ind-coproduct _ ( right-unit-htpy) ( coh-equiv-cofork-equiv-double-arrow c c' e e')))) - ( is-equiv-map-coproduct - ( is-equiv-domain-map-equiv-double-arrow a a' e) - ( is-equiv-domain-map-equiv-double-arrow a a' e)) - ( is-equiv-domain-map-equiv-double-arrow a a' e) - ( is-equiv-codomain-map-equiv-double-arrow a a' e) - ( is-equiv-map-equiv-cofork-equiv-double-arrow c c' e e') ( universal-property-pushout-universal-property-coequalizer a' c' ( up-c'))) diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md index 06f4082d85..2191989aef 100644 --- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md @@ -998,4 +998,75 @@ module _ ( h' , k' , top) ( up-top) ( W))) + +module _ + { l1 l2 l3 l4 l1' l2' l3' l4' : Level} + { A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + ( f : A → B) (g : A → C) (h : B → D) (k : C → D) + { A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'} + ( f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D') + ( hA : A' ≃ A) (hB : B' ≃ B) (hC : C' ≃ C) (hD : D' ≃ D) + ( top : coherence-square-maps g' f' k' h') + ( back-left : coherence-square-maps f' (map-equiv hA) (map-equiv hB) f) + ( back-right : coherence-square-maps g' (map-equiv hA) (map-equiv hC) g) + ( front-left : coherence-square-maps h' (map-equiv hB) (map-equiv hD) h) + ( front-right : coherence-square-maps k' (map-equiv hC) (map-equiv hD) k) + ( bottom : coherence-square-maps g f k h) + ( c : + coherence-cube-maps f g h k f' g' h' k' + ( map-equiv hA) + ( map-equiv hB) + ( map-equiv hC) + ( map-equiv hD) + ( top) + ( back-left) + ( back-right) + ( front-left) + ( front-right) + ( bottom)) + where + + universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv : + universal-property-pushout f g (h , k , bottom) → + universal-property-pushout f' g' (h' , k' , top) + universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv = + universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv + f g h k f' g' h' k' + ( map-equiv hA) + ( map-equiv hB) + ( map-equiv hC) + ( map-equiv hD) + ( top) + ( back-left) + ( back-right) + ( front-left) + ( front-right) + ( bottom) + ( c) + ( is-equiv-map-equiv hA) + ( is-equiv-map-equiv hB) + ( is-equiv-map-equiv hC) + ( is-equiv-map-equiv hD) + + universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv : + universal-property-pushout f' g' (h' , k' , top) → + universal-property-pushout f g (h , k , bottom) + universal-property-pushout-bottom-universal-property-pushout-top-cube-equiv = + universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv + f g h k f' g' h' k' + ( map-equiv hA) + ( map-equiv hB) + ( map-equiv hC) + ( map-equiv hD) + ( top) + ( back-left) + ( back-right) + ( front-left) + ( front-right) + ( bottom) + ( c) + ( is-equiv-map-equiv hA) + ( is-equiv-map-equiv hB) + ( is-equiv-map-equiv hC) + ( is-equiv-map-equiv hD) ``` From f8e0becc6b1debc43008d10ca8f15afe94d34c7e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 13:49:54 +0000 Subject: [PATCH 02/10] rename `equifibered-sequential-diagram` -> `equifibered-dependent-sequential-diagram` --- references.bib | 9 + src/synthetic-homotopy-theory.lagda.md | 2 +- ...cocones-under-sequential-diagrams.lagda.md | 20 +-- .../descent-data-sequential-colimits.lagda.md | 117 +++++++------ ...red-dependent-sequential-diagrams.lagda.md | 164 ++++++++++++++++++ .../equifibered-sequential-diagrams.lagda.md | 153 ---------------- 6 files changed, 244 insertions(+), 221 deletions(-) create mode 100644 src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md delete mode 100644 src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md diff --git a/references.bib b/references.bib index f63c1f2c16..d950d39efa 100644 --- a/references.bib +++ b/references.bib @@ -631,6 +631,15 @@ @phdthesis{Qui16 langid = {english} } +@online{Rezk10HomotopyToposes, + title = {Toposes and homotopy toposes}, + author = {Rezk, Charles}, + year = {2010}, + month = {01}, + url = {https://rezk.web.illinois.edu/homotopy-topos-sketch.pdf}, + version = {0.15} +} + @book{Rie17, title = {Category {{Theory}} in {{Context}}}, author = {Riehl, Emily}, diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index f05ba2976d..67f34fede5 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -58,7 +58,7 @@ open import synthetic-homotopy-theory.descent-property-pushouts public open import synthetic-homotopy-theory.descent-property-sequential-colimits public open import synthetic-homotopy-theory.double-loop-spaces public open import synthetic-homotopy-theory.eckmann-hilton-argument public -open import synthetic-homotopy-theory.equifibered-sequential-diagrams public +open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md index ca4adb47b0..6a9f85290f 100644 --- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md @@ -26,7 +26,7 @@ open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import synthetic-homotopy-theory.dependent-sequential-diagrams -open import synthetic-homotopy-theory.equifibered-sequential-diagrams +open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams open import synthetic-homotopy-theory.sequential-diagrams ``` @@ -266,7 +266,7 @@ which gives us a collection of type families `Pₙ : Aₙ → 𝒰`, and a colle equivalences `Pₙ a ≃ Pₙ₊₁ (aₙ a)` induced by [transporting](foundation-core.transport-along-identifications.md) in `P` along `Hₙ`. This data comes together to form an -[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-sequential-diagrams.md) +[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams.md) over `A`. ```agda @@ -276,24 +276,24 @@ module _ (P : X → UU l3) where - equifibered-sequential-diagram-family-cocone : - equifibered-sequential-diagram A l3 - pr1 equifibered-sequential-diagram-family-cocone n a = + equifibered-dependent-sequential-diagram-family-cocone : + equifibered-dependent-sequential-diagram A l3 + pr1 equifibered-dependent-sequential-diagram-family-cocone n a = P (map-cocone-sequential-diagram c n a) - pr2 equifibered-sequential-diagram-family-cocone n a = + pr2 equifibered-dependent-sequential-diagram-family-cocone n a = equiv-tr P (coherence-cocone-sequential-diagram c n a) dependent-sequential-diagram-family-cocone : dependent-sequential-diagram A l3 dependent-sequential-diagram-family-cocone = - dependent-sequential-diagram-equifibered-sequential-diagram - ( equifibered-sequential-diagram-family-cocone) + dependent-sequential-diagram-equifibered-dependent-sequential-diagram + ( equifibered-dependent-sequential-diagram-family-cocone) is-equifibered-dependent-sequential-diagram-family-cocone : is-equifibered-dependent-sequential-diagram ( dependent-sequential-diagram-family-cocone) is-equifibered-dependent-sequential-diagram-family-cocone = - is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram - ( equifibered-sequential-diagram-family-cocone) + is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram + ( equifibered-dependent-sequential-diagram-family-cocone) ``` ## Properties diff --git a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md index d498ebe3db..4f840820b2 100644 --- a/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-sequential-colimits.lagda.md @@ -15,7 +15,7 @@ open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-sequential-diagrams open import synthetic-homotopy-theory.dependent-sequential-diagrams -open import synthetic-homotopy-theory.equifibered-sequential-diagrams +open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams open import synthetic-homotopy-theory.sequential-diagrams @@ -32,7 +32,7 @@ Given a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) The data required to construct a type family is called {{#concept "descent data" Disambiguation="sequential colimits" Agda=descent-data-sequential-colimit}} for sequential colimits, and it is exactly an -[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-sequential-diagrams.md). +[equifibered sequential diagram](synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams.md). The fact that the type of descent data for a sequential diagram is equivalent to the type of type families over its colimit is recorded in @@ -49,7 +49,7 @@ module _ descent-data-sequential-colimit : (l2 : Level) → UU (l1 ⊔ lsuc l2) descent-data-sequential-colimit = - equifibered-sequential-diagram A + equifibered-dependent-sequential-diagram A ``` ### Components of descent data for sequential colimits @@ -89,7 +89,7 @@ module _ dependent-sequential-diagram-descent-data : dependent-sequential-diagram A l2 dependent-sequential-diagram-descent-data = - dependent-sequential-diagram-equifibered-sequential-diagram B + dependent-sequential-diagram-equifibered-dependent-sequential-diagram B ``` ### Morphisms of descent data for sequential colimits @@ -104,8 +104,8 @@ module _ hom-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3) hom-descent-data-sequential-colimit = hom-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram B) - ( dependent-sequential-diagram-equifibered-sequential-diagram C) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) ``` ### Equivalences of descent data for sequential colimits @@ -120,55 +120,58 @@ module _ equiv-descent-data-sequential-colimit : UU (l1 ⊔ l2 ⊔ l3) equiv-descent-data-sequential-colimit = equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram B) - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - - module _ - (e : equiv-descent-data-sequential-colimit) - where - - equiv-equiv-descent-data-sequential-colimit : - (n : ℕ) (a : family-sequential-diagram A n) → - family-descent-data-sequential-colimit B n a ≃ - family-descent-data-sequential-colimit C n a - equiv-equiv-descent-data-sequential-colimit = - equiv-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( e) - - map-equiv-descent-data-sequential-colimit : - (n : ℕ) (a : family-sequential-diagram A n) → - family-descent-data-sequential-colimit B n a → - family-descent-data-sequential-colimit C n a - map-equiv-descent-data-sequential-colimit = - map-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( e) - - is-equiv-map-equiv-descent-data-sequential-colimit : - (n : ℕ) (a : family-sequential-diagram A n) → - is-equiv (map-equiv-descent-data-sequential-colimit n a) - is-equiv-map-equiv-descent-data-sequential-colimit = - is-equiv-map-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( e) - - coh-equiv-descent-data-sequential-colimit : - coherence-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram B) - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( equiv-equiv-descent-data-sequential-colimit) - coh-equiv-descent-data-sequential-colimit = - coh-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( e) - - hom-equiv-descent-data-sequential-colimit : - hom-descent-data-sequential-colimit B C - hom-equiv-descent-data-sequential-colimit = - hom-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram C) - ( e) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + +module _ + {l1 l2 l3 : Level} {A : sequential-diagram l1} + (B : descent-data-sequential-colimit A l2) + (C : descent-data-sequential-colimit A l3) + (e : equiv-descent-data-sequential-colimit B C) + where + + equiv-equiv-descent-data-sequential-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + family-descent-data-sequential-colimit B n a ≃ + family-descent-data-sequential-colimit C n a + equiv-equiv-descent-data-sequential-colimit = + equiv-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( e) + + map-equiv-descent-data-sequential-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + family-descent-data-sequential-colimit B n a → + family-descent-data-sequential-colimit C n a + map-equiv-descent-data-sequential-colimit = + map-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( e) + + is-equiv-map-equiv-descent-data-sequential-colimit : + (n : ℕ) (a : family-sequential-diagram A n) → + is-equiv (map-equiv-descent-data-sequential-colimit n a) + is-equiv-map-equiv-descent-data-sequential-colimit = + is-equiv-map-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( e) + + coh-equiv-descent-data-sequential-colimit : + coherence-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( equiv-equiv-descent-data-sequential-colimit) + coh-equiv-descent-data-sequential-colimit = + coh-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( e) + + hom-equiv-descent-data-sequential-colimit : + hom-descent-data-sequential-colimit B C + hom-equiv-descent-data-sequential-colimit = + hom-equiv-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram C) + ( e) module _ {l1 l2 : Level} {A : sequential-diagram l1} @@ -179,7 +182,7 @@ module _ equiv-descent-data-sequential-colimit B B id-equiv-descent-data-sequential-colimit = id-equiv-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram B) + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B) ``` ### Descent data induced by families over cocones under sequential diagrams @@ -193,5 +196,5 @@ module _ descent-data-family-cocone-sequential-diagram : {l3 : Level} → (X → UU l3) → descent-data-sequential-colimit A l3 descent-data-family-cocone-sequential-diagram = - equifibered-sequential-diagram-family-cocone c + equifibered-dependent-sequential-diagram-family-cocone c ``` diff --git a/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md new file mode 100644 index 0000000000..56fd837da4 --- /dev/null +++ b/src/synthetic-homotopy-theory/equifibered-dependent-sequential-diagrams.lagda.md @@ -0,0 +1,164 @@ +# Equifibered dependent sequential diagrams + +```agda +module synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams where +``` + +
Imports + +```agda +open import elementary-number-theory.natural-numbers + +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.universe-levels + +open import synthetic-homotopy-theory.dependent-sequential-diagrams +open import synthetic-homotopy-theory.sequential-diagrams +``` + +
+ +## Idea + +An +{{#concept "equifibered dependent sequential diagram" Disambiguation="over a sequential diagram" Agda=equifibered-dependent-sequential-diagram}} +over a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) +`(A, a)` consists of a type family `B : (n : ℕ) → Aₙ → 𝒰` +[equipped](foundation.structure.md) with a family of fiberwise equivalences + +```text +bₙ : (a : Aₙ) → Bₙ a ≃ Bₙ₊₁ (aₙ a) . +``` + +The term "equifibered" comes from the equivalent definition as +[dependent sequential diagrams](synthetic-homotopy-theory.dependent-sequential-diagrams.md) +over `(A, a)` + +```text + b₀ b₁ b₂ + B₀ ---> B₁ ---> B₂ ---> ⋯ + | | | + | | | + ↡ ↡ ↡ + A₀ ---> A₁ ---> A₂ ---> ⋯ , + a₀ a₁ a₂ +``` + +which are said to be "fibered over `A`", whose maps `bₙ` are equivalences. + +The terminology was originally introduced by Charles Rezk in _Toposes and +Homotopy Toposes_ {{#cite Rezk10HomotopyToposes}}. + +## Definitions + +### Equifibered dependent sequential diagrams + +```agda +module _ + {l1 : Level} (A : sequential-diagram l1) + where + + equifibered-dependent-sequential-diagram : (l : Level) → UU (l1 ⊔ lsuc l) + equifibered-dependent-sequential-diagram l = + Σ ( (n : ℕ) → family-sequential-diagram A n → UU l) + ( λ B → + (n : ℕ) (a : family-sequential-diagram A n) → + B n a ≃ B (succ-ℕ n) (map-sequential-diagram A n a)) +``` + +### Components of an equifibered dependent sequential diagram + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + (B : equifibered-dependent-sequential-diagram A l2) + where + + family-equifibered-dependent-sequential-diagram : + (n : ℕ) → family-sequential-diagram A n → UU l2 + family-equifibered-dependent-sequential-diagram = pr1 B + + equiv-equifibered-dependent-sequential-diagram : + (n : ℕ) (a : family-sequential-diagram A n) → + family-equifibered-dependent-sequential-diagram n a ≃ + family-equifibered-dependent-sequential-diagram + ( succ-ℕ n) + ( map-sequential-diagram A n a) + equiv-equifibered-dependent-sequential-diagram = pr2 B + + map-equifibered-dependent-sequential-diagram : + (n : ℕ) (a : family-sequential-diagram A n) → + family-equifibered-dependent-sequential-diagram n a → + family-equifibered-dependent-sequential-diagram + ( succ-ℕ n) + ( map-sequential-diagram A n a) + map-equifibered-dependent-sequential-diagram n a = + map-equiv (equiv-equifibered-dependent-sequential-diagram n a) + + is-equiv-map-equifibered-dependent-sequential-diagram : + (n : ℕ) (a : family-sequential-diagram A n) → + is-equiv (map-equifibered-dependent-sequential-diagram n a) + is-equiv-map-equifibered-dependent-sequential-diagram n a = + is-equiv-map-equiv (equiv-equifibered-dependent-sequential-diagram n a) + + dependent-sequential-diagram-equifibered-dependent-sequential-diagram : + dependent-sequential-diagram A l2 + pr1 dependent-sequential-diagram-equifibered-dependent-sequential-diagram = + family-equifibered-dependent-sequential-diagram + pr2 dependent-sequential-diagram-equifibered-dependent-sequential-diagram = + map-equifibered-dependent-sequential-diagram +``` + +### The predicate on dependent sequential diagrams of being equifibered + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + where + + is-equifibered-dependent-sequential-diagram : + (B : dependent-sequential-diagram A l2) → UU (l1 ⊔ l2) + is-equifibered-dependent-sequential-diagram B = + (n : ℕ) (a : family-sequential-diagram A n) → + is-equiv (map-dependent-sequential-diagram B n a) + + is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram : + (B : equifibered-dependent-sequential-diagram A l2) → + is-equifibered-dependent-sequential-diagram + ( dependent-sequential-diagram-equifibered-dependent-sequential-diagram B) + is-equifibered-dependent-sequential-diagram-equifibered-dependent-sequential-diagram + B = + is-equiv-map-equifibered-dependent-sequential-diagram B +``` + +## Properties + +### Dependent sequential diagrams which are equifibered are equifibered dependent sequential diagrams + +To construct an equifibered dependent sequential diagram over `A`, it suffices +to construct a dependent sequential diagram `(B, b)` over `A`, and show that the +maps `bₙ` are equivalences. + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + (B : dependent-sequential-diagram A l2) + where + + equifibered-dependent-sequential-diagram-dependent-sequential-diagram : + is-equifibered-dependent-sequential-diagram B → + equifibered-dependent-sequential-diagram A l2 + pr1 + ( equifibered-dependent-sequential-diagram-dependent-sequential-diagram _) = + family-dependent-sequential-diagram B + pr2 + ( equifibered-dependent-sequential-diagram-dependent-sequential-diagram + is-equiv-map) + n a = + ( map-dependent-sequential-diagram B n a , is-equiv-map n a) +``` + +## References + +{{#bibliography}} diff --git a/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md deleted file mode 100644 index 07cb2a030f..0000000000 --- a/src/synthetic-homotopy-theory/equifibered-sequential-diagrams.lagda.md +++ /dev/null @@ -1,153 +0,0 @@ -# Equifibered sequential diagrams - -```agda -module synthetic-homotopy-theory.equifibered-sequential-diagrams where -``` - -
Imports - -```agda -open import elementary-number-theory.natural-numbers - -open import foundation.dependent-pair-types -open import foundation.equivalences -open import foundation.universe-levels - -open import synthetic-homotopy-theory.dependent-sequential-diagrams -open import synthetic-homotopy-theory.sequential-diagrams -``` - -
- -## Idea - -An -{{#concept "equifibered sequential diagram" Disambiguation="over a sequential diagram" Agda=equifibered-sequential-diagram}} -over a [sequential diagram](synthetic-homotopy-theory.sequential-diagrams.md) -`(A, a)` consists of a type family `B : (n : ℕ) → Aₙ → 𝒰` -[equipped](foundation.structure.md) with a family of fiberwise equivalences - -```text -bₙ : (a : Aₙ) → Bₙ a ≃ Bₙ₊₁ (aₙ a) . -``` - -The term "equifibered" comes from the equivalent definition as -[dependent sequential diagrams](synthetic-homotopy-theory.dependent-sequential-diagrams.md) -over `(A, a)` - -```text - b₀ b₁ b₂ - B₀ ---> B₁ ---> B₂ ---> ⋯ - | | | - | | | - ↡ ↡ ↡ - A₀ ---> A₁ ---> A₂ ---> ⋯ , - a₀ a₁ a₂ -``` - -which are said to be "fibered over `A`", whose maps `bₙ` are equivalences. - -## Definitions - -### Equifibered sequential diagrams - -```agda -module _ - {l1 : Level} (A : sequential-diagram l1) - where - - equifibered-sequential-diagram : (l : Level) → UU (l1 ⊔ lsuc l) - equifibered-sequential-diagram l = - Σ ( (n : ℕ) → family-sequential-diagram A n → UU l) - ( λ B → - (n : ℕ) (a : family-sequential-diagram A n) → - B n a ≃ B (succ-ℕ n) (map-sequential-diagram A n a)) -``` - -### Components of an equifibered sequential diagram - -```agda -module _ - {l1 l2 : Level} {A : sequential-diagram l1} - (B : equifibered-sequential-diagram A l2) - where - - family-equifibered-sequential-diagram : - (n : ℕ) → family-sequential-diagram A n → UU l2 - family-equifibered-sequential-diagram = pr1 B - - equiv-equifibered-sequential-diagram : - (n : ℕ) (a : family-sequential-diagram A n) → - family-equifibered-sequential-diagram n a ≃ - family-equifibered-sequential-diagram - ( succ-ℕ n) - ( map-sequential-diagram A n a) - equiv-equifibered-sequential-diagram = pr2 B - - map-equifibered-sequential-diagram : - (n : ℕ) (a : family-sequential-diagram A n) → - family-equifibered-sequential-diagram n a → - family-equifibered-sequential-diagram - ( succ-ℕ n) - ( map-sequential-diagram A n a) - map-equifibered-sequential-diagram n a = - map-equiv (equiv-equifibered-sequential-diagram n a) - - is-equiv-map-equifibered-sequential-diagram : - (n : ℕ) (a : family-sequential-diagram A n) → - is-equiv (map-equifibered-sequential-diagram n a) - is-equiv-map-equifibered-sequential-diagram n a = - is-equiv-map-equiv (equiv-equifibered-sequential-diagram n a) - - dependent-sequential-diagram-equifibered-sequential-diagram : - dependent-sequential-diagram A l2 - pr1 dependent-sequential-diagram-equifibered-sequential-diagram = - family-equifibered-sequential-diagram - pr2 dependent-sequential-diagram-equifibered-sequential-diagram = - map-equifibered-sequential-diagram -``` - -### The predicate on dependent sequential diagrams of being equifibered - -```agda -module _ - {l1 l2 : Level} {A : sequential-diagram l1} - where - - is-equifibered-dependent-sequential-diagram : - (B : dependent-sequential-diagram A l2) → UU (l1 ⊔ l2) - is-equifibered-dependent-sequential-diagram B = - (n : ℕ) (a : family-sequential-diagram A n) → - is-equiv (map-dependent-sequential-diagram B n a) - - is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram : - (B : equifibered-sequential-diagram A l2) → - is-equifibered-dependent-sequential-diagram - ( dependent-sequential-diagram-equifibered-sequential-diagram B) - is-equifibered-dependent-sequential-diagram-equifibered-sequential-diagram B = - is-equiv-map-equifibered-sequential-diagram B -``` - -## Properties - -### Dependent sequential diagrams which are equifibered are equifibered sequential diagrams - -To construct an equifibered sequential diagram over `A`, it suffices to -construct a dependent sequential diagram `(B, b)` over `A`, and show that the -maps `bₙ` are equivalences. - -```agda -module _ - {l1 l2 : Level} {A : sequential-diagram l1} - (B : dependent-sequential-diagram A l2) - where - - equifibered-sequential-diagram-dependent-sequential-diagram : - is-equifibered-dependent-sequential-diagram B → - equifibered-sequential-diagram A l2 - pr1 (equifibered-sequential-diagram-dependent-sequential-diagram _) = - family-dependent-sequential-diagram B - pr2 (equifibered-sequential-diagram-dependent-sequential-diagram is-equiv-map) - n a = - (map-dependent-sequential-diagram B n a , is-equiv-map n a) -``` From 3fb8f33af83d41aa094a979dc1ed43fffb90ece6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 14:29:45 +0000 Subject: [PATCH 03/10] equifibered dependent span diagrams --- src/synthetic-homotopy-theory.lagda.md | 2 + .../descent-data-pushouts.lagda.md | 143 ------ ...uifibered-dependent-span-diagrams.lagda.md | 243 +++++++++ ...quivalences-descent-data-pushouts.lagda.md | 206 -------- ...uifibered-dependent-span-diagrams.lagda.md | 466 ++++++++++++++++++ 5 files changed, 711 insertions(+), 349 deletions(-) create mode 100644 src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md create mode 100644 src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index 67f34fede5..be6e82a6c9 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -59,10 +59,12 @@ open import synthetic-homotopy-theory.descent-property-sequential-colimits publi open import synthetic-homotopy-theory.double-loop-spaces public open import synthetic-homotopy-theory.eckmann-hilton-argument public open import synthetic-homotopy-theory.equifibered-dependent-sequential-diagrams public +open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams public open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public open import synthetic-homotopy-theory.equivalences-descent-data-pushouts public +open import synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams public open import synthetic-homotopy-theory.equivalences-sequential-diagrams public open import synthetic-homotopy-theory.families-descent-data-pushouts public open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md index 5df9f42d62..23adaf8249 100644 --- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md @@ -114,140 +114,6 @@ module _ is-equiv-map-equiv (equiv-family-descent-data-pushout s) ``` -### Symmetric descent data for pushouts - -We give another equivalent definition of descent data for pushouts, that records -an additional type family `PS` over the spanning type `S` and equivalences -`PS s ≃ PA (f s)` and `PS s ≃ PB (g s)` for all `s`. - -```agda -module _ - {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) - where - - symmetric-descent-data-pushout : - (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6) - symmetric-descent-data-pushout l4 l5 l6 = - Σ ( domain-span-diagram 𝒮 → UU l4) - ( λ PA → - Σ ( codomain-span-diagram 𝒮 → UU l5) - ( λ PB → - Σ ( spanning-type-span-diagram 𝒮 → UU l6) - ( λ PS → - ( (s : spanning-type-span-diagram 𝒮) → - PS s ≃ PA (left-map-span-diagram 𝒮 s)) × - ( (s : spanning-type-span-diagram 𝒮) → - PS s ≃ PB (right-map-span-diagram 𝒮 s))))) -``` - -### Components of symmetric descent data for pushouts - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6) - where - - left-family-symmetric-descent-data-pushout : domain-span-diagram 𝒮 → UU l4 - left-family-symmetric-descent-data-pushout = pr1 P - - right-family-symmetric-descent-data-pushout : codomain-span-diagram 𝒮 → UU l5 - right-family-symmetric-descent-data-pushout = pr1 (pr2 P) - - spanning-type-family-symmetric-descent-data-pushout : - spanning-type-span-diagram 𝒮 → UU l6 - spanning-type-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 P)) - - equiv-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout s ≃ - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) - equiv-left-family-symmetric-descent-data-pushout = pr1 (pr2 (pr2 (pr2 P))) - - equiv-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout s ≃ - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) - equiv-right-family-symmetric-descent-data-pushout = pr2 (pr2 (pr2 (pr2 P))) - - map-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout s → - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) - map-left-family-symmetric-descent-data-pushout = - map-equiv ∘ equiv-left-family-symmetric-descent-data-pushout - - map-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout s → - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) - map-right-family-symmetric-descent-data-pushout = - map-equiv ∘ equiv-right-family-symmetric-descent-data-pushout - - map-inv-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) → - spanning-type-family-symmetric-descent-data-pushout s - map-inv-left-family-symmetric-descent-data-pushout = - map-inv-equiv ∘ equiv-left-family-symmetric-descent-data-pushout - - map-inv-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) → - spanning-type-family-symmetric-descent-data-pushout s - map-inv-right-family-symmetric-descent-data-pushout = - map-inv-equiv ∘ equiv-right-family-symmetric-descent-data-pushout - - is-equiv-map-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - is-equiv (map-left-family-symmetric-descent-data-pushout s) - is-equiv-map-left-family-symmetric-descent-data-pushout s = - is-equiv-map-equiv (equiv-left-family-symmetric-descent-data-pushout s) - - is-equiv-map-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - is-equiv (map-right-family-symmetric-descent-data-pushout s) - is-equiv-map-right-family-symmetric-descent-data-pushout s = - is-equiv-map-equiv (equiv-right-family-symmetric-descent-data-pushout s) - - equiv-left-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃ - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) - equiv-left-right-family-symmetric-descent-data-pushout s = - equiv-right-family-symmetric-descent-data-pushout s ∘e - inv-equiv (equiv-left-family-symmetric-descent-data-pushout s) - - map-left-right-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) → - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) - map-left-right-family-symmetric-descent-data-pushout = - map-equiv ∘ equiv-left-right-family-symmetric-descent-data-pushout - - equiv-right-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) ≃ - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) - equiv-right-left-family-symmetric-descent-data-pushout s = - equiv-left-family-symmetric-descent-data-pushout s ∘e - inv-equiv (equiv-right-family-symmetric-descent-data-pushout s) - - map-right-left-family-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout (right-map-span-diagram 𝒮 s) → - left-family-symmetric-descent-data-pushout (left-map-span-diagram 𝒮 s) - map-right-left-family-symmetric-descent-data-pushout = - map-equiv ∘ equiv-right-left-family-symmetric-descent-data-pushout - - descent-data-pushout-symmetric-descent-data-pushout : - descent-data-pushout 𝒮 l4 l5 - descent-data-pushout-symmetric-descent-data-pushout = - ( left-family-symmetric-descent-data-pushout , - right-family-symmetric-descent-data-pushout , - equiv-left-right-family-symmetric-descent-data-pushout) -``` - ### Descent data induced by families over cocones Given a [cocone](synthetic-homotopy-theory.cocones-under-spans.md) @@ -280,13 +146,4 @@ module _ ( P ∘ horizontal-map-cocone _ _ c) , ( P ∘ vertical-map-cocone _ _ c) , ( equiv-tr P ∘ coherence-square-cocone _ _ c) - - symmetric-descent-data-family-cocone-span-diagram : - {l5 : Level} → (X → UU l5) → symmetric-descent-data-pushout 𝒮 l5 l5 l5 - symmetric-descent-data-family-cocone-span-diagram P = - ( P ∘ horizontal-map-cocone _ _ c) , - ( P ∘ vertical-map-cocone _ _ c) , - ( P ∘ horizontal-map-cocone _ _ c ∘ left-map-span-diagram 𝒮) , - ( λ _ → id-equiv) , - ( equiv-tr P ∘ coherence-square-cocone _ _ c) ``` diff --git a/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md new file mode 100644 index 0000000000..a1f1512fc0 --- /dev/null +++ b/src/synthetic-homotopy-theory/equifibered-dependent-span-diagrams.lagda.md @@ -0,0 +1,243 @@ +# Equifibered dependent span diagrams + +```agda +module synthetic-homotopy-theory.equifibered-dependent-span-diagrams where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-types +open import foundation.span-diagrams +open import foundation.transport-along-identifications +open import foundation.universe-levels + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.descent-data-pushouts +``` + +
+ +## Idea + +Given a [span diagram](foundation.span-diagrams.md) `𝒮` of the form + +```text + f g + A <---- S ----> B, +``` + +a +{{#concept "equifibered dependent span diagram" Disambiguation="over a span diagram" Agda=equifibered-dependent-span-diagram}} +is a triple of type families `PA`, `PB`, `PS` over the vertices of `𝒮`, + +```text + 𝒰 𝒱 𝒲 + ↑ ↑ ↑ + A <---- S ----> B, +``` + +together with families of equivalences `PS s ≃ PA (f s)` and `PS s ≃ PB (g s)` +for every `s : S`. + +> In +> [`descent-property-pushouts`](synthetic-homotopy-theory.descent-property-pushouts.md), +> we show that this is exactly the data one needs to "glue together" a type +> family `P : X → 𝒰` over the pushout `X` of `𝒮`. + +> The [identity type](foundation-core.identity-types.md) of descent data is +> characterized in +> [`equivalences-descent-data-pushouts`](synthetic-homotopy-theory.equivalences-descent-data-pushouts.md). +> +> It may not be immediately clear why "descent data" is an appropriate name for +> this concept, because there is no apparent downward motion. Traditionally, +> descent is studied in the context of a collection of objects `Xᵢ` covering a +> single object `X`, and local structure on the individual `Xᵢ`'s descending +> onto `X`, collecting into a global structure, given that the pieces are +> appropriately compatible on any "overlaps". A pushout of `𝒮` is covered by `A` +> and `B`, and the overlaps are encoded in `f` and `g`. Then structure on `A` +> and `B`, expressed as type families `PA` and `PB`, "descends" to a structure +> on `X` (a type family over `X`). Two elements "overlap" in `X` if there is an +> identification between them coming from `S`, and the gluing/compatibility +> condition exactly requires the local structure of `PA` and `PB` to agree on +> such elements, i.e. asks for an equivalence `PA(fs) ≃ PB(gs)`. + +## Definitions + +### Equifibered dependent span diagrams + +```agda +module _ + {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) + where + + equifibered-dependent-span-diagram : + (l4 l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6) + equifibered-dependent-span-diagram l4 l5 l6 = + Σ ( domain-span-diagram 𝒮 → UU l4) + ( λ PA → + Σ ( codomain-span-diagram 𝒮 → UU l5) + ( λ PB → + Σ ( spanning-type-span-diagram 𝒮 → UU l6) + ( λ PS → + ( (s : spanning-type-span-diagram 𝒮) → + PS s ≃ PA (left-map-span-diagram 𝒮 s)) × + ( (s : spanning-type-span-diagram 𝒮) → + PS s ≃ PB (right-map-span-diagram 𝒮 s))))) +``` + +### Components of equifibered dependent span diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6) + where + + left-family-equifibered-dependent-span-diagram : + domain-span-diagram 𝒮 → UU l4 + left-family-equifibered-dependent-span-diagram = + pr1 P + + right-family-equifibered-dependent-span-diagram : + codomain-span-diagram 𝒮 → UU l5 + right-family-equifibered-dependent-span-diagram = + pr1 (pr2 P) + + spanning-type-family-equifibered-dependent-span-diagram : + spanning-type-span-diagram 𝒮 → UU l6 + spanning-type-family-equifibered-dependent-span-diagram = + pr1 (pr2 (pr2 P)) + + equiv-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram s ≃ + left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) + equiv-left-family-equifibered-dependent-span-diagram = + pr1 (pr2 (pr2 (pr2 P))) + + equiv-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram s ≃ + right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s) + equiv-right-family-equifibered-dependent-span-diagram = + pr2 (pr2 (pr2 (pr2 P))) + + map-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram s → + left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) + map-left-family-equifibered-dependent-span-diagram = + map-equiv ∘ equiv-left-family-equifibered-dependent-span-diagram + + map-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram s → + right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s) + map-right-family-equifibered-dependent-span-diagram = + map-equiv ∘ equiv-right-family-equifibered-dependent-span-diagram + + map-inv-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) → + spanning-type-family-equifibered-dependent-span-diagram s + map-inv-left-family-equifibered-dependent-span-diagram = + map-inv-equiv ∘ equiv-left-family-equifibered-dependent-span-diagram + + map-inv-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s) → + spanning-type-family-equifibered-dependent-span-diagram s + map-inv-right-family-equifibered-dependent-span-diagram = + map-inv-equiv ∘ equiv-right-family-equifibered-dependent-span-diagram + + is-equiv-map-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + is-equiv (map-left-family-equifibered-dependent-span-diagram s) + is-equiv-map-left-family-equifibered-dependent-span-diagram s = + is-equiv-map-equiv (equiv-left-family-equifibered-dependent-span-diagram s) + + is-equiv-map-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + is-equiv (map-right-family-equifibered-dependent-span-diagram s) + is-equiv-map-right-family-equifibered-dependent-span-diagram s = + is-equiv-map-equiv (equiv-right-family-equifibered-dependent-span-diagram s) + + equiv-left-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) ≃ + right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s) + equiv-left-right-family-equifibered-dependent-span-diagram s = + equiv-right-family-equifibered-dependent-span-diagram s ∘e + inv-equiv (equiv-left-family-equifibered-dependent-span-diagram s) + + map-left-right-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram (left-map-span-diagram 𝒮 s) → + right-family-equifibered-dependent-span-diagram (right-map-span-diagram 𝒮 s) + map-left-right-family-equifibered-dependent-span-diagram = + map-equiv ∘ equiv-left-right-family-equifibered-dependent-span-diagram + + equiv-right-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s) ≃ + left-family-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s) + equiv-right-left-family-equifibered-dependent-span-diagram s = + equiv-left-family-equifibered-dependent-span-diagram s ∘e + inv-equiv (equiv-right-family-equifibered-dependent-span-diagram s) + + map-right-left-family-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s) → + left-family-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s) + map-right-left-family-equifibered-dependent-span-diagram = + map-equiv ∘ equiv-right-left-family-equifibered-dependent-span-diagram + + descent-data-pushout-equifibered-dependent-span-diagram : + descent-data-pushout 𝒮 l4 l5 + descent-data-pushout-equifibered-dependent-span-diagram = + ( left-family-equifibered-dependent-span-diagram , + right-family-equifibered-dependent-span-diagram , + equiv-left-right-family-equifibered-dependent-span-diagram) +``` + +### Equifibered dependent span diagrams induced by descent data for pushouts + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + where + + equifibered-dependent-span-diagram-descent-data-pushout : + equifibered-dependent-span-diagram 𝒮 l4 l5 l4 + equifibered-dependent-span-diagram-descent-data-pushout = + ( left-family-descent-data-pushout P) , + ( right-family-descent-data-pushout P) , + ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) , + ( λ _ → id-equiv) , + ( equiv-family-descent-data-pushout P) +``` + +### Equifibered dependent span diagrams induced by families over cocones + +```agda +module _ + {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} + {X : UU l4} (c : cocone-span-diagram 𝒮 X) + where + + equifibered-dependent-span-diagram-family-cocone-span-diagram : + {l5 : Level} → (X → UU l5) → equifibered-dependent-span-diagram 𝒮 l5 l5 l5 + equifibered-dependent-span-diagram-family-cocone-span-diagram P = + equifibered-dependent-span-diagram-descent-data-pushout + ( descent-data-family-cocone-span-diagram c P) +``` diff --git a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md index 2b126bbbb2..fdcf6529d8 100644 --- a/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-descent-data-pushouts.lagda.md @@ -172,212 +172,6 @@ module _ coherence-equiv-descent-data-pushout) ``` -### Equivalences of symmetric descent data for pushouts - -Note that the descent data arguments cannot be inferred when calling -`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer -the proofs of `is-equiv` of their gluing maps. - -```agda -module _ - {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} - {𝒮 : span-diagram l1 l2 l3} - (P : symmetric-descent-data-pushout 𝒮 l4 l5 l6) - (Q : symmetric-descent-data-pushout 𝒮 l7 l8 l9) - where - - equiv-symmetric-descent-data-pushout : - UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9) - equiv-symmetric-descent-data-pushout = - Σ ( (a : domain-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout P a ≃ - left-family-symmetric-descent-data-pushout Q a) - ( λ eA → - Σ ( (b : codomain-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout P b ≃ - right-family-symmetric-descent-data-pushout Q b) - ( λ eB → - Σ ( (s : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout P s ≃ - spanning-type-family-symmetric-descent-data-pushout Q s) - ( λ eS → - ( (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( map-equiv (eS s)) - ( map-left-family-symmetric-descent-data-pushout P s) - ( map-left-family-symmetric-descent-data-pushout Q s) - ( map-equiv (eA (left-map-span-diagram 𝒮 s)))) × - ( (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( map-equiv (eS s)) - ( map-right-family-symmetric-descent-data-pushout P s) - ( map-right-family-symmetric-descent-data-pushout Q s) - ( map-equiv (eB (right-map-span-diagram 𝒮 s))))))) - - module _ - (e : equiv-symmetric-descent-data-pushout) - where - - left-equiv-equiv-symmetric-descent-data-pushout : - (a : domain-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout P a ≃ - left-family-symmetric-descent-data-pushout Q a - left-equiv-equiv-symmetric-descent-data-pushout = pr1 e - - left-map-equiv-symmetric-descent-data-pushout : - (a : domain-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout P a → - left-family-symmetric-descent-data-pushout Q a - left-map-equiv-symmetric-descent-data-pushout a = - map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) - - is-equiv-left-map-equiv-symmetric-descent-data-pushout : - (a : domain-span-diagram 𝒮) → - is-equiv (left-map-equiv-symmetric-descent-data-pushout a) - is-equiv-left-map-equiv-symmetric-descent-data-pushout a = - is-equiv-map-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) - - inv-left-map-equiv-symmetric-descent-data-pushout : - (a : domain-span-diagram 𝒮) → - left-family-symmetric-descent-data-pushout Q a → - left-family-symmetric-descent-data-pushout P a - inv-left-map-equiv-symmetric-descent-data-pushout a = - map-inv-equiv (left-equiv-equiv-symmetric-descent-data-pushout a) - - right-equiv-equiv-symmetric-descent-data-pushout : - (b : codomain-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout P b ≃ - right-family-symmetric-descent-data-pushout Q b - right-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 e) - - right-map-equiv-symmetric-descent-data-pushout : - (b : codomain-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout P b → - right-family-symmetric-descent-data-pushout Q b - right-map-equiv-symmetric-descent-data-pushout b = - map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) - - is-equiv-right-map-equiv-symmetric-descent-data-pushout : - (b : codomain-span-diagram 𝒮) → - is-equiv (right-map-equiv-symmetric-descent-data-pushout b) - is-equiv-right-map-equiv-symmetric-descent-data-pushout b = - is-equiv-map-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) - - inv-right-map-equiv-symmetric-descent-data-pushout : - (b : codomain-span-diagram 𝒮) → - right-family-symmetric-descent-data-pushout Q b → - right-family-symmetric-descent-data-pushout P b - inv-right-map-equiv-symmetric-descent-data-pushout b = - map-inv-equiv (right-equiv-equiv-symmetric-descent-data-pushout b) - - spanning-type-equiv-equiv-symmetric-descent-data-pushout : - (b : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout P b ≃ - spanning-type-family-symmetric-descent-data-pushout Q b - spanning-type-equiv-equiv-symmetric-descent-data-pushout = pr1 (pr2 (pr2 e)) - - spanning-type-map-equiv-symmetric-descent-data-pushout : - (b : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout P b → - spanning-type-family-symmetric-descent-data-pushout Q b - spanning-type-map-equiv-symmetric-descent-data-pushout b = - map-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b) - - is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout : - (b : spanning-type-span-diagram 𝒮) → - is-equiv (spanning-type-map-equiv-symmetric-descent-data-pushout b) - is-equiv-spanning-type-map-equiv-symmetric-descent-data-pushout b = - is-equiv-map-equiv - ( spanning-type-equiv-equiv-symmetric-descent-data-pushout b) - - inv-spanning-type-map-equiv-symmetric-descent-data-pushout : - (b : spanning-type-span-diagram 𝒮) → - spanning-type-family-symmetric-descent-data-pushout Q b → - spanning-type-family-symmetric-descent-data-pushout P b - inv-spanning-type-map-equiv-symmetric-descent-data-pushout b = - map-inv-equiv (spanning-type-equiv-equiv-symmetric-descent-data-pushout b) - - coherence-left-equiv-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( map-left-family-symmetric-descent-data-pushout P s) - ( map-left-family-symmetric-descent-data-pushout Q s) - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - coherence-left-equiv-symmetric-descent-data-pushout = - pr1 (pr2 (pr2 (pr2 e))) - - coherence-right-equiv-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( map-right-family-symmetric-descent-data-pushout P s) - ( map-right-family-symmetric-descent-data-pushout Q s) - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - coherence-right-equiv-symmetric-descent-data-pushout = - pr2 (pr2 (pr2 (pr2 e))) - - coherence-left-right-equiv-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - ( map-left-right-family-symmetric-descent-data-pushout P s) - ( map-left-right-family-symmetric-descent-data-pushout Q s) - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - coherence-left-right-equiv-symmetric-descent-data-pushout s = - pasting-vertical-coherence-square-maps - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - ( map-inv-left-family-symmetric-descent-data-pushout P s) - ( map-inv-left-family-symmetric-descent-data-pushout Q s) - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( map-right-family-symmetric-descent-data-pushout P s) - ( map-right-family-symmetric-descent-data-pushout Q s) - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - (vertical-inv-equiv-coherence-square-maps - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( equiv-left-family-symmetric-descent-data-pushout P s) - ( equiv-left-family-symmetric-descent-data-pushout Q s) - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - ( coherence-left-equiv-symmetric-descent-data-pushout s)) - ( coherence-right-equiv-symmetric-descent-data-pushout s) - - coherence-right-left-equiv-symmetric-descent-data-pushout : - (s : spanning-type-span-diagram 𝒮) → - coherence-square-maps - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - ( map-right-left-family-symmetric-descent-data-pushout P s) - ( map-right-left-family-symmetric-descent-data-pushout Q s) - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - coherence-right-left-equiv-symmetric-descent-data-pushout s = - pasting-vertical-coherence-square-maps - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - ( map-inv-right-family-symmetric-descent-data-pushout P s) - ( map-inv-right-family-symmetric-descent-data-pushout Q s) - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( map-left-family-symmetric-descent-data-pushout P s) - ( map-left-family-symmetric-descent-data-pushout Q s) - ( left-map-equiv-symmetric-descent-data-pushout - ( left-map-span-diagram 𝒮 s)) - (vertical-inv-equiv-coherence-square-maps - ( spanning-type-map-equiv-symmetric-descent-data-pushout s) - ( equiv-right-family-symmetric-descent-data-pushout P s) - ( equiv-right-family-symmetric-descent-data-pushout Q s) - ( right-map-equiv-symmetric-descent-data-pushout - ( right-map-span-diagram 𝒮 s)) - ( coherence-right-equiv-symmetric-descent-data-pushout s)) - ( coherence-left-equiv-symmetric-descent-data-pushout s) -``` - ### The identity equivalence of descent data for pushouts ```agda diff --git a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md new file mode 100644 index 0000000000..9ae980287b --- /dev/null +++ b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md @@ -0,0 +1,466 @@ +# Equivalences of equifibered dependent span diagrams + +```agda +module synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams where +``` + +
Imports + +```agda +open import foundation.cartesian-product-types +open import foundation.commuting-squares-of-maps +open import foundation.dependent-pair-types +open import foundation.equality-dependent-function-types +open import foundation.equivalence-extensionality +open import foundation.equivalences +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.span-diagrams +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +open import foundation.univalence +open import foundation.universe-levels + +open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams +``` + +
+ +## Idea + +Given [descent data](synthetic-homotopy-theory.descent-data-pushouts.md) for +[pushouts](synthetic-homotopy-theory.pushouts.md) `(PA, PB, PS)` and +`(QA, QB, QS)`, an +{{#concept "equivalence" Disambiguation="descent data for pushouts" Agda=equiv-descent-data-pushout}} +between them is a pair of fiberwise equivalences + +```text + eA : (a : A) → PA a ≃ QA a + eB : (b : B) → PB b ≃ QB b +``` + +equipped with a family of [homotopies](foundation-core.homotopies.md) making + +```text + eA(fs) + PA(fs) --------> QA(fs) + | | + PS s | | QS s + | | + ∨ ∨ + PB(gs) --------> QB(gs) + eB(gs) +``` + +[commute](foundation-core.commuting-squares-of-maps.md) for every `s : S`. + +We show that equivalences characterize the +[identity types](foundation-core.identity-types.md) of descent data for +pushouts. + +By forgetting that the fiberwise maps are equivalences, we get the underlying +[morphism of descent data](synthetic-homotopy-theory.morphisms-descent-data-pushouts.md). +We define homotopies of equivalences of descent data to be homotopies of the +underlying morphisms, and show that homotopies characterize the identity type of +equivalences of descent data. + +## Definitions + +### Equivalences of equifibered dependent span diagrams + +Note that the descent data arguments cannot be inferred when calling +`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer +the proofs of `is-equiv` of their gluing maps. + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} + {𝒮 : span-diagram l1 l2 l3} + (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6) + (Q : equifibered-dependent-span-diagram 𝒮 l7 l8 l9) + where + + equiv-equifibered-dependent-span-diagram : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7 ⊔ l8 ⊔ l9) + equiv-equifibered-dependent-span-diagram = + Σ ( (a : domain-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram P a ≃ + left-family-equifibered-dependent-span-diagram Q a) + ( λ eA → + Σ ( (b : codomain-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram P b ≃ + right-family-equifibered-dependent-span-diagram Q b) + ( λ eB → + Σ ( (s : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram P s ≃ + spanning-type-family-equifibered-dependent-span-diagram Q s) + ( λ eS → + ( (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( map-equiv (eS s)) + ( map-left-family-equifibered-dependent-span-diagram P s) + ( map-left-family-equifibered-dependent-span-diagram Q s) + ( map-equiv (eA (left-map-span-diagram 𝒮 s)))) × + ( (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( map-equiv (eS s)) + ( map-right-family-equifibered-dependent-span-diagram P s) + ( map-right-family-equifibered-dependent-span-diagram Q s) + ( map-equiv (eB (right-map-span-diagram 𝒮 s))))))) + + module _ + (e : equiv-equifibered-dependent-span-diagram) + where + + left-equiv-equiv-equifibered-dependent-span-diagram : + (a : domain-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram P a ≃ + left-family-equifibered-dependent-span-diagram Q a + left-equiv-equiv-equifibered-dependent-span-diagram = pr1 e + + left-map-equiv-equifibered-dependent-span-diagram : + (a : domain-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram P a → + left-family-equifibered-dependent-span-diagram Q a + left-map-equiv-equifibered-dependent-span-diagram a = + map-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a) + + is-equiv-left-map-equiv-equifibered-dependent-span-diagram : + (a : domain-span-diagram 𝒮) → + is-equiv (left-map-equiv-equifibered-dependent-span-diagram a) + is-equiv-left-map-equiv-equifibered-dependent-span-diagram a = + is-equiv-map-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a) + + inv-left-map-equiv-equifibered-dependent-span-diagram : + (a : domain-span-diagram 𝒮) → + left-family-equifibered-dependent-span-diagram Q a → + left-family-equifibered-dependent-span-diagram P a + inv-left-map-equiv-equifibered-dependent-span-diagram a = + map-inv-equiv (left-equiv-equiv-equifibered-dependent-span-diagram a) + + right-equiv-equiv-equifibered-dependent-span-diagram : + (b : codomain-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram P b ≃ + right-family-equifibered-dependent-span-diagram Q b + right-equiv-equiv-equifibered-dependent-span-diagram = pr1 (pr2 e) + + right-map-equiv-equifibered-dependent-span-diagram : + (b : codomain-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram P b → + right-family-equifibered-dependent-span-diagram Q b + right-map-equiv-equifibered-dependent-span-diagram b = + map-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b) + + is-equiv-right-map-equiv-equifibered-dependent-span-diagram : + (b : codomain-span-diagram 𝒮) → + is-equiv (right-map-equiv-equifibered-dependent-span-diagram b) + is-equiv-right-map-equiv-equifibered-dependent-span-diagram b = + is-equiv-map-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b) + + inv-right-map-equiv-equifibered-dependent-span-diagram : + (b : codomain-span-diagram 𝒮) → + right-family-equifibered-dependent-span-diagram Q b → + right-family-equifibered-dependent-span-diagram P b + inv-right-map-equiv-equifibered-dependent-span-diagram b = + map-inv-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b) + + spanning-type-equiv-equiv-equifibered-dependent-span-diagram : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram P b ≃ + spanning-type-family-equifibered-dependent-span-diagram Q b + spanning-type-equiv-equiv-equifibered-dependent-span-diagram = + pr1 (pr2 (pr2 e)) + + spanning-type-map-equiv-equifibered-dependent-span-diagram : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram P b → + spanning-type-family-equifibered-dependent-span-diagram Q b + spanning-type-map-equiv-equifibered-dependent-span-diagram b = + map-equiv (spanning-type-equiv-equiv-equifibered-dependent-span-diagram b) + + is-equiv-spanning-type-map-equiv-equifibered-dependent-span-diagram : + (b : spanning-type-span-diagram 𝒮) → + is-equiv (spanning-type-map-equiv-equifibered-dependent-span-diagram b) + is-equiv-spanning-type-map-equiv-equifibered-dependent-span-diagram b = + is-equiv-map-equiv + ( spanning-type-equiv-equiv-equifibered-dependent-span-diagram b) + + inv-spanning-type-map-equiv-equifibered-dependent-span-diagram : + (b : spanning-type-span-diagram 𝒮) → + spanning-type-family-equifibered-dependent-span-diagram Q b → + spanning-type-family-equifibered-dependent-span-diagram P b + inv-spanning-type-map-equiv-equifibered-dependent-span-diagram b = + map-inv-equiv (spanning-type-equiv-equiv-equifibered-dependent-span-diagram b) + + coherence-left-equiv-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( map-left-family-equifibered-dependent-span-diagram P s) + ( map-left-family-equifibered-dependent-span-diagram Q s) + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + coherence-left-equiv-equifibered-dependent-span-diagram = + pr1 (pr2 (pr2 (pr2 e))) + + coherence-right-equiv-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( map-right-family-equifibered-dependent-span-diagram P s) + ( map-right-family-equifibered-dependent-span-diagram Q s) + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + coherence-right-equiv-equifibered-dependent-span-diagram = + pr2 (pr2 (pr2 (pr2 e))) + + coherence-left-right-equiv-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + ( map-left-right-family-equifibered-dependent-span-diagram P s) + ( map-left-right-family-equifibered-dependent-span-diagram Q s) + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + coherence-left-right-equiv-equifibered-dependent-span-diagram s = + pasting-vertical-coherence-square-maps + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + ( map-inv-left-family-equifibered-dependent-span-diagram P s) + ( map-inv-left-family-equifibered-dependent-span-diagram Q s) + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( map-right-family-equifibered-dependent-span-diagram P s) + ( map-right-family-equifibered-dependent-span-diagram Q s) + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + (vertical-inv-equiv-coherence-square-maps + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( equiv-left-family-equifibered-dependent-span-diagram P s) + ( equiv-left-family-equifibered-dependent-span-diagram Q s) + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + ( coherence-left-equiv-equifibered-dependent-span-diagram s)) + ( coherence-right-equiv-equifibered-dependent-span-diagram s) + + coherence-right-left-equiv-equifibered-dependent-span-diagram : + (s : spanning-type-span-diagram 𝒮) → + coherence-square-maps + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + ( map-right-left-family-equifibered-dependent-span-diagram P s) + ( map-right-left-family-equifibered-dependent-span-diagram Q s) + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + coherence-right-left-equiv-equifibered-dependent-span-diagram s = + pasting-vertical-coherence-square-maps + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + ( map-inv-right-family-equifibered-dependent-span-diagram P s) + ( map-inv-right-family-equifibered-dependent-span-diagram Q s) + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( map-left-family-equifibered-dependent-span-diagram P s) + ( map-left-family-equifibered-dependent-span-diagram Q s) + ( left-map-equiv-equifibered-dependent-span-diagram + ( left-map-span-diagram 𝒮 s)) + (vertical-inv-equiv-coherence-square-maps + ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) + ( equiv-right-family-equifibered-dependent-span-diagram P s) + ( equiv-right-family-equifibered-dependent-span-diagram Q s) + ( right-map-equiv-equifibered-dependent-span-diagram + ( right-map-span-diagram 𝒮 s)) + ( coherence-right-equiv-equifibered-dependent-span-diagram s)) + ( coherence-left-equiv-equifibered-dependent-span-diagram s) +``` + +### The identity equivalence of descent data for pushouts + +```text +module _ + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + where + + id-equiv-descent-data-pushout : equiv-descent-data-pushout P P + pr1 id-equiv-descent-data-pushout a = id-equiv + pr1 (pr2 id-equiv-descent-data-pushout) b = id-equiv + pr2 (pr2 id-equiv-descent-data-pushout) s = refl-htpy +``` + +### Inverses of equivalences of descent data for pushouts + +Taking an inverse of an equivalence `(eA, eB, eS)` of descent data amounts to +taking the inverses of the fiberwise maps + +```text + a : A ⊢ eA(a)⁻¹ : QA a ≃ PA a + b : B ⊢ eB(b)⁻¹ : QB b ≃ PB b +``` + +and mirroring the coherence squares vertically to get + +```text + eA(a)⁻¹ + QA(fs) --------> PA(fs) + | | + QS s | | PS s + | | + ∨ ∨ + QB(gs) --------> PB(gs). + eB(a)⁻¹ +``` + +```text +module _ + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) + where + + inv-equiv-descent-data-pushout : + equiv-descent-data-pushout P Q → equiv-descent-data-pushout Q P + pr1 (inv-equiv-descent-data-pushout e) a = + inv-equiv (left-equiv-equiv-descent-data-pushout P Q e a) + pr1 (pr2 (inv-equiv-descent-data-pushout e)) b = + inv-equiv (right-equiv-equiv-descent-data-pushout P Q e b) + pr2 (pr2 (inv-equiv-descent-data-pushout e)) s = + horizontal-inv-equiv-coherence-square-maps + ( left-equiv-equiv-descent-data-pushout P Q e (left-map-span-diagram 𝒮 s)) + ( map-family-descent-data-pushout P s) + ( map-family-descent-data-pushout Q s) + ( right-equiv-equiv-descent-data-pushout P Q e + ( right-map-span-diagram 𝒮 s)) + ( coherence-equiv-descent-data-pushout P Q e s) +``` + +### Homotopies of equivalences of descent data for pushouts + +```text +module _ + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + (Q : descent-data-pushout 𝒮 l6 l7) + where + + htpy-equiv-descent-data-pushout : + (e f : equiv-descent-data-pushout P Q) → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) + htpy-equiv-descent-data-pushout e f = + htpy-hom-descent-data-pushout P Q + ( hom-equiv-descent-data-pushout P Q e) + ( hom-equiv-descent-data-pushout P Q f) +``` + +## Properties + +### Characterization of identity types of descent data for pushouts + +```text +module _ + {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : descent-data-pushout 𝒮 l4 l5) + where + + equiv-eq-descent-data-pushout : + (Q : descent-data-pushout 𝒮 l4 l5) → + P ＝ Q → equiv-descent-data-pushout P Q + equiv-eq-descent-data-pushout .P refl = id-equiv-descent-data-pushout P + + abstract + is-torsorial-equiv-descent-data-pushout : + is-torsorial (equiv-descent-data-pushout {l6 = l4} {l7 = l5} P) + is-torsorial-equiv-descent-data-pushout = + is-torsorial-Eq-structure + ( is-torsorial-Eq-Π + ( λ a → is-torsorial-equiv (left-family-descent-data-pushout P a))) + ( left-family-descent-data-pushout P , λ a → id-equiv) + ( is-torsorial-Eq-structure + ( is-torsorial-Eq-Π + ( λ b → is-torsorial-equiv (right-family-descent-data-pushout P b))) + ( right-family-descent-data-pushout P , λ b → id-equiv) + ( is-torsorial-Eq-Π + ( λ s → + is-torsorial-htpy-equiv (equiv-family-descent-data-pushout P s)))) + + is-equiv-equiv-eq-descent-data-pushout : + (Q : descent-data-pushout 𝒮 l4 l5) → + is-equiv (equiv-eq-descent-data-pushout Q) + is-equiv-equiv-eq-descent-data-pushout = + fundamental-theorem-id + ( is-torsorial-equiv-descent-data-pushout) + ( equiv-eq-descent-data-pushout) + + extensionality-descent-data-pushout : + (Q : descent-data-pushout 𝒮 l4 l5) → + (P ＝ Q) ≃ equiv-descent-data-pushout P Q + pr1 (extensionality-descent-data-pushout Q) = + equiv-eq-descent-data-pushout Q + pr2 (extensionality-descent-data-pushout Q) = + is-equiv-equiv-eq-descent-data-pushout Q + + eq-equiv-descent-data-pushout : + (Q : descent-data-pushout 𝒮 l4 l5) → + equiv-descent-data-pushout P Q → P ＝ Q + eq-equiv-descent-data-pushout Q = + map-inv-equiv (extensionality-descent-data-pushout Q) +``` + +### Characterization of identity types of equivalences of descent data of pushouts + +```text +module _ + {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} + {P : descent-data-pushout 𝒮 l4 l5} + {Q : descent-data-pushout 𝒮 l6 l7} + (e : equiv-descent-data-pushout P Q) + where + + htpy-eq-equiv-descent-data-pushout : + (f : equiv-descent-data-pushout P Q) → + (e ＝ f) → htpy-equiv-descent-data-pushout P Q e f + htpy-eq-equiv-descent-data-pushout .e refl = + refl-htpy-hom-descent-data-pushout P Q + ( hom-equiv-descent-data-pushout P Q e) + + abstract + is-torsorial-htpy-equiv-descent-data-pushout : + is-torsorial (htpy-equiv-descent-data-pushout P Q e) + is-torsorial-htpy-equiv-descent-data-pushout = + is-torsorial-Eq-structure + ( is-torsorial-Eq-Π + ( λ a → + is-torsorial-htpy-equiv + ( left-equiv-equiv-descent-data-pushout P Q e a))) + ( left-equiv-equiv-descent-data-pushout P Q e , λ a → refl-htpy) + ( is-torsorial-Eq-structure + ( is-torsorial-Eq-Π + ( λ b → + is-torsorial-htpy-equiv + ( right-equiv-equiv-descent-data-pushout P Q e b))) + ( right-equiv-equiv-descent-data-pushout P Q e , λ b → refl-htpy) + ( is-torsorial-Eq-Π + ( λ s → + is-torsorial-htpy + ( coherence-equiv-descent-data-pushout P Q e s ∙h refl-htpy)))) + + is-equiv-htpy-eq-equiv-descent-data-pushout : + (f : equiv-descent-data-pushout P Q) → + is-equiv (htpy-eq-equiv-descent-data-pushout f) + is-equiv-htpy-eq-equiv-descent-data-pushout = + fundamental-theorem-id + ( is-torsorial-htpy-equiv-descent-data-pushout) + ( htpy-eq-equiv-descent-data-pushout) + + extensionality-equiv-descent-data-pushout : + (f : equiv-descent-data-pushout P Q) → + (e ＝ f) ≃ + htpy-hom-descent-data-pushout P Q + ( hom-equiv-descent-data-pushout P Q e) + ( hom-equiv-descent-data-pushout P Q f) + pr1 (extensionality-equiv-descent-data-pushout f) = + htpy-eq-equiv-descent-data-pushout f + pr2 (extensionality-equiv-descent-data-pushout f) = + is-equiv-htpy-eq-equiv-descent-data-pushout f +``` From 733ad013a76e6f37fd9b766c691060beabe85921 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 16:42:39 +0000 Subject: [PATCH 04/10] fix projections flattening lemma descent data pushouts --- .../descent-data-pushouts.lagda.md | 7 + .../flattening-lemma-pushouts.lagda.md | 131 ++++++++++++++---- 2 files changed, 109 insertions(+), 29 deletions(-) diff --git a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md index 23adaf8249..4bbca60c1e 100644 --- a/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/descent-data-pushouts.lagda.md @@ -107,6 +107,13 @@ module _ map-family-descent-data-pushout s = map-equiv (equiv-family-descent-data-pushout s) + map-inv-family-descent-data-pushout : + (s : spanning-type-span-diagram 𝒮) → + right-family-descent-data-pushout (right-map-span-diagram 𝒮 s) → + left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) + map-inv-family-descent-data-pushout s = + map-inv-equiv (equiv-family-descent-data-pushout s) + is-equiv-map-family-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → is-equiv (map-family-descent-data-pushout s) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index 829dc84267..fca45c2d96 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -29,7 +29,9 @@ open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-cocones-under-spans open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.descent-data-pushouts +open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams open import synthetic-homotopy-theory.equivalences-descent-data-pushouts +open import synthetic-homotopy-theory.equivalences-equifibered-dependent-span-diagrams open import synthetic-homotopy-theory.universal-property-pushouts ``` @@ -37,10 +39,11 @@ open import synthetic-homotopy-theory.universal-property-pushouts ## Idea -The **flattening lemma** for [pushouts](synthetic-homotopy-theory.pushouts.md) -states that pushouts commute with -[dependent pair types](foundation.dependent-pair-types.md). More precisely, -given a pushout square +The +{{#concept "flattening lemma" Disambiguation="for pushouts" Agda=flattening-lemma-pushout Agda=flattening-lemma-descent-data-pushout}} +for [pushouts](synthetic-homotopy-theory.pushouts.md) states that pushouts +commute with [dependent pair types](foundation.dependent-pair-types.md). More +precisely, given a pushout square ```text g @@ -160,22 +163,22 @@ module _ vertical-map-span-flattening-descent-data-pushout : Σ ( spanning-type-span-diagram 𝒮) - ( λ s → pr1 P (left-map-span-diagram 𝒮 s)) → - Σ ( domain-span-diagram 𝒮) (pr1 P) + ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) → + Σ ( domain-span-diagram 𝒮) (left-family-descent-data-pushout P) vertical-map-span-flattening-descent-data-pushout = map-Σ-map-base ( left-map-span-diagram 𝒮) - ( pr1 P) + ( left-family-descent-data-pushout P) horizontal-map-span-flattening-descent-data-pushout : Σ ( spanning-type-span-diagram 𝒮) - ( λ s → pr1 P (left-map-span-diagram 𝒮 s)) → - Σ ( codomain-span-diagram 𝒮) (pr1 (pr2 P)) + ( left-family-descent-data-pushout P ∘ left-map-span-diagram 𝒮) → + Σ ( codomain-span-diagram 𝒮) (right-family-descent-data-pushout P) horizontal-map-span-flattening-descent-data-pushout = map-Σ - ( pr1 (pr2 P)) + ( right-family-descent-data-pushout P) ( right-map-span-diagram 𝒮) - ( λ s → map-equiv (pr2 (pr2 P) s)) + ( map-family-descent-data-pushout P) span-diagram-flattening-descent-data-pushout : span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l4) @@ -195,18 +198,24 @@ module _ where horizontal-map-cocone-flattening-descent-data-pushout : - Σ A (pr1 P) → Σ X Q + Σ A (left-family-descent-data-pushout P) → Σ X Q horizontal-map-cocone-flattening-descent-data-pushout = map-Σ Q ( horizontal-map-cocone f g c) - ( λ a → map-equiv (pr1 e a)) + ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) vertical-map-cocone-flattening-descent-data-pushout : - Σ B (pr1 (pr2 P)) → Σ X Q + Σ B (right-family-descent-data-pushout P) → Σ X Q vertical-map-cocone-flattening-descent-data-pushout = map-Σ Q ( vertical-map-cocone f g c) - ( λ b → map-equiv (pr1 (pr2 e) b)) + ( right-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) coherence-square-cocone-flattening-descent-data-pushout : coherence-square-maps @@ -217,8 +226,16 @@ module _ coherence-square-cocone-flattening-descent-data-pushout = htpy-map-Σ Q ( coherence-square-cocone f g c) - ( λ s → map-equiv (pr1 e (f s))) - ( λ s → inv-htpy (pr2 (pr2 e) s)) + ( ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) ∘ + ( f)) + ( inv-htpy ∘ + coherence-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) cocone-flattening-descent-data-pushout : cocone @@ -374,9 +391,22 @@ module _ ( horizontal-map-span-flattening-descent-data-pushout P) ( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e) ( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e) - ( tot (λ s → map-equiv (pr1 e (f s)))) - ( tot (λ a → map-equiv (pr1 e a))) - ( tot (λ b → map-equiv (pr1 (pr2 e) b))) + ( tot + ( ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) ∘ + ( f))) + ( tot + ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) + ( tot + ( right-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) ( id) ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e) ( refl-htpy) @@ -384,8 +414,17 @@ module _ ( Q ∘ vertical-map-cocone f g c) ( refl-htpy) ( λ s → - tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s)))) - ( λ s → inv-htpy (pr2 (pr2 e) s))) + ( tr Q (coherence-square-cocone f g c s)) ∘ + ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e) + ( f s))) + ( inv-htpy ∘ + coherence-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) ( refl-htpy) ( refl-htpy) ( coherence-square-cocone-flattening-pushout Q f g c) @@ -395,7 +434,13 @@ module _ ( s , t))) ∙ ( triangle-eq-pair-Σ Q ( coherence-square-cocone f g c s) - ( inv (pr2 (pr2 e) s t))) ∙ + ( inv + ( coherence-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e) + ( s) + ( t)))) ∙ ( ap ( eq-pair-Σ (coherence-square-cocone f g c s) refl ∙_) ( inv @@ -404,7 +449,13 @@ module _ ( vertical-map-cocone f g c) ( Q) ( refl) - ( inv (pr2 (pr2 e) s t)))))) + ( inv + ( coherence-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e) + ( s) + ( t))))))) abstract flattening-lemma-descent-data-pushout : @@ -419,9 +470,22 @@ module _ ( horizontal-map-span-flattening-descent-data-pushout P) ( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e) ( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e) - ( equiv-tot (pr1 e ∘ f)) - ( equiv-tot (pr1 e)) - ( equiv-tot (pr1 (pr2 e))) + ( equiv-tot + ( ( left-equiv-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e)) ∘ + ( f))) + ( equiv-tot + ( left-equiv-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) + ( equiv-tot + ( right-equiv-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) ( id-equiv) ( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e) ( refl-htpy) @@ -429,8 +493,17 @@ module _ ( Q ∘ vertical-map-cocone f g c) ( refl-htpy) ( λ s → - tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s)))) - ( λ s → inv-htpy (pr2 (pr2 e) s))) + ( tr Q (coherence-square-cocone f g c s)) ∘ + ( left-map-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e) + ( f s))) + ( inv-htpy ∘ + coherence-equiv-descent-data-pushout + ( P) + ( descent-data-family-cocone-span-diagram c Q) + ( e))) ( refl-htpy) ( refl-htpy) ( coherence-square-cocone-flattening-pushout Q f g c) From d52634d26ac494029f74097fda11588cd32e33e7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 16:54:58 +0000 Subject: [PATCH 05/10] pre-commit --- ...quivalences-equifibered-dependent-span-diagrams.lagda.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md index 9ae980287b..de6c9e4882 100644 --- a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md @@ -157,7 +157,8 @@ module _ (b : codomain-span-diagram 𝒮) → is-equiv (right-map-equiv-equifibered-dependent-span-diagram b) is-equiv-right-map-equiv-equifibered-dependent-span-diagram b = - is-equiv-map-equiv (right-equiv-equiv-equifibered-dependent-span-diagram b) + is-equiv-map-equiv + ( right-equiv-equiv-equifibered-dependent-span-diagram b) inv-right-map-equiv-equifibered-dependent-span-diagram : (b : codomain-span-diagram 𝒮) → @@ -192,7 +193,8 @@ module _ spanning-type-family-equifibered-dependent-span-diagram Q b → spanning-type-family-equifibered-dependent-span-diagram P b inv-spanning-type-map-equiv-equifibered-dependent-span-diagram b = - map-inv-equiv (spanning-type-equiv-equiv-equifibered-dependent-span-diagram b) + map-inv-equiv + ( spanning-type-equiv-equiv-equifibered-dependent-span-diagram b) coherence-left-equiv-equifibered-dependent-span-diagram : (s : spanning-type-span-diagram 𝒮) → From 79a0f3dce65c5ccf7af25350a93b9a7ed135aaf4 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 17:00:08 +0000 Subject: [PATCH 06/10] remove overlap with #1361 --- src/orthogonal-factorization-systems.lagda.md | 2 - .../anodyne-maps.lagda.md | 172 ------------ .../maps-local-at-maps.lagda.md | 13 - .../orthogonal-maps.lagda.md | 259 ++---------------- .../weakly-anodyne-maps.lagda.md | 89 ------ .../cocartesian-morphisms-arrows.lagda.md | 44 --- 6 files changed, 19 insertions(+), 560 deletions(-) delete mode 100644 src/orthogonal-factorization-systems/anodyne-maps.lagda.md delete mode 100644 src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md diff --git a/src/orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems.lagda.md index e2a8bf7286..a167d57d4a 100644 --- a/src/orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems.lagda.md @@ -9,7 +9,6 @@ ```agda module orthogonal-factorization-systems where -open import orthogonal-factorization-systems.anodyne-maps public open import orthogonal-factorization-systems.cd-structures public open import orthogonal-factorization-systems.cellular-maps public open import orthogonal-factorization-systems.closed-modalities public @@ -72,7 +71,6 @@ open import orthogonal-factorization-systems.types-local-at-maps public open import orthogonal-factorization-systems.types-separated-at-maps public open import orthogonal-factorization-systems.uniquely-eliminating-modalities public open import orthogonal-factorization-systems.universal-property-localizations-at-global-subuniverses public -open import orthogonal-factorization-systems.weakly-anodyne-maps public open import orthogonal-factorization-systems.wide-function-classes public open import orthogonal-factorization-systems.wide-global-function-classes public open import orthogonal-factorization-systems.zero-modality public diff --git a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/anodyne-maps.lagda.md deleted file mode 100644 index 9a53d0201b..0000000000 --- a/src/orthogonal-factorization-systems/anodyne-maps.lagda.md +++ /dev/null @@ -1,172 +0,0 @@ -# Anodyne maps - -```agda -module orthogonal-factorization-systems.anodyne-maps where -``` - -
Imports - -```agda -open import foundation.equivalences-arrows -open import foundation.function-types -open import foundation.functoriality-cartesian-product-types -open import foundation.functoriality-coproduct-types -open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.universe-levels - -open import orthogonal-factorization-systems.orthogonal-maps - -open import synthetic-homotopy-theory.cocartesian-morphisms-arrows -``` - -
- -## Idea - -A map $j : C → D$ is said to be -{{#concept "anodyne" Disambiguation="map of types" Agda=is-anodyne}} with -respect to a map $f : A → B$, or **$f$-anodyne**, if every map that is -orthogonal to $f$ is also orthogonal to $j$. - -## Definitions - -### The predicate of being anodyne with respect to a map - -```agda -module _ - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} - (f : A → B) (j : C → D) - where - - is-anodyne-Level : - (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6) - is-anodyne-Level l5 l6 = - {X : UU l5} {Y : UU l6} (g : X → Y) → is-orthogonal f g → is-orthogonal j g - - is-anodyne : UUω - is-anodyne = {l5 l6 : Level} → is-anodyne-Level l5 l6 -``` - -## Properties - -### Anodyne maps are closed under homotopies - -```agda -module _ - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} - (f : A → B) {j i : C → D} - where - - is-anodyne-htpy : j ~ i → is-anodyne f j → is-anodyne f i - is-anodyne-htpy K J g H = is-orthogonal-htpy-left j g K (J g H) -``` - -### Anodyne maps are closed under equivalences of maps - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6} - (f : A → B) {j : C → D} {j' : C' → D'} - where - - is-anodyne-equiv-arrow : equiv-arrow j j' → is-anodyne f j → is-anodyne f j' - is-anodyne-equiv-arrow α J g H = is-orthogonal-left-equiv-arrow α g (J g H) -``` - -### Anodyne maps are closed under retracts of maps - -> This remains to be formalized. - -### Anodyne maps compose - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} - (f : A → B) (j : C → D) (i : D → E) - where - - is-anodyne-comp : is-anodyne f j → is-anodyne f i → is-anodyne f (i ∘ j) - is-anodyne-comp J I g H = is-orthogonal-left-comp j i g (J g H) (I g H) -``` - -### Cancellation property for anodyne maps - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} - (f : A → B) (j : C → D) (i : D → E) - where - - is-anodyne-left-factor : - is-anodyne f j → is-anodyne f (i ∘ j) → is-anodyne f i - is-anodyne-left-factor J IJ g H = - is-orthogonal-left-left-factor j i g (J g H) (IJ g H) -``` - -### Anodyne maps are closed under dependent sums - -```agda -module _ - {l1 l2 l3 l4 l5 : Level} - {A : UU l1} {B : UU l2} {I : UU l3} {C : I → UU l4} {D : I → UU l5} - (f : A → B) (j : (i : I) → C i → D i) - where - - is-anodyne-tot : ((i : I) → is-anodyne f (j i)) → is-anodyne f (tot j) - is-anodyne-tot J g H = is-orthogonal-left-tot j g (λ i → J i g H) -``` - -### Anodyne maps are closed under products - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} - (f : A → B) (j : C → D) (i : E → F) - where - - is-anodyne-map-product : - is-anodyne f j → is-anodyne f i → is-anodyne f (map-product j i) - is-anodyne-map-product J I g H = - is-orthogonal-left-product j i g (J g H) (I g H) -``` - -### Anodyne maps are closed under coproducts - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} - (f : A → B) (j : C → D) (i : E → F) - where - - is-anodyne-map-coproduct : - is-anodyne f j → is-anodyne f i → is-anodyne f (map-coproduct j i) - is-anodyne-map-coproduct J I g H = - is-orthogonal-left-coproduct j i g (J g H) (I g H) -``` - -### Anodyne maps are closed under cobase change - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} - (f : A → B) (j : C → D) (i : E → F) - where - - is-anodyne-cobase-change : - cocartesian-hom-arrow j i → is-anodyne f j → is-anodyne f i - is-anodyne-cobase-change α J g H = - is-orthogonal-left-cobase-change j i g α (J g H) -``` - -### Anodyne maps are closed under pushout-products - -> This remains to be formalized. diff --git a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md index 921e0c45d7..ac69503101 100644 --- a/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md +++ b/src/orthogonal-factorization-systems/maps-local-at-maps.lagda.md @@ -147,19 +147,6 @@ module _ ( G (map-codomain-inclusion-retract-map g' g R d)) ``` -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {E : UU l5} {F : UU l6} - {f : A → B} {g : C → D} {f' : E → F} - where - - is-local-retract-map' : - is-local-map f g → f' retract-of-map f → is-local-map f' g - is-local-retract-map' F R d = - is-local-retract-map-is-local f' f R (fiber g d) (F d) -``` - ## See also - [Localizations with respect to maps](orthogonal-factorization-systems.localizations-at-maps.md) diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index 8a3d9bdcfe..ec37ad84de 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -29,7 +29,6 @@ open import foundation.functoriality-coproduct-types open import foundation.functoriality-dependent-pair-types open import foundation.functoriality-fibers-of-maps open import foundation.homotopies -open import foundation.identity-types open import foundation.morphisms-arrows open import foundation.postcomposition-functions open import foundation.postcomposition-pullbacks @@ -38,7 +37,6 @@ open import foundation.precomposition-functions open import foundation.products-pullbacks open import foundation.propositions open import foundation.pullbacks -open import foundation.type-arithmetic-cartesian-product-types open import foundation.type-arithmetic-dependent-function-types open import foundation.type-theoretic-principle-of-choice open import foundation.unit-type @@ -53,10 +51,6 @@ open import foundation.whiskering-homotopies-composition open import orthogonal-factorization-systems.lifting-structures-on-squares open import orthogonal-factorization-systems.pullback-hom open import orthogonal-factorization-systems.types-local-at-maps - -open import synthetic-homotopy-theory.cocartesian-morphisms-arrows -open import synthetic-homotopy-theory.pullback-property-pushouts -open import synthetic-homotopy-theory.pushouts ```
@@ -432,40 +426,19 @@ module _ ( ( commutative-htpy-postcomp-htpy-precomp F G) ∙h ( inv-htpy-right-unit-htpy))) - abstract - is-orthogonal-pullback-condition-htpy-left : - {f' : A → B} → f ~ f' → - is-orthogonal-pullback-condition f g → - is-orthogonal-pullback-condition f' g - is-orthogonal-pullback-condition-htpy-left F = - is-orthogonal-pullback-condition-htpy F refl-htpy - - abstract - is-orthogonal-pullback-condition-htpy-right : - {g' : X → Y} → g ~ g' → - is-orthogonal-pullback-condition f g → - is-orthogonal-pullback-condition f g' - is-orthogonal-pullback-condition-htpy-right = - is-orthogonal-pullback-condition-htpy refl-htpy - - abstract - is-orthogonal-htpy : - {f' : A → B} {g' : X → Y} → f ~ f' → g ~ g' → - is-orthogonal f g → is-orthogonal f' g' - is-orthogonal-htpy {f'} {g'} F G H = - is-orthogonal-is-orthogonal-pullback-condition f' g' - ( is-orthogonal-pullback-condition-htpy F G - ( is-orthogonal-pullback-condition-is-orthogonal f g H)) - - abstract - is-orthogonal-htpy-left : - {f' : A → B} → f ~ f' → is-orthogonal f g → is-orthogonal f' g - is-orthogonal-htpy-left F = is-orthogonal-htpy F refl-htpy - - abstract - is-orthogonal-htpy-right : - {g' : X → Y} → g ~ g' → is-orthogonal f g → is-orthogonal f g' - is-orthogonal-htpy-right = is-orthogonal-htpy refl-htpy + is-orthogonal-pullback-condition-htpy-left : + {f' : A → B} → f ~ f' → + is-orthogonal-pullback-condition f g → + is-orthogonal-pullback-condition f' g + is-orthogonal-pullback-condition-htpy-left F = + is-orthogonal-pullback-condition-htpy F refl-htpy + + is-orthogonal-pullback-condition-htpy-right : + {g' : X → Y} → g ~ g' → + is-orthogonal-pullback-condition f g → + is-orthogonal-pullback-condition f g' + is-orthogonal-pullback-condition-htpy-right = + is-orthogonal-pullback-condition-htpy refl-htpy ``` ### Equivalences are orthogonal to every map @@ -725,70 +698,6 @@ module _ ( is-orthogonal-pullback-condition-is-orthogonal (h ∘ f) g HF)) ``` -### Orthogonality is preserved by equivalences of maps - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6} - {f : A → B} {f' : A' → B'} - where - - abstract - is-orthogonal-left-equiv-arrow : - equiv-arrow f f' → (g : X → Y) → is-orthogonal f g → is-orthogonal f' g - is-orthogonal-left-equiv-arrow α g F = - is-orthogonal-htpy-left - ( map-codomain-equiv-arrow f f' α ∘ - f ∘ - map-inv-domain-equiv-arrow f f' α) - ( g) - ( ( coh-equiv-arrow f f' α ·r map-inv-domain-equiv-arrow f f' α) ∙h - ( f' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow f f' α))) - ( is-orthogonal-left-comp - ( f ∘ map-inv-domain-equiv-arrow f f' α) - ( map-codomain-equiv-arrow f f' α) - ( g) - ( is-orthogonal-left-comp - ( map-inv-domain-equiv-arrow f f' α) - ( f) - ( g) - ( is-orthogonal-equiv-left (equiv-domain-inv-equiv-arrow f f' α) g) - ( F)) - ( is-orthogonal-equiv-left (equiv-codomain-equiv-arrow f f' α) g)) - -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {X' : UU l5} {Y' : UU l6} - (f : A → B) {g : X → Y} {g' : X' → Y'} - where - - abstract - is-orthogonal-right-equiv-arrow : - equiv-arrow g g' → is-orthogonal f g → is-orthogonal f g' - is-orthogonal-right-equiv-arrow α G = - is-orthogonal-htpy-right - ( f) - ( map-codomain-equiv-arrow g g' α ∘ - g ∘ - map-inv-domain-equiv-arrow g g' α) - ( ( coh-equiv-arrow g g' α ·r map-inv-domain-equiv-arrow g g' α) ∙h - ( g' ·l is-section-map-inv-equiv (equiv-domain-equiv-arrow g g' α))) - ( is-orthogonal-right-comp - ( f) - ( g ∘ map-inv-domain-equiv-arrow g g' α) - ( map-codomain-equiv-arrow g g' α) - ( is-orthogonal-equiv-right f (equiv-codomain-equiv-arrow g g' α)) - ( is-orthogonal-right-comp - ( f) - ( map-inv-domain-equiv-arrow g g' α) - ( g) - ( G) - ( is-orthogonal-equiv-right - ( f) - ( equiv-domain-inv-equiv-arrow g g' α)))) -``` - ### Right orthogonality is preserved by dependent products If `f ⊥ gᵢ`, for each `i : I`, then `f ⊥ (map-Π g)`. @@ -1003,10 +912,10 @@ module _ (f : (i : I) → A i → B i) (g : X → Y) where - is-orthogonal-pullback-condition-left-tot : + is-orthogonal-pullback-condition-left-Σ : ((i : I) → is-orthogonal-pullback-condition (f i) g) → is-orthogonal-pullback-condition (tot f) g - is-orthogonal-pullback-condition-left-tot F = + is-orthogonal-pullback-condition-left-Σ F = is-pullback-top-is-pullback-bottom-cube-is-equiv ( map-Π (λ i → postcomp (B i) g)) ( map-Π (λ i → precomp (f i) X)) @@ -1042,56 +951,14 @@ module _ ( λ i → cone-pullback-hom (f i) g) ( F)) - is-orthogonal-left-tot : + is-orthogonal-left-Σ : ((i : I) → is-orthogonal (f i) g) → is-orthogonal (tot f) g - is-orthogonal-left-tot F = + is-orthogonal-left-Σ F = is-orthogonal-is-orthogonal-pullback-condition (tot f) g - ( is-orthogonal-pullback-condition-left-tot + ( is-orthogonal-pullback-condition-left-Σ ( λ i → is-orthogonal-pullback-condition-is-orthogonal (f i) g (F i))) ``` -### Left orthogonality is preserved by products - -If `f ⊥ g` and `f' ⊥ g`, then `(f × f') ⊥ g`. - -```agda -module _ - {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) - where - - is-orthogonal-left-map-right-product : - {l5 : Level} (C : UU l5) → - is-orthogonal f g → is-orthogonal (map-product (id' C) f) g - is-orthogonal-left-map-right-product C F = - is-orthogonal-left-tot (λ _ → f) g (λ _ → F) - - is-orthogonal-left-map-left-product : - {l5 : Level} (C : UU l5) → - is-orthogonal f g → is-orthogonal (map-product f (id' C)) g - is-orthogonal-left-map-left-product C F = - is-orthogonal-left-equiv-arrow - ( commutative-product , commutative-product , refl-htpy) - ( g) - ( is-orthogonal-left-map-right-product C F) - -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {A' : UU l3} {B' : UU l4} {X : UU l5} {Y : UU l6} - (f : A → B) (f' : A' → B') (g : X → Y) - where - - is-orthogonal-left-product : - is-orthogonal f g → is-orthogonal f' g → is-orthogonal (map-product f f') g - is-orthogonal-left-product F F' = - is-orthogonal-left-comp - ( map-product f id) - ( map-product id f') - ( g) - ( is-orthogonal-left-map-left-product f g A' F) - ( is-orthogonal-left-map-right-product f' g B F') -``` - ### Left orthogonality is preserved by coproducts If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`. @@ -1099,7 +966,7 @@ If `f ⊥ g` and `f' ⊥ g`, then `(f + f') ⊥ g`. **Proof:** We need to show that the square ```text - - ∘ (f + f') + - ∘ (f + f') ((B + B') → X) ---------------> ((A + A') → X) | | | | @@ -1247,94 +1114,6 @@ module _ ( is-orthogonal-pullback-condition-is-orthogonal f g G)) ``` -### Left orthogonality is preserved under cobase change - -Given a pushout square - -```text - A ------> A' - | | - f'| | f' - ∨ ⌜ ∨ - B ------> B', -``` - -if `f ⊥ g`, then `f' ⊥ g`. - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {A' : UU l5} {B' : UU l6} - (f : A → B) (f' : A' → B') (g : X → Y) (α : cocartesian-hom-arrow f f') - where - - abstract - is-orthogonal-pullback-condition-left-cobase-change : - is-orthogonal-pullback-condition f g → - is-orthogonal-pullback-condition f' g - is-orthogonal-pullback-condition-left-cobase-change F = - is-pullback-swap-cone - ( postcomp A' g) - ( precomp f' Y) - ( precomp f' X , postcomp B' g , refl-htpy) - ( is-pullback-back-left-is-pullback-back-right-cube - ( refl-htpy) - ( refl-htpy) - ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) X)) - ( inv-htpy (htpy-precomp (coh-cocartesian-hom-arrow f f' α) Y)) - ( refl-htpy) - ( refl-htpy) - ( right-unit-htpy ∙h - ( inv ·l - commutative-postcomp-htpy-precomp g - ( coh-cocartesian-hom-arrow f f' α)) ∙h - ( inv-htpy - ( left-whisker-inv-htpy - ( postcomp A g) - ( htpy-precomp (coh-cocartesian-hom-arrow f f' α) X))) ∙h - ( inv-htpy-right-unit-htpy)) - ( is-pullback-swap-cone - ( precomp f Y) - ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y) - ( cone-hom-arrow - ( precomp (map-codomain-cocartesian-hom-arrow f f' α) Y) - ( precomp (map-domain-cocartesian-hom-arrow f f' α) Y) - ( transpose-precomp-hom-arrow f f' - ( hom-arrow-cocartesian-hom-arrow f f' α) - ( Y))) - ( pullback-property-pushout-is-pushout - ( f) - ( map-domain-cocartesian-hom-arrow f f' α) - ( cocone-cocartesian-hom-arrow f f' α) - ( is-cocartesian-cocartesian-hom-arrow f f' α) - ( Y))) - ( is-pullback-swap-cone - ( precomp f Y) - ( postcomp A g) - ( cone-pullback-hom f g) - ( F)) - ( is-pullback-swap-cone - ( precomp f X) - ( precomp (map-domain-cocartesian-hom-arrow f f' α) X) - ( cone-hom-arrow - ( precomp (map-codomain-cocartesian-hom-arrow f f' α) X) - ( precomp (map-domain-cocartesian-hom-arrow f f' α) X) - ( transpose-precomp-hom-arrow f f' - ( hom-arrow-cocartesian-hom-arrow f f' α) - ( X))) - ( pullback-property-pushout-is-pushout f - ( map-domain-cocartesian-hom-arrow f f' α) - ( cocone-cocartesian-hom-arrow f f' α) - ( is-cocartesian-cocartesian-hom-arrow f f' α) X))) - - is-orthogonal-left-cobase-change : - is-orthogonal f g → is-orthogonal f' g - is-orthogonal-left-cobase-change F = - is-orthogonal-is-orthogonal-pullback-condition f' g - ( is-orthogonal-pullback-condition-left-cobase-change - ( is-orthogonal-pullback-condition-is-orthogonal f g F)) -``` - ### A type is `f`-local if and only if its terminal map is `f`-orthogonal **Proof (forward direction):** If the terminal map is right orthogonal to `f`, diff --git a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md b/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md deleted file mode 100644 index c057f9195d..0000000000 --- a/src/orthogonal-factorization-systems/weakly-anodyne-maps.lagda.md +++ /dev/null @@ -1,89 +0,0 @@ -# Weakly anodyne maps - -```agda -module orthogonal-factorization-systems.weakly-anodyne-maps where -``` - -
Imports - -```agda -open import foundation.equivalences-arrows -open import foundation.fibers-of-maps -open import foundation.function-types -open import foundation.functoriality-cartesian-product-types -open import foundation.functoriality-coproduct-types -open import foundation.functoriality-dependent-pair-types -open import foundation.homotopies -open import foundation.retracts-of-maps -open import foundation.unit-type -open import foundation.universe-levels - -open import orthogonal-factorization-systems.anodyne-maps -open import orthogonal-factorization-systems.maps-local-at-maps -open import orthogonal-factorization-systems.orthogonal-maps -open import orthogonal-factorization-systems.types-local-at-maps - -open import synthetic-homotopy-theory.cocartesian-morphisms-arrows -``` - -
- -## Idea - -A map $j : C → D$ is said to be -{{#concept "weakly anodyne" Disambiguation="map of types" Agda=is-weakly-anodyne}} -with respect to a map $f : A → B$, or **weakly $f$-anodyne**, if every map that -is local at $f$ is also local at $j$. - -## Definitions - -### The predicate of being weakly anodyne with respect to a map - -```agda -module _ - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} - (f : A → B) (j : C → D) - where - - is-weakly-anodyne-Level : - (l5 l6 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5 ⊔ lsuc l6) - is-weakly-anodyne-Level l5 l6 = - {X : UU l5} {Y : UU l6} (g : X → Y) → is-local-map f g → is-local-map j g - - is-weakly-anodyne : UUω - is-weakly-anodyne = {l5 l6 : Level} → is-weakly-anodyne-Level l5 l6 -``` - -## Properties - -### Anodyne maps are weakly anodyne - -```agda -module _ - {l1 l2 l3 l4 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} - (f : A → B) {j : C → D} - where - - is-weakly-anodyne-is-anodyne : is-anodyne f j → is-weakly-anodyne f j - is-weakly-anodyne-is-anodyne J g G x = - is-local-is-orthogonal-terminal-map j - ( J ( terminal-map (fiber g x)) - ( is-orthogonal-terminal-map-is-local f (G x))) -``` - -### Weakly anodyne maps are closed under retracts of maps - -```agda -module _ - {l1 l2 l3 l4 l5 l6 : Level} - {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} {C' : UU l5} {D' : UU l6} - (f : A → B) {j : C → D} {j' : C' → D'} - where - - is-weakly-anodyne-retract-map : - retract-map j j' → is-weakly-anodyne f j → is-weakly-anodyne f j' - is-weakly-anodyne-retract-map α J g G x = - is-local-retract-map-is-local j' j α (fiber g x) (J g G x) -``` diff --git a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md index e1188a0d13..9e34713e9c 100644 --- a/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md +++ b/src/synthetic-homotopy-theory/cocartesian-morphisms-arrows.lagda.md @@ -7,17 +7,13 @@ module synthetic-homotopy-theory.cocartesian-morphisms-arrows where
Imports ```agda -open import foundation.cartesian-morphisms-arrows open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.morphisms-arrows -open import foundation.precomposition-functions open import foundation.propositions -open import foundation.pullbacks open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans -open import synthetic-homotopy-theory.pullback-property-pushouts open import synthetic-homotopy-theory.pushouts open import synthetic-homotopy-theory.universal-property-pushouts ``` @@ -125,46 +121,6 @@ module _ ( is-cocartesian-cocartesian-hom-arrow) ``` -### The cartesian morphism on precomposition maps - -```agda -module _ - {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} - (f : A → B) (g : X → Y) (α : cocartesian-hom-arrow f g) (S : UU l) - where - - precomp-cocartesian-hom-arrow : hom-arrow (precomp g S) (precomp f S) - precomp-cocartesian-hom-arrow = - precomp-hom-arrow f g (hom-arrow-cocartesian-hom-arrow f g α) S - - is-cartesian-precomp-cocartesian-hom-arrow : - is-cartesian-hom-arrow - ( precomp g S) - ( precomp f S) - ( precomp-cocartesian-hom-arrow) - is-cartesian-precomp-cocartesian-hom-arrow = - is-pullback-swap-cone - ( precomp f S) - ( precomp (map-domain-cocartesian-hom-arrow f g α) S) - ( cone-hom-arrow - ( precomp (map-codomain-cocartesian-hom-arrow f g α) S) - ( precomp (map-domain-cocartesian-hom-arrow f g α) S) - ( transpose-precomp-hom-arrow f g - ( hom-arrow-cocartesian-hom-arrow f g α) - ( S))) - ( pullback-property-pushout-is-pushout - ( f) - ( map-domain-cocartesian-hom-arrow f g α) - ( cocone-cocartesian-hom-arrow f g α) - ( is-cocartesian-cocartesian-hom-arrow f g α) S) - - precomp-cartesian-hom-arrow-cocartesian-hom-arrow : - cartesian-hom-arrow (precomp g S) (precomp f S) - precomp-cartesian-hom-arrow-cocartesian-hom-arrow = - ( precomp-cocartesian-hom-arrow , - is-cartesian-precomp-cocartesian-hom-arrow) -``` - ## See also - [Cartesian morphisms of arrows](foundation.cartesian-morphisms-arrows.md) for From 90a2a78d6231f49a133fd72475fd182a6c945130 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 17:12:27 +0000 Subject: [PATCH 07/10] `span-diagram-flattening-equifibered-dependent-span-diagram` --- .../flattening-lemma-pushouts.lagda.md | 40 ++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index fca45c2d96..aa152adfbb 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -149,7 +149,7 @@ module _ ( horizontal-map-span-flattening-pushout P _ _ c) ``` -### The statement of the flattening lemma for pushouts, phrased using descent data +### The statement of the flattening lemma for pushouts, using descent data The above statement of the flattening lemma works with a provided type family over the pushout. We can instead accept a definition of this family via descent @@ -258,6 +258,44 @@ module _ ( cocone-flattening-descent-data-pushout) ``` +### The statement of the flattening lemma for pushouts, using equifibered dependent span diagrams + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6) + where + + vertical-map-span-flattening-equifibered-dependent-span-diagram : + Σ ( spanning-type-span-diagram 𝒮) + ( spanning-type-family-equifibered-dependent-span-diagram P) → + Σ ( domain-span-diagram 𝒮) + ( left-family-equifibered-dependent-span-diagram P) + vertical-map-span-flattening-equifibered-dependent-span-diagram = + map-Σ + ( left-family-equifibered-dependent-span-diagram P) + ( left-map-span-diagram 𝒮) + ( map-left-family-equifibered-dependent-span-diagram P) + + horizontal-map-span-flattening-equifibered-dependent-span-diagram : + Σ ( spanning-type-span-diagram 𝒮) + ( spanning-type-family-equifibered-dependent-span-diagram P) → + Σ ( codomain-span-diagram 𝒮) + ( right-family-equifibered-dependent-span-diagram P) + horizontal-map-span-flattening-equifibered-dependent-span-diagram = + map-Σ + ( right-family-equifibered-dependent-span-diagram P) + ( right-map-span-diagram 𝒮) + ( map-right-family-equifibered-dependent-span-diagram P) + + span-diagram-flattening-equifibered-dependent-span-diagram : + span-diagram (l1 ⊔ l4) (l2 ⊔ l5) (l3 ⊔ l6) + span-diagram-flattening-equifibered-dependent-span-diagram = + make-span-diagram + ( vertical-map-span-flattening-equifibered-dependent-span-diagram) + ( horizontal-map-span-flattening-equifibered-dependent-span-diagram) +``` + ## Properties ### Proof of the flattening lemma for pushouts From caf1bdf32b773df7ebacd8d6bbbf95015d53607c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 18:21:12 +0000 Subject: [PATCH 08/10] cocone maps `flattening-equifibered-dependent-span-diagram` --- ...uifibered-dependent-span-diagrams.lagda.md | 238 +----------------- .../flattening-lemma-pushouts.lagda.md | 32 +++ 2 files changed, 45 insertions(+), 225 deletions(-) diff --git a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md index de6c9e4882..21c7509b9c 100644 --- a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md @@ -30,50 +30,10 @@ open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams ## Idea -Given [descent data](synthetic-homotopy-theory.descent-data-pushouts.md) for -[pushouts](synthetic-homotopy-theory.pushouts.md) `(PA, PB, PS)` and -`(QA, QB, QS)`, an -{{#concept "equivalence" Disambiguation="descent data for pushouts" Agda=equiv-descent-data-pushout}} -between them is a pair of fiberwise equivalences - -```text - eA : (a : A) → PA a ≃ QA a - eB : (b : B) → PB b ≃ QB b -``` - -equipped with a family of [homotopies](foundation-core.homotopies.md) making - -```text - eA(fs) - PA(fs) --------> QA(fs) - | | - PS s | | QS s - | | - ∨ ∨ - PB(gs) --------> QB(gs) - eB(gs) -``` - -[commute](foundation-core.commuting-squares-of-maps.md) for every `s : S`. - -We show that equivalences characterize the -[identity types](foundation-core.identity-types.md) of descent data for -pushouts. - -By forgetting that the fiberwise maps are equivalences, we get the underlying -[morphism of descent data](synthetic-homotopy-theory.morphisms-descent-data-pushouts.md). -We define homotopies of equivalences of descent data to be homotopies of the -underlying morphisms, and show that homotopies characterize the identity type of -equivalences of descent data. - ## Definitions ### Equivalences of equifibered dependent span diagrams -Note that the descent data arguments cannot be inferred when calling -`left-equiv-equiv-descent-data-pushout` and the like, since Agda cannot infer -the proofs of `is-equiv` of their gluing maps. - ```agda module _ {l1 l2 l3 l4 l5 l6 l7 l8 l9 : Level} @@ -267,7 +227,7 @@ module _ ( map-left-family-equifibered-dependent-span-diagram Q s) ( left-map-equiv-equifibered-dependent-span-diagram ( left-map-span-diagram 𝒮 s)) - (vertical-inv-equiv-coherence-square-maps + ( vertical-inv-equiv-coherence-square-maps ( spanning-type-map-equiv-equifibered-dependent-span-diagram s) ( equiv-right-family-equifibered-dependent-span-diagram P s) ( equiv-right-family-equifibered-dependent-span-diagram Q s) @@ -277,192 +237,20 @@ module _ ( coherence-left-equiv-equifibered-dependent-span-diagram s) ``` -### The identity equivalence of descent data for pushouts - -```text -module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4 l5) - where - - id-equiv-descent-data-pushout : equiv-descent-data-pushout P P - pr1 id-equiv-descent-data-pushout a = id-equiv - pr1 (pr2 id-equiv-descent-data-pushout) b = id-equiv - pr2 (pr2 id-equiv-descent-data-pushout) s = refl-htpy -``` - -### Inverses of equivalences of descent data for pushouts - -Taking an inverse of an equivalence `(eA, eB, eS)` of descent data amounts to -taking the inverses of the fiberwise maps - -```text - a : A ⊢ eA(a)⁻¹ : QA a ≃ PA a - b : B ⊢ eB(b)⁻¹ : QB b ≃ PB b -``` - -and mirroring the coherence squares vertically to get - -```text - eA(a)⁻¹ - QA(fs) --------> PA(fs) - | | - QS s | | PS s - | | - ∨ ∨ - QB(gs) --------> PB(gs). - eB(a)⁻¹ -``` - -```text -module _ - {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4 l5) - (Q : descent-data-pushout 𝒮 l6 l7) - where +### The identity equivalence of equifibered dependent span diagrams - inv-equiv-descent-data-pushout : - equiv-descent-data-pushout P Q → equiv-descent-data-pushout Q P - pr1 (inv-equiv-descent-data-pushout e) a = - inv-equiv (left-equiv-equiv-descent-data-pushout P Q e a) - pr1 (pr2 (inv-equiv-descent-data-pushout e)) b = - inv-equiv (right-equiv-equiv-descent-data-pushout P Q e b) - pr2 (pr2 (inv-equiv-descent-data-pushout e)) s = - horizontal-inv-equiv-coherence-square-maps - ( left-equiv-equiv-descent-data-pushout P Q e (left-map-span-diagram 𝒮 s)) - ( map-family-descent-data-pushout P s) - ( map-family-descent-data-pushout Q s) - ( right-equiv-equiv-descent-data-pushout P Q e - ( right-map-span-diagram 𝒮 s)) - ( coherence-equiv-descent-data-pushout P Q e s) -``` - -### Homotopies of equivalences of descent data for pushouts - -```text -module _ - {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4 l5) - (Q : descent-data-pushout 𝒮 l6 l7) - where - - htpy-equiv-descent-data-pushout : - (e f : equiv-descent-data-pushout P Q) → - UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6 ⊔ l7) - htpy-equiv-descent-data-pushout e f = - htpy-hom-descent-data-pushout P Q - ( hom-equiv-descent-data-pushout P Q e) - ( hom-equiv-descent-data-pushout P Q f) -``` - -## Properties - -### Characterization of identity types of descent data for pushouts - -```text -module _ - {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} - (P : descent-data-pushout 𝒮 l4 l5) - where - - equiv-eq-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4 l5) → - P ＝ Q → equiv-descent-data-pushout P Q - equiv-eq-descent-data-pushout .P refl = id-equiv-descent-data-pushout P - - abstract - is-torsorial-equiv-descent-data-pushout : - is-torsorial (equiv-descent-data-pushout {l6 = l4} {l7 = l5} P) - is-torsorial-equiv-descent-data-pushout = - is-torsorial-Eq-structure - ( is-torsorial-Eq-Π - ( λ a → is-torsorial-equiv (left-family-descent-data-pushout P a))) - ( left-family-descent-data-pushout P , λ a → id-equiv) - ( is-torsorial-Eq-structure - ( is-torsorial-Eq-Π - ( λ b → is-torsorial-equiv (right-family-descent-data-pushout P b))) - ( right-family-descent-data-pushout P , λ b → id-equiv) - ( is-torsorial-Eq-Π - ( λ s → - is-torsorial-htpy-equiv (equiv-family-descent-data-pushout P s)))) - - is-equiv-equiv-eq-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4 l5) → - is-equiv (equiv-eq-descent-data-pushout Q) - is-equiv-equiv-eq-descent-data-pushout = - fundamental-theorem-id - ( is-torsorial-equiv-descent-data-pushout) - ( equiv-eq-descent-data-pushout) - - extensionality-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4 l5) → - (P ＝ Q) ≃ equiv-descent-data-pushout P Q - pr1 (extensionality-descent-data-pushout Q) = - equiv-eq-descent-data-pushout Q - pr2 (extensionality-descent-data-pushout Q) = - is-equiv-equiv-eq-descent-data-pushout Q - - eq-equiv-descent-data-pushout : - (Q : descent-data-pushout 𝒮 l4 l5) → - equiv-descent-data-pushout P Q → P ＝ Q - eq-equiv-descent-data-pushout Q = - map-inv-equiv (extensionality-descent-data-pushout Q) -``` - -### Characterization of identity types of equivalences of descent data of pushouts - -```text +```agda module _ - {l1 l2 l3 l4 l5 l6 l7 : Level} {𝒮 : span-diagram l1 l2 l3} - {P : descent-data-pushout 𝒮 l4 l5} - {Q : descent-data-pushout 𝒮 l6 l7} - (e : equiv-descent-data-pushout P Q) + {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} + (P : equifibered-dependent-span-diagram 𝒮 l4 l5 l6) where - htpy-eq-equiv-descent-data-pushout : - (f : equiv-descent-data-pushout P Q) → - (e ＝ f) → htpy-equiv-descent-data-pushout P Q e f - htpy-eq-equiv-descent-data-pushout .e refl = - refl-htpy-hom-descent-data-pushout P Q - ( hom-equiv-descent-data-pushout P Q e) - - abstract - is-torsorial-htpy-equiv-descent-data-pushout : - is-torsorial (htpy-equiv-descent-data-pushout P Q e) - is-torsorial-htpy-equiv-descent-data-pushout = - is-torsorial-Eq-structure - ( is-torsorial-Eq-Π - ( λ a → - is-torsorial-htpy-equiv - ( left-equiv-equiv-descent-data-pushout P Q e a))) - ( left-equiv-equiv-descent-data-pushout P Q e , λ a → refl-htpy) - ( is-torsorial-Eq-structure - ( is-torsorial-Eq-Π - ( λ b → - is-torsorial-htpy-equiv - ( right-equiv-equiv-descent-data-pushout P Q e b))) - ( right-equiv-equiv-descent-data-pushout P Q e , λ b → refl-htpy) - ( is-torsorial-Eq-Π - ( λ s → - is-torsorial-htpy - ( coherence-equiv-descent-data-pushout P Q e s ∙h refl-htpy)))) - - is-equiv-htpy-eq-equiv-descent-data-pushout : - (f : equiv-descent-data-pushout P Q) → - is-equiv (htpy-eq-equiv-descent-data-pushout f) - is-equiv-htpy-eq-equiv-descent-data-pushout = - fundamental-theorem-id - ( is-torsorial-htpy-equiv-descent-data-pushout) - ( htpy-eq-equiv-descent-data-pushout) - - extensionality-equiv-descent-data-pushout : - (f : equiv-descent-data-pushout P Q) → - (e ＝ f) ≃ - htpy-hom-descent-data-pushout P Q - ( hom-equiv-descent-data-pushout P Q e) - ( hom-equiv-descent-data-pushout P Q f) - pr1 (extensionality-equiv-descent-data-pushout f) = - htpy-eq-equiv-descent-data-pushout f - pr2 (extensionality-equiv-descent-data-pushout f) = - is-equiv-htpy-eq-equiv-descent-data-pushout f + id-equiv-equifibered-dependent-span-diagram : + equiv-equifibered-dependent-span-diagram P P + id-equiv-equifibered-dependent-span-diagram = + ( λ _ → id-equiv) , + ( λ _ → id-equiv) , + ( λ _ → id-equiv) , + ( λ _ → refl-htpy) , + ( λ _ → refl-htpy) ``` diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index aa152adfbb..6b1b93fc92 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -294,6 +294,38 @@ module _ make-span-diagram ( vertical-map-span-flattening-equifibered-dependent-span-diagram) ( horizontal-map-span-flattening-equifibered-dependent-span-diagram) + +module _ + { l1 l2 l3 l4 l5 l6 l7 l8 : Level} + { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} + ( f : S → A) (g : S → B) (c : cocone f g X) + ( P : equifibered-dependent-span-diagram (make-span-diagram f g) l5 l6 l7) + ( Q : X → UU l8) + ( e : + equiv-equifibered-dependent-span-diagram + ( P) + ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q)) + where + + horizontal-map-cocone-flattening-equifibered-dependent-span-diagram : + Σ A (left-family-equifibered-dependent-span-diagram P) → Σ X Q + horizontal-map-cocone-flattening-equifibered-dependent-span-diagram = + map-Σ Q + ( horizontal-map-cocone f g c) + ( left-map-equiv-equifibered-dependent-span-diagram + ( P) + ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) + ( e)) + + vertical-map-cocone-flattening-equifibered-dependent-span-diagram : + Σ B (right-family-equifibered-dependent-span-diagram P) → Σ X Q + vertical-map-cocone-flattening-equifibered-dependent-span-diagram = + map-Σ Q + ( vertical-map-cocone f g c) + ( right-map-equiv-equifibered-dependent-span-diagram + ( P) + ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) + ( e)) ``` ## Properties From 510ca18ebd4b7d856598393204b7d6bed03f0146 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 15 Mar 2025 18:26:00 +0000 Subject: [PATCH 09/10] idea --- ...uivalences-equifibered-dependent-span-diagrams.lagda.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md index 21c7509b9c..a14d92f545 100644 --- a/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/equivalences-equifibered-dependent-span-diagrams.lagda.md @@ -30,6 +30,13 @@ open import synthetic-homotopy-theory.equifibered-dependent-span-diagrams ## Idea +An +{{#concept "equivalence" Disambiguation="of equifibered dependent span diagrams" Agda=equiv-equifibered-dependent-span-diagram}} +of two +[equifibered dependent span diagrams](synthetic-homotopy-theory.equifibered-dependent-span-diagrams.md) +is a coherent system of equivalences of families over the base +[span diagram](foundation.span-diagrams.md). + ## Definitions ### Equivalences of equifibered dependent span diagrams From 374ab642354be8f3cb2d4a5d235f4c9c26c15870 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 21 Mar 2025 14:07:07 +0000 Subject: [PATCH 10/10] scribbles mather's second cube theorem --- src/synthetic-homotopy-theory.lagda.md | 1 + .../flattening-lemma-pushouts.lagda.md | 69 ++++- .../mathers-second-cube-theorem.lagda.md | 244 ++++++++++++++++++ 3 files changed, 307 insertions(+), 7 deletions(-) create mode 100644 src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md diff --git a/src/synthetic-homotopy-theory.lagda.md b/src/synthetic-homotopy-theory.lagda.md index be6e82a6c9..97dc6e5c19 100644 --- a/src/synthetic-homotopy-theory.lagda.md +++ b/src/synthetic-homotopy-theory.lagda.md @@ -92,6 +92,7 @@ open import synthetic-homotopy-theory.left-half-smash-products public open import synthetic-homotopy-theory.loop-homotopy-circle public open import synthetic-homotopy-theory.loop-spaces public open import synthetic-homotopy-theory.maps-of-prespectra public +open import synthetic-homotopy-theory.mathers-second-cube-theorem public open import synthetic-homotopy-theory.mere-spheres public open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequential-diagrams public open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows public diff --git a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md index 6b1b93fc92..bbb97722bb 100644 --- a/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/flattening-lemma-pushouts.lagda.md @@ -46,13 +46,13 @@ commute with [dependent pair types](foundation.dependent-pair-types.md). More precisely, given a pushout square ```text - g - S -----> B - | | - f| | j - ∨ ⌜ ∨ - A -----> X - i + g + S ------> B + | | + f| | j + ∨ ⌜ ∨ + A ------> X + i ``` with homotopy `H : i ∘ f ~ j ∘ g`, and for any type family `P` over `X`, the @@ -326,6 +326,61 @@ module _ ( P) ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) ( e)) + + -- coherence-square-cocone-flattening-equifibered-dependent-span-diagram : + -- coherence-square-maps + -- ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P) + -- ( vertical-map-span-flattening-equifibered-dependent-span-diagram P) + -- ( vertical-map-cocone-flattening-equifibered-dependent-span-diagram) + -- ( horizontal-map-cocone-flattening-equifibered-dependent-span-diagram) + -- coherence-square-cocone-flattening-equifibered-dependent-span-diagram = + -- htpy-map-Σ Q + -- ( coherence-square-cocone f g c) + -- (λ s t → + -- left-map-equiv-equifibered-dependent-span-diagram + -- ( P) + -- ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) + -- ( e) + -- ( f s) + -- ( map-left-family-equifibered-dependent-span-diagram P s t)) + -- λ s t → + -- equational-reasoning + -- {! (tr Q (pr2 (pr2 c) s) ∘ (λ t₁ → pr1 (pr1 e (f s)) (map-left-family-equifibered-dependent-span-diagram P s t₁))) t !} + -- ＝ {! !} by {! !} + -- ＝ {! !} by {! !} + -- ＝ {! !} by {! !} + -- htpy-map-Σ Q + -- ( coherence-square-cocone f g c) + -- ( ( left-map-equiv-equifibered-dependent-span-diagram + -- ( P) + -- ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) + -- ( e)) ∘ + -- ( f)) + -- ( inv-htpy ∘ + -- coherence-equiv-equifibered-dependent-span-diagram + -- ( P) + -- ( equifibered-dependent-span-diagram-family-cocone-span-diagram c Q) + -- ( e)) + +-- cocone-flattening-equifibered-dependent-span-diagram : +-- cocone +-- ( vertical-map-span-flattening-equifibered-dependent-span-diagram P) +-- ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P) +-- ( Σ X Q) +-- pr1 cocone-flattening-equifibered-dependent-span-diagram = +-- horizontal-map-cocone-flattening-equifibered-dependent-span-diagram +-- pr1 (pr2 cocone-flattening-equifibered-dependent-span-diagram) = +-- vertical-map-cocone-flattening-equifibered-dependent-span-diagram +-- pr2 (pr2 cocone-flattening-equifibered-dependent-span-diagram) = +-- coherence-square-cocone-flattening-equifibered-dependent-span-diagram + +-- flattening-lemma-equifibered-dependent-span-diagram-statement : UUω +-- flattening-lemma-equifibered-dependent-span-diagram-statement = +-- universal-property-pushout f g c → +-- universal-property-pushout +-- ( vertical-map-span-flattening-equifibered-dependent-span-diagram P) +-- ( horizontal-map-span-flattening-equifibered-dependent-span-diagram P) +-- ( cocone-flattening-equifibered-dependent-span-diagram) ``` ## Properties diff --git a/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md new file mode 100644 index 0000000000..fbd86f59e9 --- /dev/null +++ b/src/synthetic-homotopy-theory/mathers-second-cube-theorem.lagda.md @@ -0,0 +1,244 @@ +# Mather's second cube theorem + +```agda +module synthetic-homotopy-theory.mathers-second-cube-theorem where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.commuting-cubes-of-maps +open import foundation.commuting-squares-of-maps +open import foundation.commuting-triangles-of-maps +open import foundation.dependent-pair-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.fibers-of-maps +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.functoriality-fibers-of-maps +open import foundation.homotopies +open import foundation.identity-types +open import foundation.morphisms-arrows +open import foundation.pullbacks +open import foundation.span-diagrams +open import foundation.transport-along-identifications +open import foundation.universal-property-dependent-pair-types +open import foundation.universal-property-pullbacks +open import foundation.universe-levels + +open import synthetic-homotopy-theory.cocones-under-spans +open import synthetic-homotopy-theory.dependent-cocones-under-spans +open import synthetic-homotopy-theory.dependent-universal-property-pushouts +open import synthetic-homotopy-theory.descent-data-pushouts +open import synthetic-homotopy-theory.equivalences-descent-data-pushouts +open import synthetic-homotopy-theory.flattening-lemma-pushouts +open import synthetic-homotopy-theory.pushouts +open import synthetic-homotopy-theory.universal-property-pushouts +``` + +
+ +## Idea + +{{#concept "Mather's second cube theorem" Disambiguation="for types"}} states +that every base change of a pushout square is a pushout. In other words, if we +are given a commuting cube where the bottom face is a pushout and the vertical +faces are pullbacks + +```text + ∙ ----------------> ∙ + | \ ⌟ | \ + | ⌟\ | ⌟\ + | ∨ | ∨ + | ∙ ----------------> ∙ + | | ⌟ | | + ∨ | ∨ | + ∙ ----|-----------> ∙ | + \ | \ | + \ | \ | + ∨ ∨ ⌜ ∨ ∨ + ∙ ----------------> ∙, +``` + +then the top face is also a pushout. + +## Theorem + +```agda +module _ + {l1 l2 l3 l4 l1' l2' l3' l4' : Level} + {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4} + (f : A → B) (g : A → C) (h : B → D) (k : C → D) + {A' : UU l1'} {B' : UU l2'} {C' : UU l3'} {D' : UU l4'} + (f' : A' → B') (g' : A' → C') (h' : B' → D') (k' : C' → D') + (hA : A' → A) (hB : B' → B) (hC : C' → C) (hD : D' → D) + (top : h' ∘ f' ~ k' ∘ g') + (left : f ∘ hA ~ hB ∘ f') + (back : g ∘ hA ~ hC ∘ g') + (front : h ∘ hB ~ hD ∘ h') + (right : k ∘ hC ~ hD ∘ k') + (bottom : h ∘ f ~ k ∘ g) + (c : + coherence-cube-maps + f g h k f' g' h' k' hA hB hC hD + top left back front right bottom) + where + + mathers-second-cube-theorem : + universal-property-pushout f g (h , k , bottom) → + universal-property-pullback h hD (hB , h' , front) → + universal-property-pullback k hD (hC , k' , right) → + universal-property-pullback f hB (hA , f' , left) → + universal-property-pullback g hC (hA , g' , back) → + universal-property-pushout f' g' (h' , k' , top) + mathers-second-cube-theorem po-bottom pb-front pb-right pb-left pb-back = + universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv + _ _ _ _ + f' g' h' k' + ( equiv-tot e-left ∘e inv-equiv-total-fiber' hA) + ( inv-equiv-total-fiber' hB) + ( inv-equiv-total-fiber' hC) + ( inv-equiv-total-fiber' hD) + ( top) + ( λ x → + eq-pair-Σ (left x) (inv-compute-tr-self-fiber' hB (f' x , left x))) + ( λ x → + equational-reasoning + g (hA x) , {! pr1 (pr1 (pr1 (is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' k hD (hC , k' , right) pb-right (g (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x))))) (pr1 (equiv-tr (fiber' hD) (bottom (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x))) ∘e e-front (f (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x)))) (pr2 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x)))) !} , {! pr2 (pr1 (pr1 (is-fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' k hD (hC , k' , right) pb-right (g (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x))))) (pr1 (equiv-tr (fiber' hD) (bottom (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x))) ∘e e-front (f (pr1 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x)))) (pr2 (map-equiv (equiv-tot e-left ∘e inv-equiv-total-fiber' hA) x)))) !} + ＝ hC (g' x) , g' x , refl + by + eq-pair-Σ + ( back x) + ( equational-reasoning {! !} ＝ g' x , refl by {! !})) + ( λ x → + eq-pair-Σ (front x) (inv-compute-tr-self-fiber' hD (h' x , front x))) + ( λ x → + eq-pair-Σ (right x) (inv-compute-tr-self-fiber' hD (k' x , right x))) + ( λ x → {! !}) + -- equational-reasoning + -- {! pr1 + -- (map-Σ + -- (λ x₁ → + -- Id + -- (h + -- (pr1 + -- (vertical-map-span-flattening-descent-data-pushout + -- (fiber' hB , + -- fiber' hC , + -- (λ s → + -- inv-equiv (e-right (g s)) ∘e + -- equiv-tr (fiber' hD) (bottom s) ∘e e-front (f s))) + -- x))) + -- (hD x₁)) + -- h' (λ a p → ap h p ∙ front a) + -- (pr2 + -- (vertical-map-span-flattening-descent-data-pushout + -- (fiber' hB , + -- fiber' hC , + -- (λ s → + -- inv-equiv (e-right (g s)) ∘e + -- equiv-tr (fiber' hD) (bottom s) ∘e e-front (f s))) + -- x))) !} , , {! !} + -- ＝ {! !} , {! !} , {! !} by {! !}) + {! !} + ( flattening-lemma-descent-data-pushout + ( f) + ( g) + ( h , k , bottom) + ( ( fiber' hB) , + ( fiber' hC) , + ( λ s → + ( inv-equiv (e-right (g s))) ∘e + ( equiv-tr (fiber' hD) (bottom s)) ∘e + ( e-front (f s)))) + ( fiber' hD) + ( ( e-front) , + ( e-right) , + {! !}) + ( po-bottom)) + where + e-left = + fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + f hB (hA , f' , left) pb-left + e-front = + fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + h hD (hB , h' , front) pb-front + e-right = + fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + k hD (hC , k' , right) pb-right + -- universal-property-pushout-top-universal-property-pushout-bottom-cube-equiv + -- ( vertical-map-span-flattening-pushout (fiber' hD) f g (h , k , bottom)) + -- ( horizontal-map-span-flattening-pushout (fiber' hD) f g (h , k , bottom)) + -- ( horizontal-map-cocone-flattening-pushout (fiber' hD) f g (h , k , bottom)) + -- ( vertical-map-cocone-flattening-pushout (fiber' hD) f g (h , k , bottom)) + -- f' g' h' k' + -- ( equiv-tot + -- ( λ x → + -- ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + -- h hD (hB , h' , front) pb-front (f x)) ∘e + -- ( fiberwise-equiv-map-fiber-vertical-map-cone-universal-property-pullback' + -- f hB (hA , f' , left) pb-left x)) ∘e + -- ( inv-equiv-total-fiber' hA)) + -- ( ( equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' + -- h hD + -- ( hB , h' , front) + -- ( pb-front)) ∘e + -- ( inv-equiv-total-fiber' hB)) + -- ( ( equiv-tot-map-fiber-vertical-map-cone-universal-property-pullback' + -- k hD + -- ( hC , k' , right) + -- ( pb-right)) ∘e + -- ( inv-equiv-total-fiber' hC)) + -- ( inv-equiv-total-fiber' hD) + -- ( top) + -- ( λ x → + -- equational-reasoning + -- ( f (hA x) , h' (f' x) , ap h (left x) ∙ front (f' x)) + -- ＝ ( hB (f' x) , h' (f' x) , {! !}) by {! !} + -- ＝ ( hB (f' x) , h' (f' x) , front (f' x)) by {! !}) + -- (λ x → equational-reasoning g (hA x) , {!pr1 (tr (λ b → Σ D' (λ x₁ → Id b (hD x₁))) (bottom (hA x)) (map-Σ (λ x₁ → Id (h (f (hA x))) (hD x₁)) h' (λ a p → ap h p ∙ front a) (map-Σ (λ x₁ → Id (f (hA x)) (hB x₁)) f' (λ a p → ap f p ∙ left a) (pr2 (map-inv-equiv-total-fiber' hA x))))) !} , {! !} ＝ hC (g' x) , {! pr1 (map-Σ (λ x₁ → map-codomain-hom-arrow hC hD (hom-arrow-cone k hD (hC , k' , right)) (pr1 (pr1 (inv-equiv-total-fiber' hC) (g' x))) ＝ hD x₁) (pr1 (hom-arrow-cone k hD (hC , k' , right))) (λ a p → ap (map-codomain-hom-arrow hC hD (hom-arrow-cone k hD (hC , k' , right))) p ∙ coh-hom-arrow hC hD (hom-arrow-cone k hD (hC , k' , right)) a) (pr2 (pr1 (inv-equiv-total-fiber' hC) (g' x)))) !} , {! !} by {! !}) + -- {! !} + -- {! !} + -- ( λ x → eq-pair-Σ (bottom (pr1 x)) refl) + -- {! !} + -- ( flattening-lemma-pushout (fiber' hD) f g (h , k , bottom) po-bottom) + + -- universal-property-pushout-bottom-universal-property-pushout-top-cube-is-equiv + -- f' g' h' k' + -- ( vertical-map-span-flattening-pushout (fiber hD) f g (h , k , bottom)) + -- ( horizontal-map-span-flattening-pushout (fiber hD) f g (h , k , bottom)) + -- ( horizontal-map-cocone-flattening-pushout (fiber hD) f g (h , k , bottom)) + -- ( vertical-map-cocone-flattening-pushout (fiber hD) f g (h , k , bottom)) + -- (map-equiv-total-fiber hA ∘ tot (λ x → {! !} )) + -- {! !} + -- {! !} + -- ( map-equiv-total-fiber hD) + -- ( λ x → eq-pair-Σ (bottom (pr1 x)) refl) + -- {! !} + -- {! !} + -- {! !} + -- {! !} + -- top + -- {! !} + -- {! !} + -- {! !} + -- {! !} + -- ( is-equiv-map-equiv-total-fiber hD) + -- ( flattening-lemma-pushout (fiber hD) f g (h , k , bottom) po-bottom) +``` + +## See also + +- Mather's second cube theorem is an + [unstraightened](foundation.type-duality.md) rephrasing of the + [flattening lemma for pushouts](synthetic-homotopy-theory.flattening-lemma-pushouts.md) +- The + [descent property for pushouts](synthetic-homotopy-theory.descent-property-pushouts.md). + +## External links + +- [Mather's Second Cube Theorem](https://kerodon.net/tag/011H) on Kerodon