Propositional maps

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-02-07.
Last modified on 2023-09-06.

module foundation-core.propositional-maps where
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.embeddings
open import foundation-core.fibers-of-maps
open import foundation-core.identity-types
open import foundation-core.propositions


A map is said to be propositional if its fibers are propositions. This condition is equivalent to being an embedding.


module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  is-prop-map : (A  B)  UU (l1  l2)
  is-prop-map f = (b : B)  is-prop (fiber f b)


The fibers of a map are propositions if and only if it is an embedding

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B}

    is-emb-is-prop-map : is-prop-map f  is-emb f
    is-emb-is-prop-map is-prop-map-f x =
        ( is-contr-equiv'
          ( fiber f (f x))
          ( equiv-fiber f (f x))
          ( is-proof-irrelevant-is-prop (is-prop-map-f (f x)) (x , refl)))
        ( λ _  ap f)

    is-prop-map-is-emb : is-emb f  is-prop-map f
    is-prop-map-is-emb is-emb-f y =
      is-prop-is-proof-irrelevant α
      α : (t : fiber f y)  is-contr (fiber f y)
      α (x , refl) =
          ( fiber' f (f x))
          ( equiv-fiber f (f x))
          ( fundamental-theorem-id'  _  ap f) (is-emb-f x))

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2}

  is-prop-map-emb : (f : A  B)  is-prop-map (map-emb f)
  is-prop-map-emb f = is-prop-map-is-emb (is-emb-map-emb f)

  is-prop-map-emb' : (f : A  B)  (b : B)  is-prop (fiber' (map-emb f) b)
  is-prop-map-emb' f y =
    is-prop-equiv' (equiv-fiber (map-emb f) y) (is-prop-map-emb f y)

  fiber-emb-Prop : A  B  B  Prop (l1  l2)
  pr1 (fiber-emb-Prop f y) = fiber (map-emb f) y
  pr2 (fiber-emb-Prop f y) = is-prop-map-emb f y

  fiber-emb-Prop' : A  B  B  Prop (l1  l2)
  pr1 (fiber-emb-Prop' f y) = fiber' (map-emb f) y
  pr2 (fiber-emb-Prop' f y) = is-prop-map-emb' f y

Recent changes