This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Propositional maps

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

Idea

A map is said to be propositional if its fibers are propositions. This condition is the same as the condition of being a -1-truncated map, and it is equivalent to being an embedding.

Note: Of the three equivalent conditions mentioned above, propositional maps, -1-truncated maps, and embeddings, the central notion of in the agda-unimath library is that of embedding. This means that most infrastructure is available for embeddings, and that it is easy to convert from any of the other two notions to the notion of embedding.

Definitions

The predicate of being a propositional map

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)

The type of propositional maps

module _
  {l1 l2 : Level}
  where

  prop-map : (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
  prop-map A B = Σ (A → B) is-prop-map

  module _
    {A : UU l1} {B : UU l2} (f : prop-map A B)
    where

    map-prop-map : A → B
    map-prop-map = pr1 f

    is-prop-map-prop-map : is-prop-map map-prop-map
    is-prop-map-prop-map = pr2 f

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

  emb-prop-map : prop-map A B → A ↪ B
  pr1 (emb-prop-map (f , p)) = f
  pr2 (emb-prop-map (f , p)) = is-emb-is-prop-map p

  prop-map-emb : A ↪ B → prop-map A B
  pr1 (prop-map-emb (f , p)) = f
  pr2 (prop-map-emb (f , p)) = is-prop-map-is-emb p

  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