# Decidable dependent function types

```agda
module elementary-number-theory.decidable-dependent-function-types where

open import foundation.decidable-dependent-function-types public
```

<details><summary>Imports</summary>

```agda

```

</details>

## Idea

We describe conditions under which dependent products are decidable.