Propositional maps
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-09-11.
module foundation.propositional-maps where open import foundation-core.propositional-maps public
Imports
open import foundation.dependent-pair-types open import foundation.embeddings open import foundation.logical-equivalences open import foundation.truncated-maps open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.propositions open import foundation-core.truncation-levels
Properties
Being a propositional map is a property
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where is-prop-is-prop-map : (f : A → B) → is-prop (is-prop-map f) is-prop-is-prop-map f = is-prop-is-trunc-map neg-one-𝕋 f is-prop-map-Prop : (A → B) → Prop (l1 ⊔ l2) pr1 (is-prop-map-Prop f) = is-prop-map f pr2 (is-prop-map-Prop f) = is-prop-is-prop-map f
Being a propositional map is equivalent to being an embedding
module _ {l1 l2 : Level} {A : UU l1} {B : UU l2} where equiv-is-emb-is-prop-map : (f : A → B) → is-prop-map f ≃ is-emb f equiv-is-emb-is-prop-map f = equiv-iff ( is-prop-map-Prop f) ( is-emb-Prop f) ( is-emb-is-prop-map) ( is-prop-map-is-emb) equiv-is-prop-map-is-emb : (f : A → B) → is-emb f ≃ is-prop-map f equiv-is-prop-map-is-emb f = equiv-iff ( is-emb-Prop f) ( is-prop-map-Prop f) ( is-prop-map-is-emb) ( is-emb-is-prop-map)
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).