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