Decidable embeddings

module foundation.decidable-embeddings where
Imports
open import foundation.decidable-maps
open import foundation.decidable-subtypes
open import foundation.decidable-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.functoriality-cartesian-product-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositional-maps
open import foundation.structured-type-duality
open import foundation.type-theoretic-principle-of-choice

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.decidable-propositions
open import foundation-core.dependent-pair-types
open import foundation-core.empty-types
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.fundamental-theorem-of-identity-types
open import foundation-core.propositions
open import foundation-core.subtype-identity-principle
open import foundation-core.type-arithmetic-dependent-pair-types
open import foundation-core.universe-levels

Idea

A map is said to be a decidable embedding if it is an embedding and its fibers are decidable types.

Definitions

The condition on a map of being a decidable embedding

is-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}  (X  Y)  UU (l1  l2)
is-decidable-emb {Y = Y} f = is-emb f × is-decidable-map f

abstract
  is-emb-is-decidable-emb :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X  Y} 
    is-decidable-emb f  is-emb f
  is-emb-is-decidable-emb H = pr1 H

is-decidable-map-is-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X  Y} 
  is-decidable-emb f  is-decidable-map f
is-decidable-map-is-decidable-emb H = pr2 H

Decidably propositional maps

is-decidable-prop-map :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}  (X  Y)  UU (l1  l2)
is-decidable-prop-map {Y = Y} f = (y : Y)  is-decidable-prop (fib f y)

abstract
  is-prop-map-is-decidable-prop-map :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X  Y} 
    is-decidable-prop-map f  is-prop-map f
  is-prop-map-is-decidable-prop-map H y = pr1 (H y)

is-decidable-map-is-decidable-prop-map :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X  Y} 
  is-decidable-prop-map f  is-decidable-map f
is-decidable-map-is-decidable-prop-map H y = pr2 (H y)

The type of decidable embeddings

_↪d_ :
  {l1 l2 : Level} (X : UU l1) (Y : UU l2)  UU (l1  l2)
X ↪d Y = Σ (X  Y) is-decidable-emb

map-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}  X ↪d Y  X  Y
map-decidable-emb e = pr1 e

abstract
  is-decidable-emb-map-decidable-emb :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ↪d Y) 
    is-decidable-emb (map-decidable-emb e)
  is-decidable-emb-map-decidable-emb e = pr2 e

abstract
  is-emb-map-decidable-emb :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ↪d Y) 
    is-emb (map-decidable-emb e)
  is-emb-map-decidable-emb e =
    is-emb-is-decidable-emb (is-decidable-emb-map-decidable-emb e)

abstract
  is-decidable-map-map-decidable-emb :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (e : X ↪d Y) 
    is-decidable-map (map-decidable-emb e)
  is-decidable-map-map-decidable-emb e =
    is-decidable-map-is-decidable-emb (is-decidable-emb-map-decidable-emb e)

emb-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2}  X ↪d Y  X  Y
pr1 (emb-decidable-emb e) = map-decidable-emb e
pr2 (emb-decidable-emb e) = is-emb-map-decidable-emb e

Properties

Being a decidably propositional map is a proposition

abstract
  is-prop-is-decidable-prop-map :
    {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f : X  Y) 
    is-prop (is-decidable-prop-map f)
  is-prop-is-decidable-prop-map f =
    is-prop-Π  y  is-prop-is-decidable-prop (fib f y))

Any map of which the fibers are decidable propositions is a decidable embedding

module _
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} {f : X  Y}
  where

  abstract
    is-decidable-emb-is-decidable-prop-map :
      is-decidable-prop-map f  is-decidable-emb f
    pr1 (is-decidable-emb-is-decidable-prop-map H) =
      is-emb-is-prop-map (is-prop-map-is-decidable-prop-map H)
    pr2 (is-decidable-emb-is-decidable-prop-map H) =
      is-decidable-map-is-decidable-prop-map H

  abstract
    is-prop-map-is-decidable-emb : is-decidable-emb f  is-prop-map f
    is-prop-map-is-decidable-emb H =
      is-prop-map-is-emb (is-emb-is-decidable-emb H)

  abstract
    is-decidable-prop-map-is-decidable-emb :
      is-decidable-emb f  is-decidable-prop-map f
    pr1 (is-decidable-prop-map-is-decidable-emb H y) =
      is-prop-map-is-decidable-emb H y
    pr2 (is-decidable-prop-map-is-decidable-emb H y) = pr2 H y

decidable-subtype-decidable-emb :
  {l1 l2 : Level} {X : UU l1} {Y : UU l2} 
  (X ↪d Y)  (decidable-subtype (l1  l2) Y)
pr1 (decidable-subtype-decidable-emb f y) = fib (map-decidable-emb f) y
pr2 (decidable-subtype-decidable-emb f y) =
  is-decidable-prop-map-is-decidable-emb (pr2 f) y

The type of all decidable embeddings into a type A is equivalent to the type of decidable subtypes of A

equiv-Fib-Decidable-Prop :
  (l : Level) {l1 : Level} (A : UU l1) 
  Σ (UU (l1  l))  X  X ↪d A)  (decidable-subtype (l1  l) A)
equiv-Fib-Decidable-Prop l A =
  ( equiv-Fib-structure l is-decidable-prop A) ∘e
  ( equiv-tot
    ( λ X 
      equiv-tot
        ( λ f 
          ( inv-distributive-Π-Σ) ∘e
          ( equiv-prod (equiv-is-prop-map-is-emb f) id-equiv))))

Any equivalence is a decidable embedding

abstract
  is-decidable-emb-is-equiv :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A  B} 
    is-equiv f  is-decidable-emb f
  pr1 (is-decidable-emb-is-equiv H) = is-emb-is-equiv H
  pr2 (is-decidable-emb-is-equiv H) x = inl (center (is-contr-map-is-equiv H x))

abstract
  is-decidable-emb-id :
    {l1 : Level} {A : UU l1}  is-decidable-emb (id {A = A})
  pr1 (is-decidable-emb-id {l1} {A}) = is-emb-id
  pr2 (is-decidable-emb-id {l1} {A}) x = inl (pair x refl)

decidable-emb-id :
  {l1 : Level} {A : UU l1}  A ↪d A
pr1 (decidable-emb-id {l1} {A}) = id
pr2 (decidable-emb-id {l1} {A}) = is-decidable-emb-id

Being a decidable embedding is a property

abstract
  is-prop-is-decidable-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    is-prop (is-decidable-emb f)
  is-prop-is-decidable-emb f =
    is-prop-is-inhabited
      ( λ H 
        is-prop-prod
          ( is-prop-is-emb f)
          ( is-prop-Π
            ( λ y  is-prop-is-decidable (is-prop-map-is-emb (pr1 H) y))))

Decidable embeddings are closed under composition

abstract
  is-decidable-emb-comp :
    {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
    {g : B  C} {f : A  B} 
    is-decidable-emb f  is-decidable-emb g  is-decidable-emb (g  f)
  pr1 (is-decidable-emb-comp {g = g} {f} H K) =
    is-emb-comp _ _ (pr1 K) (pr1 H)
  pr2 (is-decidable-emb-comp {g = g} {f} H K) x =
    ind-coprod
      ( λ t  is-decidable (fib (g  f) x))
      ( λ u 
        is-decidable-equiv
          ( equiv-compute-fib-comp g f x)
          ( is-decidable-equiv
            ( left-unit-law-Σ-is-contr
              ( is-proof-irrelevant-is-prop
                ( is-prop-map-is-emb (is-emb-is-decidable-emb K) x) ( u))
              ( u))
            ( is-decidable-map-is-decidable-emb H (pr1 u))))
      ( λ α  inr  t  α (pair (f (pr1 t)) (pr2 t))))
      ( pr2 K x)

Decidable embeddings are closed under homotopies

abstract
  is-decidable-emb-htpy :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A  B} 
    f ~ g  is-decidable-emb g  is-decidable-emb f
  pr1 (is-decidable-emb-htpy {f = f} {g} H K) =
    is-emb-htpy f g H (is-emb-is-decidable-emb K)
  pr2 (is-decidable-emb-htpy {f = f} {g} H K) b =
    is-decidable-equiv
      ( equiv-tot  a  equiv-concat (inv (H a)) b))
      ( is-decidable-map-is-decidable-emb K b)

Characterizing equality in the type of decidable embeddings

htpy-decidable-emb :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f g : A ↪d B)  UU (l1  l2)
htpy-decidable-emb f g = map-decidable-emb f ~ map-decidable-emb g

refl-htpy-decidable-emb :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A ↪d B)  htpy-decidable-emb f f
refl-htpy-decidable-emb f = refl-htpy

htpy-eq-decidable-emb :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f g : A ↪d B) 
  f  g  htpy-decidable-emb f g
htpy-eq-decidable-emb f .f refl = refl-htpy-decidable-emb f

abstract
  is-contr-total-htpy-decidable-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A ↪d B) 
    is-contr (Σ (A ↪d B) (htpy-decidable-emb f))
  is-contr-total-htpy-decidable-emb f =
    is-contr-total-Eq-subtype
      ( is-contr-total-htpy (map-decidable-emb f))
      ( is-prop-is-decidable-emb)
      ( map-decidable-emb f)
      ( refl-htpy)
      ( is-decidable-emb-map-decidable-emb f)

abstract
  is-equiv-htpy-eq-decidable-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f g : A ↪d B) 
    is-equiv (htpy-eq-decidable-emb f g)
  is-equiv-htpy-eq-decidable-emb f =
    fundamental-theorem-id
      ( is-contr-total-htpy-decidable-emb f)
      ( htpy-eq-decidable-emb f)

eq-htpy-decidable-emb :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A ↪d B} 
  htpy-decidable-emb f g  f  g
eq-htpy-decidable-emb {f = f} {g} =
  map-inv-is-equiv (is-equiv-htpy-eq-decidable-emb f g)

Precomposing decidable embeddings with equivalences

equiv-precomp-decidable-emb-equiv :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} (e : A  B) 
  (C : UU l3)  (B ↪d C)  (A ↪d C)
equiv-precomp-decidable-emb-equiv e C =
  equiv-Σ
    ( is-decidable-emb)
    ( equiv-precomp e C)
    ( λ g 
      equiv-prop
        ( is-prop-is-decidable-emb g)
        ( is-prop-is-decidable-emb (g  map-equiv e))
        ( is-decidable-emb-comp (is-decidable-emb-is-equiv (pr2 e)))
        ( λ d 
          is-decidable-emb-htpy
            ( λ b  ap g (inv (issec-map-inv-equiv e b)))
            ( is-decidable-emb-comp
              ( is-decidable-emb-is-equiv (is-equiv-map-inv-equiv e))
              ( d))))

Any map out of the empty type is a decidable embedding

abstract
  is-decidable-emb-ex-falso :
    {l : Level} {X : UU l}  is-decidable-emb (ex-falso {l} {X})
  pr1 (is-decidable-emb-ex-falso {l} {X}) = is-emb-ex-falso
  pr2 (is-decidable-emb-ex-falso {l} {X}) x = inr pr1

decidable-emb-ex-falso :
  {l : Level} {X : UU l}  empty ↪d X
pr1 decidable-emb-ex-falso = ex-falso
pr2 decidable-emb-ex-falso = is-decidable-emb-ex-falso

decidable-emb-is-empty :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  is-empty A  A ↪d B
decidable-emb-is-empty {A = A} f =
  map-equiv
    ( equiv-precomp-decidable-emb-equiv (equiv-is-empty f id) _)
    ( decidable-emb-ex-falso)

The map on total spaces induced by a family of decidable embeddings is a decidable embeddings

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

  is-decidable-emb-tot :
    {f : (x : A)  B x  C x} 
    ((x : A)  is-decidable-emb (f x))  is-decidable-emb (tot f)
  is-decidable-emb-tot H =
    ( is-emb-tot  x  is-emb-is-decidable-emb (H x)) ,
      is-decidable-map-tot λ x  is-decidable-map-is-decidable-emb (H x))

  decidable-emb-tot : ((x : A)  B x ↪d C x)  Σ A B ↪d Σ A C
  pr1 (decidable-emb-tot f) = tot  x  map-decidable-emb (f x))
  pr2 (decidable-emb-tot f) =
    is-decidable-emb-tot  x  is-decidable-emb-map-decidable-emb (f x))