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
Imports 
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

Idea

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

Definition

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

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

Properties

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}
  where

  abstract
    is-emb-is-prop-map : is-prop-map f → is-emb f
    is-emb-is-prop-map is-prop-map-f x =
      fundamental-theorem-id
        ( 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)

  abstract
    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 α
      where
      α : (t : fiber f y) → is-contr (fiber f y)
      α (x , refl) =
        is-contr-equiv
          ( 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}
  where

  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