Decidable maps

module foundation.decidable-maps where
Imports
open import foundation.decidable-equality
open import foundation.decidable-types

open import foundation-core.dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.fibers-of-maps
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.retractions
open import foundation-core.universe-levels

Definition

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

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 (fib f y)
is-decidable-map-retr :
  {l1 l2 : Level} {A : UU l1} {B : UU l2}  has-decidable-equality B 
  (i : A  B)  retr i  is-decidable-map i
is-decidable-map-retr d i (pair r R) b =
  is-decidable-iff
    ( λ (p : i (r b)  b)  pair (r b) p)
    ( λ t  ap (i  r) (inv (pr2 t))  (ap i (R (pr1 t))  pr2 t))
    ( d (i (r b)) b)

Properties

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-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-is-equiv
      ( is-equiv-map-equiv
        ( compute-fib-tot f x))
      ( H (pr1 x) (pr2 x))