------------------------------------------------------------------------ -- Products of nullary relations ------------------------------------------------------------------------ module Relation.Nullary.Product where open import Data.Product open import Data.Function open import Relation.Nullary -- Some properties which are preserved by _×_. _×-dec_ : ∀ {P Q} → Dec P → Dec Q → Dec (P × Q) yes p ×-dec yes q = yes (p , q) no ¬p ×-dec _ = no (¬p ∘ proj₁) _ ×-dec no ¬q = no (¬q ∘ proj₂)