Decidable

Let $P:A\to \mathrm{Prop}$ be a predicate. We say that $P$ is decidable iff there is a procedure

$$f_P:\prod _{a:A}Pa\uplus \neg Pa$$

That produces a proof of $Pa$ or $\neg Pa$ for all $a$.