------------------------------------------------------------------------
-- Unary relations (variant for Set₁)
------------------------------------------------------------------------

-- I want universe polymorphism.

module Relation.Unary1 where

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

Pred : Set → Set₂
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 : Set} -- The universe of discourse.
          where

  -- Set membership.

  infix  _∈_

  _∈_ : a → Pred a → Set₁
  x ∈ P = P x

  -- The property of being universal.

  Universal : Pred a → Set₁
  Universal P = ∀ x → x ∈ P

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

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

  _⊆_ : 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

open Dummy public