Decidable dependent function types

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

Created on 2022-02-14.
Last modified on 2023-06-07.

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.

Recent changes

• 2023-06-07. Fredrik Bakke. Move public imports before “Imports” block (#642).
• 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
• 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
• 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
• 2023-02-13. Jonathan Prieto-Cubides. Nueva era (#445).