Decidability of dependent function types

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

Created on 2022-02-14.
Last modified on 2025-08-14.

module foundation.decidable-dependent-function-types where
Imports 
open import foundation.decidable-propositions
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.functoriality-dependent-function-types
open import foundation.irrefutable-equality
open import foundation.maybe
open import foundation.mere-equality
open import foundation.propositions
open import foundation.uniformly-decidable-type-families
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-maybe
open import foundation.universe-levels

open import foundation-core.coproduct-types
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.function-types

open import logic.propositionally-decidable-types

Idea

We describe conditions under which dependent function types are decidable.

Properties

Decidability of dependent products of uniformly decidable families

is-decidable-Π-uniformly-decidable-family :
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
  is-decidable A →
  is-uniformly-decidable-family B →
  is-decidable ((a : A) → (B a))
is-decidable-Π-uniformly-decidable-family (inl a) (inl b) =
  inl b
is-decidable-Π-uniformly-decidable-family (inl a) (inr b) =
  inr (λ f → b a (f a))
is-decidable-Π-uniformly-decidable-family (inr na) _ =
  inl (ex-falso ∘ na)

abstract
  is-decidable-prop-Π-uniformly-decidable-family :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-decidable A →
    is-uniformly-decidable-family B →
    ((x : A) → is-prop (B x)) →
    is-decidable-prop ((a : A) → (B a))
  is-decidable-prop-Π-uniformly-decidable-family dA dB H =
    ( is-prop-Π H , is-decidable-Π-uniformly-decidable-family dA dB)

abstract
  is-decidable-prop-Π-uniformly-decidable-family' :
    {l1 l2 : Level} {A : UU l1} {B : A → UU l2} →
    is-inhabited-or-empty A →
    is-uniformly-decidable-family B →
    ((x : A) → is-prop (B x)) →
    is-decidable-prop ((a : A) → (B a))
  is-decidable-prop-Π-uniformly-decidable-family' {A = A} {B} dA dB H =
    elim-is-inhabited-or-empty-Prop'
      ( is-decidable-prop-Prop ((a : A) → (B a)))
      ( λ d → is-decidable-prop-Π-uniformly-decidable-family d dB H)
      ( dA)

Decidablitilty of dependent products over coproducts

is-decidable-Π-coproduct :
  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : A + B → UU l3} →
  is-decidable ((a : A) → C (inl a)) →
  is-decidable ((b : B) → C (inr b)) →
  is-decidable ((x : A + B) → C x)
is-decidable-Π-coproduct {C = C} dA dB =
  is-decidable-equiv
    ( equiv-dependent-universal-property-coproduct C)
    ( is-decidable-product dA dB)

Decidability of dependent products over Maybe

is-decidable-Π-Maybe :
  {l1 l2 : Level} {A : UU l1} {B : Maybe A → UU l2} →
  is-decidable ((x : A) → B (unit-Maybe x)) →
  is-decidable (B exception-Maybe) →
  is-decidable ((x : Maybe A) → B x)
is-decidable-Π-Maybe {B = B} du de =
  is-decidable-equiv
    ( equiv-dependent-universal-property-Maybe B)
    ( is-decidable-product du de)

Dependent products of decidable propositions over a base with all elements merely equal are decidable propositions

Assuming that all elements are merely equal in a type A then a dependent product of decidable propositions over A is again a decidable proposition.

module _
  {l1 l2 : Level} {A : UU l1} (B : A → Decidable-Prop l2)
  where

  is-decidable-Π-all-elements-merely-equal-base :
    all-elements-merely-equal A →
    is-decidable A →
    is-decidable ((x : A) → type-Decidable-Prop (B x))
  is-decidable-Π-all-elements-merely-equal-base H dA =
    is-decidable-Π-uniformly-decidable-family dA
      ( is-uniformly-decidable-family-all-elements-merely-equal-base
        ( H)
        ( λ x → is-decidable-Decidable-Prop (B x))
        ( dA))

  is-decidable-prop-Π-all-elements-merely-equal-base :
    all-elements-merely-equal A →
    is-decidable A →
    is-decidable-prop ((x : A) → type-Decidable-Prop (B x))
  is-decidable-prop-Π-all-elements-merely-equal-base H dA =
    is-decidable-prop-Π-uniformly-decidable-family dA
      ( is-uniformly-decidable-family-all-elements-merely-equal-base
        ( H)
        ( λ x → is-decidable-Decidable-Prop (B x))
        ( dA))
      ( λ x → is-prop-type-Decidable-Prop (B x))

  is-decidable-prop-Π-all-elements-merely-equal-base' :
    all-elements-merely-equal A →
    is-inhabited-or-empty A →
    is-decidable-prop ((x : A) → type-Decidable-Prop (B x))
  is-decidable-prop-Π-all-elements-merely-equal-base' H dA =
    is-decidable-prop-Π-uniformly-decidable-family' dA
      ( is-uniformly-decidable-family-all-elements-merely-equal-base'
        ( H)
        ( λ x → is-decidable-Decidable-Prop (B x))
        ( dA)
        ( λ x → is-prop-type-Decidable-Prop (B x)))
      ( λ x → is-prop-type-Decidable-Prop (B x))

Decidability of dependent products over an equivalence

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : A → UU l3} {D : B → UU l4}
  (e : A ≃ B) (f : (x : A) → C x ≃ D (map-equiv e x))
  where

  is-decidable-Π-equiv :
    is-decidable ((x : A) → C x) → is-decidable ((y : B) → D y)
  is-decidable-Π-equiv = is-decidable-equiv' (equiv-Π D e f)

  is-decidable-Π-equiv' :
    is-decidable ((y : B) → D y) → is-decidable ((x : A) → C x)
  is-decidable-Π-equiv' = is-decidable-equiv (equiv-Π D e f)

Recent changes