------------------------------------------------------------------------
-- Unary relations
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Relation.Unary where

open import Data.Empty
open import Function
open import Data.Unit
open import Data.Product
open import Data.Sum
open import Level
open import Relation.Nullary

------------------------------------------------------------------------
-- Unary relations

Pred :  {a}  Set a  ( : Level)  Set (a  suc )
Pred A  = A  Set 

------------------------------------------------------------------------
-- Unary relations can be seen as sets

-- I.e., they can be seen as subsets of the universe of discourse.

private
 module Dummy {a} {A : Set a} -- The universe of discourse.
          where

  -- Set membership.

  infix 4 _∈_ _∉_

  _∈_ :  {}  A  Pred A   Set _
  x  P = P x

  _∉_ :  {}  A  Pred A   Set _
  x  P = ¬ x  P

  -- The empty set.

   : Pred A zero
   = λ _  

  -- The property of being empty.

  Empty :  {}  Pred A   Set _
  Empty P =  x  x  P

  ∅-Empty : Empty 
  ∅-Empty x ()

  -- The universe, i.e. the subset containing all elements in A.

  U : Pred A zero
  U = λ _  

  -- The property of being universal.

  Universal :  {}  Pred A   Set _
  Universal P =  x  x  P

  U-Universal : Universal U
  U-Universal = λ _  _

  -- Set complement.

   :  {}  Pred A   Pred A 
   P = λ x  x  P

  ∁∅-Universal : Universal ( )
  ∁∅-Universal = λ x x∈∅  x∈∅

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

  -- P ⊆ Q means that P is a subset of Q. _⊆′_ is a variant of _⊆_.

  infix 4 _⊆_ _⊇_ _⊆′_ _⊇′_

  _⊆_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Set _
  P  Q =  {x}  x  P  x  Q

  _⊆′_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Set _
  P ⊆′ Q =  x  x  P  x  Q

  _⊇_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Set _
  Q  P = P  Q

  _⊇′_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Set _
  Q ⊇′ P = P ⊆′ Q

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

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

  -- Set union.

  infixl 6 _∪_

  _∪_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Pred A _
  P  Q = λ x  x  P  x  Q

  -- Set intersection.

  infixl 7 _∩_

  _∩_ :  {ℓ₁ ℓ₂}  Pred A ℓ₁  Pred A ℓ₂  Pred A _
  P  Q = λ x  x  P × x  Q

open Dummy public

------------------------------------------------------------------------
-- Unary relation combinators

infixr 2 _⟨×⟩_
infixr 1 _⟨⊎⟩_
infixr 0 _⟨→⟩_

_⟨×⟩_ :  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} 
        Pred A ℓ₁  Pred B ℓ₂  Pred (A × B) _
(P ⟨×⟩ Q) p = P (proj₁ p) × Q (proj₂ p)

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

_⟨→⟩_ :  {a b ℓ₁ ℓ₂} {A : Set a} {B : Set b} 
        Pred A ℓ₁  Pred B ℓ₂  Pred (A  B) _
(P ⟨→⟩ Q) f = P  Q  f