------------------------------------------------------------------------ -- The Agda standard library -- -- Products of nullary relations ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Relation.Nullary.Product where open import Data.Bool.Base open import Data.Product open import Function.Base using (_∘_) open import Level open import Relation.Nullary.Reflects open import Relation.Nullary private variable p q : Level P : Set p Q : Set q ------------------------------------------------------------------------ -- Some properties which are preserved by _×_. infixr 2 _×-reflects_ _×-dec_ _×-reflects_ : ∀ {bp bq} → Reflects P bp → Reflects Q bq → Reflects (P × Q) (bp ∧ bq) ofʸ p ×-reflects ofʸ q = ofʸ (p , q) ofʸ p ×-reflects ofⁿ ¬q = ofⁿ (¬q ∘ proj₂) ofⁿ ¬p ×-reflects _ = ofⁿ (¬p ∘ proj₁) _×-dec_ : Dec P → Dec Q → Dec (P × Q) does (p? ×-dec q?) = does p? ∧ does q? proof (p? ×-dec q?) = proof p? ×-reflects proof q?