This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Decidable dependent function types

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

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

Idea

We describe conditions under which dependent products are decidable.