From 99154dc4c9091b2d4876fc9fdcb7c8c88cc003d1 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 02:17:14 +0000 Subject: [PATCH 1/9] coherently constant maps --- references.bib | 18 ++ src/foundation-core/constant-maps.lagda.md | 1 + src/foundation.lagda.md | 1 + .../coherently-constant-maps.lagda.md | 265 ++++++++++++++++++ src/foundation/constant-maps.lagda.md | 1 + src/foundation/null-homotopic-maps.lagda.md | 10 +- src/foundation/weakly-constant-maps.lagda.md | 4 + 7 files changed, 296 insertions(+), 4 deletions(-) create mode 100644 src/foundation/coherently-constant-maps.lagda.md diff --git a/references.bib b/references.bib index f63c1f2c16..3cf00524ce 100644 --- a/references.bib +++ b/references.bib @@ -443,6 +443,24 @@ @article{KECA17 eprintclass = {cs} } +@inproceedings{Kraus15, + author = {Kraus, Nicolai}, + title = {{The General Universal Property of the Propositional Truncation}}, + booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, + pages = {111--145}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + isbn = {978-3-939897-88-0}, + issn = {1868-8969}, + year = {2015}, + volume = {39}, + editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + urn = {urn:nbn:de:0030-drops-54944}, + doi = {10.4230/LIPIcs.TYPES.2014.111}, + annote = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy} +} + @book{Kunen11, author = {Kunen, Kenneth}, title = {Set theory}, diff --git a/src/foundation-core/constant-maps.lagda.md b/src/foundation-core/constant-maps.lagda.md index 46e9ad8b04..577b33af65 100644 --- a/src/foundation-core/constant-maps.lagda.md +++ b/src/foundation-core/constant-maps.lagda.md @@ -33,3 +33,4 @@ const A b x = b ## See also - [Constant pointed maps](structured-types.constant-pointed-maps.md) +- [Coherently constant maps](foundation.coherently-constant-maps.md) diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index fa5ed4f5b6..0b05bdebc4 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -57,6 +57,7 @@ open import foundation.category-of-sets public open import foundation.choice-of-representatives-equivalence-relation public open import foundation.coalgebras-maybe public open import foundation.codiagonal-maps-of-types public +open import foundation.coherently-constant-maps public open import foundation.coherently-idempotent-maps public open import foundation.coherently-invertible-maps public open import foundation.coinhabited-pairs-of-types public diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md new file mode 100644 index 0000000000..131989f817 --- /dev/null +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -0,0 +1,265 @@ +# Coherently constant maps + +```agda +module foundation.coherently-constant-maps where +``` + +
Imports + +```agda +open import foundation.action-on-identifications-functions +open import foundation.commuting-triangles-of-identifications +open import foundation.dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.propositional-truncations +open import foundation.propositions +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +open import foundation.type-arithmetic-dependent-pair-types +open import foundation.universe-levels +open import foundation.weakly-constant-maps + +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +``` + +
+ +## Idea + +A map `f : A → B` is said to be +{{#concept "(coherently) constant" Disambiguation="map of types" WD="constant function "WDID=Q746264 Agda=is-constant Agda=constant-map}} +if there is a [partial element](foundation.partial-elements.md) of `B`, +`b : ║A║₋₁ → B` such that for every `x : A` we have `f x ＝ b`. +{{#cite Kraus15}} + +## Definition + +### The type of coherent constancies of a map + +```agda +is-constant : + {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) +is-constant {A = A} {B} f = + Σ (║ A ║₋₁ → B) (λ b → (x : A) → f x ＝ b (unit-trunc-Prop x)) + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-constant f) + where + + center-partial-element-is-constant : ║ A ║₋₁ → B + center-partial-element-is-constant = pr1 H + + contraction-is-constant' : + (x : A) → f x ＝ center-partial-element-is-constant (unit-trunc-Prop x) + contraction-is-constant' = pr2 H + + contraction-is-constant : + (x : A) {|x| : ║ A ║₋₁} → f x ＝ center-partial-element-is-constant |x| + contraction-is-constant x = + contraction-is-constant' x ∙ + ap center-partial-element-is-constant (eq-type-Prop (trunc-Prop A)) +``` + +### The type of coherently constant maps + +```agda +constant-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +constant-map A B = Σ (A → B) is-constant + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : constant-map A B) + where + + map-constant-map : A → B + map-constant-map = pr1 f + + is-constant-map-constant-map : is-constant map-constant-map + is-constant-map-constant-map = pr2 f + + center-partial-element-constant-map : ║ A ║₋₁ → B + center-partial-element-constant-map = + center-partial-element-is-constant is-constant-map-constant-map + + contraction-constant-map' : + (x : A) → + map-constant-map x ＝ center-partial-element-constant-map (unit-trunc-Prop x) + contraction-constant-map' = + contraction-is-constant' is-constant-map-constant-map + + contraction-constant-map : + (x : A) {|x| : ║ A ║₋₁} → + map-constant-map x ＝ center-partial-element-constant-map |x| + contraction-constant-map = + contraction-is-constant is-constant-map-constant-map +``` + +## Properties + +### Characterizing equality of coherent constancy witnesses + +Two constancy witnesses `H` and `K` are equal if there is a homotopy +[equality](foundation-core.identity-types.md) of partial base points +`p : H₀ ~ K₀` such that for every `x : A` we have a +[commuting triangle of identifications](foundation.commuting-triangles-of-identifications.md) + +```text + f x + / \ + H₁x / \ K₁x + ∨ ∨ + H₀ ----> K₀. + p +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + coherence-htpy-is-constant : + (H K : is-constant f) + (p : center-partial-element-is-constant H ~ center-partial-element-is-constant K) → + UU (l1 ⊔ l2) + coherence-htpy-is-constant H K p = + (x : A) → + coherence-triangle-identifications + ( contraction-is-constant' K x) + ( p (unit-trunc-Prop x)) + ( contraction-is-constant' H x) + + htpy-is-constant : (H K : is-constant f) → UU (l1 ⊔ l2) + htpy-is-constant H K = + Σ ( center-partial-element-is-constant H ~ center-partial-element-is-constant K) + ( coherence-htpy-is-constant H K) + + refl-htpy-is-constant : + (H : is-constant f) → htpy-is-constant H H + refl-htpy-is-constant H = (refl-htpy , inv-htpy-right-unit-htpy) + + htpy-eq-is-constant : + (H K : is-constant f) → H ＝ K → htpy-is-constant H K + htpy-eq-is-constant H .H refl = refl-htpy-is-constant H + + is-torsorial-htpy-is-constant : + (H : is-constant f) → is-torsorial (htpy-is-constant H) + is-torsorial-htpy-is-constant H = + is-torsorial-Eq-structure + ( is-torsorial-htpy (center-partial-element-is-constant H)) + ( center-partial-element-is-constant H , refl-htpy) + (is-torsorial-htpy' (contraction-is-constant' H ∙h refl-htpy)) + + is-equiv-htpy-eq-is-constant : + (H K : is-constant f) → is-equiv (htpy-eq-is-constant H K) + is-equiv-htpy-eq-is-constant H = + fundamental-theorem-id + ( is-torsorial-htpy-is-constant H) + ( htpy-eq-is-constant H) + + extensionality-htpy-is-constant : + (H K : is-constant f) → (H ＝ K) ≃ htpy-is-constant H K + extensionality-htpy-is-constant H K = + ( htpy-eq-is-constant H K , is-equiv-htpy-eq-is-constant H K) + + eq-htpy-is-constant : + (H K : is-constant f) → htpy-is-constant H K → H ＝ K + eq-htpy-is-constant H K = + map-inv-is-equiv (is-equiv-htpy-eq-is-constant H K) +``` + +### If the domain has an element then the center partial element is unique + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + eq-center-is-constant-has-element-domain : + A → (H K : is-constant f) → + center-partial-element-is-constant H ~ center-partial-element-is-constant K + eq-center-is-constant-has-element-domain a H K _ = + inv (contraction-is-constant H a) ∙ contraction-is-constant K a +``` + +### If the codomain is a set then being constant is a property + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + (is-set-B : is-set B) + {f : A → B} + where + + eq-center-is-constant-is-set-codomain : + (H K : is-constant f) → + center-partial-element-is-constant H ~ center-partial-element-is-constant K + eq-center-is-constant-is-set-codomain H K |x| = + rec-trunc-Prop + ( Id-Prop + ( B , is-set-B) + ( center-partial-element-is-constant H |x|) + ( center-partial-element-is-constant K |x|)) + ( λ x → eq-center-is-constant-has-element-domain x H K |x|) + ( |x|) + + all-elements-equal-is-constant-is-set-codomain : + all-elements-equal (is-constant f) + all-elements-equal-is-constant-is-set-codomain H K = + eq-htpy-is-constant H K + ( ( eq-center-is-constant-is-set-codomain H K) , + ( λ x → + eq-is-prop + ( is-set-B + ( f x) + ( center-partial-element-is-constant K (unit-trunc-Prop x))))) + + is-prop-is-constant-is-set-codomain : + is-prop (is-constant f) + is-prop-is-constant-is-set-codomain = + is-prop-all-elements-equal + ( all-elements-equal-is-constant-is-set-codomain) +``` + +### Coherently constant maps from `A` to `B` are in correspondence with partial elements of `B` over `║ A ║₋₁` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + compute-constant-map : constant-map A B ≃ (║ A ║₋₁ → B) + compute-constant-map = + equivalence-reasoning + Σ (A → B) (is-constant) + ≃ Σ (║ A ║₋₁ → B) (λ b → Σ (A → B) (λ f → f ~ b ∘ unit-trunc-Prop)) + by equiv-left-swap-Σ + ≃ (║ A ║₋₁ → B) + by + right-unit-law-Σ-is-contr (λ b → is-torsorial-htpy' (b ∘ unit-trunc-Prop)) +``` + +### Coherently constant maps are weakly constant + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-weakly-constant-is-constant : + is-constant f → is-weakly-constant f + is-weakly-constant-is-constant H x y = + contraction-is-constant' H x ∙ inv (contraction-is-constant H y) +``` + +## References + +{{#bibliography}} {{#reference Kraus15}} + +## See also + +- [Null-homotopic maps](foundation.null-homotopic-maps.md) are coherently + constant, and if the domain is pointed the two notions coincide. diff --git a/src/foundation/constant-maps.lagda.md b/src/foundation/constant-maps.lagda.md index ec686e7417..2bdee58398 100644 --- a/src/foundation/constant-maps.lagda.md +++ b/src/foundation/constant-maps.lagda.md @@ -203,3 +203,4 @@ abstract ## See also - [Constant pointed maps](structured-types.constant-pointed-maps.md) +- [Coherently constant maps](foundation.coherently-constant-maps.md) diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index 2500c019f4..0f3124a31e 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -40,9 +40,9 @@ open import foundation-core.homotopies ## Idea A map `f : A → B` is said to be -{{#concept "null-homotopic" Disambiguation="map of types" Agda=is-null-homotopic}}, -or _constant_, if there is an element `y : B` such for every `x : A` we have -`f x ＝ y`. In other words, `f` is null-homotopic if it is +{{#concept "null-homotopic" Disambiguation="map of types" Agda=is-null-homotopic}} +if there is an element `y : B` such for every `x : A` we have `f x ＝ y`. In +other words, `f` is null-homotopic if it is [homotopic](foundation-core.homotopies.md) to a [constant](foundation-core.constant-maps.md) function. @@ -254,7 +254,9 @@ module _ ## See also -- [Weakly constant maps](foundation.weakly-constant-maps.md) +- Null-homotopic maps are + [coherently constant](foundation.coherently-constant-maps.md), and if the + domain is pointed the two notions coincide. ## External links diff --git a/src/foundation/weakly-constant-maps.lagda.md b/src/foundation/weakly-constant-maps.lagda.md index 741e4c32c8..1afdbc43a3 100644 --- a/src/foundation/weakly-constant-maps.lagda.md +++ b/src/foundation/weakly-constant-maps.lagda.md @@ -138,3 +138,7 @@ module _ ## References {{#bibliography}} {{#reference KECA17}} + +## See also + +- [Coherently constant maps](foundation.coherently-constant-maps.md) From 60650bd23d72d6755837fa01125c97aedc26edab Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 02:19:19 +0000 Subject: [PATCH 2/9] pre-commit --- src/foundation/coherently-constant-maps.lagda.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md index 131989f817..e7cd37c91b 100644 --- a/src/foundation/coherently-constant-maps.lagda.md +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -123,7 +123,9 @@ module _ coherence-htpy-is-constant : (H K : is-constant f) - (p : center-partial-element-is-constant H ~ center-partial-element-is-constant K) → + (p : + center-partial-element-is-constant H ~ + center-partial-element-is-constant K) → UU (l1 ⊔ l2) coherence-htpy-is-constant H K p = (x : A) → @@ -134,7 +136,8 @@ module _ htpy-is-constant : (H K : is-constant f) → UU (l1 ⊔ l2) htpy-is-constant H K = - Σ ( center-partial-element-is-constant H ~ center-partial-element-is-constant K) + Σ ( center-partial-element-is-constant H ~ + center-partial-element-is-constant K) ( coherence-htpy-is-constant H K) refl-htpy-is-constant : From 07812b646bd9c82af1f271b47ceb4a5c8a50d78d Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 02:21:31 +0000 Subject: [PATCH 3/9] fix typo --- src/foundation/coherently-constant-maps.lagda.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md index e7cd37c91b..dce1cc6a6f 100644 --- a/src/foundation/coherently-constant-maps.lagda.md +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -102,9 +102,8 @@ module _ ### Characterizing equality of coherent constancy witnesses -Two constancy witnesses `H` and `K` are equal if there is a homotopy -[equality](foundation-core.identity-types.md) of partial base points -`p : H₀ ~ K₀` such that for every `x : A` we have a +Two constancy witnesses `H` and `K` are equal if there is a homotopy of partial +base points `p : H₀ ~ K₀` such that for every `x : A` we have a [commuting triangle of identifications](foundation.commuting-triangles-of-identifications.md) ```text From cbde02aebb315ddc2cb9a7ebb4652e65b35afbd6 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 14:01:15 +0000 Subject: [PATCH 4/9] more additions --- src/foundation-core/constant-maps.lagda.md | 3 +- .../coherently-constant-maps.lagda.md | 268 +++++++++------- src/foundation/constant-maps.lagda.md | 3 +- src/foundation/null-homotopic-maps.lagda.md | 293 ++++++++++++------ src/foundation/split-idempotent-maps.lagda.md | 68 ++-- ...ropositional-truncation-into-sets.lagda.md | 40 +-- src/foundation/weakly-constant-maps.lagda.md | 151 ++++++--- ...otents-in-intensional-type-theory.lagda.md | 4 +- 8 files changed, 529 insertions(+), 301 deletions(-) diff --git a/src/foundation-core/constant-maps.lagda.md b/src/foundation-core/constant-maps.lagda.md index 577b33af65..d6fa02a4c1 100644 --- a/src/foundation-core/constant-maps.lagda.md +++ b/src/foundation-core/constant-maps.lagda.md @@ -32,5 +32,6 @@ const A b x = b ## See also +- [Coherently constant maps](foundation.coherently-constant-maps.md) for the + condition on a map of being constant - [Constant pointed maps](structured-types.constant-pointed-maps.md) -- [Coherently constant maps](foundation.coherently-constant-maps.md) diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md index dce1cc6a6f..2a8f02b244 100644 --- a/src/foundation/coherently-constant-maps.lagda.md +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -22,8 +22,10 @@ open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation.weakly-constant-maps +open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.function-types +open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies ``` @@ -32,44 +34,44 @@ open import foundation-core.homotopies ## Idea A map `f : A → B` is said to be -{{#concept "(coherently) constant" Disambiguation="map of types" WD="constant function "WDID=Q746264 Agda=is-constant Agda=constant-map}} +{{#concept "(coherently) constant" Disambiguation="map of types" WD="constant function" WDID=Q746264 Agda=is-constant-map Agda=constant-map}} if there is a [partial element](foundation.partial-elements.md) of `B`, `b : ║A║₋₁ → B` such that for every `x : A` we have `f x ＝ b`. {{#cite Kraus15}} ## Definition -### The type of coherent constancies of a map +### The type of constancy witnesses of a map ```agda -is-constant : +is-constant-map : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) -is-constant {A = A} {B} f = +is-constant-map {A = A} {B} f = Σ (║ A ║₋₁ → B) (λ b → (x : A) → f x ＝ b (unit-trunc-Prop x)) module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-constant f) + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-constant-map f) where - center-partial-element-is-constant : ║ A ║₋₁ → B - center-partial-element-is-constant = pr1 H + center-partial-element-is-constant-map : ║ A ║₋₁ → B + center-partial-element-is-constant-map = pr1 H - contraction-is-constant' : - (x : A) → f x ＝ center-partial-element-is-constant (unit-trunc-Prop x) - contraction-is-constant' = pr2 H + contraction-is-constant-map' : + (x : A) → f x ＝ center-partial-element-is-constant-map (unit-trunc-Prop x) + contraction-is-constant-map' = pr2 H - contraction-is-constant : - (x : A) {|x| : ║ A ║₋₁} → f x ＝ center-partial-element-is-constant |x| - contraction-is-constant x = - contraction-is-constant' x ∙ - ap center-partial-element-is-constant (eq-type-Prop (trunc-Prop A)) + contraction-is-constant-map : + (x : A) {|x| : ║ A ║₋₁} → f x ＝ center-partial-element-is-constant-map |x| + contraction-is-constant-map x = + contraction-is-constant-map' x ∙ + ap center-partial-element-is-constant-map (eq-type-Prop (trunc-Prop A)) ``` ### The type of coherently constant maps ```agda constant-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) -constant-map A B = Σ (A → B) is-constant +constant-map A B = Σ (A → B) is-constant-map module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : constant-map A B) @@ -78,32 +80,101 @@ module _ map-constant-map : A → B map-constant-map = pr1 f - is-constant-map-constant-map : is-constant map-constant-map - is-constant-map-constant-map = pr2 f + is-constant-constant-map : is-constant-map map-constant-map + is-constant-constant-map = pr2 f center-partial-element-constant-map : ║ A ║₋₁ → B center-partial-element-constant-map = - center-partial-element-is-constant is-constant-map-constant-map + center-partial-element-is-constant-map is-constant-constant-map contraction-constant-map' : (x : A) → map-constant-map x ＝ center-partial-element-constant-map (unit-trunc-Prop x) contraction-constant-map' = - contraction-is-constant' is-constant-map-constant-map + contraction-is-constant-map' is-constant-constant-map contraction-constant-map : (x : A) {|x| : ║ A ║₋₁} → map-constant-map x ＝ center-partial-element-constant-map |x| contraction-constant-map = - contraction-is-constant is-constant-map-constant-map + contraction-is-constant-map is-constant-constant-map ``` ## Properties -### Characterizing equality of coherent constancy witnesses +### Coherently constant maps from `A` to `B` are in correspondence with partial elements of `B` over `║ A ║₋₁` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + compute-constant-map : constant-map A B ≃ (║ A ║₋₁ → B) + compute-constant-map = + equivalence-reasoning + Σ (A → B) (is-constant-map) + ≃ Σ (║ A ║₋₁ → B) (λ b → Σ (A → B) (λ f → f ~ b ∘ unit-trunc-Prop)) + by equiv-left-swap-Σ + ≃ (║ A ║₋₁ → B) + by + right-unit-law-Σ-is-contr (λ b → is-torsorial-htpy' (b ∘ unit-trunc-Prop)) +``` + +### Characterizing equality of coherently constant maps + +Equality of constant maps is characterized by homotopy of their centers. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + htpy-constant-map : (f g : constant-map A B) → UU (l1 ⊔ l2) + htpy-constant-map f g = + center-partial-element-constant-map f ~ + center-partial-element-constant-map g + + refl-htpy-constant-map : + (f : constant-map A B) → htpy-constant-map f f + refl-htpy-constant-map f = refl-htpy + + htpy-eq-constant-map : + (f g : constant-map A B) → f ＝ g → htpy-constant-map f g + htpy-eq-constant-map f .f refl = refl-htpy-constant-map f + + is-torsorial-htpy-constant-map : + (f : constant-map A B) → is-torsorial (htpy-constant-map f) + is-torsorial-htpy-constant-map f = + is-contr-equiv + ( Σ (║ A ║₋₁ → B) (center-partial-element-constant-map f ~_)) + ( equiv-Σ-equiv-base + ( center-partial-element-constant-map f ~_) + ( compute-constant-map)) + ( is-torsorial-htpy (center-partial-element-constant-map f)) + + is-equiv-htpy-eq-constant-map : + (f g : constant-map A B) → is-equiv (htpy-eq-constant-map f g) + is-equiv-htpy-eq-constant-map f = + fundamental-theorem-id + ( is-torsorial-htpy-constant-map f) + ( htpy-eq-constant-map f) + + extensionality-constant-map : + (f g : constant-map A B) → (f ＝ g) ≃ htpy-constant-map f g + extensionality-constant-map f g = + ( htpy-eq-constant-map f g , + is-equiv-htpy-eq-constant-map f g) + + eq-htpy-constant-map : + (f g : constant-map A B) → htpy-constant-map f g → f ＝ g + eq-htpy-constant-map f g = + map-inv-equiv (extensionality-constant-map f g) +``` + +### Characterizing equality of constancy witnesses -Two constancy witnesses `H` and `K` are equal if there is a homotopy of partial -base points `p : H₀ ~ K₀` such that for every `x : A` we have a +Two constancy witnesses `H` and `K` are equal if there is a homotopy of centers +`p : H₀ ~ K₀` such that for every `x : A` we have a [commuting triangle of identifications](foundation.commuting-triangles-of-identifications.md) ```text @@ -120,57 +191,57 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - coherence-htpy-is-constant : - (H K : is-constant f) + coherence-htpy-is-constant-map : + (H K : is-constant-map f) (p : - center-partial-element-is-constant H ~ - center-partial-element-is-constant K) → + center-partial-element-is-constant-map H ~ + center-partial-element-is-constant-map K) → UU (l1 ⊔ l2) - coherence-htpy-is-constant H K p = + coherence-htpy-is-constant-map H K p = (x : A) → coherence-triangle-identifications - ( contraction-is-constant' K x) + ( contraction-is-constant-map' K x) ( p (unit-trunc-Prop x)) - ( contraction-is-constant' H x) + ( contraction-is-constant-map' H x) - htpy-is-constant : (H K : is-constant f) → UU (l1 ⊔ l2) - htpy-is-constant H K = - Σ ( center-partial-element-is-constant H ~ - center-partial-element-is-constant K) - ( coherence-htpy-is-constant H K) + htpy-is-constant-map : (H K : is-constant-map f) → UU (l1 ⊔ l2) + htpy-is-constant-map H K = + Σ ( center-partial-element-is-constant-map H ~ + center-partial-element-is-constant-map K) + ( coherence-htpy-is-constant-map H K) - refl-htpy-is-constant : - (H : is-constant f) → htpy-is-constant H H - refl-htpy-is-constant H = (refl-htpy , inv-htpy-right-unit-htpy) + refl-htpy-is-constant-map : + (H : is-constant-map f) → htpy-is-constant-map H H + refl-htpy-is-constant-map H = (refl-htpy , inv-htpy-right-unit-htpy) - htpy-eq-is-constant : - (H K : is-constant f) → H ＝ K → htpy-is-constant H K - htpy-eq-is-constant H .H refl = refl-htpy-is-constant H + htpy-eq-is-constant-map : + (H K : is-constant-map f) → H ＝ K → htpy-is-constant-map H K + htpy-eq-is-constant-map H .H refl = refl-htpy-is-constant-map H - is-torsorial-htpy-is-constant : - (H : is-constant f) → is-torsorial (htpy-is-constant H) - is-torsorial-htpy-is-constant H = + is-torsorial-htpy-is-constant-map : + (H : is-constant-map f) → is-torsorial (htpy-is-constant-map H) + is-torsorial-htpy-is-constant-map H = is-torsorial-Eq-structure - ( is-torsorial-htpy (center-partial-element-is-constant H)) - ( center-partial-element-is-constant H , refl-htpy) - (is-torsorial-htpy' (contraction-is-constant' H ∙h refl-htpy)) + ( is-torsorial-htpy (center-partial-element-is-constant-map H)) + ( center-partial-element-is-constant-map H , refl-htpy) + (is-torsorial-htpy' (contraction-is-constant-map' H ∙h refl-htpy)) - is-equiv-htpy-eq-is-constant : - (H K : is-constant f) → is-equiv (htpy-eq-is-constant H K) - is-equiv-htpy-eq-is-constant H = + is-equiv-htpy-eq-is-constant-map : + (H K : is-constant-map f) → is-equiv (htpy-eq-is-constant-map H K) + is-equiv-htpy-eq-is-constant-map H = fundamental-theorem-id - ( is-torsorial-htpy-is-constant H) - ( htpy-eq-is-constant H) - - extensionality-htpy-is-constant : - (H K : is-constant f) → (H ＝ K) ≃ htpy-is-constant H K - extensionality-htpy-is-constant H K = - ( htpy-eq-is-constant H K , is-equiv-htpy-eq-is-constant H K) - - eq-htpy-is-constant : - (H K : is-constant f) → htpy-is-constant H K → H ＝ K - eq-htpy-is-constant H K = - map-inv-is-equiv (is-equiv-htpy-eq-is-constant H K) + ( is-torsorial-htpy-is-constant-map H) + ( htpy-eq-is-constant-map H) + + extensionality-is-constant-map : + (H K : is-constant-map f) → (H ＝ K) ≃ htpy-is-constant-map H K + extensionality-is-constant-map H K = + ( htpy-eq-is-constant-map H K , is-equiv-htpy-eq-is-constant-map H K) + + eq-htpy-is-constant-map : + (H K : is-constant-map f) → htpy-is-constant-map H K → H ＝ K + eq-htpy-is-constant-map H K = + map-inv-is-equiv (is-equiv-htpy-eq-is-constant-map H K) ``` ### If the domain has an element then the center partial element is unique @@ -180,11 +251,12 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - eq-center-is-constant-has-element-domain : - A → (H K : is-constant f) → - center-partial-element-is-constant H ~ center-partial-element-is-constant K - eq-center-is-constant-has-element-domain a H K _ = - inv (contraction-is-constant H a) ∙ contraction-is-constant K a + htpy-center-is-constant-map-has-element-domain : + A → (H K : is-constant-map f) → + center-partial-element-is-constant-map H ~ + center-partial-element-is-constant-map K + htpy-center-is-constant-map-has-element-domain a H K _ = + inv (contraction-is-constant-map H a) ∙ contraction-is-constant-map K a ``` ### If the codomain is a set then being constant is a property @@ -196,52 +268,34 @@ module _ {f : A → B} where - eq-center-is-constant-is-set-codomain : - (H K : is-constant f) → - center-partial-element-is-constant H ~ center-partial-element-is-constant K - eq-center-is-constant-is-set-codomain H K |x| = + htpy-center-is-constant-map-is-set-codomain : + (H K : is-constant-map f) → + center-partial-element-is-constant-map H ~ + center-partial-element-is-constant-map K + htpy-center-is-constant-map-is-set-codomain H K |x| = rec-trunc-Prop ( Id-Prop ( B , is-set-B) - ( center-partial-element-is-constant H |x|) - ( center-partial-element-is-constant K |x|)) - ( λ x → eq-center-is-constant-has-element-domain x H K |x|) + ( center-partial-element-is-constant-map H |x|) + ( center-partial-element-is-constant-map K |x|)) + ( λ x → htpy-center-is-constant-map-has-element-domain x H K |x|) ( |x|) - all-elements-equal-is-constant-is-set-codomain : - all-elements-equal (is-constant f) - all-elements-equal-is-constant-is-set-codomain H K = - eq-htpy-is-constant H K - ( ( eq-center-is-constant-is-set-codomain H K) , + all-elements-equal-is-constant-map-is-set-codomain : + all-elements-equal (is-constant-map f) + all-elements-equal-is-constant-map-is-set-codomain H K = + eq-htpy-is-constant-map H K + ( ( htpy-center-is-constant-map-is-set-codomain H K) , ( λ x → eq-is-prop ( is-set-B ( f x) - ( center-partial-element-is-constant K (unit-trunc-Prop x))))) + ( center-partial-element-is-constant-map K (unit-trunc-Prop x))))) - is-prop-is-constant-is-set-codomain : - is-prop (is-constant f) - is-prop-is-constant-is-set-codomain = + is-prop-is-constant-map-is-set-codomain : is-prop (is-constant-map f) + is-prop-is-constant-map-is-set-codomain = is-prop-all-elements-equal - ( all-elements-equal-is-constant-is-set-codomain) -``` - -### Coherently constant maps from `A` to `B` are in correspondence with partial elements of `B` over `║ A ║₋₁` - -```agda -module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} - where - - compute-constant-map : constant-map A B ≃ (║ A ║₋₁ → B) - compute-constant-map = - equivalence-reasoning - Σ (A → B) (is-constant) - ≃ Σ (║ A ║₋₁ → B) (λ b → Σ (A → B) (λ f → f ~ b ∘ unit-trunc-Prop)) - by equiv-left-swap-Σ - ≃ (║ A ║₋₁ → B) - by - right-unit-law-Σ-is-contr (λ b → is-torsorial-htpy' (b ∘ unit-trunc-Prop)) + ( all-elements-equal-is-constant-map-is-set-codomain) ``` ### Coherently constant maps are weakly constant @@ -251,10 +305,10 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - is-weakly-constant-is-constant : - is-constant f → is-weakly-constant f - is-weakly-constant-is-constant H x y = - contraction-is-constant' H x ∙ inv (contraction-is-constant H y) + is-weakly-constant-map-is-constant-map : + is-constant-map f → is-weakly-constant-map f + is-weakly-constant-map-is-constant-map H x y = + contraction-is-constant-map' H x ∙ inv (contraction-is-constant-map H y) ``` ## References diff --git a/src/foundation/constant-maps.lagda.md b/src/foundation/constant-maps.lagda.md index 2bdee58398..dd9b92514d 100644 --- a/src/foundation/constant-maps.lagda.md +++ b/src/foundation/constant-maps.lagda.md @@ -202,5 +202,6 @@ abstract ## See also +- [Coherently constant maps](foundation.coherently-constant-maps.md) for the + condition on a map of being constant - [Constant pointed maps](structured-types.constant-pointed-maps.md) -- [Coherently constant maps](foundation.coherently-constant-maps.md) diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index 0f3124a31e..54a5854b83 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -7,6 +7,7 @@ module foundation.null-homotopic-maps where
Imports ```agda +open import foundation.coherently-constant-maps open import foundation.commuting-triangles-of-identifications open import foundation.constant-maps open import foundation.dependent-pair-types @@ -15,23 +16,19 @@ open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopy-induction open import foundation.identity-types -open import foundation.images open import foundation.inhabited-types -open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.type-arithmetic-dependent-pair-types -open import foundation.unit-type open import foundation.universal-property-empty-type open import foundation.universe-levels open import foundation.weakly-constant-maps open import foundation-core.contractible-types open import foundation-core.equivalences -open import foundation-core.function-types open import foundation-core.homotopies ``` @@ -40,7 +37,7 @@ open import foundation-core.homotopies ## Idea A map `f : A → B` is said to be -{{#concept "null-homotopic" Disambiguation="map of types" Agda=is-null-homotopic}} +{{#concept "null-homotopic" Disambiguation="map of types" Agda=is-null-homotopic-map}} if there is an element `y : B` such for every `x : A` we have `f x ＝ y`. In other words, `f` is null-homotopic if it is [homotopic](foundation-core.homotopies.md) to a @@ -51,23 +48,118 @@ other words, `f` is null-homotopic if it is ### The type of null-homotopies of a map ```agda -is-null-homotopic : +is-null-homotopic-map : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) -is-null-homotopic {A = A} {B} f = Σ B (λ y → (x : A) → f x ＝ y) +is-null-homotopic-map {A = A} {B} f = Σ B (λ y → (x : A) → f x ＝ y) module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} (H : is-null-homotopic f) + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + (H : is-null-homotopic-map f) where - center-is-null-homotopic : B - center-is-null-homotopic = pr1 H + center-is-null-homotopic-map : B + center-is-null-homotopic-map = pr1 H - contraction-is-null-homotopic : (x : A) → f x ＝ center-is-null-homotopic - contraction-is-null-homotopic = pr2 H + contraction-is-null-homotopic-map : + (x : A) → f x ＝ center-is-null-homotopic-map + contraction-is-null-homotopic-map = pr2 H +``` + +### The type of null-homotopic maps + +```agda +null-homotopic-map : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2) +null-homotopic-map A B = Σ (A → B) is-null-homotopic-map + +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : null-homotopic-map A B) + where + + map-null-homotopic-map : A → B + map-null-homotopic-map = pr1 f + + is-null-homotopic-null-homotopic-map : + is-null-homotopic-map map-null-homotopic-map + is-null-homotopic-null-homotopic-map = pr2 f + + center-null-homotopic-map : B + center-null-homotopic-map = + center-is-null-homotopic-map is-null-homotopic-null-homotopic-map + + contraction-null-homotopic-map : + (x : A) → + map-null-homotopic-map x ＝ center-null-homotopic-map + contraction-null-homotopic-map = + contraction-is-null-homotopic-map is-null-homotopic-null-homotopic-map ``` ## Properties +### Null-homotopic maps from `A` to `B` are in correspondence with elements of `B` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + compute-null-homotopic-map : null-homotopic-map A B ≃ B + compute-null-homotopic-map = + equivalence-reasoning + Σ (A → B) (is-null-homotopic-map) + ≃ Σ B (λ b → Σ (A → B) (λ f → f ~ const A b)) by equiv-left-swap-Σ + ≃ B by right-unit-law-Σ-is-contr (λ b → is-torsorial-htpy' (const A b)) +``` + +### Characterizing equality of null-homotopic maps + +Equality of null-homotopic maps is characterized by equality of their centers. + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} + where + + Eq-null-homotopic-map : (f g : null-homotopic-map A B) → UU l2 + Eq-null-homotopic-map f g = + center-null-homotopic-map f ＝ center-null-homotopic-map g + + refl-Eq-null-homotopic-map : + (f : null-homotopic-map A B) → Eq-null-homotopic-map f f + refl-Eq-null-homotopic-map f = refl + + Eq-eq-null-homotopic-map : + (f g : null-homotopic-map A B) → f ＝ g → Eq-null-homotopic-map f g + Eq-eq-null-homotopic-map f .f refl = refl-Eq-null-homotopic-map f + + is-torsorial-Eq-null-homotopic-map : + (f : null-homotopic-map A B) → is-torsorial (Eq-null-homotopic-map f) + is-torsorial-Eq-null-homotopic-map f = + is-contr-equiv + ( Σ B (Id (center-null-homotopic-map f))) + ( equiv-Σ-equiv-base + ( Id (center-null-homotopic-map f)) + ( compute-null-homotopic-map)) + ( is-torsorial-Id (center-null-homotopic-map f)) + + is-equiv-Eq-eq-null-homotopic-map : + (f g : null-homotopic-map A B) → is-equiv (Eq-eq-null-homotopic-map f g) + is-equiv-Eq-eq-null-homotopic-map f = + fundamental-theorem-id + ( is-torsorial-Eq-null-homotopic-map f) + ( Eq-eq-null-homotopic-map f) + + extensionality-null-homotopic-map : + (f g : null-homotopic-map A B) → (f ＝ g) ≃ Eq-null-homotopic-map f g + extensionality-null-homotopic-map f g = + ( Eq-eq-null-homotopic-map f g , + is-equiv-Eq-eq-null-homotopic-map f g) + + eq-Eq-null-homotopic-map : + (f g : null-homotopic-map A B) → Eq-null-homotopic-map f g → f ＝ g + eq-Eq-null-homotopic-map f g = + map-inv-equiv (extensionality-null-homotopic-map f g) +``` + ### Characterizing equality of null-homotopies Two null-homotopies `H` and `K` are equal if there is an @@ -89,54 +181,56 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - coherence-htpy-is-null-homotopic : - (H K : is-null-homotopic f) - (p : center-is-null-homotopic H ＝ center-is-null-homotopic K) → + coherence-htpy-is-null-homotopic-map : + (H K : is-null-homotopic-map f) + (p : center-is-null-homotopic-map H ＝ center-is-null-homotopic-map K) → UU (l1 ⊔ l2) - coherence-htpy-is-null-homotopic H K p = + coherence-htpy-is-null-homotopic-map H K p = (x : A) → coherence-triangle-identifications - ( contraction-is-null-homotopic K x) + ( contraction-is-null-homotopic-map K x) ( p) - ( contraction-is-null-homotopic H x) + ( contraction-is-null-homotopic-map H x) - htpy-is-null-homotopic : (H K : is-null-homotopic f) → UU (l1 ⊔ l2) - htpy-is-null-homotopic H K = - Σ ( center-is-null-homotopic H ＝ center-is-null-homotopic K) - ( coherence-htpy-is-null-homotopic H K) + htpy-is-null-homotopic-map : (H K : is-null-homotopic-map f) → UU (l1 ⊔ l2) + htpy-is-null-homotopic-map H K = + Σ ( center-is-null-homotopic-map H ＝ center-is-null-homotopic-map K) + ( coherence-htpy-is-null-homotopic-map H K) - refl-htpy-is-null-homotopic : - (H : is-null-homotopic f) → htpy-is-null-homotopic H H - refl-htpy-is-null-homotopic H = (refl , inv-htpy-right-unit-htpy) + refl-htpy-is-null-homotopic-map : + (H : is-null-homotopic-map f) → htpy-is-null-homotopic-map H H + refl-htpy-is-null-homotopic-map H = (refl , inv-htpy-right-unit-htpy) - htpy-eq-is-null-homotopic : - (H K : is-null-homotopic f) → H ＝ K → htpy-is-null-homotopic H K - htpy-eq-is-null-homotopic H .H refl = refl-htpy-is-null-homotopic H + htpy-eq-is-null-homotopic-map : + (H K : is-null-homotopic-map f) → H ＝ K → htpy-is-null-homotopic-map H K + htpy-eq-is-null-homotopic-map H .H refl = refl-htpy-is-null-homotopic-map H - is-torsorial-htpy-is-null-homotopic : - (H : is-null-homotopic f) → is-torsorial (htpy-is-null-homotopic H) - is-torsorial-htpy-is-null-homotopic H = + is-torsorial-htpy-is-null-homotopic-map : + (H : is-null-homotopic-map f) → is-torsorial (htpy-is-null-homotopic-map H) + is-torsorial-htpy-is-null-homotopic-map H = is-torsorial-Eq-structure - ( is-torsorial-Id (center-is-null-homotopic H)) - ( center-is-null-homotopic H , refl) - ( is-torsorial-htpy' (contraction-is-null-homotopic H ∙h refl-htpy)) - - is-equiv-htpy-eq-is-null-homotopic : - (H K : is-null-homotopic f) → is-equiv (htpy-eq-is-null-homotopic H K) - is-equiv-htpy-eq-is-null-homotopic H = + ( is-torsorial-Id (center-is-null-homotopic-map H)) + ( center-is-null-homotopic-map H , refl) + ( is-torsorial-htpy' (contraction-is-null-homotopic-map H ∙h refl-htpy)) + + is-equiv-htpy-eq-is-null-homotopic-map : + (H K : is-null-homotopic-map f) → + is-equiv (htpy-eq-is-null-homotopic-map H K) + is-equiv-htpy-eq-is-null-homotopic-map H = fundamental-theorem-id - ( is-torsorial-htpy-is-null-homotopic H) - ( htpy-eq-is-null-homotopic H) - - extensionality-htpy-is-null-homotopic : - (H K : is-null-homotopic f) → (H ＝ K) ≃ htpy-is-null-homotopic H K - extensionality-htpy-is-null-homotopic H K = - ( htpy-eq-is-null-homotopic H K , is-equiv-htpy-eq-is-null-homotopic H K) - - eq-htpy-is-null-homotopic : - (H K : is-null-homotopic f) → htpy-is-null-homotopic H K → H ＝ K - eq-htpy-is-null-homotopic H K = - map-inv-is-equiv (is-equiv-htpy-eq-is-null-homotopic H K) + ( is-torsorial-htpy-is-null-homotopic-map H) + ( htpy-eq-is-null-homotopic-map H) + + extensionality-is-null-homotopic-map : + (H K : is-null-homotopic-map f) → (H ＝ K) ≃ htpy-is-null-homotopic-map H K + extensionality-is-null-homotopic-map H K = + ( htpy-eq-is-null-homotopic-map H K , + is-equiv-htpy-eq-is-null-homotopic-map H K) + + eq-htpy-is-null-homotopic-map : + (H K : is-null-homotopic-map f) → htpy-is-null-homotopic-map H K → H ＝ K + eq-htpy-is-null-homotopic-map H K = + map-inv-is-equiv (is-equiv-htpy-eq-is-null-homotopic-map H K) ``` ### If the domain is empty the type of null-homotopies is equivalent to elements of `B` @@ -146,8 +240,8 @@ module _ {l : Level} {B : UU l} {f : empty → B} where - compute-is-null-homotopic-empty-domain : is-null-homotopic f ≃ B - compute-is-null-homotopic-empty-domain = + compute-is-null-homotopic-map-empty-domain : is-null-homotopic-map f ≃ B + compute-is-null-homotopic-map-empty-domain = right-unit-law-Σ-is-contr ( λ y → dependent-universal-property-empty' (λ x → f x ＝ y)) ``` @@ -159,12 +253,13 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - eq-center-is-null-homotopic-has-element-domain : + eq-center-is-null-homotopic-map-has-element-domain : A → - (H K : is-null-homotopic f) → - center-is-null-homotopic H ＝ center-is-null-homotopic K - eq-center-is-null-homotopic-has-element-domain a H K = - inv (contraction-is-null-homotopic H a) ∙ contraction-is-null-homotopic K a + (H K : is-null-homotopic-map f) → + center-is-null-homotopic-map H ＝ center-is-null-homotopic-map K + eq-center-is-null-homotopic-map-has-element-domain a H K = + inv (contraction-is-null-homotopic-map H a) ∙ + contraction-is-null-homotopic-map K a ``` ### If the codomain is a set and the domain has an element then being null-homotopic is a property @@ -176,18 +271,19 @@ module _ {f : A → B} where - all-elements-equal-is-null-homotopic-has-element-domain-is-set-codomain : - all-elements-equal (is-null-homotopic f) - all-elements-equal-is-null-homotopic-has-element-domain-is-set-codomain H K = - eq-htpy-is-null-homotopic H K - ( ( eq-center-is-null-homotopic-has-element-domain a H K) , - ( λ x → eq-is-prop (is-set-B (f x) (center-is-null-homotopic K)))) - - is-prop-is-null-homotopic-has-element-domain-is-set-codomain : - is-prop (is-null-homotopic f) - is-prop-is-null-homotopic-has-element-domain-is-set-codomain = + all-elements-equal-is-null-homotopic-map-has-element-domain-is-set-codomain : + all-elements-equal (is-null-homotopic-map f) + all-elements-equal-is-null-homotopic-map-has-element-domain-is-set-codomain + H K = + eq-htpy-is-null-homotopic-map H K + ( ( eq-center-is-null-homotopic-map-has-element-domain a H K) , + ( λ x → eq-is-prop (is-set-B (f x) (center-is-null-homotopic-map K)))) + + is-prop-is-null-homotopic-map-has-element-domain-is-set-codomain : + is-prop (is-null-homotopic-map f) + is-prop-is-null-homotopic-map-has-element-domain-is-set-codomain = is-prop-all-elements-equal - ( all-elements-equal-is-null-homotopic-has-element-domain-is-set-codomain) + ( all-elements-equal-is-null-homotopic-map-has-element-domain-is-set-codomain) ``` ### If the codomain is a set and the domain is inhabited then being null-homotopic is a property @@ -199,45 +295,45 @@ module _ {f : A → B} where - eq-center-is-null-homotopic-is-inhabited-domain-is-set-codomain : - (H K : is-null-homotopic f) → - center-is-null-homotopic H ＝ center-is-null-homotopic K - eq-center-is-null-homotopic-is-inhabited-domain-is-set-codomain H K = + eq-center-is-null-homotopic-map-is-inhabited-domain-is-set-codomain : + (H K : is-null-homotopic-map f) → + center-is-null-homotopic-map H ＝ center-is-null-homotopic-map K + eq-center-is-null-homotopic-map-is-inhabited-domain-is-set-codomain H K = rec-trunc-Prop ( Id-Prop ( B , is-set-B) - ( center-is-null-homotopic H) - ( center-is-null-homotopic K)) - ( λ x → eq-center-is-null-homotopic-has-element-domain x H K) + ( center-is-null-homotopic-map H) + ( center-is-null-homotopic-map K)) + ( λ x → eq-center-is-null-homotopic-map-has-element-domain x H K) ( a) - all-elements-equal-is-null-homotopic-is-inhabited-domain-is-set-codomain : - all-elements-equal (is-null-homotopic f) - all-elements-equal-is-null-homotopic-is-inhabited-domain-is-set-codomain H K = - eq-htpy-is-null-homotopic H K - ( ( eq-center-is-null-homotopic-is-inhabited-domain-is-set-codomain H K) , - ( λ x → eq-is-prop (is-set-B (f x) (center-is-null-homotopic K)))) - - is-prop-is-null-homotopic-is-inhabited-domain-is-set-codomain : - is-prop (is-null-homotopic f) - is-prop-is-null-homotopic-is-inhabited-domain-is-set-codomain = + all-elements-equal-is-null-homotopic-map-is-inhabited-domain-is-set-codomain : + all-elements-equal (is-null-homotopic-map f) + all-elements-equal-is-null-homotopic-map-is-inhabited-domain-is-set-codomain + H K = + eq-htpy-is-null-homotopic-map H K + ( ( eq-center-is-null-homotopic-map-is-inhabited-domain-is-set-codomain + ( H) + ( K)) , + ( λ x → eq-is-prop (is-set-B (f x) (center-is-null-homotopic-map K)))) + + is-prop-is-null-homotopic-map-is-inhabited-domain-is-set-codomain : + is-prop (is-null-homotopic-map f) + is-prop-is-null-homotopic-map-is-inhabited-domain-is-set-codomain = is-prop-all-elements-equal - ( all-elements-equal-is-null-homotopic-is-inhabited-domain-is-set-codomain) + ( all-elements-equal-is-null-homotopic-map-is-inhabited-domain-is-set-codomain) ``` -### Null-homotopic maps from `A` to `B` are in correspondence with elements of `B` +### Null-homotopic maps are constant ```agda module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - compute-null-homotopic-map : Σ (A → B) (is-null-homotopic) ≃ B - compute-null-homotopic-map = - equivalence-reasoning - Σ (A → B) (is-null-homotopic) - ≃ Σ B (λ b → Σ (A → B) (λ f → f ~ const A b)) by equiv-left-swap-Σ - ≃ B by right-unit-law-Σ-is-contr (λ b → is-torsorial-htpy' (const A b)) + is-constant-map-is-null-homotopic-map : + is-null-homotopic-map f → is-constant-map f + is-constant-map-is-null-homotopic-map (b , H) = ((λ _ → b) , H) ``` ### Null-homotopic maps are weakly constant @@ -247,16 +343,17 @@ module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} where - is-weakly-constant-is-null-homotopic : - is-null-homotopic f → is-weakly-constant f - is-weakly-constant-is-null-homotopic (b , H) x y = H x ∙ inv (H y) + is-weakly-constant-map-is-null-homotopic-map : + is-null-homotopic-map f → is-weakly-constant-map f + is-weakly-constant-map-is-null-homotopic-map (b , H) x y = H x ∙ inv (H y) ``` ## See also - Null-homotopic maps are [coherently constant](foundation.coherently-constant-maps.md), and if the - domain is pointed the two notions coincide. + domain is pointed the two notions coincide +- [Constant pointed maps](structured-types.constant-pointed-types.md) ## External links diff --git a/src/foundation/split-idempotent-maps.lagda.md b/src/foundation/split-idempotent-maps.lagda.md index e3a320b622..6935652587 100644 --- a/src/foundation/split-idempotent-maps.lagda.md +++ b/src/foundation/split-idempotent-maps.lagda.md @@ -620,60 +620,60 @@ This is Theorem 3.9 of {{#cite Shu17}}. ```agda module _ {l : Level} {A : UU l} {f : A → A} - (H : is-idempotent f) (W : is-weakly-constant f) + (H : is-idempotent f) (W : is-weakly-constant-map f) where - splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent : + splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent : UU l - splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent = + splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent = fixed-point f - inclusion-is-split-idempotent-is-weakly-constant-is-idempotent : - splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent → + inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent : + splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent → A - inclusion-is-split-idempotent-is-weakly-constant-is-idempotent = pr1 + inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent = pr1 - map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent : A → - splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent - map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent x = + splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent + map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent x = ( f x , H x) - is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent : is-retraction - ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) - ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) - is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent + ( inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent) + ( map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent) + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent _ = - eq-is-prop (is-prop-fixed-point-is-weakly-constant W) + eq-is-prop (is-prop-fixed-point-is-weakly-constant-map W) - retraction-is-split-idempotent-is-weakly-constant-is-idempotent : + retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent : retraction - ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent) - retraction-is-split-idempotent-is-weakly-constant-is-idempotent = - ( map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent , - is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent) + ( inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent) + retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent = + ( map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent , + is-retraction-map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent) - retract-is-split-idempotent-is-weakly-constant-is-idempotent : + retract-is-split-idempotent-is-weakly-constant-map-is-idempotent : retract ( A) - ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent) - retract-is-split-idempotent-is-weakly-constant-is-idempotent = - ( inclusion-is-split-idempotent-is-weakly-constant-is-idempotent , - retraction-is-split-idempotent-is-weakly-constant-is-idempotent) - - htpy-is-split-idempotent-is-weakly-constant-is-idempotent : - inclusion-is-split-idempotent-is-weakly-constant-is-idempotent ∘ - map-retraction-is-split-idempotent-is-weakly-constant-is-idempotent ~ + ( splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent) + retract-is-split-idempotent-is-weakly-constant-map-is-idempotent = + ( inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent , + retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent) + + htpy-is-split-idempotent-is-weakly-constant-map-is-idempotent : + inclusion-is-split-idempotent-is-weakly-constant-map-is-idempotent ∘ + map-retraction-is-split-idempotent-is-weakly-constant-map-is-idempotent ~ f - htpy-is-split-idempotent-is-weakly-constant-is-idempotent = refl-htpy + htpy-is-split-idempotent-is-weakly-constant-map-is-idempotent = refl-htpy - is-split-idempotent-is-weakly-constant-is-idempotent : + is-split-idempotent-is-weakly-constant-map-is-idempotent : is-split-idempotent l f - is-split-idempotent-is-weakly-constant-is-idempotent = - ( splitting-type-is-split-idempotent-is-weakly-constant-is-idempotent , - retract-is-split-idempotent-is-weakly-constant-is-idempotent , - htpy-is-split-idempotent-is-weakly-constant-is-idempotent) + is-split-idempotent-is-weakly-constant-map-is-idempotent = + ( splitting-type-is-split-idempotent-is-weakly-constant-map-is-idempotent , + retract-is-split-idempotent-is-weakly-constant-map-is-idempotent , + htpy-is-split-idempotent-is-weakly-constant-map-is-idempotent) ``` ### Quasicoherently idempotent maps split 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 124181f37d..27f1fb5de1 100644 --- a/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md +++ b/src/foundation/universal-property-propositional-truncation-into-sets.lagda.md @@ -38,21 +38,21 @@ universal property of the propositional truncations with respect to sets. ### The precomposition map that is used to state the universal property ```agda -is-weakly-constant-precomp-unit-trunc-Prop : +is-weakly-constant-map-precomp-unit-trunc-Prop : {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : type-trunc-Prop A → B) → - is-weakly-constant (g ∘ unit-trunc-Prop) -is-weakly-constant-precomp-unit-trunc-Prop g x y = + is-weakly-constant-map (g ∘ unit-trunc-Prop) +is-weakly-constant-map-precomp-unit-trunc-Prop g x y = ap ( g) ( eq-is-prop (is-prop-type-trunc-Prop)) precomp-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → - (type-trunc-Prop A → type-Set B) → Σ (A → type-Set B) is-weakly-constant + (type-trunc-Prop A → type-Set B) → Σ (A → type-Set B) is-weakly-constant-map pr1 (precomp-universal-property-set-quotient-trunc-Prop B g) = g ∘ unit-trunc-Prop pr2 (precomp-universal-property-set-quotient-trunc-Prop B g) = - is-weakly-constant-precomp-unit-trunc-Prop g + is-weakly-constant-map-precomp-unit-trunc-Prop g ``` ## Properties @@ -61,11 +61,11 @@ pr2 (precomp-universal-property-set-quotient-trunc-Prop B g) = ```agda abstract - all-elements-equal-image-is-weakly-constant : + all-elements-equal-image-is-weakly-constant-map : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant f → + 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 B f H (x , s) (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 @@ -76,21 +76,21 @@ abstract ( λ v → inv (pr2 u) ∙ H (pr1 u) (pr1 v) ∙ pr2 v))) abstract - is-prop-image-is-weakly-constant : + is-prop-image-is-weakly-constant-map : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant f → + is-weakly-constant-map f → is-prop (Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b))) - is-prop-image-is-weakly-constant B f H = + is-prop-image-is-weakly-constant-map B f H = is-prop-all-elements-equal - ( all-elements-equal-image-is-weakly-constant B f H) + ( all-elements-equal-image-is-weakly-constant-map B f H) image-weakly-constant-map-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant f → Prop (l1 ⊔ l2) + is-weakly-constant-map f → Prop (l1 ⊔ l2) pr1 (image-weakly-constant-map-Prop B f H) = Σ (type-Set B) (λ b → type-trunc-Prop (fiber f b)) pr2 (image-weakly-constant-map-Prop B f H) = - is-prop-image-is-weakly-constant B f H + is-prop-image-is-weakly-constant-map B f H ``` ### The universal property @@ -98,7 +98,7 @@ pr2 (image-weakly-constant-map-Prop B f H) = ```agda map-universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) → - is-weakly-constant f → type-trunc-Prop A → type-Set B + is-weakly-constant-map f → type-trunc-Prop A → type-Set B map-universal-property-set-quotient-trunc-Prop B f H = ( pr1) ∘ ( map-universal-property-trunc-Prop @@ -107,20 +107,20 @@ map-universal-property-set-quotient-trunc-Prop B f H = map-universal-property-set-quotient-trunc-Prop' : {l1 l2 : Level} {A : UU l1} (B : Set l2) → - Σ (A → type-Set B) is-weakly-constant → type-trunc-Prop A → type-Set B + Σ (A → type-Set B) is-weakly-constant-map → type-trunc-Prop A → type-Set B 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 f) → + (H : is-weakly-constant-map 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) ( eq-is-prop' - ( is-prop-image-is-weakly-constant B f H) + ( is-prop-image-is-weakly-constant-map B f H) ( map-universal-property-trunc-Prop ( image-weakly-constant-map-Prop B f H) ( λ x → (f x , unit-trunc-Prop (x , refl))) @@ -133,7 +133,7 @@ abstract ( map-universal-property-set-quotient-trunc-Prop' B)) ~ id is-section-map-universal-property-set-quotient-trunc-Prop B (f , H) = eq-type-subtype - ( is-weakly-constant-prop-Set B) + ( is-weakly-constant-map-prop-Set B) ( eq-htpy (htpy-universal-property-set-quotient-trunc-Prop B f H)) is-retraction-map-universal-property-set-quotient-trunc-Prop : @@ -151,7 +151,7 @@ abstract ( g x)) ( htpy-universal-property-set-quotient-trunc-Prop B ( g ∘ unit-trunc-Prop) - ( is-weakly-constant-precomp-unit-trunc-Prop g))) + ( is-weakly-constant-map-precomp-unit-trunc-Prop g))) universal-property-set-quotient-trunc-Prop : {l1 l2 : Level} {A : UU l1} (B : Set l2) → diff --git a/src/foundation/weakly-constant-maps.lagda.md b/src/foundation/weakly-constant-maps.lagda.md index 1afdbc43a3..b01859024f 100644 --- a/src/foundation/weakly-constant-maps.lagda.md +++ b/src/foundation/weakly-constant-maps.lagda.md @@ -15,7 +15,9 @@ open import foundation.iterated-dependent-product-types open import foundation.universe-levels open import foundation-core.contractible-types +open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types +open import foundation-core.homotopies open import foundation-core.propositions open import foundation-core.sets open import foundation-core.torsorial-type-families @@ -26,25 +28,27 @@ open import foundation-core.torsorial-type-families ## Idea A map `f : A → B` is said to be -{{#concept "weakly constant" Disambiguation="map of types" Agda=is-weakly-constant}} -if any two elements in `A` are mapped to -[identical elements](foundation-core.identity-types.md) in `B`. +{{#concept "weakly constant" Disambiguation="map of types" Agda=is-weakly-constant-map}}, +or **steady**, if any two elements in `A` are mapped to +[identical elements](foundation-core.identity-types.md) in `B`. This concept is +considered in {{#cite KECA17}} where it is in particular used to give a +generalization of Hedberg's theorem. ## Definitions ### The structure on a map of being weakly constant ```agda -is-weakly-constant : +is-weakly-constant-map : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) -is-weakly-constant {A = A} f = (x y : A) → f x ＝ f y +is-weakly-constant-map {A = A} f = (x y : A) → f x ＝ f y ``` ### The type of weakly constant maps ```agda weakly-constant-map : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2) -weakly-constant-map A B = Σ (A → B) (is-weakly-constant) +weakly-constant-map A B = Σ (A → B) (is-weakly-constant-map) module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : weakly-constant-map A B) @@ -53,11 +57,27 @@ module _ map-weakly-constant-map : A → B map-weakly-constant-map = pr1 f - is-weakly-constant-weakly-constant-map : - is-weakly-constant map-weakly-constant-map - is-weakly-constant-weakly-constant-map = pr2 f + is-weakly-constant-map-weakly-constant-map : + is-weakly-constant-map map-weakly-constant-map + is-weakly-constant-map-weakly-constant-map = pr2 f ``` +### Factorizations through propositions + +```agda +factorization-through-Prop : + {l1 l2 : Level} (l3 : Level) {A : UU l1} {B : UU l2} → + (A → B) → UU (l1 ⊔ l2 ⊔ lsuc l3) +factorization-through-Prop l3 {A} {B} f = + Σ ( Prop l3) + ( λ P → Σ (type-Prop P → B) (λ i → Σ (A → type-Prop P) (λ j → i ∘ j ~ f))) +``` + +**Comment.** We need this type to state a factorization property of weakly +constant maps, but placing it in its appropriate place +(`orthogonal-factorization-systems.factorizations-of-maps`) leads to circular +dependencies. + ## Properties ### Being weakly constant is a property if the codomain is a set @@ -68,13 +88,41 @@ module _ where abstract - is-prop-is-weakly-constant-Set : is-prop (is-weakly-constant f) - is-prop-is-weakly-constant-Set = + is-prop-is-weakly-constant-map-Set : is-prop (is-weakly-constant-map f) + is-prop-is-weakly-constant-map-Set = is-prop-iterated-Π 2 (λ x y → is-set-type-Set B (f x) (f y)) - is-weakly-constant-prop-Set : Prop (l1 ⊔ l2) - pr1 is-weakly-constant-prop-Set = is-weakly-constant f - pr2 is-weakly-constant-prop-Set = is-prop-is-weakly-constant-Set + is-weakly-constant-map-prop-Set : Prop (l1 ⊔ l2) + pr1 is-weakly-constant-map-prop-Set = is-weakly-constant-map f + pr2 is-weakly-constant-map-prop-Set = is-prop-is-weakly-constant-map-Set +``` + +### The type of fixed points of a weakly constant endomap is a proposition + +This is Lemma 4.1 of {{#cite KECA17}}. We follow the second proof, due to +Christian Sattler. + +```agda +module _ + {l : Level} {A : UU l} {f : A → A} (W : is-weakly-constant-map f) + where + + is-proof-irrelevant-fixed-point-is-weakly-constant-map : + is-proof-irrelevant (fixed-point f) + is-proof-irrelevant-fixed-point-is-weakly-constant-map (x , p) = + is-contr-equiv + ( Σ A (λ z → f x ＝ z)) + ( equiv-tot (λ z → equiv-concat (W x z) z)) + ( is-torsorial-Id (f x)) + + is-prop-fixed-point-is-weakly-constant-map : is-prop (fixed-point f) + is-prop-fixed-point-is-weakly-constant-map = + is-prop-is-proof-irrelevant + ( is-proof-irrelevant-fixed-point-is-weakly-constant-map) + + prop-fixed-point-is-weakly-constant-map : Prop l + prop-fixed-point-is-weakly-constant-map = + ( fixed-point f , is-prop-fixed-point-is-weakly-constant-map) ``` ### The action on identifications of a weakly constant map is weakly constant @@ -84,17 +132,17 @@ This is Auxiliary Lemma 4.3 of {{#cite KECA17}}. ```agda module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X → Y} - (W : is-weakly-constant f) + (W : is-weakly-constant-map f) where - compute-ap-is-weakly-constant : + compute-ap-is-weakly-constant-map : {x y : X} (p : x ＝ y) → inv (W x x) ∙ W x y ＝ ap f p - compute-ap-is-weakly-constant {x} refl = left-inv (W x x) + compute-ap-is-weakly-constant-map {x} refl = left-inv (W x x) - is-weakly-constant-ap : {x y : X} → is-weakly-constant (ap f {x} {y}) - is-weakly-constant-ap {x} {y} p q = - ( inv (compute-ap-is-weakly-constant p)) ∙ - ( compute-ap-is-weakly-constant q) + is-weakly-constant-map-ap : {x y : X} → is-weakly-constant-map (ap f {x} {y}) + is-weakly-constant-map-ap {x} {y} p q = + ( inv (compute-ap-is-weakly-constant-map p)) ∙ + ( compute-ap-is-weakly-constant-map q) module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} @@ -108,33 +156,54 @@ module _ ( map-weakly-constant-map f x ＝ map-weakly-constant-map f y) ap-weakly-constant-map {x} {y} = ( ap (map-weakly-constant-map f) {x} {y} , - is-weakly-constant-ap (is-weakly-constant-weakly-constant-map f)) + is-weakly-constant-map-ap (is-weakly-constant-map-weakly-constant-map f)) ``` -### The type of fixed points of a weakly constant endomap is a proposition - -This is Lemma 4.1 of {{#cite KECA17}}. We follow the second proof, due to -Christian Sattler. +### Weakly constant maps are closed under composition with arbitrary maps ```agda module _ - {l : Level} {A : UU l} {f : A → A} (W : is-weakly-constant f) + {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3} where - is-proof-irrelevant-fixed-point-is-weakly-constant : - is-proof-irrelevant (fixed-point f) - is-proof-irrelevant-fixed-point-is-weakly-constant (x , p) = - is-contr-equiv - ( Σ A (λ z → f x ＝ z)) - ( equiv-tot (λ z → equiv-concat (W x z) z)) - ( is-torsorial-Id (f x)) + is-weakly-constant-map-right-comp : + {f : A → B} (g : B → C) → + is-weakly-constant-map f → is-weakly-constant-map (g ∘ f) + is-weakly-constant-map-right-comp g W x y = ap g (W x y) - is-prop-fixed-point-is-weakly-constant : is-prop (fixed-point f) - is-prop-fixed-point-is-weakly-constant = - is-prop-is-proof-irrelevant - ( is-proof-irrelevant-fixed-point-is-weakly-constant) + is-weakly-constant-map-left-comp : + (f : A → B) {g : B → C} → + is-weakly-constant-map g → is-weakly-constant-map (g ∘ f) + is-weakly-constant-map-left-comp f W x y = W (f x) (f y) ``` +### A map is weakly constant if and only if it factors through a proposition + +A map `f : A → B` is weakly constant if and only if there exists a proposition +`P` and a commuting diagram + +```text + P + ∧ \ + / \ + / ∨ + A --------> B + f +``` + +```agda +module _ + {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + where + + is-weakly-constant-map-factors-through-Prop : + {l3 : Level} → factorization-through-Prop l3 f → is-weakly-constant-map f + is-weakly-constant-map-factors-through-Prop (P , i , j , H) x y = + inv (H x) ∙ ap i (eq-type-Prop P) ∙ H y +``` + +> The converse remains to be formalized. + ## References {{#bibliography}} {{#reference KECA17}} @@ -142,3 +211,9 @@ module _ ## See also - [Coherently constant maps](foundation.coherently-constant-maps.md) +- [Null-homotopic maps](foundation.null-homotopic-maps.md) + +## External links + +- [weakly constant function](https://ncatlab.org/nlab/show/weakly+constant+function) + at $n$Lab diff --git a/src/literature/idempotents-in-intensional-type-theory.lagda.md b/src/literature/idempotents-in-intensional-type-theory.lagda.md index 448cd6e695..d16ea8d224 100644 --- a/src/literature/idempotents-in-intensional-type-theory.lagda.md +++ b/src/literature/idempotents-in-intensional-type-theory.lagda.md @@ -205,12 +205,12 @@ splitting. ```agda open import foundation.weakly-constant-maps using - ( is-weakly-constant -- "the type of witnesses that a map is weakly constant" + ( is-weakly-constant-map -- "the type of witnesses that a map is weakly constant" ; weakly-constant-map -- "the type of weakly constant maps" ) open import foundation.split-idempotent-maps using - ( is-split-idempotent-is-weakly-constant-is-idempotent + ( is-split-idempotent-is-weakly-constant-map-is-idempotent ) ``` From 7fb9949ca04e8573adef8a944a4df645101f336e Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 14:08:59 +0000 Subject: [PATCH 5/9] done --- .../coherently-constant-maps.lagda.md | 9 ++++++-- src/foundation/null-homotopic-maps.lagda.md | 21 +++++++++++++++---- 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md index 2a8f02b244..3ab24ae450 100644 --- a/src/foundation/coherently-constant-maps.lagda.md +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -302,13 +302,18 @@ module _ ```agda module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-weakly-constant-map-is-constant-map : - is-constant-map f → is-weakly-constant-map f + {f : A → B} → is-constant-map f → is-weakly-constant-map f is-weakly-constant-map-is-constant-map H x y = contraction-is-constant-map' H x ∙ inv (contraction-is-constant-map H y) + + is-weakly-constant-constant-map : + (f : constant-map A B) → is-weakly-constant-map (map-constant-map f) + is-weakly-constant-constant-map f = + is-weakly-constant-map-is-constant-map (is-constant-constant-map f) ``` ## References diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index 54a5854b83..cf868ebad9 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -328,24 +328,37 @@ module _ ```agda module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-constant-map-is-null-homotopic-map : - is-null-homotopic-map f → is-constant-map f + {f : A → B} → is-null-homotopic-map f → is-constant-map f is-constant-map-is-null-homotopic-map (b , H) = ((λ _ → b) , H) + + is-constant-null-homotopic-map : + (f : null-homotopic-map A B) → is-constant-map (map-null-homotopic-map f) + is-constant-null-homotopic-map f = + is-constant-map-is-null-homotopic-map + ( is-null-homotopic-null-homotopic-map f) ``` ### Null-homotopic maps are weakly constant ```agda module _ - {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} + {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-weakly-constant-map-is-null-homotopic-map : - is-null-homotopic-map f → is-weakly-constant-map f + {f : A → B} → is-null-homotopic-map f → is-weakly-constant-map f is-weakly-constant-map-is-null-homotopic-map (b , H) x y = H x ∙ inv (H y) + + is-weakly-constant-null-homotopic-map : + (f : null-homotopic-map A B) → + is-weakly-constant-map (map-null-homotopic-map f) + is-weakly-constant-null-homotopic-map f = + is-weakly-constant-map-is-null-homotopic-map + ( is-null-homotopic-null-homotopic-map f) ``` ## See also From c4614508e8ef1f7ae882140d697bec48d3bc3ca7 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 14:14:51 +0000 Subject: [PATCH 6/9] edit --- src/foundation/weakly-constant-maps.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation/weakly-constant-maps.lagda.md b/src/foundation/weakly-constant-maps.lagda.md index b01859024f..eb9db871f3 100644 --- a/src/foundation/weakly-constant-maps.lagda.md +++ b/src/foundation/weakly-constant-maps.lagda.md @@ -28,7 +28,7 @@ open import foundation-core.torsorial-type-families ## Idea A map `f : A → B` is said to be -{{#concept "weakly constant" Disambiguation="map of types" Agda=is-weakly-constant-map}}, +{{#concept "weakly constant" Disambiguation="map of types" Agda=is-weakly-constant-map Agda=weakly-constant-map}}, or **steady**, if any two elements in `A` are mapped to [identical elements](foundation-core.identity-types.md) in `B`. This concept is considered in {{#cite KECA17}} where it is in particular used to give a From aaf65a59623a9c90d026e7e746ab2812af756f50 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 26 Mar 2025 14:55:55 +0000 Subject: [PATCH 7/9] fix link --- src/foundation/null-homotopic-maps.lagda.md | 2 +- src/synthetic-homotopy-theory/homotopy-groups.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index cf868ebad9..729c859fba 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -366,7 +366,7 @@ module _ - Null-homotopic maps are [coherently constant](foundation.coherently-constant-maps.md), and if the domain is pointed the two notions coincide -- [Constant pointed maps](structured-types.constant-pointed-types.md) +- [Constant pointed maps](structured-types.constant-pointed-maps.md) ## External links diff --git a/src/synthetic-homotopy-theory/homotopy-groups.lagda.md b/src/synthetic-homotopy-theory/homotopy-groups.lagda.md index 5d30f801f9..e6f739ed10 100644 --- a/src/synthetic-homotopy-theory/homotopy-groups.lagda.md +++ b/src/synthetic-homotopy-theory/homotopy-groups.lagda.md @@ -37,8 +37,8 @@ where - `π₀ A` is the set of [connected components](foundation.connected-components.md) of `A`, and - `πᵢ₊₁ A` is the set `πᵢ ΩA` equipped with the - [group structure](group-theory.groups.md) obtained from the [loop - space](synthetic-homotopy theory.loop-spaces.md). + [group structure](group-theory.groups.md) obtained from the + [loop space](synthetic-homotopy-theory.loop-spaces.md). For `i ≥ 2`, the `i`-th homotopy group `πᵢ A` of `A` is [abelian](group-theory.abelian-groups.md) by the From 6de1f89924edbf082b8a22d4569dc69cef8b99d3 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Wed, 14 May 2025 10:39:48 +0100 Subject: [PATCH 8/9] pre-commit --- references.bib | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/references.bib b/references.bib index ff9af1af7c..97b5e98597 100644 --- a/references.bib +++ b/references.bib @@ -462,21 +462,21 @@ @article{KECA17 } @inproceedings{Kraus15, - author = {Kraus, Nicolai}, - title = {{The General Universal Property of the Propositional Truncation}}, - booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, - pages = {111--145}, - series = {Leibniz International Proceedings in Informatics (LIPIcs)}, - isbn = {978-3-939897-88-0}, - issn = {1868-8969}, - year = {2015}, - volume = {39}, - editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, - publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, - address = {Dagstuhl, Germany}, - urn = {urn:nbn:de:0030-drops-54944}, - doi = {10.4230/LIPIcs.TYPES.2014.111}, - annote = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy} + title = {{The General Universal Property of the Propositional Truncation}}, + author = {Kraus, Nicolai}, + year = 2015, + booktitle = {20th International Conference on Types for Proofs and Programs (TYPES 2014)}, + publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, + address = {Dagstuhl, Germany}, + series = {Leibniz International Proceedings in Informatics (LIPIcs)}, + volume = 39, + pages = {111--145}, + doi = {10.4230/LIPIcs.TYPES.2014.111}, + isbn = {978-3-939897-88-0}, + issn = {1868-8969}, + editor = {Herbelin, Hugo and Letouzey, Pierre and Sozeau, Matthieu}, + urn = {urn:nbn:de:0030-drops-54944}, + annote = {Keywords: coherence conditions, propositional truncation, Reedy limits, universal property, well-behaved constancy}, } @book{Kunen11, From 20ca9071ceff771cc1b819d480f66a559fe85cea Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Tue, 15 Jul 2025 15:32:55 +0200 Subject: [PATCH 9/9] review <3 --- .../coherently-constant-maps.lagda.md | 34 +++++++++--------- src/foundation/null-homotopic-maps.lagda.md | 35 ++++++++++--------- src/foundation/weakly-constant-maps.lagda.md | 2 +- 3 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/foundation/coherently-constant-maps.lagda.md b/src/foundation/coherently-constant-maps.lagda.md index 3ab24ae450..f25433ab2d 100644 --- a/src/foundation/coherently-constant-maps.lagda.md +++ b/src/foundation/coherently-constant-maps.lagda.md @@ -142,15 +142,16 @@ module _ (f g : constant-map A B) → f ＝ g → htpy-constant-map f g htpy-eq-constant-map f .f refl = refl-htpy-constant-map f - is-torsorial-htpy-constant-map : - (f : constant-map A B) → is-torsorial (htpy-constant-map f) - is-torsorial-htpy-constant-map f = - is-contr-equiv - ( Σ (║ A ║₋₁ → B) (center-partial-element-constant-map f ~_)) - ( equiv-Σ-equiv-base - ( center-partial-element-constant-map f ~_) - ( compute-constant-map)) - ( is-torsorial-htpy (center-partial-element-constant-map f)) + abstract + is-torsorial-htpy-constant-map : + (f : constant-map A B) → is-torsorial (htpy-constant-map f) + is-torsorial-htpy-constant-map f = + is-contr-equiv + ( Σ (║ A ║₋₁ → B) (center-partial-element-constant-map f ~_)) + ( equiv-Σ-equiv-base + ( center-partial-element-constant-map f ~_) + ( compute-constant-map)) + ( is-torsorial-htpy (center-partial-element-constant-map f)) is-equiv-htpy-eq-constant-map : (f g : constant-map A B) → is-equiv (htpy-eq-constant-map f g) @@ -218,13 +219,14 @@ module _ (H K : is-constant-map f) → H ＝ K → htpy-is-constant-map H K htpy-eq-is-constant-map H .H refl = refl-htpy-is-constant-map H - is-torsorial-htpy-is-constant-map : - (H : is-constant-map f) → is-torsorial (htpy-is-constant-map H) - is-torsorial-htpy-is-constant-map H = - is-torsorial-Eq-structure - ( is-torsorial-htpy (center-partial-element-is-constant-map H)) - ( center-partial-element-is-constant-map H , refl-htpy) - (is-torsorial-htpy' (contraction-is-constant-map' H ∙h refl-htpy)) + abstract + is-torsorial-htpy-is-constant-map : + (H : is-constant-map f) → is-torsorial (htpy-is-constant-map H) + is-torsorial-htpy-is-constant-map H = + is-torsorial-Eq-structure + ( is-torsorial-htpy (center-partial-element-is-constant-map H)) + ( center-partial-element-is-constant-map H , refl-htpy) + ( is-torsorial-htpy' (contraction-is-constant-map' H ∙h refl-htpy)) is-equiv-htpy-eq-is-constant-map : (H K : is-constant-map f) → is-equiv (htpy-eq-is-constant-map H K) diff --git a/src/foundation/null-homotopic-maps.lagda.md b/src/foundation/null-homotopic-maps.lagda.md index 729c859fba..4a3da066c0 100644 --- a/src/foundation/null-homotopic-maps.lagda.md +++ b/src/foundation/null-homotopic-maps.lagda.md @@ -131,15 +131,16 @@ module _ (f g : null-homotopic-map A B) → f ＝ g → Eq-null-homotopic-map f g Eq-eq-null-homotopic-map f .f refl = refl-Eq-null-homotopic-map f - is-torsorial-Eq-null-homotopic-map : - (f : null-homotopic-map A B) → is-torsorial (Eq-null-homotopic-map f) - is-torsorial-Eq-null-homotopic-map f = - is-contr-equiv - ( Σ B (Id (center-null-homotopic-map f))) - ( equiv-Σ-equiv-base - ( Id (center-null-homotopic-map f)) - ( compute-null-homotopic-map)) - ( is-torsorial-Id (center-null-homotopic-map f)) + abstract + is-torsorial-Eq-null-homotopic-map : + (f : null-homotopic-map A B) → is-torsorial (Eq-null-homotopic-map f) + is-torsorial-Eq-null-homotopic-map f = + is-contr-equiv + ( Σ B (Id (center-null-homotopic-map f))) + ( equiv-Σ-equiv-base + ( Id (center-null-homotopic-map f)) + ( compute-null-homotopic-map)) + ( is-torsorial-Id (center-null-homotopic-map f)) is-equiv-Eq-eq-null-homotopic-map : (f g : null-homotopic-map A B) → is-equiv (Eq-eq-null-homotopic-map f g) @@ -205,13 +206,15 @@ module _ (H K : is-null-homotopic-map f) → H ＝ K → htpy-is-null-homotopic-map H K htpy-eq-is-null-homotopic-map H .H refl = refl-htpy-is-null-homotopic-map H - is-torsorial-htpy-is-null-homotopic-map : - (H : is-null-homotopic-map f) → is-torsorial (htpy-is-null-homotopic-map H) - is-torsorial-htpy-is-null-homotopic-map H = - is-torsorial-Eq-structure - ( is-torsorial-Id (center-is-null-homotopic-map H)) - ( center-is-null-homotopic-map H , refl) - ( is-torsorial-htpy' (contraction-is-null-homotopic-map H ∙h refl-htpy)) + abstract + is-torsorial-htpy-is-null-homotopic-map : + (H : is-null-homotopic-map f) → + is-torsorial (htpy-is-null-homotopic-map H) + is-torsorial-htpy-is-null-homotopic-map H = + is-torsorial-Eq-structure + ( is-torsorial-Id (center-is-null-homotopic-map H)) + ( center-is-null-homotopic-map H , refl) + ( is-torsorial-htpy' (contraction-is-null-homotopic-map H ∙h refl-htpy)) is-equiv-htpy-eq-is-null-homotopic-map : (H K : is-null-homotopic-map f) → diff --git a/src/foundation/weakly-constant-maps.lagda.md b/src/foundation/weakly-constant-maps.lagda.md index eb9db871f3..a33ba336e6 100644 --- a/src/foundation/weakly-constant-maps.lagda.md +++ b/src/foundation/weakly-constant-maps.lagda.md @@ -32,7 +32,7 @@ A map `f : A → B` is said to be or **steady**, if any two elements in `A` are mapped to [identical elements](foundation-core.identity-types.md) in `B`. This concept is considered in {{#cite KECA17}} where it is in particular used to give a -generalization of Hedberg's theorem. +generalization of [Hedberg's theorem](foundation.decidable-equality.md). ## Definitions