Decidable maps

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

Created on 2022-01-27.
Last modified on 2025-08-14.

module foundation.decidable-maps where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.cartesian-morphisms-arrows
open import foundation.coproduct-types
open import foundation.decidable-equality
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.hilbert-epsilon-operators-maps
open import foundation.identity-types
open import foundation.retracts-of-maps
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.injective-maps
open import foundation-core.retractions
open import foundation-core.sections

Idea

A map is said to be decidable if its fibers are decidable types.

Definition

The structure on a map of decidability

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

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

The type of decidable maps

infix 5 _→ᵈ_

_→ᵈ_ : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
A →ᵈ B = Σ (A → B) (is-decidable-map)

decidable-map : {l1 l2 : Level} (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2)
decidable-map = _→ᵈ_

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A →ᵈ B)
  where

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

  is-decidable-decidable-map : is-decidable-map map-decidable-map
  is-decidable-decidable-map = pr2 f

Properties

Decidable maps are closed under homotopy

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

Composition of decidable maps

The composite g ∘ f of two decidable maps is decidable if g is injective.

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

  abstract
    is-decidable-map-comp :
      is-injective g →
      is-decidable-map g →
      is-decidable-map f →
      is-decidable-map (g ∘ f)
    is-decidable-map-comp H G F x =
      rec-coproduct
        ( λ u →
          is-decidable-iff
            ( λ v → (pr1 v) , ap g (pr2 v) ∙ pr2 u)
            ( λ w → pr1 w , H (pr2 w ∙ inv (pr2 u)))
            ( F (pr1 u)))
        ( λ α → inr (λ t → α (f (pr1 t) , pr2 t)))
        ( G x)

Left cancellation for decidable maps

If a composite g ∘ f is decidable and g is injective then f is decidable.

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

  abstract
    is-decidable-map-right-factor' :
      is-decidable-map (g ∘ f) → is-injective g → is-decidable-map f
    is-decidable-map-right-factor' GF G y =
      rec-coproduct
        ( λ q → inl (pr1 q , G (pr2 q)))
        ( λ q → inr (λ x → q ((pr1 x) , ap g (pr2 x))))
        ( GF (g y))

Retracts into types with decidable equality are decidable

is-decidable-map-retraction :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} → has-decidable-equality B →
  (i : A → B) → retraction i → is-decidable-map i
is-decidable-map-retraction d i (r , R) b =
  is-decidable-iff
    ( λ (p : i (r b) ＝ b) → r b , p)
    ( λ t → ap (i ∘ r) (inv (pr2 t)) ∙ ap i (R (pr1 t)) ∙ pr2 t)
    ( d (i (r b)) b)

Maps with sections are decidable

is-decidable-map-section :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  (i : A → B) → section i → is-decidable-map i
is-decidable-map-section i (s , S) b = inl (s b , S b)

Any map out of the empty type is decidable

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

The identity map is decidable

abstract
  is-decidable-map-id :
    {l : Level} {X : UU l} → is-decidable-map (id {l} {X})
  is-decidable-map-id y = inl (y , refl)

Equivalences are decidable maps

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

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

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

  is-decidable-map-tot :
    {f : (x : A) → B x → C x} →
    ((x : A) → is-decidable-map (f x)) → is-decidable-map (tot f)
  is-decidable-map-tot {f} H x =
    is-decidable-equiv (compute-fiber-tot f x) (H (pr1 x) (pr2 x))

The map on total spaces induced by a decidable map on the base is decidable

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

  is-decidable-map-Σ-map-base :
    {f : A → B} → is-decidable-map f → is-decidable-map (map-Σ-map-base f C)
  is-decidable-map-Σ-map-base {f} H x =
    is-decidable-equiv' (compute-fiber-map-Σ-map-base f C x) (H (pr1 x))

Products of decidable maps are decidable

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

  is-decidable-map-product :
    {f : A → B} {g : C → D} →
    is-decidable-map f → is-decidable-map g → is-decidable-map (map-product f g)
  is-decidable-map-product {f} {g} F G x =
    is-decidable-equiv
      ( compute-fiber-map-product f g x)
      ( is-decidable-product (F (pr1 x)) (G (pr2 x)))

Coproducts of decidable maps are decidable

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

  is-decidable-map-coproduct :
    {f : A → B} {g : C → D} →
    is-decidable-map f →
    is-decidable-map g →
    is-decidable-map (map-coproduct f g)
  is-decidable-map-coproduct {f} {g} F G (inl x) =
    is-decidable-equiv' (compute-fiber-inl-map-coproduct f g x) (F x)
  is-decidable-map-coproduct {f} {g} F G (inr y) =
    is-decidable-equiv' (compute-fiber-inr-map-coproduct f g y) (G y)

Decidable maps are closed under base change

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {D : UU l4}
  {f : A → B} {g : C → D}
  where

  is-decidable-map-base-change :
    cartesian-hom-arrow g f → is-decidable-map f → is-decidable-map g
  is-decidable-map-base-change α F d =
    is-decidable-equiv
      ( equiv-fibers-cartesian-hom-arrow g f α d)
      ( F (map-codomain-cartesian-hom-arrow g f α d))

Decidable maps are closed under retracts of maps

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
  {f : A → B} {g : X → Y}
  where

  is-decidable-retract-map :
    f retract-of-map g → is-decidable-map g → is-decidable-map f
  is-decidable-retract-map R G x =
    is-decidable-retract-of
      ( retract-fiber-retract-map f g R x)
      ( G (map-codomain-inclusion-retract-map f g R x))

Decidable maps have Hilbert ε-operators

A decidable map f induces “eliminators” on the propositional truncations of its fibers

 ε : (x : A) → ║ fiber f x ║₋₁ → fiber f x.

Such “eliminators” are called Hilbert ε-operators, or split supports.

ε-operator-map-is-decidable-map :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} {f : A → B} →
  is-decidable-map f → ε-operator-map f
ε-operator-map-is-decidable-map F = ε-operator-is-decidable ∘ F

Decidable injective maps are embeddings

Proof. Given a decidable map f : A → B then f decomposes B ≃ (im f) + B∖(im f). Restricting to im f we have a section given by the Hilbert ε-operator on f. Now, by injectivity of f we know this restriction map is an equivalence. Hence, f is a composite of embeddings and so must be an embedding as well.

    im f ╰────→ im f + B\(im f)
    ↟ ⋮              │
    │ ⋮ ~            │ ~
    │ ↓      f       ↓
     A ────────────→ B

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

  is-emb-is-injective-is-decidable-map :
    is-decidable-map f → is-injective f → is-emb f
  is-emb-is-injective-is-decidable-map H K =
    is-emb-is-injective-ε-operator-map (ε-operator-map-is-decidable-map H) K

There is also an analogous proof using the double negation image. This analogous proof avoids the use of propositional truncations, but cannot be included here due to introducing cyclic dependencies. See foundation.double-negation-images instead.

Recent changes