------------------------------------------------------------------------
-- Some definitions related to Dec
------------------------------------------------------------------------

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

module Dec where

open import Logical-equivalence hiding (_∘_)
open import Prelude

private
  variable
    a   : Level
    A B : Type a

mutual

  -- A map function for Dec.

  Dec-map : A  B  Dec A  Dec B
  Dec-map A⇔B = Dec-map₀ to from
    where
    open _⇔_ A⇔B

  -- A generalisation of Dec-map.

  Dec-map₀ : (A  B)  @0 (B  A)  Dec A  Dec B
  Dec-map₀ to from = ⊎-map to  f x  ⊥-elim₀ (f (from x)))

-- Dec preserves logical equivalences.

Dec-preserves : A  B  Dec A  Dec B
Dec-preserves A⇔B = record
  { to   = Dec-map A⇔B
  ; from = Dec-map (inverse A⇔B)
  }

-- If A and B are decided, then A × B is.

Dec-× : Dec A  Dec B  Dec (A × B)
Dec-× =
  [  a  [  b  yes (a , b))
           ,  ¬b  no (¬b  proj₂))
           ])
  ,  ¬a _  no (¬a  proj₁))
  ]

-- If A and B are decided, then A ⊎ B is.

Dec-⊎ : Dec A  Dec B  Dec (A  B)
Dec-⊎ =
  [  a _  yes (inj₁ a))
  ,  ¬a 
       [  b  yes (inj₂ b))
       ,  ¬b  no [ ¬a , ¬b ])
       ])
  ]