    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Unary relations
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Unary where

    open import Data.Empty using (⊥)
    open import Data.Unit.Base using (⊤)
    open import Data.Product.Base using (_×_; _,_; Σ-syntax; ∃; uncurry; swap)
    open import Data.Sum.Base using (_⊎_; [_,_])
    open import Function.Base using (_∘_; _|>_)
    open import Level using (Level; _⊔_; 0ℓ; suc; Lift)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)
    open import Relation.Nullary as Nullary using (¬_; Dec; True)

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

    ------------------------------------------------------------------------
    -- Definition

    -- Unary relations are known as predicates and `Pred A ℓ` can be viewed
    -- as some property that elements of type A might satisfy.

    -- Consequently `P : Pred A ℓ` can also be seen as a subset of A
    -- containing all the elements of A that satisfy property P. This view
    -- informs much of the notation used below.

    Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
    Pred A ℓ = A → Set ℓ

    ------------------------------------------------------------------------
    -- Special sets

    -- The empty set.
    -- Explicitly not level polymorphic as this often causes unsolved metas;
    -- see `Relation.Unary.Polymorphic` for a level-polymorphic version.

    ∅ : Pred A 0ℓ
    ∅ = λ _ → ⊥

    -- The singleton set.

    ｛_｝ : A → Pred A _
    ｛ x ｝ = x ≡_

    -- The universal set.
    -- Explicitly not level polymorphic (see comments for `∅` for more details)

    U : Pred A 0ℓ
    U = λ _ → ⊤

    ------------------------------------------------------------------------
    -- Membership

    infix 4 _∈_ _∉_

    _∈_ : A → Pred A ℓ → Set _
    x ∈ P = P x

    _∉_ : A → Pred A ℓ → Set _
    x ∉ P = ¬ x ∈ P

    ------------------------------------------------------------------------
    -- Subset relations

    infix 4 _⊆_ _⊇_ _⊈_ _⊉_ _⊂_ _⊃_ _⊄_ _⊅_ _≐_ _≐′_

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

    _⊇_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊇ Q = Q ⊆ P

    _⊈_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊈ Q = ¬ (P ⊆ Q)

    _⊉_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊉ Q = ¬ (P ⊇ Q)

    _⊂_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊂ Q = P ⊆ Q × Q ⊈ P

    _⊃_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊃ Q = Q ⊂ P

    _⊄_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊄ Q = ¬ (P ⊂ Q)

    _⊅_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊅ Q = ¬ (P ⊃ Q)

    _≐_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ≐ Q = (P ⊆ Q) × (Q ⊆ P)

    -- The following primed variants of _⊆_ can be used when 'x' can't
    -- be inferred from 'x ∈ P'.

    infix 4 _⊆′_ _⊇′_ _⊈′_ _⊉′_ _⊂′_ _⊃′_ _⊄′_ _⊅′_

    _⊆′_ : 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 _
    P ⊈′ Q = ¬ (P ⊆′ Q)

    _⊉′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊉′ Q = ¬ (P ⊇′ Q)

    _⊂′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊂′ Q = P ⊆′ Q × Q ⊈′ P

    _⊃′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊃′ Q = Q ⊂′ P

    _⊄′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊄′ Q = ¬ (P ⊂′ Q)

    _⊅′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊅′ Q = ¬ (P ⊃′ Q)

    _≐′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ≐′ Q = (P ⊆′ Q) × (Q ⊆′ P)

    ------------------------------------------------------------------------
    -- Properties of sets

    infix 10 Satisfiable Universal IUniversal

    -- Emptiness - no element satisfies P.

    Empty : Pred A ℓ → Set _
    Empty P = ∀ x → x ∉ P

    -- Satisfiable - at least one element satisfies P.

    Satisfiable : Pred A ℓ → Set _
    Satisfiable P = ∃ λ x → x ∈ P

    syntax Satisfiable P = ∃⟨ P ⟩

    -- Universality - all elements satisfy P.

    Universal : Pred A ℓ → Set _
    Universal P = ∀ x → x ∈ P

    syntax Universal  P = Π[ P ]

    -- Implicit universality - all elements satisfy P.

    IUniversal : Pred A ℓ → Set _
    IUniversal P = ∀ {x} → x ∈ P

    syntax IUniversal P = ∀[ P ]

    -- Irrelevance - any two proofs that an element satifies P are
    -- indistinguishable.

    Irrelevant : Pred A ℓ → Set _
    Irrelevant P = ∀ {x} → Nullary.Irrelevant (P x)

    -- Recomputability - we can rebuild a relevant proof given an
    -- irrelevant one.

    Recomputable : Pred A ℓ → Set _
    Recomputable P = ∀ {x} → Nullary.Recomputable (P x)

    -- Stability - instances of P are stable wrt double negation

    Stable : Pred A ℓ → Set _
    Stable P = ∀ x → Nullary.Stable (P x)

    -- Weak Decidability

    WeaklyDecidable : Pred A ℓ → Set _
    WeaklyDecidable P = ∀ x → Nullary.WeaklyDecidable (P x)

    -- Decidability - it is possible to determine if an arbitrary element
    -- satisfies P.

    Decidable : Pred A ℓ → Set _
    Decidable P = ∀ x → Dec (P x)

    -- Erasure: A decidable predicate gives rise to another one, more
    -- amenable to η-expansion

    ⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
    ⌊ P? ⌋ a = Lift _ (True (P? a))

    ------------------------------------------------------------------------
    -- Operations on sets

    infix 10 ⋃ ⋂
    infixr 9 _⊢_
    infixr 8 _⇒_
    infixr 7 _∩_
    infixr 6 _∪_
    infixr 6 _∖_
    infix 4 _≬_ _⊥_ _⊥′_

    -- Complement.

    ∁ : Pred A ℓ → Pred A ℓ
    ∁ P = λ x → x ∉ P

    -- Implication.

    _⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
    P ⇒ Q = λ x → x ∈ P → x ∈ Q

    -- Union.

    _∪_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
    P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q

    -- Intersection.

    _∩_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
    P ∩ Q = λ x → x ∈ P × x ∈ Q

    -- Difference.

    _∖_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
    P ∖ Q = λ x → x ∈ P × x ∉ Q

    -- Infinitary union.

    ⋃ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
    ⋃ I P = λ x → Σ[ i ∈ I ] P i x

    syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P

    -- Infinitary intersection.

    ⋂ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
    ⋂ I P = λ x → (i : I) → P i x

    syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P

    -- Positive version of non-disjointness, dual to inclusion.

    _≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q

    -- Disjoint

    _⊥_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊥ Q = P ∩ Q ⊆ ∅

    _⊥′_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
    P ⊥′ Q = P ∩ Q ⊆′ ∅

    -- Update.

    _⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
    f ⊢ P = λ x → P (f x)

    ------------------------------------------------------------------------
    -- Predicate combinators

    -- These differ from the set operations above, as the carrier set of the
    -- resulting predicates are not the same as the carrier set of the
    -- component predicates.

    infixr  2 _⟨×⟩_
    infixr  2 _⟨⊙⟩_
    infixr  1 _⟨⊎⟩_
    infixr  0 _⟨→⟩_
    infixl  9 _⟨·⟩_
    infix  10 _~
    infixr  9 _⟨∘⟩_
    infixr  2 _//_ _\\_

    -- Product.

    _⟨×⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
    (P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q

    -- Sum over one element.

    _⟨⊎⟩_ : Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
    P ⟨⊎⟩ Q = [ P , Q ]

    -- Sum over two elements.

    _⟨⊙⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
    (P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q

    -- Implication.

    _⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
    (P ⟨→⟩ Q) f = P ⊆ Q ∘ f

    -- Product.

    _⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
            (P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry _|>_
    (P ⟨·⟩ Q) (p , f) = f p

    -- Converse.

    _~ : Pred (A × B) ℓ → Pred (B × A) ℓ
    P ~ = P ∘ swap

    -- Composition.

    _⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
    (P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q

    -- Post-division.

    _//_ : Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
    (P // Q) (x , y) = Q ∘ (y ,_) ⊆ P ∘ (x ,_)

    -- Pre-division.

    _\\_ : Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
    P \\ Q = (P ~ // Q ~) ~