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}