------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of constructions over unary relations
------------------------------------------------------------------------

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

module Relation.Unary.Properties where

open import Data.Product using (_×_; _,_; swap; proj₁)
open import Data.Sum.Base using (inj₁; inj₂)
open import Data.Unit using (tt)
open import Level
open import Relation.Binary.Core
open import Relation.Binary.Definitions hiding (Decidable; Universal)
open import Relation.Unary
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Product using (_×-dec_)
open import Relation.Nullary.Sum using (_⊎-dec_)
open import Relation.Nullary.Negation using (¬?)
open import Function.Base using (_$_; _∘_)

private
  variable
    a b  ℓ₁ ℓ₂ : Level
    A : Set a
    B : Set b

----------------------------------------------------------------------
-- The empty set

∅? : Decidable {A = A} 
∅? _ = no λ()

∅-Empty : Empty {A = A} 
∅-Empty x ()

∁∅-Universal : Universal {A = A} ( )
∁∅-Universal = λ x x∈∅  x∈∅

----------------------------------------------------------------------
-- The universe

U? : Decidable {A = A} U
U? _ = yes tt

U-Universal : Universal {A = A} U
U-Universal = λ _  _

∁U-Empty : Empty {A = A} ( U)
∁U-Empty = λ x x∈∁U  x∈∁U _

----------------------------------------------------------------------
-- Subset properties

∅-⊆ : (P : Pred A )    P
∅-⊆ P ()

⊆-U : (P : Pred A )  P  U
⊆-U P _ = _

⊆-refl : Reflexive (_⊆_ {A = A} {})
⊆-refl x∈P = x∈P

⊆-trans : Transitive (_⊆_ {A = A} {})
⊆-trans P⊆Q Q⊆R x∈P = Q⊆R (P⊆Q x∈P)

⊂-asym : Asymmetric (_⊂_ {A = A} {})
⊂-asym (_ , Q⊈P) = Q⊈P  proj₁

----------------------------------------------------------------------
-- Decidability properties

∁? : {P : Pred A }  Decidable P  Decidable ( P)
∁? P? x = ¬? (P? x)

_∪?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} 
       Decidable P  Decidable Q  Decidable (P  Q)
_∪?_ P? Q? x = (P? x) ⊎-dec (Q? x)

_∩?_ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} 
       Decidable P  Decidable Q  Decidable (P  Q)
_∩?_ P? Q? x = (P? x) ×-dec (Q? x)

_×?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} 
       Decidable P  Decidable Q  Decidable (P ⟨×⟩ Q)
_×?_ P? Q? (a , b) = (P? a) ×-dec (Q? b)

_⊙?_ : {P : Pred A ℓ₁} {Q : Pred B ℓ₂} 
       Decidable P  Decidable Q  Decidable (P ⟨⊙⟩ Q)
_⊙?_ P? Q? (a , b) = (P? a) ⊎-dec (Q? b)

_⊎?_ : {P : Pred A } {Q : Pred B } 
       Decidable P  Decidable Q  Decidable (P ⟨⊎⟩ Q)
_⊎?_ P? Q? (inj₁ a) = P? a
_⊎?_ P? Q? (inj₂ b) = Q? b

_~? : {P : Pred (A × B) }  Decidable P  Decidable (P ~)
_~? P? = P?  swap