{-# OPTIONS --cubical-compatible #-}

module Terra.Data.Decision where
open import Terra.Data.Level
open import Terra.Data.Negation
open import Terra.Data.Unit
open import Terra.Data.Counit
open import Terra.Data.Bool
open import Terra.Data.Equality
-- Decision désigne une preuve ou une contre preuve d'une propriété ou
-- proposition.

private
  variable
    ℓ ℓ′ : Level

data Decision {ℓ} (P : Set ℓ) : Set ℓ where
  yes : P -> Decision P
  no : ¬ P -> Decision P

⌊_⌋ : {P : Set ℓ} -> Decision P -> Set
⌊ yes x ⌋ = ⊤
⌊ no x ⌋ = ⊥

¬⌊_⌋ : {P : Set ℓ} -> Decision P -> Set
¬⌊ yes x ⌋ = ⊥
¬⌊ no x ⌋ = ⊤

⌊⌋-elim : {P : Set ℓ} -> {d : Decision P} -> ⌊ d ⌋ -> P
⌊⌋-elim {d = yes x} tt = x

¬⌊⌋-elim : {P : Set ℓ} -> {d : Decision P} -> ¬⌊ d ⌋ -> ¬ P
¬⌊⌋-elim {d = no x} v = x

dec-elim : {P : Set ℓ} {A : Set ℓ′} -> (P -> A) -> (¬ P -> A) -> Decision P -> A
dec-elim y n (yes x) = y x
dec-elim y n (no x) = n x

T : Bool -> Set
T b = b ≡ true

-- ¬′_ : {P : Set ℓ} -> Decision P -> Decision (¬ P)
-- ¬′ yes x = no {!λ f -> ?!}
-- ¬′ no x = {!!}