------------------------------------------------------------------------
-- 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?