Decidable types

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Eléonore Mangel.

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

module foundation.decidable-types where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.double-negation
open import foundation.double-negation-dense-equality
open import foundation.empty-types
open import foundation.equivalences
open import foundation.evaluation-functions
open import foundation.functoriality-coproduct-types
open import foundation.hilberts-epsilon-operators
open import foundation.irrefutable-equality
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.raising-universe-levels
open import foundation.retracts-of-types
open import foundation.transport-along-identifications
open import foundation.type-arithmetic-empty-type
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.function-types
open import foundation-core.retractions
open import foundation-core.sections

Idea

A type is said to be decidable if we can either construct an element, or we can prove that it is empty. In other words, we interpret decidability via the Curry–Howard interpretation of logic into type theory. A related concept is that a type is either inhabited or empty, where inhabitedness of a type is expressed using the propositional truncation.

Definitions

The Curry–Howard interpretation of decidability

is-decidable : {l : Level} (A : UU l) → UU l
is-decidable A = A + (¬ A)

Examples

The unit type and the empty type are decidable

is-decidable-unit : is-decidable unit
is-decidable-unit = inl star

is-decidable-empty : is-decidable empty
is-decidable-empty = inr id

Properties

Coproducts of decidable types are decidable

is-decidable-coproduct :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → is-decidable B → is-decidable (A + B)
is-decidable-coproduct (inl a) y = inl (inl a)
is-decidable-coproduct (inr na) (inl b) = inl (inr b)
is-decidable-coproduct (inr na) (inr nb) = inr (rec-coproduct na nb)

Cartesian products of decidable types are decidable

is-decidable-product :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → is-decidable B → is-decidable (A × B)
is-decidable-product (inl a) (inl b) = inl (a , b)
is-decidable-product (inl a) (inr g) = inr (g ∘ pr2)
is-decidable-product (inr f) (inl b) = inr (f ∘ pr1)
is-decidable-product (inr f) (inr g) = inr (f ∘ pr1)

is-decidable-product' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → (A → is-decidable B) → is-decidable (A × B)
is-decidable-product' (inl a) d =
  rec-coproduct (λ b → inl (a , b)) (λ nb → inr (nb ∘ pr2)) (d a)
is-decidable-product' (inr na) d = inr (na ∘ pr1)

is-decidable-left-factor :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable (A × B) → B → is-decidable A
is-decidable-left-factor (inl (x , y)) b = inl x
is-decidable-left-factor (inr f) b = inr (λ a → f (a , b))

is-decidable-right-factor :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable (A × B) → A → is-decidable B
is-decidable-right-factor (inl (x , y)) a = inl y
is-decidable-right-factor (inr f) a = inr (λ b → f (a , b))

Function types of decidable types are decidable

is-decidable-function-type :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → is-decidable B → is-decidable (A → B)
is-decidable-function-type (inl a) (inl b) = inl (λ _ → b)
is-decidable-function-type (inl a) (inr nb) = inr (map-neg (ev a) nb)
is-decidable-function-type (inr f) _ = inl (ex-falso ∘ f)

is-decidable-function-type' :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} →
  is-decidable A → (A → is-decidable B) → is-decidable (A → B)
is-decidable-function-type' (inl a) d =
  rec-coproduct (λ b → inl (λ _ → b)) (λ nb → inr (map-neg (ev a) nb)) (d a)
is-decidable-function-type' (inr na) d = inl (ex-falso ∘ na)

The negation of a decidable type is decidable

is-decidable-neg :
  {l : Level} {A : UU l} → is-decidable A → is-decidable (¬ A)
is-decidable-neg d = is-decidable-function-type d is-decidable-empty

The double negation of a decidable type is decidable

is-decidable-double-negation :
  {l : Level} {A : UU l} → is-decidable A → is-decidable (¬¬ A)
is-decidable-double-negation d = is-decidable-neg (is-decidable-neg d)

Decidable types are closed under coinhabited types

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

  is-decidable-iff :
    (A → B) → (B → A) → is-decidable A → is-decidable B
  is-decidable-iff f g (inl a) = inl (f a)
  is-decidable-iff f g (inr na) = inr (na ∘ g)

  is-decidable-iff' :
    A ↔ B → is-decidable A → is-decidable B
  is-decidable-iff' (f , g) = is-decidable-iff f g

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

  iff-is-decidable : A ↔ B → is-decidable A ↔ is-decidable B
  iff-is-decidable e = is-decidable-iff' e , is-decidable-iff' (inv-iff e)

Decidable types are closed under retracts

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

  is-decidable-retract-of :
    A retract-of B → is-decidable B → is-decidable A
  is-decidable-retract-of R = is-decidable-iff' (iff-retract' R)

  is-decidable-retract-of' :
    A retract-of B → is-decidable A → is-decidable B
  is-decidable-retract-of' R = is-decidable-iff' (inv-iff (iff-retract' R))

Decidable types are closed under equivalences

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

  is-decidable-is-equiv :
    {f : A → B} → is-equiv f → is-decidable B → is-decidable A
  is-decidable-is-equiv {f} H =
    is-decidable-retract-of (retract-equiv (f , H))

  is-decidable-equiv :
    A ≃ B → is-decidable B → is-decidable A
  is-decidable-equiv e = is-decidable-iff (map-inv-equiv e) (map-equiv e)

  is-decidable-equiv' :
    A ≃ B → is-decidable A → is-decidable B
  is-decidable-equiv' e = is-decidable-iff (map-equiv e) (map-inv-equiv e)

Equivalent types have equivalent decidability predicates

module _
  {l1 l2 : Level} {A : UU l1} {B : UU l2} (e : A ≃ B)
  where

  map-equiv-is-decidable : is-decidable A → is-decidable B
  map-equiv-is-decidable = is-decidable-equiv' e

  map-inv-equiv-is-decidable : is-decidable B → is-decidable A
  map-inv-equiv-is-decidable = is-decidable-equiv e

  is-section-map-inv-equiv-is-decidable :
    is-section map-equiv-is-decidable map-inv-equiv-is-decidable
  is-section-map-inv-equiv-is-decidable (inl x) =
    ap inl (is-section-map-inv-equiv e x)
  is-section-map-inv-equiv-is-decidable (inr x) =
    ap inr eq-neg

  is-retraction-map-inv-equiv-is-decidable :
    is-retraction map-equiv-is-decidable map-inv-equiv-is-decidable
  is-retraction-map-inv-equiv-is-decidable (inl x) =
    ap inl (is-retraction-map-inv-equiv e x)
  is-retraction-map-inv-equiv-is-decidable (inr x) =
    ap inr eq-neg

  is-equiv-map-equiv-is-decidable : is-equiv map-equiv-is-decidable
  is-equiv-map-equiv-is-decidable =
    is-equiv-is-invertible
      map-inv-equiv-is-decidable
      is-section-map-inv-equiv-is-decidable
      is-retraction-map-inv-equiv-is-decidable

  equiv-is-decidable : is-decidable A ≃ is-decidable B
  equiv-is-decidable = map-equiv-is-decidable , is-equiv-map-equiv-is-decidable

Decidability implies double negation elimination

double-negation-elim-is-decidable :
  {l : Level} {P : UU l} → is-decidable P → (¬¬ P → P)
double-negation-elim-is-decidable (inl x) p = x
double-negation-elim-is-decidable (inr x) p = ex-falso (p x)

See also double negation stable propositions.

Decidable types have ε-operators

ε-operator-is-decidable :
  {l : Level} {A : UU l} → is-decidable A → ε-operator-Hilbert A
ε-operator-is-decidable (inl a) x = a
ε-operator-is-decidable (inr f) x =
  ex-falso (apply-universal-property-trunc-Prop x empty-Prop f)

is-decidable is an idempotent operation

module _
  {l : Level} {P : UU l}
  where

  map-idempotent-is-decidable : is-decidable P → is-decidable (is-decidable P)
  map-idempotent-is-decidable = inl

  map-inv-idempotent-is-decidable :
    is-decidable (is-decidable P) → is-decidable P
  map-inv-idempotent-is-decidable (inl (inl p)) = inl p
  map-inv-idempotent-is-decidable (inl (inr np)) = inr np
  map-inv-idempotent-is-decidable (inr np) = inr (λ p → np (inl p))

Any inhabited type is a fixed point for is-decidable

is-fixed-point-is-decidable-is-inhabited :
  {l : Level} {X : UU l} → type-trunc-Prop X → is-decidable X ≃ X
is-fixed-point-is-decidable-is-inhabited {l} {X} t =
  right-unit-law-coproduct-is-empty X (¬ X) (is-nonempty-is-inhabited t)

The dependent sum of a family of decidable propositions over a decidable base with double negation dense equality is decidable

This is a special case of the more general fact that a type has decidable sums if and only if its totally separated reflection does, and totally separated types have double negation stable equality. [Esc]

is-decidable-Σ-has-double-negation-dense-equality-base :
  {l1 l2 : Level} {P : UU l1} {Q : P → UU l2} →
  has-double-negation-dense-equality P →
  is-decidable P →
  ((x : P) → is-decidable (Q x)) → is-decidable (Σ P Q)
is-decidable-Σ-has-double-negation-dense-equality-base {Q = Q} hP (inl p) dQ =
  map-coproduct
    ( pair p)
    ( λ nq pq → hP (pr1 pq) p (λ r → nq (tr Q r (pr2 pq))))
    ( dQ p)
is-decidable-Σ-has-double-negation-dense-equality-base hP (inr np) _ =
  inr (map-neg pr1 np)

Raising universe level preserves decidability

module _
  (l : Level) {l1 : Level} (A : UU l1)
  where

  is-decidable-raise : is-decidable A → is-decidable (raise l A)
  is-decidable-raise = is-decidable-equiv' (compute-raise l A)

See also

References

[Esc]
Martín Hötzel Escardó and contributors. TypeTopology. GitHub repository. Agda development. URL: https://github.com/martinescardo/TypeTopology.

Recent changes