From 556a187fc5347c0679074ad2efc6f748b44bd83b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 18:42:47 +0100 Subject: [PATCH 01/16] refactor universal property of pullbacks --- src/foundation-core/pullbacks.lagda.md | 14 ++++---- .../universal-property-pullbacks.lagda.md | 32 +++++++++++-------- src/foundation/fibers-of-maps.lagda.md | 2 +- src/foundation/pullback-squares.lagda.md | 28 ++++++++++------ ...-property-cartesian-product-types.lagda.md | 3 +- ...universal-property-fiber-products.lagda.md | 3 +- .../universal-property-pullbacks.lagda.md | 16 +++++----- .../pullback-hom.lagda.md | 3 +- 8 files changed, 54 insertions(+), 47 deletions(-) diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index b0f4ec9cd8..88788d230e 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -171,8 +171,7 @@ module _ abstract universal-property-pullback-standard-pullback : - {l : Level} → - universal-property-pullback l f g (cone-standard-pullback f g) + universal-property-pullback f g (cone-standard-pullback f g) universal-property-pullback-standard-pullback C = is-equiv-comp ( tot (λ p → map-distributive-Π-Σ)) @@ -208,8 +207,7 @@ module _ abstract is-pullback-universal-property-pullback : - (c : cone f g C) → - ({l : Level} → universal-property-pullback l f g c) → is-pullback f g c + (c : cone f g C) → universal-property-pullback f g c → is-pullback f g c is-pullback-universal-property-pullback c = is-equiv-up-pullback-up-pullback ( cone-standard-pullback f g) @@ -221,7 +219,7 @@ module _ abstract universal-property-pullback-is-pullback : (c : cone f g C) → is-pullback f g c → - {l : Level} → universal-property-pullback l f g c + universal-property-pullback f g c universal-property-pullback-is-pullback c is-pullback-c = up-pullback-up-pullback-is-equiv ( cone-standard-pullback f g) @@ -652,8 +650,8 @@ module _ abstract universal-property-pullback-is-fiberwise-equiv : - is-fiberwise-equiv g → {l : Level} → - universal-property-pullback l f pr1 cone-map-Σ + is-fiberwise-equiv g → + universal-property-pullback f pr1 cone-map-Σ universal-property-pullback-is-fiberwise-equiv is-equiv-g = universal-property-pullback-is-pullback f pr1 cone-map-Σ ( is-pullback-is-fiberwise-equiv is-equiv-g) @@ -671,7 +669,7 @@ module _ abstract is-fiberwise-equiv-universal-property-pullback : - ( {l : Level} → universal-property-pullback l f pr1 cone-map-Σ) → + ( universal-property-pullback f pr1 cone-map-Σ) → is-fiberwise-equiv g is-fiberwise-equiv-universal-property-pullback up = is-fiberwise-equiv-is-pullback diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md index 36e41e34e5..d98c5fa3bb 100644 --- a/src/foundation-core/universal-property-pullbacks.lagda.md +++ b/src/foundation-core/universal-property-pullbacks.lagda.md @@ -31,28 +31,32 @@ open import foundation-core.identity-types ```agda module _ - {l1 l2 l3 l4 : Level} (l : Level) {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) {C : UU l4} + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C) where - universal-property-pullback : - (c : cone f g C) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) - universal-property-pullback c = + universal-property-pullback-Level : + (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) + universal-property-pullback-Level l = (C' : UU l) → is-equiv (cone-map f g c {C'}) + universal-property-pullback : UUω + universal-property-pullback = + {l : Level} → universal-property-pullback-Level l + module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C) where map-universal-property-pullback : - ({l : Level} → universal-property-pullback l f g c) → + universal-property-pullback f g c → {C' : UU l5} (c' : cone f g C') → C' → C map-universal-property-pullback up-c {C'} c' = map-inv-is-equiv (up-c C') c' compute-map-universal-property-pullback : - (up-c : {l : Level} → universal-property-pullback l f g c) → + (up-c : universal-property-pullback f g c) → {C' : UU l5} (c' : cone f g C') → cone-map f g c (map-universal-property-pullback up-c c') ＝ c' compute-map-universal-property-pullback up-c {C'} c' = @@ -86,8 +90,8 @@ module _ abstract is-equiv-up-pullback-up-pullback : - ({l : Level} → universal-property-pullback l f g c) → - ({l : Level} → universal-property-pullback l f g c') → + universal-property-pullback f g c → + universal-property-pullback f g c' → is-equiv h is-equiv-up-pullback-up-pullback up up' = is-equiv-is-equiv-postcomp h @@ -103,8 +107,8 @@ module _ abstract up-pullback-up-pullback-is-equiv : is-equiv h → - ({l : Level} → universal-property-pullback l f g c) → - ({l : Level} → universal-property-pullback l f g c') + universal-property-pullback f g c → + universal-property-pullback f g c' up-pullback-up-pullback-is-equiv is-equiv-h up D = is-equiv-left-map-triangle ( cone-map f g c') @@ -116,9 +120,9 @@ module _ abstract up-pullback-is-equiv-up-pullback : - ({l : Level} → universal-property-pullback l f g c') → + universal-property-pullback f g c' → is-equiv h → - ({l : Level} → universal-property-pullback l f g c) + universal-property-pullback f g c up-pullback-is-equiv-up-pullback up' is-equiv-h D = is-equiv-right-map-triangle ( cone-map f g c') @@ -139,7 +143,7 @@ module _ abstract uniqueness-universal-property-pullback : - ({l : Level} → universal-property-pullback l f g c) → + universal-property-pullback f g c → {l5 : Level} (C' : UU l5) (c' : cone f g C') → is-contr (Σ (C' → C) (λ h → htpy-cone f g (cone-map f g c h) c')) uniqueness-universal-property-pullback up C' c' = diff --git a/src/foundation/fibers-of-maps.lagda.md b/src/foundation/fibers-of-maps.lagda.md index b68c2e768d..536cc0b1b8 100644 --- a/src/foundation/fibers-of-maps.lagda.md +++ b/src/foundation/fibers-of-maps.lagda.md @@ -55,7 +55,7 @@ module _ abstract universal-property-pullback-cone-fiber : - {l : Level} → universal-property-pullback l f (const unit B b) cone-fiber + universal-property-pullback f (const unit B b) cone-fiber universal-property-pullback-cone-fiber = universal-property-pullback-is-pullback f ( const unit B b) diff --git a/src/foundation/pullback-squares.lagda.md b/src/foundation/pullback-squares.lagda.md index 25938b8b89..6ded80adcd 100644 --- a/src/foundation/pullback-squares.lagda.md +++ b/src/foundation/pullback-squares.lagda.md @@ -9,6 +9,7 @@ module foundation.pullback-squares where ```agda open import foundation.cones-over-cospans open import foundation.dependent-pair-types +open import foundation.pullbacks open import foundation.universe-levels open import foundation-core.commuting-squares-of-maps @@ -30,38 +31,38 @@ satisfies the ```agda module _ - {l1 l2 l3 l4 : Level} (l : Level) {A : UU l1} {B : UU l2} {C : UU l3} + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} (f : A → C) (g : B → C) (X : UU l4) where - pullback-cone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) - pullback-cone = Σ (cone f g X) (universal-property-pullback l f g) + pullback-cone : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + pullback-cone = Σ (cone f g X) (is-pullback f g) ``` ### Pullback squares ```agda module _ - {l1 l2 l3 l4 : Level} (l : Level) (A : UU l1) (B : UU l2) (C : UU l3) + {l1 l2 l3 l4 : Level} (A : UU l1) (B : UU l2) (C : UU l3) (X : UU l4) where - pullback-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) + pullback-square : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) pullback-square = Σ ( A → C) ( λ f → Σ ( B → C) ( λ g → Σ ( cone f g X) - ( universal-property-pullback l f g))) + ( is-pullback f g))) ``` ### Components of a pullback cone ```agda module _ - {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} - (f : A → C) (g : B → C) (c : pullback-cone l f g X) + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} + (f : A → C) (g : B → C) (c : pullback-cone f g X) where cone-pullback-cone : cone f g X @@ -80,8 +81,15 @@ module _ ( f) coherence-square-pullback-cone = coherence-square-cone f g cone-pullback-cone - universal-property-pullback-cone : universal-property-pullback l f g (pr1 c) - universal-property-pullback-cone = pr2 c + is-pullback-pullback-cone : is-pullback f g cone-pullback-cone + is-pullback-pullback-cone = pr2 c + + universal-property-pullback-cone : + universal-property-pullback f g (pr1 c) + universal-property-pullback-cone = + universal-property-pullback-is-pullback f g + ( cone-pullback-cone) + ( is-pullback-pullback-cone) ``` ## Table of files about pullbacks diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md index 4cba37f1d2..57e37b065e 100644 --- a/src/foundation/universal-property-cartesian-product-types.lagda.md +++ b/src/foundation/universal-property-cartesian-product-types.lagda.md @@ -100,8 +100,7 @@ We conclude that cartesian products satisfy the universal property of pullbacks. ```agda abstract universal-property-pullback-prod : - {l : Level} → - universal-property-pullback l + universal-property-pullback ( const A unit star) ( const B unit star) ( cone-prod) diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index ca15f68dab..4579ee3267 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -82,8 +82,7 @@ map. abstract universal-property-pullback-fiberwise-prod : - {l : Level} → - universal-property-pullback l + universal-property-pullback ( pr1 {B = P}) ( pr1 {B = Q}) ( cone-fiberwise-prod) diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index d68b15a208..01162f2405 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -50,15 +50,15 @@ A -----> X ```agda module _ - {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C) where abstract - is-prop-universal-property-pullback : - is-prop (universal-property-pullback l5 f g c) - is-prop-universal-property-pullback = - is-prop-Π (λ C' → is-property-is-equiv (cone-map f g c)) + is-prop-universal-property-pullback-Level : + is-prop (universal-property-pullback-Level f g c l) + is-prop-universal-property-pullback-Level = + is-prop-Π (λ _ → is-property-is-equiv (cone-map f g c)) ``` ### The homotopy of cones obtained from the universal property of pullbacks @@ -70,7 +70,7 @@ module _ where htpy-cone-map-universal-property-pullback : - (c : cone f g C) (up : {l : Level} → universal-property-pullback l f g c) → + (c : cone f g C) (up : universal-property-pullback f g c) → {l5 : Level} {C' : UU l5} (c' : cone f g C') → htpy-cone f g ( cone-map f g c (map-universal-property-pullback f g c up c')) @@ -93,8 +93,8 @@ module _ abstract uniquely-unique-pullback : ( c' : cone f g C') (c : cone f g C) → - ( up-c' : {l : Level} → universal-property-pullback l f g c') → - ( up-c : {l : Level} → universal-property-pullback l f g c) → + ( up-c' : universal-property-pullback f g c') → + ( up-c : universal-property-pullback f g c) → is-contr ( Σ (C' ≃ C) (λ e → htpy-cone f g (cone-map f g c (map-equiv e)) c')) uniquely-unique-pullback c' c up-c' up-c = diff --git a/src/orthogonal-factorization-systems/pullback-hom.lagda.md b/src/orthogonal-factorization-systems/pullback-hom.lagda.md index 8c1b02ae7b..c902b1ebf7 100644 --- a/src/orthogonal-factorization-systems/pullback-hom.lagda.md +++ b/src/orthogonal-factorization-systems/pullback-hom.lagda.md @@ -155,8 +155,7 @@ fibered maps. is-equiv-map-equiv equiv-type-standard-pullback-hom-fibered-map universal-property-pullback-fibered-map : - {l : Level} → - universal-property-pullback l + universal-property-pullback ( precomp f Y) (postcomp A g) (cone-pullback-hom) universal-property-pullback-fibered-map = universal-property-pullback-is-pullback From 8c649d98533857f076bb8951095c8789c4aa9b91 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 18:48:55 +0100 Subject: [PATCH 02/16] touch up universal property of fiber products --- ...universal-property-fiber-products.lagda.md | 24 ++++++++++++------- tables/pullbacks.md | 1 + 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index 4579ee3267..5c43b1bd77 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -28,10 +28,11 @@ open import foundation-core.universal-property-pullbacks ## Idea -The fiberwise product of two families `P` and `Q` over a type `X` is the family -of types `(P x) × (Q x)` over `X`. Similarly, the fiber product of two maps -`f :A → X` and `g : B → X` is the type `Σ X (λ x → fiber f x × fiber g x)`, -which fits in a pullback diagram on `f` and `g`. +The **fiberwise product** of two families `P` and `Q` over a type `X` is the +family of types `(P x) × (Q x)` over `X`. Similarly, the fiber product of two +maps `f : A → X` and `g : B → X` is the type +`Σ X (λ x → fiber f x × fiber g x)`, which fits in a +[pullback](foundation-core.pullbacks.md) diagram on `f` and `g`. ```agda module _ @@ -40,8 +41,8 @@ module _ cone-fiberwise-prod : cone (pr1 {B = P}) (pr1 {B = Q}) (Σ X (λ x → (P x) × (Q x))) - pr1 cone-fiberwise-prod = tot (λ x → pr1) - pr1 (pr2 cone-fiberwise-prod) = tot (λ x → pr2) + pr1 cone-fiberwise-prod = tot (λ _ → pr1) + pr1 (pr2 cone-fiberwise-prod) = tot (λ _ → pr2) pr2 (pr2 cone-fiberwise-prod) = refl-htpy ``` @@ -63,8 +64,7 @@ map. abstract is-section-inv-gap-fiberwise-prod : (gap-fiberwise-prod ∘ inv-gap-fiberwise-prod) ~ id - is-section-inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)) = - eq-pair-Σ refl (eq-pair-Σ refl refl) + is-section-inv-gap-fiberwise-prod ((x , p) , (.x , q) , refl) = refl abstract is-retraction-inv-gap-fiberwise-prod : @@ -124,7 +124,7 @@ module _ is-retraction-inv-gap-total-prod-fibers : (inv-gap-total-prod-fibers ∘ gap-total-prod-fibers) ~ id is-retraction-inv-gap-total-prod-fibers (.(g b) , (a , p) , (b , refl)) = - eq-pair-Σ refl (eq-pair (eq-pair-Σ refl right-unit) refl) + eq-pair-eq-pr2 (eq-pair (eq-pair-eq-pr2 right-unit) refl) abstract is-pullback-total-prod-fibers : @@ -135,3 +135,9 @@ module _ is-section-inv-gap-total-prod-fibers is-retraction-inv-gap-total-prod-fibers ``` + +## Table of files about pullbacks + +The following table lists files that are about pullbacks as a general concept. + +{{#include tables/pullbacks.md}} diff --git a/tables/pullbacks.md b/tables/pullbacks.md index f93aa884ec..257eb4584c 100644 --- a/tables/pullbacks.md +++ b/tables/pullbacks.md @@ -5,6 +5,7 @@ | Cones over cospans | [`foundation.cones-over-cospans`](foundation.cones-over-cospans.md) | | The universal property of pullbacks (foundation-core) | [`foundation-core.universal-property-pullbacks`](foundation-core.universal-property-pullbacks.md) | | The universal property of pullbacks (foundation) | [`foundation.universal-property-pullbacks`](foundation.universal-property-pullbacks.md) | +| The universal property of fiber products | [`foundation.universal-property-fiber-products`](foundation.universal-property-fiber-products.md) | | Pullbacks (foundation-core) | [`foundation-core.pullbacks`](foundation-core.pullbacks.md) | | Pullbacks (foundation) | [`foundation.pullbacks`](foundation.pullbacks.md) | | Functoriality of pullbacks | [`foundation.functoriality-pullbacks`](foundation.functoriality-pullbacks.md) | From fac2cc263bab06941bc5860c8477633b07a8b963 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 18:58:52 +0100 Subject: [PATCH 03/16] touch up universal property of images --- .../universal-property-image.lagda.md | 78 +++++++++---------- 1 file changed, 37 insertions(+), 41 deletions(-) diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index b76f1e211b..48bbab2017 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -38,8 +38,8 @@ open import foundation-core.whiskering-homotopies ## Idea -The image of a map `f : A → X` is the least subtype of `X` containing all the -values of `f`. +The **image** of a map `f : A → X` is the least +[subtype](foundation-core.subtypes.md) of `X` containing all the values of `f`. ## Definition @@ -140,7 +140,7 @@ module _ map-hom-slice (map-emb i) (map-emb j) hom-slice-universal-property-image triangle-hom-slice-universal-property-image : - (map-emb i) ~ (map-emb j ∘ map-hom-slice-universal-property-image) + map-emb i ~ map-emb j ∘ map-hom-slice-universal-property-image triangle-hom-slice-universal-property-image = triangle-hom-slice ( map-emb i) @@ -215,11 +215,13 @@ module _ abstract is-image-has-section : (l : Level) {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → - section f → is-image f id-emb (pair f refl-htpy) - is-image-has-section l f (pair g H) = + section f → is-image f id-emb (f , refl-htpy) + is-image-has-section l f (g , H) = is-image-is-image' - f id-emb (pair f refl-htpy) - ( λ B m h → pair ((pr1 h) ∘ g) ( λ x → (inv (H x)) ∙ (pr2 h (g x)))) + ( f) + ( id-emb) + ( f , refl-htpy) + ( λ B m h → ((pr1 h ∘ g) , (λ x → inv (H x) ∙ pr2 h (g x)))) ``` ### Any embedding is its own image inclusion @@ -228,11 +230,9 @@ abstract abstract is-image-is-emb : (l : Level) {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → - (H : is-emb f) → is-image f (pair f H) (pair id refl-htpy) + (H : is-emb f) → is-image f (f , H) (id , refl-htpy) is-image-is-emb l f H = - is-image-is-image' - f (pair f H) (pair id refl-htpy) - ( λ B m h → h) + is-image-is-image' f (f , H) (id , refl-htpy) (λ B m h → h) ``` ### The image of `f` is the image of `f` @@ -248,22 +248,21 @@ abstract { A = (fiber f x)} ( fiber-emb-Prop m x) ( λ t → - pair - ( map-hom-slice f (map-emb m) h (pr1 t)) + ( map-hom-slice f (map-emb m) h (pr1 t)) , ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙ ( pr2 t))) map-is-image-im : {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → (m : B ↪ X) (h : hom-slice f (map-emb m)) → im f → B - map-is-image-im f m h (pair x t) = + map-is-image-im f m h (x , t) = pr1 (fiberwise-map-is-image-im f m h x t) triangle-is-image-im : {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → (m : B ↪ X) (h : hom-slice f (map-emb m)) → - inclusion-im f ~ ((map-emb m) ∘ (map-is-image-im f m h)) - triangle-is-image-im f m h (pair x t) = + inclusion-im f ~ map-emb m ∘ map-is-image-im f m h + triangle-is-image-im f m h (x , t) = inv (pr2 (fiberwise-map-is-image-im f m h x t)) is-image-im : @@ -271,11 +270,10 @@ abstract is-image f (emb-im f) (unit-im f) is-image-im f {l} = is-image-is-image' - f (emb-im f) (unit-im f) - ( λ B m h → - pair - ( map-is-image-im f m h) - ( triangle-is-image-im f m h)) + ( f) + ( emb-im f) + ( unit-im f) + ( λ B m h → (map-is-image-im f m h , triangle-is-image-im f m h)) ``` ### A factorization of a map through an embedding is the image factorization if and only if the right factor is surjective @@ -302,16 +300,16 @@ abstract ( up-i ( Σ B ( λ b → type-trunc-Prop (fiber (map-hom-slice f (map-emb i) q) b))) - ( pair g is-emb-g)) - ( pair (map-unit-im (pr1 q)) (pr2 q)) + ( g , is-emb-g)) + ( map-unit-im (pr1 q) , pr2 q) β : type-trunc-Prop (fiber (map-hom-slice f (map-emb i) q) (pr1 (pr1 α b))) β = pr2 (pr1 α b) γ : fiber (map-hom-slice f (map-emb i) q) (pr1 (pr1 α b)) → type-Prop (trunc-Prop (fiber (pr1 q) b)) - γ (pair a p) = + γ (a , p) = unit-trunc-Prop - ( pair a (p ∙ inv (is-injective-is-emb (is-emb-map-emb i) (pr2 α b)))) + ( a , p ∙ inv (is-injective-is-emb (is-emb-map-emb i) (pr2 α b))) abstract is-image-is-surjective' : @@ -322,19 +320,18 @@ abstract is-image-is-surjective' f i q H B' m = map-equiv ( ( equiv-hom-slice-fiberwise-hom (map-emb i) (map-emb m)) ∘e - ( ( inv-equiv (reduce-Π-fiber (map-emb i) (fiber (map-emb m)))) ∘e - ( inv-equiv - ( equiv-dependent-universal-property-surj-is-surjective - ( pr1 q) - ( H) - ( λ b → - pair - ( fiber (map-emb m) (pr1 i b)) - ( is-prop-map-emb m (pr1 i b)))) ∘e - ( ( equiv-Π-equiv-family - ( λ a → equiv-tr (fiber (map-emb m)) (pr2 q a))) ∘e - ( ( reduce-Π-fiber f (fiber (map-emb m))) ∘e - ( equiv-fiberwise-hom-hom-slice f (map-emb m))))))) + ( inv-equiv (reduce-Π-fiber (map-emb i) (fiber (map-emb m)))) ∘e + ( inv-equiv + ( equiv-dependent-universal-property-surj-is-surjective + ( pr1 q) + ( H) + ( λ b → + ( fiber (map-emb m) (pr1 i b)) , + ( is-prop-map-emb m (pr1 i b))))) ∘e + ( equiv-Π-equiv-family + ( λ a → equiv-tr (fiber (map-emb m)) (pr2 q a))) ∘e + ( reduce-Π-fiber f (fiber (map-emb m))) ∘e + ( equiv-fiberwise-hom-hom-slice f (map-emb m))) abstract is-image-is-surjective : @@ -342,7 +339,6 @@ abstract (f : A → X) (i : B ↪ X) (q : hom-slice f (map-emb i)) → is-surjective (map-hom-slice f (map-emb i) q) → is-image f i q - is-image-is-surjective f i q H {l} = - is-image-is-image' f i q - ( is-image-is-surjective' f i q H) + is-image-is-surjective f i q H = + is-image-is-image' f i q (is-image-is-surjective' f i q H) ``` From 07a5cee1b50fa3dc3c56eebfefbb90633c681c64 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 19:06:23 +0100 Subject: [PATCH 04/16] refactor universal property of sequential limits --- src/foundation/sequential-limits.lagda.md | 7 ++-- ...versal-property-sequential-limits.lagda.md | 38 ++++++++++--------- 2 files changed, 24 insertions(+), 21 deletions(-) diff --git a/src/foundation/sequential-limits.lagda.md b/src/foundation/sequential-limits.lagda.md index 9a340a834a..8a7ed26027 100644 --- a/src/foundation/sequential-limits.lagda.md +++ b/src/foundation/sequential-limits.lagda.md @@ -229,8 +229,7 @@ module _ is-section-gap-tower x = refl universal-property-standard-sequential-limit : - {l : Level} → - universal-property-sequential-limit l A (cone-standard-sequential-limit A) + universal-property-sequential-limit A (cone-standard-sequential-limit A) pr1 (pr1 (universal-property-standard-sequential-limit X)) = gap-tower A pr2 (pr1 (universal-property-standard-sequential-limit X)) = is-section-gap-tower @@ -264,7 +263,7 @@ module _ is-sequential-limit-universal-property-sequential-limit : (c : cone-tower A X) → - ({l : Level} → universal-property-sequential-limit l A c) → + universal-property-sequential-limit A c → is-sequential-limit A c is-sequential-limit-universal-property-sequential-limit c = is-equiv-universal-property-sequential-limit-universal-property-sequential-limit @@ -276,7 +275,7 @@ module _ universal-property-is-sequential-limit : (c : cone-tower A X) → is-sequential-limit A c → - {l : Level} → universal-property-sequential-limit l A c + universal-property-sequential-limit A c universal-property-is-sequential-limit c is-lim-c = universal-property-sequential-limit-universal-property-sequential-limit-is-equiv ( cone-standard-sequential-limit A) diff --git a/src/foundation/universal-property-sequential-limits.lagda.md b/src/foundation/universal-property-sequential-limits.lagda.md index 2b5d63cb8d..ba36f88ca8 100644 --- a/src/foundation/universal-property-sequential-limits.lagda.md +++ b/src/foundation/universal-property-sequential-limits.lagda.md @@ -56,26 +56,30 @@ that cone as a composite of `g` with the cone of `limₙ Aₙ` over `A`. ```agda module _ - {l1 l2 : Level} (l : Level) (A : tower l1) {X : UU l2} + {l1 l2 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X) where - universal-property-sequential-limit : - (c : cone-tower A X) → UU (l1 ⊔ l2 ⊔ lsuc l) - universal-property-sequential-limit c = + universal-property-sequential-limit-Level : + (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) + universal-property-sequential-limit-Level l = (Y : UU l) → is-equiv (cone-map-tower A {Y = Y} c) + universal-property-sequential-limit : UUω + universal-property-sequential-limit = + {l : Level} → universal-property-sequential-limit-Level l + module _ {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X) where map-universal-property-sequential-limit : - ({l : Level} → universal-property-sequential-limit l A c) → + universal-property-sequential-limit A c → {Y : UU l3} (c' : cone-tower A Y) → Y → X map-universal-property-sequential-limit up-c {Y} c' = map-inv-is-equiv (up-c Y) c' compute-map-universal-property-sequential-limit : - (up-c : {l : Level} → universal-property-sequential-limit l A c) → + (up-c : universal-property-sequential-limit A c) → {Y : UU l3} (c' : cone-tower A Y) → cone-map-tower A c (map-universal-property-sequential-limit up-c c') ＝ c' compute-map-universal-property-sequential-limit up-c {Y} c' = @@ -109,8 +113,8 @@ module _ abstract is-equiv-universal-property-sequential-limit-universal-property-sequential-limit : - ({l : Level} → universal-property-sequential-limit l A c) → - ({l : Level} → universal-property-sequential-limit l A c') → + universal-property-sequential-limit A c → + universal-property-sequential-limit A c' → is-equiv h is-equiv-universal-property-sequential-limit-universal-property-sequential-limit up up' = @@ -127,8 +131,8 @@ module _ abstract universal-property-sequential-limit-universal-property-sequential-limit-is-equiv : is-equiv h → - ({l : Level} → universal-property-sequential-limit l A c) → - ({l : Level} → universal-property-sequential-limit l A c') + universal-property-sequential-limit A c → + universal-property-sequential-limit A c' universal-property-sequential-limit-universal-property-sequential-limit-is-equiv is-equiv-h up D = is-equiv-left-map-triangle @@ -141,9 +145,9 @@ module _ abstract universal-property-sequential-limit-is-equiv-universal-property-sequential-limit : - ({l : Level} → universal-property-sequential-limit l A c') → + universal-property-sequential-limit A c' → is-equiv h → - ({l : Level} → universal-property-sequential-limit l A c) + universal-property-sequential-limit A c universal-property-sequential-limit-is-equiv-universal-property-sequential-limit up' is-equiv-h D = is-equiv-right-map-triangle @@ -164,7 +168,7 @@ module _ abstract uniqueness-universal-property-sequential-limit : - ({l : Level} → universal-property-sequential-limit l A c) → + universal-property-sequential-limit A c → {l3 : Level} (Y : UU l3) (c' : cone-tower A Y) → is-contr (Σ (Y → X) (λ h → htpy-cone-tower A (cone-map-tower A c h) c')) uniqueness-universal-property-sequential-limit up Y c' = @@ -184,7 +188,7 @@ module _ abstract is-prop-universal-property-sequential-limit : - is-prop (universal-property-sequential-limit l3 A c) + is-prop (universal-property-sequential-limit-Level A c l3) is-prop-universal-property-sequential-limit = is-prop-Π (λ Y → is-property-is-equiv (cone-map-tower A c)) ``` @@ -198,7 +202,7 @@ module _ htpy-cone-map-universal-property-sequential-limit : (c : cone-tower A X) - (up : {l : Level} → universal-property-sequential-limit l A c) → + (up : universal-property-sequential-limit A c) → {l3 : Level} {Y : UU l3} (c' : cone-tower A Y) → htpy-cone-tower A ( cone-map-tower A c (map-universal-property-sequential-limit A c up c')) @@ -220,8 +224,8 @@ module _ abstract uniquely-unique-sequential-limit : ( c' : cone-tower A Y) (c : cone-tower A X) → - ( up-c' : {l : Level} → universal-property-sequential-limit l A c') → - ( up-c : {l : Level} → universal-property-sequential-limit l A c) → + ( up-c' : universal-property-sequential-limit A c') → + ( up-c : universal-property-sequential-limit A c) → is-contr ( Σ (Y ≃ X) ( λ e → htpy-cone-tower A (cone-map-tower A c (map-equiv e)) c')) From a6737875dcf08cc9d22da0db5dc32091a1054c67 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 19:24:27 +0100 Subject: [PATCH 05/16] refactor universal properties of propositional truncations --- .../propositional-truncations.lagda.md | 16 +- src/foundation/surjective-maps.lagda.md | 5 +- ...property-propositional-truncation.lagda.md | 183 ++++++++++-------- 3 files changed, 116 insertions(+), 88 deletions(-) diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md index 5bf838a3a7..8e0c239e69 100644 --- a/src/foundation/propositional-truncations.lagda.md +++ b/src/foundation/propositional-truncations.lagda.md @@ -119,13 +119,13 @@ abstract ```agda abstract is-propositional-truncation-trunc-Prop : - {l1 l2 : Level} (A : UU l1) → - is-propositional-truncation l2 (trunc-Prop A) unit-trunc-Prop + {l : Level} (A : UU l) → + is-propositional-truncation (trunc-Prop A) unit-trunc-Prop is-propositional-truncation-trunc-Prop A = is-propositional-truncation-extension-property ( trunc-Prop A) ( unit-trunc-Prop) - ( λ {l} Q → ind-trunc-Prop (λ x → Q)) + ( λ Q → ind-trunc-Prop (λ x → Q)) ``` ### The defined propositional truncations satisfy the universal property of propositional truncations @@ -133,12 +133,12 @@ abstract ```agda abstract universal-property-trunc-Prop : - {l1 l2 : Level} (A : UU l1) → - universal-property-propositional-truncation l2 + {l : Level} (A : UU l) → + universal-property-propositional-truncation ( trunc-Prop A) ( unit-trunc-Prop) universal-property-trunc-Prop A = - universal-property-is-propositional-truncation _ + universal-property-is-propositional-truncation ( trunc-Prop A) ( unit-trunc-Prop) ( is-propositional-truncation-trunc-Prop A) @@ -254,8 +254,8 @@ module _ ```agda abstract dependent-universal-property-trunc-Prop : - {l1 : Level} {A : UU l1} {l : Level} → - dependent-universal-property-propositional-truncation l + {l : Level} {A : UU l} → + dependent-universal-property-propositional-truncation ( trunc-Prop A) ( unit-trunc-Prop) dependent-universal-property-trunc-Prop {A = A} = diff --git a/src/foundation/surjective-maps.lagda.md b/src/foundation/surjective-maps.lagda.md index 61bd607522..d672423644 100644 --- a/src/foundation/surjective-maps.lagda.md +++ b/src/foundation/surjective-maps.lagda.md @@ -393,8 +393,7 @@ apply-dependent-universal-property-surjection f = abstract is-surjective-is-propositional-truncation : {l1 l2 : Level} {A : UU l1} {P : Prop l2} (f : A → type-Prop P) → - ( {l : Level} → - dependent-universal-property-propositional-truncation l P f) → + dependent-universal-property-propositional-truncation P f → is-surjective f is-surjective-is-propositional-truncation f duppt-f = is-surjective-dependent-universal-property-surj f duppt-f @@ -403,7 +402,7 @@ abstract is-propsitional-truncation-is-surjective : {l1 l2 : Level} {A : UU l1} {P : Prop l2} (f : A → type-Prop P) → is-surjective f → - {l : Level} → dependent-universal-property-propositional-truncation l P f + dependent-universal-property-propositional-truncation P f is-propsitional-truncation-is-surjective f is-surj-f = dependent-universal-property-surj-is-surjective f is-surj-f ``` diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index c35a668fcd..47521315af 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -35,38 +35,53 @@ open import foundation-core.type-theoretic-principle-of-choice ## Idea -A map `f : A → P` into a proposition `P` is said to satisfy the universal -property of the propositional truncation of `A`, or is said to be a -propositional truncation of `A`, if any map `g : A → Q` into a proposition `Q` -extends uniquely along `f`. +A map `f : A → P` into a [proposition](foundation-core.propositions.md) `P` is +said to satisfy the **universal property of the propositional truncation** of +`A`, or is said to be a **propositional truncation** of `A`, if any map +`g : A → Q` into a proposition `Q` extends uniquely along `f`. ## Definition ### The condition of being a propositional truncation ```agda -precomp-Prop : - { l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) → - (A → type-Prop P) → (Q : Prop l3) → - (type-hom-Prop P Q) → (A → type-Prop Q) -precomp-Prop P f Q g = g ∘ f - -is-propositional-truncation : - ( l : Level) {l1 l2 : Level} {A : UU l1} (P : Prop l2) → - ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2) -is-propositional-truncation l P f = - (Q : Prop l) → is-equiv (precomp-Prop P f Q) +module _ + {l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) + where + + precomp-Prop : + {l3 : Level} (Q : Prop l3) → + type-hom-Prop P Q → A → type-Prop Q + precomp-Prop Q g = g ∘ f + + is-propositional-truncation-Level : + ( l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + is-propositional-truncation-Level l = + (Q : Prop l) → is-equiv (precomp-Prop Q) + + is-propositional-truncation : UUω + is-propositional-truncation = + {l : Level} → is-propositional-truncation-Level l ``` ### The universal property of the propositional truncation ```agda -universal-property-propositional-truncation : - ( l : Level) {l1 l2 : Level} {A : UU l1} - (P : Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2) -universal-property-propositional-truncation l {A = A} P f = - (Q : Prop l) (g : A → type-Prop Q) → - is-contr (Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g)) +module _ + {l1 l2 : Level} {A : UU l1} + (P : Prop l2) (f : A → type-Prop P) + where + + universal-property-propositional-truncation-Level : + (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + universal-property-propositional-truncation-Level l = + (Q : Prop l) (g : A → type-Prop Q) → + is-contr (Σ (type-hom-Prop P Q) (λ h → h ∘ f ~ g)) + + universal-property-propositional-truncation : UUω + universal-property-propositional-truncation = + {l : Level} → universal-property-propositional-truncation-Level l + ``` ### Extension property of the propositional truncation @@ -75,21 +90,37 @@ This is a simplified form of the universal properties, that works because we're mapping into propositions. ```agda -extension-property-propositional-truncation : - ( l : Level) {l1 l2 : Level} {A : UU l1} (P : Prop l2) → - ( A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2) -extension-property-propositional-truncation l {A = A} P f = - (Q : Prop l) → (A → type-Prop Q) → (type-hom-Prop P Q) +module _ + {l1 l2 : Level} {A : UU l1} + (P : Prop l2) (f : A → type-Prop P) + where + + extension-property-propositional-truncation-Level : + (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + extension-property-propositional-truncation-Level l = + (Q : Prop l) → (A → type-Prop Q) → type-hom-Prop P Q + + extension-property-propositional-truncation : UUω + extension-property-propositional-truncation = + {l : Level} → extension-property-propositional-truncation-Level l ``` ### The dependent universal property of the propositional truncation ```agda -dependent-universal-property-propositional-truncation : - ( l : Level) {l1 l2 : Level} {A : UU l1} - ( P : Prop l2) (f : A → type-Prop P) → UU (lsuc l ⊔ l1 ⊔ l2) -dependent-universal-property-propositional-truncation l {l1} {l2} {A} P f = - ( Q : type-Prop P → Prop l) → is-equiv (precomp-Π f (type-Prop ∘ Q)) +module _ + {l1 l2 : Level} {A : UU l1} + (P : Prop l2) (f : A → type-Prop P) + where + + dependent-universal-property-propositional-truncation-Level : + (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + dependent-universal-property-propositional-truncation-Level l = + ( Q : type-Prop P → Prop l) → is-equiv (precomp-Π f (type-Prop ∘ Q)) + + dependent-universal-property-propositional-truncation : UUω + dependent-universal-property-propositional-truncation = + {l : Level} → dependent-universal-property-propositional-truncation-Level l ``` ## Properties @@ -99,43 +130,42 @@ dependent-universal-property-propositional-truncation l {l1} {l2} {A} P f = ```agda abstract universal-property-is-propositional-truncation : - (l : Level) {l1 l2 : Level} {A : UU l1} - (P : Prop l2) (f : A → type-Prop P) → - is-propositional-truncation l P f → - universal-property-propositional-truncation l P f - universal-property-is-propositional-truncation l P f is-ptr-f Q g = + {l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → + is-propositional-truncation P f → + universal-property-propositional-truncation P f + universal-property-is-propositional-truncation P f is-ptr-f Q g = is-contr-equiv' - ( Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ＝ g)) - ( equiv-tot (λ h → equiv-funext)) + ( Σ (type-hom-Prop P Q) (λ h → h ∘ f ＝ g)) + ( equiv-tot (λ _ → equiv-funext)) ( is-contr-map-is-equiv (is-ptr-f Q) g) abstract map-is-propositional-truncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - ({l : Level} → is-propositional-truncation l P f) → + is-propositional-truncation P f → (Q : Prop l3) (g : A → type-Prop Q) → type-hom-Prop P Q map-is-propositional-truncation P f is-ptr-f Q g = pr1 ( center - ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g)) + ( universal-property-is-propositional-truncation P f is-ptr-f Q g)) htpy-is-propositional-truncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - (is-ptr-f : {l : Level} → is-propositional-truncation l P f) → + (is-ptr-f : is-propositional-truncation P f) → (Q : Prop l3) (g : A → type-Prop Q) → ((map-is-propositional-truncation P f is-ptr-f Q g) ∘ f) ~ g htpy-is-propositional-truncation P f is-ptr-f Q g = pr2 ( center - ( universal-property-is-propositional-truncation _ P f is-ptr-f Q g)) + ( universal-property-is-propositional-truncation P f is-ptr-f Q g)) abstract is-propositional-truncation-universal-property : - (l : Level) {l1 l2 : Level} {A : UU l1} + {l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - universal-property-propositional-truncation l P f → - is-propositional-truncation l P f - is-propositional-truncation-universal-property l P f up-f Q = + universal-property-propositional-truncation P f → + is-propositional-truncation P f + is-propositional-truncation-universal-property P f up-f Q = is-equiv-is-contr-map ( λ g → is-contr-equiv ( Σ (type-hom-Prop P Q) (λ h → (h ∘ f) ~ g)) @@ -150,9 +180,9 @@ abstract is-propositional-truncation-extension-property : { l1 l2 : Level} {A : UU l1} (P : Prop l2) ( f : A → type-Prop P) → - ( {l : Level} → extension-property-propositional-truncation l P f) → - ( {l : Level} → is-propositional-truncation l P f) - is-propositional-truncation-extension-property P f up-P {l} Q = + extension-property-propositional-truncation P f → + is-propositional-truncation P f + is-propositional-truncation-extension-property P f up-P Q = is-equiv-is-prop ( is-prop-Π (λ x → is-prop-type-Prop Q)) ( is-prop-Π (λ x → is-prop-type-Prop Q)) @@ -167,8 +197,8 @@ abstract {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') (H : (h ∘ f) ~ f') → - ({l : Level} → is-propositional-truncation l P f) → - ({l : Level} → is-propositional-truncation l P' f') → + is-propositional-truncation P f → + is-propositional-truncation P' f' → is-equiv h is-equiv-is-ptruncation-is-ptruncation P P' f f' h H is-ptr-P is-ptr-P' = is-equiv-is-prop @@ -180,8 +210,8 @@ abstract is-ptruncation-is-ptruncation-is-equiv : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') → - is-equiv h → ({l : Level} → is-propositional-truncation l P f) → - ({l : Level} → is-propositional-truncation l P' f') + is-equiv h → (is-propositional-truncation P f) → + (is-propositional-truncation P' f') is-ptruncation-is-ptruncation-is-equiv P P' f f' h is-equiv-h is-ptr-f = is-propositional-truncation-extension-property P' f' ( λ R g → @@ -192,8 +222,8 @@ abstract is-ptruncation-is-equiv-is-ptruncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') → - ({l : Level} → is-propositional-truncation l P' f') → is-equiv h → - ({l : Level} → is-propositional-truncation l P f) + (is-propositional-truncation P' f') → is-equiv h → + (is-propositional-truncation P f) is-ptruncation-is-equiv-is-ptruncation P P' f f' h is-ptr-f' is-equiv-h = is-propositional-truncation-extension-property P f ( λ R g → (map-is-propositional-truncation P' f' is-ptr-f' R g) ∘ h) @@ -202,12 +232,12 @@ abstract is-uniquely-unique-propositional-truncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') → - ({l : Level} → is-propositional-truncation l P f) → - ({l : Level} → is-propositional-truncation l P' f') → + (is-propositional-truncation P f) → + (is-propositional-truncation P' f') → is-contr (Σ (type-equiv-Prop P P') (λ e → (map-equiv e ∘ f) ~ f')) is-uniquely-unique-propositional-truncation P P' f f' is-ptr-f is-ptr-f' = is-torsorial-Eq-subtype - ( universal-property-is-propositional-truncation _ P f is-ptr-f P' f') + ( universal-property-is-propositional-truncation P f is-ptr-f P' f') ( is-property-is-equiv) ( map-is-propositional-truncation P f is-ptr-f P' f') ( htpy-is-propositional-truncation P f is-ptr-f P' f') @@ -224,8 +254,8 @@ abstract abstract dependent-universal-property-is-propositional-truncation : { l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - ( {l : Level} → is-propositional-truncation l P f) → - ( {l : Level} → dependent-universal-property-propositional-truncation l P f) + is-propositional-truncation P f → + dependent-universal-property-propositional-truncation P f dependent-universal-property-is-propositional-truncation {l1} {l2} {A} P f is-ptr-f Q = is-fiberwise-equiv-is-equiv-map-Σ @@ -252,9 +282,8 @@ abstract abstract is-propositional-truncation-dependent-universal-property : { l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - ( {l : Level} → - dependent-universal-property-propositional-truncation l P f) → - ( {l : Level} → is-propositional-truncation l P f) + dependent-universal-property-propositional-truncation P f → + is-propositional-truncation P f is-propositional-truncation-dependent-universal-property P f dup-f Q = dup-f (λ p → Q) ``` @@ -264,8 +293,8 @@ abstract ```agda abstract is-propositional-truncation-has-section : - {l l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → - (g : type-Prop P → A) → is-propositional-truncation l P f + {l1 l2 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → + (g : type-Prop P → A) → is-propositional-truncation P f is-propositional-truncation-has-section {A = A} P f g Q = is-equiv-is-prop ( is-prop-function-type (is-prop-type-Prop Q)) @@ -278,8 +307,8 @@ abstract ```agda abstract is-propositional-truncation-terminal-map : - { l l1 : Level} (A : UU l1) (a : A) → - is-propositional-truncation l unit-Prop (terminal-map {A = A}) + { l1 : Level} (A : UU l1) (a : A) → + is-propositional-truncation unit-Prop (terminal-map {A = A}) is-propositional-truncation-terminal-map A a = is-propositional-truncation-has-section ( unit-Prop) @@ -292,9 +321,9 @@ abstract ```agda abstract is-propositional-truncation-is-equiv : - {l l1 l2 : Level} (P : Prop l1) (Q : Prop l2) + {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) {f : type-hom-Prop P Q} → - is-equiv f → is-propositional-truncation l Q f + is-equiv f → is-propositional-truncation Q f is-propositional-truncation-is-equiv P Q {f} is-equiv-f R = is-equiv-precomp-is-equiv f is-equiv-f (type-Prop R) @@ -302,14 +331,14 @@ abstract is-propositional-truncation-map-equiv : { l1 l2 : Level} (P : Prop l1) (Q : Prop l2) (e : type-equiv-Prop P Q) → - ( l : Level) → is-propositional-truncation l Q (map-equiv e) - is-propositional-truncation-map-equiv P Q e l R = + is-propositional-truncation Q (map-equiv e) + is-propositional-truncation-map-equiv P Q e R = is-equiv-precomp-is-equiv (map-equiv e) (is-equiv-map-equiv e) (type-Prop R) abstract is-equiv-is-propositional-truncation : {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) {f : type-hom-Prop P Q} → - ({l : Level} → is-propositional-truncation l Q f) → is-equiv f + (is-propositional-truncation Q f) → is-equiv f is-equiv-is-propositional-truncation P Q {f} H = is-equiv-is-equiv-precomp-Prop P Q f H ``` @@ -320,8 +349,8 @@ abstract abstract is-propositional-truncation-id : { l1 : Level} (P : Prop l1) → - ( l : Level) → is-propositional-truncation l P id - is-propositional-truncation-id P l Q = is-equiv-id + is-propositional-truncation P id + is-propositional-truncation-id P Q = is-equiv-id ``` ### A product of propositional truncations is a propositional truncation @@ -332,9 +361,9 @@ abstract {l1 l2 l3 l4 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) {A' : UU l3} (P' : Prop l4) (f' : A' → type-Prop P') → - ({l : Level} → is-propositional-truncation l P f) → - ({l : Level} → is-propositional-truncation l P' f') → - {l : Level} → is-propositional-truncation l (prod-Prop P P') (map-prod f f') + (is-propositional-truncation P f) → + (is-propositional-truncation P' f') → + is-propositional-truncation (prod-Prop P P') (map-prod f f') is-propositional-truncation-prod P f P' f' is-ptr-f is-ptr-f' Q = is-equiv-top-is-equiv-bottom-square ( ev-pair) From 3f1c96535ae3397dceb66297ee755eeaeba7cbf8 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 19:43:21 +0100 Subject: [PATCH 06/16] refactor pullback stable function classes --- .../function-classes.lagda.md | 29 +++++++++---------- .../global-function-classes.lagda.md | 12 ++++---- ...-orthogonal-factorization-systems.lagda.md | 9 +++--- 3 files changed, 24 insertions(+), 26 deletions(-) diff --git a/src/orthogonal-factorization-systems/function-classes.lagda.md b/src/orthogonal-factorization-systems/function-classes.lagda.md index 9beecb93fb..0a411e2f64 100644 --- a/src/orthogonal-factorization-systems/function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/function-classes.lagda.md @@ -165,17 +165,17 @@ module _ {l1 l2 l3 : Level} (P : function-class l1 l2 l3) where - is-pullback-stable-function-class-Level : - (l : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ l3 ⊔ lsuc l) - is-pullback-stable-function-class-Level l = + is-pullback-stable-function-class : + UU (lsuc l1 ⊔ lsuc l2 ⊔ l3) + is-pullback-stable-function-class = {A : UU l1} {B C : UU l2} (f : A → C) (g : B → C) - (p : Σ (UU l1) (pullback-cone l f g)) → + (p : Σ (UU l1) (pullback-cone f g)) → is-in-function-class P f → is-in-function-class P (horizontal-map-pullback-cone f g (pr2 p)) is-prop-is-pullback-stable-function-class : - (l : Level) → is-prop (is-pullback-stable-function-class-Level l) - is-prop-is-pullback-stable-function-class l = + is-prop (is-pullback-stable-function-class) + is-prop-is-pullback-stable-function-class = is-prop-iterated-implicit-Π 3 ( λ A B C → is-prop-iterated-Π 4 @@ -183,18 +183,17 @@ module _ is-prop-is-in-function-class P ( horizontal-map-pullback-cone f g (pr2 p)))) - is-pullback-stable-function-class-Prop : - (l : Level) → Prop (lsuc l1 ⊔ lsuc l2 ⊔ l3 ⊔ lsuc l) - pr1 (is-pullback-stable-function-class-Prop l) = - is-pullback-stable-function-class-Level l - pr2 (is-pullback-stable-function-class-Prop l) = - is-prop-is-pullback-stable-function-class l + is-pullback-stable-function-class-Prop : Prop (lsuc l1 ⊔ lsuc l2 ⊔ l3) + pr1 is-pullback-stable-function-class-Prop = + is-pullback-stable-function-class + pr2 is-pullback-stable-function-class-Prop = + is-prop-is-pullback-stable-function-class pullback-stable-function-class : - (l1 l2 l3 l4 : Level) → UU (lsuc (l1 ⊔ l2 ⊔ l3 ⊔ l4)) -pullback-stable-function-class l1 l2 l3 l4 = + (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) +pullback-stable-function-class l1 l2 l3 = Σ ( function-class l1 l2 l3) - ( λ P → is-pullback-stable-function-class-Level P l4) + ( is-pullback-stable-function-class) ``` ## Properties diff --git a/src/orthogonal-factorization-systems/global-function-classes.lagda.md b/src/orthogonal-factorization-systems/global-function-classes.lagda.md index 39fd85f212..4e1999c89c 100644 --- a/src/orthogonal-factorization-systems/global-function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/global-function-classes.lagda.md @@ -190,18 +190,18 @@ module _ where is-pullback-stable-global-function-class-Level : - (l1 l2 l3 l4 l5 : Level) → - UU (β l1 l3 ⊔ β l4 l2 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3 ⊔ lsuc l4 ⊔ lsuc l5) - is-pullback-stable-global-function-class-Level l1 l2 l3 l4 l5 = + (l1 l2 l3 l4 : Level) → + UU (β l1 l3 ⊔ β l4 l2 ⊔ lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3 ⊔ lsuc l4) + is-pullback-stable-global-function-class-Level l1 l2 l3 l4 = {A : UU l1} {B : UU l2} {C : UU l3} (f : A → C) (g : B → C) - (c : Σ (UU l4) (pullback-cone l5 f g)) → + (c : Σ (UU l4) (pullback-cone f g)) → is-in-global-function-class P f → is-in-global-function-class P (horizontal-map-pullback-cone f g (pr2 c)) is-pullback-stable-global-function-class : UUω is-pullback-stable-global-function-class = - {l1 l2 l3 l4 l5 : Level} → - is-pullback-stable-global-function-class-Level l1 l2 l3 l4 l5 + {l1 l2 l3 l4 : Level} → + is-pullback-stable-global-function-class-Level l1 l2 l3 l4 ``` ## Properties diff --git a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md index bb7bfe35ea..7a42c85792 100644 --- a/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md +++ b/src/orthogonal-factorization-systems/stable-orthogonal-factorization-systems.lagda.md @@ -28,12 +28,11 @@ pullbacks. ```agda is-stable-orthogonal-factorization-system : - {l1 lL lR : Level} (l2 : Level) → - orthogonal-factorization-system l1 lL lR → UU (lsuc l1 ⊔ lL ⊔ lsuc l2) -is-stable-orthogonal-factorization-system l2 OFS = - is-pullback-stable-function-class-Level + {l1 lL lR : Level} → + orthogonal-factorization-system l1 lL lR → UU (lsuc l1 ⊔ lL) +is-stable-orthogonal-factorization-system OFS = + is-pullback-stable-function-class ( left-class-orthogonal-factorization-system OFS) - ( l2) ``` ## See also From 043ac2af6906d7eea6e9d33413254ac5c2fc886a Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 2 Dec 2023 20:01:45 +0100 Subject: [PATCH 07/16] refactor universal property of truncations --- .../universal-property-truncation.lagda.md | 102 +++++++++++------- src/foundation/truncations.lagda.md | 13 ++- src/foundation/uniqueness-truncation.lagda.md | 4 +- ...ropositional-truncation-into-sets.lagda.md | 29 +++-- ...property-propositional-truncation.lagda.md | 1 - .../universal-property-truncation.lagda.md | 9 +- .../function-classes.lagda.md | 3 +- 7 files changed, 88 insertions(+), 73 deletions(-) diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md index a4840faef6..b4d31f1e4c 100644 --- a/src/foundation-core/universal-property-truncation.lagda.md +++ b/src/foundation-core/universal-property-truncation.lagda.md @@ -46,33 +46,46 @@ precomp-Trunc : (B → type-Truncated-Type C) → (A → type-Truncated-Type C) precomp-Trunc f C = precomp f (type-Truncated-Type C) -is-truncation : - (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1} - (B : Truncated-Type l2 k) → (A → type-Truncated-Type B) → - UU (l1 ⊔ l2 ⊔ lsuc l) -is-truncation l {k = k} B f = - (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C) - -equiv-is-truncation : - {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k) - (f : A → type-Truncated-Type B) - (H : {l : Level} → is-truncation l B f) → - (C : Truncated-Type l3 k) → - (type-Truncated-Type B → type-Truncated-Type C) ≃ (A → type-Truncated-Type C) -pr1 (equiv-is-truncation B f H C) = precomp-Trunc f C -pr2 (equiv-is-truncation B f H C) = H C +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} + (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) + where + + is-truncation-Level : + (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) + is-truncation-Level l = + (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C) + + is-truncation : UUω + is-truncation = {l : Level} → is-truncation-Level l + + equiv-is-truncation : + {l3 : Level} + (H : is-truncation) → + (C : Truncated-Type l3 k) → + ( type-Truncated-Type B → type-Truncated-Type C) ≃ + ( A → type-Truncated-Type C) + pr1 (equiv-is-truncation H C) = precomp-Trunc f C + pr2 (equiv-is-truncation H C) = H C ``` ### The universal property of truncations ```agda -universal-property-truncation : - (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1} - (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) → - UU (lsuc l ⊔ l1 ⊔ l2) -universal-property-truncation l {k = k} {A} B f = - (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → - is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ~ g)) +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} + (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) + where + + universal-property-truncation-Level : + (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) + universal-property-truncation-Level l = + (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → + is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g)) + + universal-property-truncation : UUω + universal-property-truncation = + {l : Level} → universal-property-truncation-Level l ``` ### The dependent universal property of truncations @@ -85,12 +98,20 @@ precomp-Π-Truncated-Type : ((a : A) → type-Truncated-Type (C (f a))) precomp-Π-Truncated-Type f C h a = h (f a) -dependent-universal-property-truncation : - {l1 l2 : Level} (l : Level) {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k) - (f : A → type-Truncated-Type B) → UU (l1 ⊔ l2 ⊔ lsuc l) -dependent-universal-property-truncation l {k} B f = - (X : type-Truncated-Type B → Truncated-Type l k) → - is-equiv (precomp-Π-Truncated-Type f X) +module _ + {l1 l2 : Level} {k : 𝕋} {A : UU l1} + (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) + where + + dependent-universal-property-truncation-Level : + (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) + dependent-universal-property-truncation-Level l = + (X : type-Truncated-Type B → Truncated-Type l k) → + is-equiv (precomp-Π-Truncated-Type f X) + + dependent-universal-property-truncation : UUω + dependent-universal-property-truncation = + {l : Level} → dependent-universal-property-truncation-Level l ``` ## Properties @@ -101,7 +122,7 @@ dependent-universal-property-truncation l {k} B f = abstract is-truncation-id : {l1 : Level} {k : 𝕋} {A : UU l1} (H : is-trunc k A) → - {l : Level} → is-truncation l (A , H) id + is-truncation (A , H) id is-truncation-id H B = is-equiv-precomp-is-equiv id is-equiv-id (type-Truncated-Type B) @@ -109,7 +130,7 @@ abstract is-truncation-equiv : {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k) (e : A ≃ type-Truncated-Type B) → - {l : Level} → is-truncation l B (map-equiv e) + is-truncation B (map-equiv e) is-truncation-equiv B e C = is-equiv-precomp-is-equiv ( map-equiv e) @@ -127,8 +148,8 @@ module _ abstract is-truncation-universal-property-truncation : - ({l : Level} → universal-property-truncation l B f) → - ({l : Level} → is-truncation l B f) + universal-property-truncation B f → + is-truncation B f is-truncation-universal-property-truncation H C = is-equiv-is-contr-map ( λ g → @@ -139,8 +160,7 @@ module _ abstract universal-property-truncation-is-truncation : - ({l : Level} → is-truncation l B f) → - ({l : Level} → universal-property-truncation l B f) + is-truncation B f → universal-property-truncation B f universal-property-truncation-is-truncation H C g = is-contr-equiv' ( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ＝ g)) @@ -148,14 +168,14 @@ module _ ( is-contr-map-is-equiv (H C) g) map-is-truncation : - ({l : Level} → is-truncation l B f) → + (is-truncation B f) → ({l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → type-hom-Truncated-Type k B C) map-is-truncation H C g = pr1 (center (universal-property-truncation-is-truncation H C g)) triangle-is-truncation : - (H : {l : Level} → is-truncation l B f) → + (H : is-truncation B f) → {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → (map-is-truncation H C g ∘ f) ~ g triangle-is-truncation H C g = @@ -172,8 +192,8 @@ module _ abstract dependent-universal-property-truncation-is-truncation : - ({l : Level} → is-truncation l B f) → - {l : Level} → dependent-universal-property-truncation l B f + (is-truncation B f) → + dependent-universal-property-truncation B f dependent-universal-property-truncation-is-truncation H X = is-fiberwise-equiv-is-equiv-map-Σ ( λ (h : A → type-Truncated-Type B) → @@ -191,13 +211,13 @@ module _ abstract is-truncation-dependent-universal-property-truncation : - ({l : Level} → dependent-universal-property-truncation l B f) → - {l : Level} → is-truncation l B f + (dependent-universal-property-truncation B f) → + is-truncation B f is-truncation-dependent-universal-property-truncation H X = H (λ b → X) section-is-truncation : - ({l : Level} → is-truncation l B f) → + (is-truncation B f) → {l3 : Level} (C : Truncated-Type l3 k) (h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) → f ~ (g ∘ h) → section g diff --git a/src/foundation/truncations.lagda.md b/src/foundation/truncations.lagda.md index de56d45512..506c51c962 100644 --- a/src/foundation/truncations.lagda.md +++ b/src/foundation/truncations.lagda.md @@ -57,8 +57,8 @@ postulate postulate is-truncation-trunc : - {l1 l2 : Level} {k : 𝕋} {A : UU l1} → - is-truncation l2 (trunc k A) unit-trunc + {l : Level} {k : 𝕋} {A : UU l} → + is-truncation (trunc k A) unit-trunc equiv-universal-property-trunc : {l1 l2 : Level} {k : 𝕋} (A : UU l1) (B : Truncated-Type l2 k) → @@ -74,7 +74,7 @@ pr2 (equiv-universal-property-trunc A B) = is-truncation-trunc B ```agda universal-property-trunc : {l1 : Level} (k : 𝕋) (A : UU l1) → - {l2 : Level} → universal-property-truncation l2 (trunc k A) unit-trunc + universal-property-truncation (trunc k A) unit-trunc universal-property-trunc k A = universal-property-truncation-is-truncation ( trunc k A) @@ -88,7 +88,7 @@ module _ apply-universal-property-trunc : (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) → Σ ( type-trunc k A → type-Truncated-Type B) - ( λ h → (h ∘ unit-trunc) ~ f) + ( λ h → h ∘ unit-trunc ~ f) apply-universal-property-trunc B f = center ( universal-property-truncation-is-truncation @@ -106,7 +106,7 @@ module _ triangle-universal-property-trunc : (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) → - (map-universal-property-trunc B f ∘ unit-trunc) ~ f + map-universal-property-trunc B f ∘ unit-trunc ~ f triangle-universal-property-trunc B f = pr2 (apply-universal-property-trunc B f) ``` @@ -119,8 +119,7 @@ module _ where dependent-universal-property-trunc : - {l : Level} → - dependent-universal-property-truncation l (trunc k A) unit-trunc + dependent-universal-property-truncation (trunc k A) unit-trunc dependent-universal-property-trunc = dependent-universal-property-truncation-is-truncation ( trunc k A) diff --git a/src/foundation/uniqueness-truncation.lagda.md b/src/foundation/uniqueness-truncation.lagda.md index 3820dc9b86..92b78f4998 100644 --- a/src/foundation/uniqueness-truncation.lagda.md +++ b/src/foundation/uniqueness-truncation.lagda.md @@ -34,8 +34,8 @@ module _ abstract is-equiv-is-truncation-is-truncation : - ({l : Level} → is-truncation l B f) → - ({l : Level} → is-truncation l C g) → + is-truncation B f → + is-truncation C g → is-equiv h is-equiv-is-truncation-is-truncation K L = is-equiv-is-invertible diff --git a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md index 156b5631cc..35ca2662b1 100644 --- a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md +++ b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md @@ -65,7 +65,7 @@ abstract {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → is-weakly-constant-map f → all-elements-equal (Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b))) - all-elements-equal-image-is-weakly-constant-map B f H (pair x s) (pair y t) = + all-elements-equal-image-is-weakly-constant-map B f H (x , s) (y , t) = eq-type-subtype ( λ b → trunc-Prop (fiber f b)) ( apply-universal-property-trunc-Prop s @@ -73,7 +73,7 @@ abstract ( λ u → apply-universal-property-trunc-Prop t ( Id-Prop B x y) - ( λ v → inv (pr2 u) ∙ (H (pr1 u) (pr1 v) ∙ pr2 v)))) + ( λ v → inv (pr2 u) ∙ H (pr1 u) (pr1 v) ∙ pr2 v))) abstract is-prop-image-is-weakly-constant-map : @@ -103,34 +103,35 @@ map-universal-property-set-quotient-trunc-Prop B f H = ( pr1) ∘ ( map-universal-property-trunc-Prop ( image-weakly-constant-map-Prop B f H) - ( λ a → pair (f a) (unit-trunc-Prop (pair a refl)))) + ( λ a → (f a , unit-trunc-Prop (a , refl)))) map-universal-property-set-quotient-trunc-Prop' : {l1 l2 : Level} {A : UU l1} (B : Set l2) → Σ (A → type-Set B) is-weakly-constant-map → type-trunc-Prop A → type-Set B -map-universal-property-set-quotient-trunc-Prop' B (pair f H) = +map-universal-property-set-quotient-trunc-Prop' B (f , H) = map-universal-property-set-quotient-trunc-Prop B f H abstract htpy-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → (H : is-weakly-constant-map f) → - (map-universal-property-set-quotient-trunc-Prop B f H ∘ unit-trunc-Prop) ~ f + map-universal-property-set-quotient-trunc-Prop B f H ∘ unit-trunc-Prop ~ f htpy-universal-property-set-quotient-trunc-Prop B f H a = - ap ( pr1) + ap + ( pr1) ( eq-is-prop' ( is-prop-image-is-weakly-constant-map B f H) ( map-universal-property-trunc-Prop ( image-weakly-constant-map-Prop B f H) - ( λ x → pair (f x) (unit-trunc-Prop (pair x refl))) + ( λ x → (f x , unit-trunc-Prop (x , refl))) ( unit-trunc-Prop a)) - ( pair (f a) (unit-trunc-Prop (pair a refl)))) + ( f a , unit-trunc-Prop (a , refl))) is-section-map-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → ( ( precomp-universal-property-set-quotient-trunc-Prop {A = A} B) ∘ ( map-universal-property-set-quotient-trunc-Prop' B)) ~ id - is-section-map-universal-property-set-quotient-trunc-Prop B (pair f H) = + is-section-map-universal-property-set-quotient-trunc-Prop B (f , H) = eq-type-subtype ( is-weakly-constant-map-Prop B) ( eq-htpy (htpy-universal-property-set-quotient-trunc-Prop B f H)) @@ -148,16 +149,14 @@ abstract ( precomp-universal-property-set-quotient-trunc-Prop B g) ( x)) ( g x)) - ( λ x → - htpy-universal-property-set-quotient-trunc-Prop B - ( g ∘ unit-trunc-Prop) - ( is-weakly-constant-map-precomp-unit-trunc-Prop g) - ( x))) + ( htpy-universal-property-set-quotient-trunc-Prop B + ( g ∘ unit-trunc-Prop) + ( is-weakly-constant-map-precomp-unit-trunc-Prop g))) universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → is-equiv (precomp-universal-property-set-quotient-trunc-Prop {A = A} B) - universal-property-set-quotient-trunc-Prop {A = A} B = + universal-property-set-quotient-trunc-Prop B = is-equiv-is-invertible ( map-universal-property-set-quotient-trunc-Prop' B) ( is-section-map-universal-property-set-quotient-trunc-Prop B) diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index 47521315af..cea50b3265 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -81,7 +81,6 @@ module _ universal-property-propositional-truncation : UUω universal-property-propositional-truncation = {l : Level} → universal-property-propositional-truncation-Level l - ``` ### Extension property of the propositional truncation diff --git a/src/foundation/universal-property-truncation.lagda.md b/src/foundation/universal-property-truncation.lagda.md index 6e7010ea63..8d3c9a65e0 100644 --- a/src/foundation/universal-property-truncation.lagda.md +++ b/src/foundation/universal-property-truncation.lagda.md @@ -42,8 +42,7 @@ module _ {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 (succ-𝕋 k)) {f : A → type-Truncated-Type B} (H : is-surjective f) ( K : - {l : Level} (x y : A) → - is-truncation l (Id-Truncated-Type B (f x) (f y)) (ap f {x} {y})) + (x y : A) → is-truncation (Id-Truncated-Type B (f x) (f y)) (ap f {x} {y})) where unique-extension-fiber-is-truncation-is-truncation-ap : @@ -51,7 +50,7 @@ module _ (g : A → type-Truncated-Type C) (y : type-Truncated-Type B) → is-contr ( Σ ( type-Truncated-Type C) - ( λ z → (t : fiber f y) → Id (g (pr1 t)) z)) + ( λ z → (t : fiber f y) → g (pr1 t) ＝ z)) unique-extension-fiber-is-truncation-is-truncation-ap C g = apply-dependent-universal-property-surj-is-surjective f H ( λ y → is-contr-Prop _) @@ -72,7 +71,7 @@ module _ ( is-torsorial-path (g x))) is-truncation-is-truncation-ap : - {l : Level} → is-truncation l B f + is-truncation B f is-truncation-is-truncation-ap C = is-equiv-is-contr-map ( λ g → @@ -98,7 +97,7 @@ module _ where is-surjective-is-truncation : - ({l : Level} → is-truncation l B f) → is-surjective f + (is-truncation B f) → is-surjective f is-surjective-is-truncation H = map-inv-is-equiv ( dependent-universal-property-truncation-is-truncation B f H diff --git a/src/orthogonal-factorization-systems/function-classes.lagda.md b/src/orthogonal-factorization-systems/function-classes.lagda.md index 0a411e2f64..93d067180c 100644 --- a/src/orthogonal-factorization-systems/function-classes.lagda.md +++ b/src/orthogonal-factorization-systems/function-classes.lagda.md @@ -192,8 +192,7 @@ module _ pullback-stable-function-class : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3) pullback-stable-function-class l1 l2 l3 = - Σ ( function-class l1 l2 l3) - ( is-pullback-stable-function-class) + Σ ( function-class l1 l2 l3) (is-pullback-stable-function-class) ``` ## Properties From cbfd50469a55a89deba496eddf10bfbbf3038a95 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 3 Dec 2023 22:09:40 +0100 Subject: [PATCH 08/16] remove purposeless definitions for UPs of limits --- .../universal-property-pullbacks.lagda.md | 7 +---- .../universal-property-truncation.lagda.md | 26 ++++------------ src/foundation/replacement.lagda.md | 2 +- ...property-propositional-truncation.lagda.md | 31 ++++--------------- .../universal-property-pullbacks.lagda.md | 15 --------- ...versal-property-sequential-limits.lagda.md | 21 +------------ 6 files changed, 15 insertions(+), 87 deletions(-) diff --git a/src/foundation-core/universal-property-pullbacks.lagda.md b/src/foundation-core/universal-property-pullbacks.lagda.md index d98c5fa3bb..cd89005e20 100644 --- a/src/foundation-core/universal-property-pullbacks.lagda.md +++ b/src/foundation-core/universal-property-pullbacks.lagda.md @@ -35,14 +35,9 @@ module _ (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C) where - universal-property-pullback-Level : - (l : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l) - universal-property-pullback-Level l = - (C' : UU l) → is-equiv (cone-map f g c {C'}) - universal-property-pullback : UUω universal-property-pullback = - {l : Level} → universal-property-pullback-Level l + {l : Level} (C' : UU l) → is-equiv (cone-map f g c {C'}) module _ {l1 l2 l3 l4 l5 : Level} {A : UU l1} {B : UU l2} {X : UU l3} diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md index b4d31f1e4c..572d775f30 100644 --- a/src/foundation-core/universal-property-truncation.lagda.md +++ b/src/foundation-core/universal-property-truncation.lagda.md @@ -51,13 +51,9 @@ module _ (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) where - is-truncation-Level : - (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) - is-truncation-Level l = - (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C) - is-truncation : UUω - is-truncation = {l : Level} → is-truncation-Level l + is-truncation = + {l : Level} (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C) equiv-is-truncation : {l3 : Level} @@ -77,15 +73,10 @@ module _ (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) where - universal-property-truncation-Level : - (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - universal-property-truncation-Level l = - (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → - is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g)) - universal-property-truncation : UUω universal-property-truncation = - {l : Level} → universal-property-truncation-Level l + {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → + is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g)) ``` ### The dependent universal property of truncations @@ -103,15 +94,10 @@ module _ (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) where - dependent-universal-property-truncation-Level : - (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) - dependent-universal-property-truncation-Level l = - (X : type-Truncated-Type B → Truncated-Type l k) → - is-equiv (precomp-Π-Truncated-Type f X) - dependent-universal-property-truncation : UUω dependent-universal-property-truncation = - {l : Level} → dependent-universal-property-truncation-Level l + {l : Level} (X : type-Truncated-Type B → Truncated-Type l k) → + is-equiv (precomp-Π-Truncated-Type f X) ``` ## Properties diff --git a/src/foundation/replacement.lagda.md b/src/foundation/replacement.lagda.md index 23bf1e829f..0104411031 100644 --- a/src/foundation/replacement.lagda.md +++ b/src/foundation/replacement.lagda.md @@ -34,7 +34,7 @@ instance-replacement l {A = A} {B} f = replacement-axiom-Level : (l l1 l2 : Level) → UU (lsuc l ⊔ lsuc l1 ⊔ lsuc l2) replacement-axiom-Level l l1 l2 = - {A : UU l1} {B : UU l2} → (f : A → B) → instance-replacement l f + {A : UU l1} {B : UU l2} (f : A → B) → instance-replacement l f replacement-axiom : UUω replacement-axiom = {l l1 l2 : Level} → replacement-axiom-Level l l1 l2 diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index cea50b3265..334a649e49 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -54,14 +54,9 @@ module _ type-hom-Prop P Q → A → type-Prop Q precomp-Prop Q g = g ∘ f - is-propositional-truncation-Level : - ( l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - is-propositional-truncation-Level l = - (Q : Prop l) → is-equiv (precomp-Prop Q) - is-propositional-truncation : UUω is-propositional-truncation = - {l : Level} → is-propositional-truncation-Level l + {l : Level} (Q : Prop l) → is-equiv (precomp-Prop Q) ``` ### The universal property of the propositional truncation @@ -72,15 +67,10 @@ module _ (P : Prop l2) (f : A → type-Prop P) where - universal-property-propositional-truncation-Level : - (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - universal-property-propositional-truncation-Level l = - (Q : Prop l) (g : A → type-Prop Q) → - is-contr (Σ (type-hom-Prop P Q) (λ h → h ∘ f ~ g)) - universal-property-propositional-truncation : UUω universal-property-propositional-truncation = - {l : Level} → universal-property-propositional-truncation-Level l + {l : Level} (Q : Prop l) (g : A → type-Prop Q) → + is-contr (Σ (type-hom-Prop P Q) (λ h → h ∘ f ~ g)) ``` ### Extension property of the propositional truncation @@ -94,14 +84,9 @@ module _ (P : Prop l2) (f : A → type-Prop P) where - extension-property-propositional-truncation-Level : - (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - extension-property-propositional-truncation-Level l = - (Q : Prop l) → (A → type-Prop Q) → type-hom-Prop P Q - extension-property-propositional-truncation : UUω extension-property-propositional-truncation = - {l : Level} → extension-property-propositional-truncation-Level l + {l : Level} (Q : Prop l) → (A → type-Prop Q) → type-hom-Prop P Q ``` ### The dependent universal property of the propositional truncation @@ -112,14 +97,10 @@ module _ (P : Prop l2) (f : A → type-Prop P) where - dependent-universal-property-propositional-truncation-Level : - (l : Level) → UU (lsuc l ⊔ l1 ⊔ l2) - dependent-universal-property-propositional-truncation-Level l = - ( Q : type-Prop P → Prop l) → is-equiv (precomp-Π f (type-Prop ∘ Q)) - dependent-universal-property-propositional-truncation : UUω dependent-universal-property-propositional-truncation = - {l : Level} → dependent-universal-property-propositional-truncation-Level l + {l : Level} → (Q : type-Prop P → Prop l) → + is-equiv (precomp-Π f (type-Prop ∘ Q)) ``` ## Properties diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index 01162f2405..01e0994c99 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -46,21 +46,6 @@ A -----> X ## Properties -### The universal property of pullbacks at a universe level is a property - -```agda -module _ - {l1 l2 l3 l4 l : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (g : B → X) {C : UU l4} (c : cone f g C) - where - - abstract - is-prop-universal-property-pullback-Level : - is-prop (universal-property-pullback-Level f g c l) - is-prop-universal-property-pullback-Level = - is-prop-Π (λ _ → is-property-is-equiv (cone-map f g c)) -``` - ### The homotopy of cones obtained from the universal property of pullbacks ```agda diff --git a/src/foundation/universal-property-sequential-limits.lagda.md b/src/foundation/universal-property-sequential-limits.lagda.md index ba36f88ca8..48c3b4c24a 100644 --- a/src/foundation/universal-property-sequential-limits.lagda.md +++ b/src/foundation/universal-property-sequential-limits.lagda.md @@ -59,14 +59,9 @@ module _ {l1 l2 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X) where - universal-property-sequential-limit-Level : - (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) - universal-property-sequential-limit-Level l = - (Y : UU l) → is-equiv (cone-map-tower A {Y = Y} c) - universal-property-sequential-limit : UUω universal-property-sequential-limit = - {l : Level} → universal-property-sequential-limit-Level l + {l : Level} (Y : UU l) → is-equiv (cone-map-tower A {Y = Y} c) module _ {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X) @@ -179,20 +174,6 @@ module _ ( is-contr-map-is-equiv (up Y) c') ``` -### The universal property of sequential limits at a universe level is a property - -```agda -module _ - {l1 l2 l3 : Level} (A : tower l1) {X : UU l2} (c : cone-tower A X) - where - - abstract - is-prop-universal-property-sequential-limit : - is-prop (universal-property-sequential-limit-Level A c l3) - is-prop-universal-property-sequential-limit = - is-prop-Π (λ Y → is-property-is-equiv (cone-map-tower A c)) -``` - ### The homotopy of cones obtained from the universal property of sequential limits ```agda From d4e5457c2114560c0e5c9ab44f3adba43f2f8821 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 6 Dec 2023 14:28:37 +0100 Subject: [PATCH 09/16] fix --- src/foundation/universal-property-image.lagda.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index edcb9c44dc..831ddcad44 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -321,7 +321,10 @@ abstract is-image-is-surjective' f i q H B' m = map-equiv ( ( equiv-hom-slice-fiberwise-hom (map-emb i) (map-emb m)) ∘e - ( inv-equiv (reduce-Π-fiber (map-emb i) (fiber (map-emb m)))) ∘e + ( inv-equiv + ( equiv-universal-property-family-of-fibers + ( map-emb i) + ( fiber (map-emb m)))) ∘e ( inv-equiv ( equiv-dependent-universal-property-surj-is-surjective ( pr1 q) @@ -331,7 +334,7 @@ abstract ( is-prop-map-emb m (pr1 i b))))) ∘e ( equiv-Π-equiv-family ( λ a → equiv-tr (fiber (map-emb m)) (pr2 q a))) ∘e - ( reduce-Π-fiber f (fiber (map-emb m))) ∘e + ( equiv-universal-property-family-of-fibers f (fiber (map-emb m))) ∘e ( equiv-fiberwise-hom-hom-slice f (map-emb m))) abstract From 08e7319b656168803c88181c1406874a1251f8e0 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 01:48:45 +0100 Subject: [PATCH 10/16] Apply suggestions from code review --- .../universal-property-truncation.lagda.md | 12 +++++----- src/foundation/uniqueness-truncation.lagda.md | 4 +--- ...universal-property-fiber-products.lagda.md | 2 +- .../universal-property-image.lagda.md | 2 +- ...property-propositional-truncation.lagda.md | 22 +++++++++---------- .../universal-property-truncation.lagda.md | 2 +- 6 files changed, 20 insertions(+), 24 deletions(-) diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md index 572d775f30..9868e42639 100644 --- a/src/foundation-core/universal-property-truncation.lagda.md +++ b/src/foundation-core/universal-property-truncation.lagda.md @@ -134,8 +134,7 @@ module _ abstract is-truncation-universal-property-truncation : - universal-property-truncation B f → - is-truncation B f + universal-property-truncation B f → is-truncation B f is-truncation-universal-property-truncation H C = is-equiv-is-contr-map ( λ g → @@ -154,7 +153,7 @@ module _ ( is-contr-map-is-equiv (H C) g) map-is-truncation : - (is-truncation B f) → + is-truncation B f → ({l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → type-hom-Truncated-Type k B C) map-is-truncation H C g = @@ -178,7 +177,7 @@ module _ abstract dependent-universal-property-truncation-is-truncation : - (is-truncation B f) → + is-truncation B f → dependent-universal-property-truncation B f dependent-universal-property-truncation-is-truncation H X = is-fiberwise-equiv-is-equiv-map-Σ @@ -197,13 +196,12 @@ module _ abstract is-truncation-dependent-universal-property-truncation : - (dependent-universal-property-truncation B f) → - is-truncation B f + dependent-universal-property-truncation B f → is-truncation B f is-truncation-dependent-universal-property-truncation H X = H (λ b → X) section-is-truncation : - (is-truncation B f) → + is-truncation B f → {l3 : Level} (C : Truncated-Type l3 k) (h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) → f ~ (g ∘ h) → section g diff --git a/src/foundation/uniqueness-truncation.lagda.md b/src/foundation/uniqueness-truncation.lagda.md index 92b78f4998..25971b85f3 100644 --- a/src/foundation/uniqueness-truncation.lagda.md +++ b/src/foundation/uniqueness-truncation.lagda.md @@ -34,9 +34,7 @@ module _ abstract is-equiv-is-truncation-is-truncation : - is-truncation B f → - is-truncation C g → - is-equiv h + is-truncation B f → is-truncation C g → is-equiv h is-equiv-is-truncation-is-truncation K L = is-equiv-is-invertible ( map-inv-is-equiv (L B) f) diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index 5c43b1bd77..e6afc47890 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -28,7 +28,7 @@ open import foundation-core.universal-property-pullbacks ## Idea -The **fiberwise product** of two families `P` and `Q` over a type `X` is the +The {{#concept "fiberwise product" Disambiguation="types"}} of two families `P` and `Q` over a type `X` is the family of types `(P x) × (Q x)` over `X`. Similarly, the fiber product of two maps `f : A → X` and `g : B → X` is the type `Σ X (λ x → fiber f x × fiber g x)`, which fits in a diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index 831ddcad44..a6c881fe0b 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -39,7 +39,7 @@ open import foundation-core.whiskering-homotopies ## Idea -The **image** of a map `f : A → X` is the least +The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map `f : A → X` is the least [subtype](foundation-core.subtypes.md) of `X` containing all the values of `f`. ## Definition diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index 334a649e49..4e71235313 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -36,8 +36,8 @@ open import foundation-core.type-theoretic-principle-of-choice ## Idea A map `f : A → P` into a [proposition](foundation-core.propositions.md) `P` is -said to satisfy the **universal property of the propositional truncation** of -`A`, or is said to be a **propositional truncation** of `A`, if any map +said to satisfy the {{#concept "universal property of the propositional truncation" Agda=universal-property-propositional-truncation}} of +`A`, or is said to be a {{#concept "propositional truncation" Agda=is-propositional-truncation}} of `A`, if any map `g : A → Q` into a proposition `Q` extends uniquely along `f`. ## Definition @@ -190,8 +190,8 @@ abstract is-ptruncation-is-ptruncation-is-equiv : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') → - is-equiv h → (is-propositional-truncation P f) → - (is-propositional-truncation P' f') + is-equiv h → is-propositional-truncation P f → + is-propositional-truncation P' f' is-ptruncation-is-ptruncation-is-equiv P P' f f' h is-equiv-h is-ptr-f = is-propositional-truncation-extension-property P' f' ( λ R g → @@ -202,8 +202,8 @@ abstract is-ptruncation-is-equiv-is-ptruncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') (h : type-hom-Prop P P') → - (is-propositional-truncation P' f') → is-equiv h → - (is-propositional-truncation P f) + is-propositional-truncation P' f' → is-equiv h → + is-propositional-truncation P f is-ptruncation-is-equiv-is-ptruncation P P' f f' h is-ptr-f' is-equiv-h = is-propositional-truncation-extension-property P f ( λ R g → (map-is-propositional-truncation P' f' is-ptr-f' R g) ∘ h) @@ -212,8 +212,8 @@ abstract is-uniquely-unique-propositional-truncation : {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (P' : Prop l3) (f : A → type-Prop P) (f' : A → type-Prop P') → - (is-propositional-truncation P f) → - (is-propositional-truncation P' f') → + is-propositional-truncation P f → + is-propositional-truncation P' f' → is-contr (Σ (type-equiv-Prop P P') (λ e → (map-equiv e ∘ f) ~ f')) is-uniquely-unique-propositional-truncation P P' f f' is-ptr-f is-ptr-f' = is-torsorial-Eq-subtype @@ -318,7 +318,7 @@ abstract abstract is-equiv-is-propositional-truncation : {l1 l2 : Level} (P : Prop l1) (Q : Prop l2) {f : type-hom-Prop P Q} → - (is-propositional-truncation Q f) → is-equiv f + is-propositional-truncation Q f → is-equiv f is-equiv-is-propositional-truncation P Q {f} H = is-equiv-is-equiv-precomp-Prop P Q f H ``` @@ -341,8 +341,8 @@ abstract {l1 l2 l3 l4 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) {A' : UU l3} (P' : Prop l4) (f' : A' → type-Prop P') → - (is-propositional-truncation P f) → - (is-propositional-truncation P' f') → + is-propositional-truncation P f → + is-propositional-truncation P' f' → is-propositional-truncation (prod-Prop P P') (map-prod f f') is-propositional-truncation-prod P f P' f' is-ptr-f is-ptr-f' Q = is-equiv-top-is-equiv-bottom-square diff --git a/src/foundation/universal-property-truncation.lagda.md b/src/foundation/universal-property-truncation.lagda.md index 8d3c9a65e0..c04edde203 100644 --- a/src/foundation/universal-property-truncation.lagda.md +++ b/src/foundation/universal-property-truncation.lagda.md @@ -97,7 +97,7 @@ module _ where is-surjective-is-truncation : - (is-truncation B f) → is-surjective f + is-truncation B f → is-surjective f is-surjective-is-truncation H = map-inv-is-equiv ( dependent-universal-property-truncation-is-truncation B f H From 85d1f4b5b8edd47ba6a0593f7936756a3ff94921 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 01:49:15 +0100 Subject: [PATCH 11/16] Update src/foundation/universal-property-propositional-truncation.lagda.md --- .../universal-property-propositional-truncation.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index 4e71235313..e506ee07d6 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -133,7 +133,7 @@ abstract {l1 l2 l3 : Level} {A : UU l1} (P : Prop l2) (f : A → type-Prop P) → (is-ptr-f : is-propositional-truncation P f) → (Q : Prop l3) (g : A → type-Prop Q) → - ((map-is-propositional-truncation P f is-ptr-f Q g) ∘ f) ~ g + map-is-propositional-truncation P f is-ptr-f Q g ∘ f ~ g htpy-is-propositional-truncation P f is-ptr-f Q g = pr2 ( center From 08aa0d203fd941bae813367f50827d5cbb44318c Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 14:58:08 +0100 Subject: [PATCH 12/16] pre-commit --- src/foundation/universal-property-fiber-products.lagda.md | 6 +++--- src/foundation/universal-property-image.lagda.md | 5 +++-- .../universal-property-propositional-truncation.lagda.md | 8 +++++--- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/foundation/universal-property-fiber-products.lagda.md b/src/foundation/universal-property-fiber-products.lagda.md index e6afc47890..50a5befa1e 100644 --- a/src/foundation/universal-property-fiber-products.lagda.md +++ b/src/foundation/universal-property-fiber-products.lagda.md @@ -28,9 +28,9 @@ open import foundation-core.universal-property-pullbacks ## Idea -The {{#concept "fiberwise product" Disambiguation="types"}} of two families `P` and `Q` over a type `X` is the -family of types `(P x) × (Q x)` over `X`. Similarly, the fiber product of two -maps `f : A → X` and `g : B → X` is the type +The {{#concept "fiberwise product" Disambiguation="types"}} of two families `P` +and `Q` over a type `X` is the family of types `(P x) × (Q x)` over `X`. +Similarly, the fiber product of two maps `f : A → X` and `g : B → X` is the type `Σ X (λ x → fiber f x × fiber g x)`, which fits in a [pullback](foundation-core.pullbacks.md) diagram on `f` and `g`. diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index a6c881fe0b..1599b9b791 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -39,8 +39,9 @@ open import foundation-core.whiskering-homotopies ## Idea -The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map `f : A → X` is the least -[subtype](foundation-core.subtypes.md) of `X` containing all the values of `f`. +The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map +`f : A → X` is the least [subtype](foundation-core.subtypes.md) of `X` +containing all the values of `f`. ## Definition diff --git a/src/foundation/universal-property-propositional-truncation.lagda.md b/src/foundation/universal-property-propositional-truncation.lagda.md index e506ee07d6..b92212ebbc 100644 --- a/src/foundation/universal-property-propositional-truncation.lagda.md +++ b/src/foundation/universal-property-propositional-truncation.lagda.md @@ -36,9 +36,11 @@ open import foundation-core.type-theoretic-principle-of-choice ## Idea A map `f : A → P` into a [proposition](foundation-core.propositions.md) `P` is -said to satisfy the {{#concept "universal property of the propositional truncation" Agda=universal-property-propositional-truncation}} of -`A`, or is said to be a {{#concept "propositional truncation" Agda=is-propositional-truncation}} of `A`, if any map -`g : A → Q` into a proposition `Q` extends uniquely along `f`. +said to satisfy the +{{#concept "universal property of the propositional truncation" Agda=universal-property-propositional-truncation}} +of `A`, or is said to be a +{{#concept "propositional truncation" Agda=is-propositional-truncation}} of `A`, +if any map `g : A → Q` into a proposition `Q` extends uniquely along `f`. ## Definition From 369b108ecab04cd7fc9a87c631b81f9dad7f5ea7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 15:02:55 +0100 Subject: [PATCH 13/16] small fixes up truncation --- .../universal-property-truncation.lagda.md | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/foundation-core/universal-property-truncation.lagda.md b/src/foundation-core/universal-property-truncation.lagda.md index 9868e42639..1f7366ca3a 100644 --- a/src/foundation-core/universal-property-truncation.lagda.md +++ b/src/foundation-core/universal-property-truncation.lagda.md @@ -56,9 +56,7 @@ module _ {l : Level} (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C) equiv-is-truncation : - {l3 : Level} - (H : is-truncation) → - (C : Truncated-Type l3 k) → + {l3 : Level} (H : is-truncation) (C : Truncated-Type l3 k) → ( type-Truncated-Type B → type-Truncated-Type C) ≃ ( A → type-Truncated-Type C) pr1 (equiv-is-truncation H C) = precomp-Trunc f C @@ -154,15 +152,15 @@ module _ map-is-truncation : is-truncation B f → - ({l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → - type-hom-Truncated-Type k B C) + {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → + type-hom-Truncated-Type k B C map-is-truncation H C g = pr1 (center (universal-property-truncation-is-truncation H C g)) triangle-is-truncation : (H : is-truncation B f) → {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) → - (map-is-truncation H C g ∘ f) ~ g + map-is-truncation H C g ∘ f ~ g triangle-is-truncation H C g = pr2 (center (universal-property-truncation-is-truncation H C g)) ``` @@ -197,18 +195,17 @@ module _ abstract is-truncation-dependent-universal-property-truncation : dependent-universal-property-truncation B f → is-truncation B f - is-truncation-dependent-universal-property-truncation H X = - H (λ b → X) + is-truncation-dependent-universal-property-truncation H X = H (λ _ → X) section-is-truncation : is-truncation B f → {l3 : Level} (C : Truncated-Type l3 k) (h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) → - f ~ (g ∘ h) → section g + f ~ g ∘ h → section g section-is-truncation H C h g K = map-distributive-Π-Σ ( map-inv-is-equiv ( dependent-universal-property-truncation-is-truncation H ( fiber-Truncated-Type C B g)) - ( λ a → h a , inv (K a))) + ( λ a → (h a , inv (K a)))) ``` From c68e6a858b1bf513d7c7beeadedf3808de84a4e5 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 15:16:59 +0100 Subject: [PATCH 14/16] fix up image idea --- src/foundation/universal-property-image.lagda.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index 1599b9b791..2f44a890d4 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -39,9 +39,10 @@ open import foundation-core.whiskering-homotopies ## Idea -The {{#concept "image" Disambiguation="maps of types" Agda=is-image}} of a map -`f : A → X` is the least [subtype](foundation-core.subtypes.md) of `X` -containing all the values of `f`. +The +{{#concept "universal property of the image" Disambiguation="maps of types" Agda=is-image}} +of a map `f : A → X` states that the [image](foundation.images.md) is the least +[subtype](foundation-core.subtypes.md) of `X` containing all the values of `f`. ## Definition @@ -250,9 +251,9 @@ abstract { A = (fiber f x)} ( fiber-emb-Prop m x) ( λ t → - ( map-hom-slice f (map-emb m) h (pr1 t)) , - ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙ - ( pr2 t))) + ( map-hom-slice f (map-emb m) h (pr1 t)) , + ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙ + ( pr2 t))) map-is-image-im : {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → From cc4523d4890d9e5ea677925c0b216e00ce3059df Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 15:22:53 +0100 Subject: [PATCH 15/16] megaminor nitpick --- src/foundation/universal-property-image.lagda.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index 2f44a890d4..e40ec880b6 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -53,11 +53,10 @@ module _ where precomp-emb : - {l4 : Level} {C : UU l4} ( j : C ↪ X) → + {l4 : Level} {C : UU l4} (j : C ↪ X) → hom-slice (map-emb i) (map-emb j) → hom-slice f (map-emb j) pr1 (precomp-emb j r) = - ( map-hom-slice (map-emb i) (map-emb j) r) ∘ - ( map-hom-slice f (map-emb i) q) + map-hom-slice (map-emb i) (map-emb j) r ∘ map-hom-slice f (map-emb i) q pr2 (precomp-emb j r) = ( triangle-hom-slice f (map-emb i) q) ∙h ( ( triangle-hom-slice (map-emb i) (map-emb j) r) ·r @@ -248,7 +247,7 @@ abstract (x : X) → type-trunc-Prop (fiber f x) → fiber (map-emb m) x fiberwise-map-is-image-im f m h x = map-universal-property-trunc-Prop - { A = (fiber f x)} + { A = fiber f x} ( fiber-emb-Prop m x) ( λ t → ( map-hom-slice f (map-emb m) h (pr1 t)) , From 7f8cc17b4ddbf1c5092ff50c6a209ac276c1b957 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sun, 10 Dec 2023 15:37:20 +0100 Subject: [PATCH 16/16] use modules up image --- .../universal-property-image.lagda.md | 95 +++++++++---------- 1 file changed, 45 insertions(+), 50 deletions(-) diff --git a/src/foundation/universal-property-image.lagda.md b/src/foundation/universal-property-image.lagda.md index e40ec880b6..2e78eabebf 100644 --- a/src/foundation/universal-property-image.lagda.md +++ b/src/foundation/universal-property-image.lagda.md @@ -189,26 +189,25 @@ module _ ```agda module _ {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) - where - - abstract - forward-implication-is-image-subtype-subtype-im : - {l : Level} (B : subtype l X) → - subtype-im f ⊆ B → (a : A) → is-in-subtype B (f a) - forward-implication-is-image-subtype-subtype-im B H a = - H (f a) (unit-trunc-Prop (a , refl)) - - backward-implication-is-image-subtype-subtype-im : - {l : Level} (B : subtype l X) → - ((a : A) → is-in-subtype B (f a)) → subtype-im f ⊆ B - backward-implication-is-image-subtype-subtype-im B H x K = - apply-universal-property-trunc-Prop K (B x) (λ where (a , refl) → H a) - - is-image-subtype-subtype-im : is-image-subtype f (subtype-im f) - pr1 (is-image-subtype-subtype-im B) = - forward-implication-is-image-subtype-subtype-im B - pr2 (is-image-subtype-subtype-im B) = - backward-implication-is-image-subtype-subtype-im B + where abstract + + forward-implication-is-image-subtype-subtype-im : + {l : Level} (B : subtype l X) → + subtype-im f ⊆ B → (a : A) → is-in-subtype B (f a) + forward-implication-is-image-subtype-subtype-im B H a = + H (f a) (unit-trunc-Prop (a , refl)) + + backward-implication-is-image-subtype-subtype-im : + {l : Level} (B : subtype l X) → + ((a : A) → is-in-subtype B (f a)) → subtype-im f ⊆ B + backward-implication-is-image-subtype-subtype-im B H x K = + apply-universal-property-trunc-Prop K (B x) (λ where (a , refl) → H a) + + is-image-subtype-subtype-im : is-image-subtype f (subtype-im f) + pr1 (is-image-subtype-subtype-im B) = + forward-implication-is-image-subtype-subtype-im B + pr2 (is-image-subtype-subtype-im B) = + backward-implication-is-image-subtype-subtype-im B ``` ### The identity embedding is the image inclusion of any map that has a section @@ -240,37 +239,37 @@ abstract ### The image of `f` is the image of `f` ```agda -abstract +module _ + {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) + (m : B ↪ X) (h : hom-slice f (map-emb m)) + where abstract + fiberwise-map-is-image-im : - {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → - (m : B ↪ X) (h : hom-slice f (map-emb m)) → (x : X) → type-trunc-Prop (fiber f x) → fiber (map-emb m) x - fiberwise-map-is-image-im f m h x = + fiberwise-map-is-image-im x = map-universal-property-trunc-Prop { A = fiber f x} ( fiber-emb-Prop m x) ( λ t → ( map-hom-slice f (map-emb m) h (pr1 t)) , - ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙ - ( pr2 t))) + ( ( inv (triangle-hom-slice f (map-emb m) h (pr1 t))) ∙ ( pr2 t))) + + map-is-image-im : im f → B + map-is-image-im (x , t) = pr1 (fiberwise-map-is-image-im x t) - map-is-image-im : - {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → - (m : B ↪ X) (h : hom-slice f (map-emb m)) → im f → B - map-is-image-im f m h (x , t) = - pr1 (fiberwise-map-is-image-im f m h x t) + inv-triangle-is-image-im : + map-emb m ∘ map-is-image-im ~ inclusion-im f + inv-triangle-is-image-im (x , t) = pr2 (fiberwise-map-is-image-im x t) triangle-is-image-im : - {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (f : A → X) → - (m : B ↪ X) (h : hom-slice f (map-emb m)) → - inclusion-im f ~ map-emb m ∘ map-is-image-im f m h - triangle-is-image-im f m h (x , t) = - inv (pr2 (fiberwise-map-is-image-im f m h x t)) + inclusion-im f ~ map-emb m ∘ map-is-image-im + triangle-is-image-im = inv-htpy inv-triangle-is-image-im +abstract is-image-im : {l1 l2 : Level} {X : UU l1} {A : UU l2} (f : A → X) → is-image f (emb-im f) (unit-im f) - is-image-im f {l} = + is-image-im f = is-image-is-image' ( f) ( emb-im f) @@ -281,12 +280,14 @@ abstract ### A factorization of a map through an embedding is the image factorization if and only if the right factor is surjective ```agda -abstract +module _ + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} + (f : A → X) (i : B ↪ X) (q : hom-slice f (map-emb i)) + where abstract + is-surjective-is-image : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (i : B ↪ X) (q : hom-slice f (map-emb i)) → is-image f i q → is-surjective (map-hom-slice f (map-emb i) q) - is-surjective-is-image {A = A} {B} {X} f i q up-i b = + is-surjective-is-image up-i b = apply-universal-property-trunc-Prop β ( trunc-Prop (fiber (map-hom-slice f (map-emb i) q) b)) ( γ) @@ -313,13 +314,10 @@ abstract unit-trunc-Prop ( a , p ∙ inv (is-injective-is-emb (is-emb-map-emb i) (pr2 α b))) -abstract is-image-is-surjective' : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (i : B ↪ X) (q : hom-slice f (map-emb i)) → is-surjective (map-hom-slice f (map-emb i) q) → is-image' f i q - is-image-is-surjective' f i q H B' m = + is-image-is-surjective' H B' m = map-equiv ( ( equiv-hom-slice-fiberwise-hom (map-emb i) (map-emb m)) ∘e ( inv-equiv @@ -338,12 +336,9 @@ abstract ( equiv-universal-property-family-of-fibers f (fiber (map-emb m))) ∘e ( equiv-fiberwise-hom-hom-slice f (map-emb m))) -abstract is-image-is-surjective : - {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} - (f : A → X) (i : B ↪ X) (q : hom-slice f (map-emb i)) → is-surjective (map-hom-slice f (map-emb i) q) → is-image f i q - is-image-is-surjective f i q H = - is-image-is-image' f i q (is-image-is-surjective' f i q H) + is-image-is-surjective H = + is-image-is-image' f i q (is-image-is-surjective' H) ```