{-# OPTIONS --safe #-}
module Cubical.Relation.Nullary.DecidablePropositions where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Equiv renaming (_∙ₑ_ to _⋆_)

open import Cubical.Data.Bool
open import Cubical.Data.Sigma

open import Cubical.Relation.Nullary.Base
open import Cubical.Relation.Nullary.Properties

private
  variable
    ℓ ℓ'  : Level

DecProp : (ℓ : Level) → Type (ℓ-suc ℓ)
DecProp ℓ = Σ[ P ∈ hProp ℓ ] Dec (P .fst)

isSetDecProp : isSet (DecProp ℓ)
isSetDecProp = isOfHLevelΣ  isSetHProp (λ P → isProp→isSet (isPropDec (P .snd)))

-- the following is an alternative formulation of decidable propositions
-- it separates the boolean value from more proof-relevant part
-- so it performs better when doing computation

isDecProp : Type ℓ → Type ℓ
isDecProp P = Σ[ t ∈ Bool ] P ≃ Bool→Type t

DecProp' : (ℓ : Level) → Type (ℓ-suc ℓ)
DecProp' ℓ = Σ[ P ∈ Type ℓ ] isDecProp P

-- properties of the alternative formulation

isDecProp→isProp : {P : Type ℓ} → isDecProp P → isProp P
isDecProp→isProp h = isOfHLevelRespectEquiv  (invEquiv (h .snd)) isPropBool→Type

isDecProp→Dec : {P : Type ℓ} → isDecProp P → Dec P
isDecProp→Dec h = EquivPresDec (invEquiv (h .snd)) DecBool→Type

isPropIsDecProp : {P : Type ℓ} → isProp (isDecProp P)
isPropIsDecProp p q =
  Σ≡PropEquiv (λ _ → isOfHLevel⁺≃ᵣ  isPropBool→Type) .fst
    (Bool→TypeInj _ _ (invEquiv (p .snd) ⋆ q .snd))

isDecPropRespectEquiv : {P : Type ℓ} {Q : Type ℓ'}
  → P ≃ Q → isDecProp Q → isDecProp P
isDecPropRespectEquiv e (t , e') = t , e ⋆ e'