{-# 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_
    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