Martin Escardo, January 2018, May 2020 \begin{code} {-# OPTIONS --safe --without-K #-} module Dominance.Decidable where open import Dominance.Definition open import MLTT.Spartan open import NotionsOfDecidability.Decidable open import UF.FunExt open import UF.Subsingletons open import UF.Subsingletons-FunExt decidable-dominance : Fun-Ext → Dominance {𝓤} {𝓤} decidable-dominance fe = (λ P → is-prop P × is-decidable P) , (λ P → Σ-is-prop (being-prop-is-prop fe) (decidability-of-prop-is-prop fe)) , (λ X → pr₁) , (𝟙-is-prop , inl ⋆) , λ P Q dP dQ → Σ-is-prop (pr₁ dP) (λ p → pr₁ (dQ p)) , decidable-closed-under-Σ (pr₁ dP) (pr₂ dP) λ p → pr₂ (dQ p) \end{code}