Weakly constant maps
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-02-09.
Last modified on 2023-06-08.
module foundation.weakly-constant-maps where
Imports
open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.sets
Idea
A map f : A → B
is said to be weakly constant if any two elements in A
are
mapped to identical elements in B
.
Definition
is-weakly-constant-map : {l1 l2 : Level} {A : UU l1} {B : UU l2} → (A → B) → UU (l1 ⊔ l2) is-weakly-constant-map {A = A} f = (x y : A) → f x = f y module _ {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A → type-Set B) where abstract is-prop-is-weakly-constant-map-Set : is-prop (is-weakly-constant-map f) is-prop-is-weakly-constant-map-Set = is-prop-Π (λ x → is-prop-Π (λ y → is-set-type-Set B (f x) (f y))) is-weakly-constant-map-Prop : Prop (l1 ⊔ l2) pr1 is-weakly-constant-map-Prop = is-weakly-constant-map f pr2 is-weakly-constant-map-Prop = is-prop-is-weakly-constant-map-Set
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490). - 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).