{-# OPTIONS --cubical --safe #-}

module DepthComonads.Dec where

open import DepthComonads.Level
open import DepthComonads.Bool
open import DepthComonads.Empty
open import DepthComonads.Stable

Reflects : Type a → Bool → Type a
Reflects A true  = A
Reflects A false = ¬ A

record Dec {a} (A : Type a) : Type a where
  constructor _because_
  field
    does  : Bool
    why   : Reflects A does
open Dec public

pattern yes p  = true   because p
pattern no ¬p  = false  because ¬p

map-reflects : (A → B) → (¬ A → ¬ B) → ∀ {d} → Reflects A d → Reflects B d
map-reflects {A = A} {B = B} to fro {d = d} = bool {P = λ d → Reflects A d → Reflects B d} fro to d

map-dec : (A → B) → (¬ A → ¬ B) → Dec A → Dec B
map-dec to fro dec .does = dec .does
map-dec to fro dec .why = map-reflects to fro (dec .why)

T? : (b : Bool) → Dec (T b)
T? b .does = b
T? false .why ()
T? true  .why = _

Dec→Stable : Dec A → Stable A
Dec→Stable (no ¬x) ¬¬x = ⊥-elim (¬¬x ¬x)
Dec→Stable (yes x) ¬¬x = x