diff --git a/references.bib b/references.bib
index d11d699b03..97b5e98597 100644
--- a/references.bib
+++ b/references.bib
@@ -461,6 +461,24 @@ @article{KECA17
keywords = {Computer Science - Logic in Computer Science ; 03B15 ; F.4.1},
}
+@inproceedings{Kraus15,
+ 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,
title = {Set theory},
author = {Kunen, Kenneth},
diff --git a/src/foundation-core/constant-maps.lagda.md b/src/foundation-core/constant-maps.lagda.md
index 46e9ad8b04..d6fa02a4c1 100644
--- a/src/foundation-core/constant-maps.lagda.md
+++ b/src/foundation-core/constant-maps.lagda.md
@@ -32,4 +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)
diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md
index 154bf0d8b6..fd81511d50 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..3ab24ae450
--- /dev/null
+++ b/src/foundation/coherently-constant-maps.lagda.md
@@ -0,0 +1,326 @@
+# 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.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
+```
+
+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,9 +37,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-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
[constant](foundation-core.constant-maps.md) function.
@@ -51,23 +48,118 @@ or _constant_, if there is an element `y : B` such for every `x : A` we have
### 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-map : B
+ center-is-null-homotopic-map = pr1 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
- center-is-null-homotopic : B
- center-is-null-homotopic = pr1 H
+ 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-is-null-homotopic : (x : A) → f x ＝ center-is-null-homotopic
- contraction-is-null-homotopic = pr2 H
+ 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,62 +295,78 @@ 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}
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 :
+ {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-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 :
+ {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
-- [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
+- [Constant pointed maps](structured-types.constant-pointed-maps.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 741e4c32c8..eb9db871f3 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 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
+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,64 @@ 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}}
+
+## 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
)
```