# Decidability of dependent pair types

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

Created on 2022-02-14.

module univalent-combinatorics.decidable-dependent-pair-types where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.coproduct-types
open import foundation.decidable-dependent-pair-types
open import foundation.decidable-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.unit-type
open import foundation.universe-levels

open import univalent-combinatorics.counting
open import univalent-combinatorics.standard-finite-types


## Idea

We describe conditions under which dependent sums are decidable.

## Note

It is not the case for a family B of decidable types over a finite type A, that the dependent pair type Σ A B is decidable.

## Properties

### The Σ-type of any family of decidable types over Fin k is decidable

is-decidable-Σ-Fin :
{l : Level} (k : ℕ) {P : Fin k → UU l} →
((x : Fin k) → is-decidable (P x)) → is-decidable (Σ (Fin k) P)
is-decidable-Σ-Fin zero-ℕ {P} d = inr pr1
is-decidable-Σ-Fin (succ-ℕ k) {P} d with d (inr star)
... | inl p = inl (pair (inr star) p)
... | inr f =
is-decidable-iff
( λ t → pair (inl (pr1 t)) (pr2 t))
( g)
( is-decidable-Σ-Fin k {P ∘ inl} (λ x → d (inl x)))
where
g : Σ (Fin (succ-ℕ k)) P → Σ (Fin k) (P ∘ inl)
g (pair (inl x) p) = pair x p
g (pair (inr star) p) = ex-falso (f p)


### The Σ-type of any family of decidable types over a type equipped with count is decidable

is-decidable-Σ-count :
{l1 l2 : Level} {A : UU l1} {B : A → UU l2} → count A →
((x : A) → is-decidable (B x)) → is-decidable (Σ A B)
is-decidable-Σ-count e d =
is-decidable-Σ-equiv
( equiv-count e)
( λ x → id-equiv)
( is-decidable-Σ-Fin
( number-of-elements-count e)
( λ x → d (map-equiv-count e x)))