------------------------------------------------------------------------
-- The Agda standard library
--
-- Sums of nullary relations
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Relation.Nullary.Sum where

open import Data.Bool.Base
open import Data.Sum.Base
open import Data.Empty
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 1 _¬-⊎_ _⊎-reflects_ _⊎-dec_

_¬-⊎_ : ¬ P  ¬ Q  ¬ (P  Q)
_¬-⊎_ = [_,_]

_⊎-reflects_ :  {bp bq}  Reflects P bp  Reflects Q bq 
                           Reflects (P  Q) (bp  bq)
ofʸ  p ⊎-reflects      _ = ofʸ (inj₁ p)
ofⁿ ¬p ⊎-reflects ofʸ  q = ofʸ (inj₂ q)
ofⁿ ¬p ⊎-reflects ofⁿ ¬q = ofⁿ (¬p ¬-⊎ ¬q)

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