{-# OPTIONS --cubical-compatible --safe #-}
module Dec where
open import Logical-equivalence hiding (_∘_)
open import Prelude
private
variable
a : Level
A B : Type a
mutual
Dec-map : A ⇔ B → Dec A → Dec B
Dec-map A⇔B = Dec-map₀ to from
where
open _⇔_ A⇔B
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 : A ⇔ B → Dec A ⇔ Dec B
Dec-preserves A⇔B = record
{ to = Dec-map A⇔B
; from = Dec-map (inverse A⇔B)
}
Dec-× : Dec A → Dec B → Dec (A × B)
Dec-× =
[ (λ a → [ (λ b → yes (a , b))
, (λ ¬b → no (¬b ∘ proj₂))
])
, (λ ¬a _ → no (¬a ∘ proj₁))
]
Dec-⊎ : Dec A → Dec B → Dec (A ⊎ B)
Dec-⊎ =
[ (λ a _ → yes (inj₁ a))
, (λ ¬a →
[ (λ b → yes (inj₂ b))
, (λ ¬b → no [ ¬a , ¬b ])
])
]