# 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.