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

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

    module Relation.Unary.Properties where

    open import Data.Product.Base as Product using (_×_; _,_; swap; proj₁; zip′)
    open import Data.Sum.Base using (inj₁; inj₂)
    open import Data.Unit.Base using (tt)
    open import Function.Base using (id; _$_; _∘_; _∘₂_)
    open import Level using (Level)
    open import Relation.Binary.Core as Binary
    open import Relation.Binary.Definitions
      hiding (Decidable; Universal; Irrelevant; Empty)
    open import Relation.Binary.PropositionalEquality.Core using (refl; _≗_)
    open import Relation.Nullary.Decidable as Dec
      using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
    open import Relation.Nullary.Negation.Core using (¬_)
    open import Relation.Unary

    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 = Pred A ℓ} _⊆_
    ⊆-refl x∈P = x∈P

    ⊆-reflexive : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐_ _⊆_
    ⊆-reflexive (P⊆Q , Q⊆P) = P⊆Q

    ⊆-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊆_ _⊆_ _⊆_
    ⊆-trans P⊆Q Q⊆R x∈P = Q⊆R (P⊆Q x∈P)

    ⊆-antisym : Antisymmetric {A = Pred A ℓ} _≐_ _⊆_
    ⊆-antisym = _,_

    ⊆-min : Min {B = Pred A ℓ} _⊆_ ∅
    ⊆-min = ∅-⊆

    ⊆-max : Max {A = Pred A ℓ} _⊆_ U
    ⊆-max = ⊆-U

    ⊂⇒⊆ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂_ _⊆_
    ⊂⇒⊆ = proj₁

    ⊂-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊂_ _⊂_ _⊂_
    ⊂-trans (P⊆Q , Q⊈P) (Q⊆R , R⊈Q) = (λ x∈P → Q⊆R (P⊆Q x∈P)) , (λ R⊆P → R⊈Q (λ x∈R → P⊆Q (R⊆P x∈R)))

    ⊂-⊆-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊂_ _⊆_ _⊂_
    ⊂-⊆-trans (P⊆Q , Q⊈P) Q⊆R = (λ x∈P → Q⊆R (P⊆Q x∈P)) , (λ R⊆P → Q⊈P (λ x∈Q → R⊆P (Q⊆R x∈Q)))

    ⊆-⊂-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊆_ _⊂_ _⊂_
    ⊆-⊂-trans P⊆Q (Q⊆R , R⊈Q) = (λ x∈P → Q⊆R (P⊆Q x∈P)) , (λ R⊆P → R⊈Q (λ R⊆Q → P⊆Q (R⊆P R⊆Q)))

    ⊂-respʳ-≐ : _Respectsʳ_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂_ _≐_
    ⊂-respʳ-≐ (Q⊆R , _) P⊂Q = ⊂-⊆-trans P⊂Q Q⊆R

    ⊂-respˡ-≐ : _Respectsˡ_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂_ _≐_
    ⊂-respˡ-≐ (_ , R⊆Q) P⊂Q = ⊆-⊂-trans R⊆Q P⊂Q

    ⊂-resp-≐ : _Respects₂_ {A = Pred A ℓ} _⊂_ _≐_
    ⊂-resp-≐ = ⊂-respʳ-≐ , ⊂-respˡ-≐

    ⊂-irrefl : Irreflexive {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐_ _⊂_
    ⊂-irrefl (_ , Q⊆P) (_ , Q⊈P) = Q⊈P Q⊆P

    ⊂-antisym : Antisymmetric {A = Pred A ℓ} _≐_ _⊂_
    ⊂-antisym (P⊆Q , _) (Q⊆P , _) = ⊆-antisym P⊆Q Q⊆P

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

    ∅-⊆′ : (P : Pred A ℓ) → ∅ ⊆′ P
    ∅-⊆′ _ _ = λ ()

    ⊆′-U : (P : Pred A ℓ) → P ⊆′ U
    ⊆′-U _ _ _ = _

    ⊆′-refl : Reflexive {A = Pred A ℓ} _⊆′_
    ⊆′-refl x x∈P = x∈P

    ⊆′-reflexive : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _⊆′_
    ⊆′-reflexive (P⊆Q , Q⊆P) = P⊆Q

    ⊆′-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊆′_ _⊆′_ _⊆′_
    ⊆′-trans P⊆Q Q⊆R x x∈P = Q⊆R x (P⊆Q x x∈P)

    ⊆′-antisym : Antisymmetric {A = Pred A ℓ} _≐′_ _⊆′_
    ⊆′-antisym = _,_

    ⊆′-min : Min {B = Pred A ℓ} _⊆′_ ∅
    ⊆′-min = ∅-⊆′

    ⊆′-max : Max {A = Pred A ℓ} _⊆′_ U
    ⊆′-max = ⊆′-U

    ⊂′⇒⊆′ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂′_ _⊆′_
    ⊂′⇒⊆′ = proj₁

    ⊂′-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊂′_ _⊂′_ _⊂′_
    ⊂′-trans (P⊆Q , Q⊈P) (Q⊆R , R⊈Q) = ⊆′-trans P⊆Q Q⊆R , λ R⊆P → R⊈Q (⊆′-trans R⊆P P⊆Q)

    ⊂′-⊆′-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊂′_ _⊆′_ _⊂′_
    ⊂′-⊆′-trans (P⊆Q , Q⊈P) Q⊆R = ⊆′-trans P⊆Q Q⊆R , λ R⊆P → Q⊈P (⊆′-trans Q⊆R R⊆P)

    ⊆′-⊂′-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _⊆′_ _⊂′_ _⊂′_
    ⊆′-⊂′-trans P⊆Q (Q⊆R , R⊈Q) = ⊆′-trans P⊆Q Q⊆R , λ R⊆P → R⊈Q (⊆′-trans R⊆P P⊆Q)

    ⊂′-respʳ-≐′ : _Respectsʳ_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂′_ _≐′_
    ⊂′-respʳ-≐′ (Q⊆R , _) P⊂Q = ⊂′-⊆′-trans P⊂Q Q⊆R

    ⊂′-respˡ-≐′ : _Respectsˡ_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂′_ _≐′_
    ⊂′-respˡ-≐′ (_ , R⊆Q) P⊂Q = ⊆′-⊂′-trans R⊆Q P⊂Q

    ⊂′-resp-≐′ : _Respects₂_ {A = Pred A ℓ₁} _⊂′_ _≐′_
    ⊂′-resp-≐′ = ⊂′-respʳ-≐′ , ⊂′-respˡ-≐′

    ⊂′-irrefl : Irreflexive {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _⊂′_
    ⊂′-irrefl (_ , Q⊆P) (_ , Q⊈P) = Q⊈P Q⊆P

    ⊂′-antisym : Antisymmetric {A = Pred A ℓ} _≐′_ _⊂′_
    ⊂′-antisym (P⊆Q , _) (Q⊆P , _) = ⊆′-antisym P⊆Q Q⊆P

    ⊆⇒⊆′ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆_ _⊆′_
    ⊆⇒⊆′ P⊆Q _ x∈P = P⊆Q x∈P

    ⊆′⇒⊆ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊆′_ _⊆_
    ⊆′⇒⊆ P⊆Q x∈P = P⊆Q _ x∈P

    ⊂⇒⊂′ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂_ _⊂′_
    ⊂⇒⊂′ = Product.map ⊆⇒⊆′ (_∘ ⊆′⇒⊆)

    ⊂′⇒⊂ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊂′_ _⊂_
    ⊂′⇒⊂ = Product.map ⊆′⇒⊆ (_∘ ⊆⇒⊆′)

    ------------------------------------------------------------------------
    -- Equality properties

    ≐-refl : Reflexive {A = Pred A ℓ} _≐_
    ≐-refl = id , id

    ≐-sym : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐_ _≐_
    ≐-sym = swap

    ≐-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _≐_ _≐_ _≐_
    ≐-trans = zip′ (λ P⊆Q Q⊆R x∈P → Q⊆R (P⊆Q x∈P)) (λ Q⊆P R⊆Q x∈R → Q⊆P (R⊆Q x∈R))

    ≐′-refl : Reflexive {A = Pred A ℓ} _≐′_
    ≐′-refl = (λ _ → id) , (λ _ → id)

    ≐′-sym : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _≐′_
    ≐′-sym = swap

    ≐′-trans : Trans {A = Pred A ℓ₁} {B = Pred A ℓ₂} {C = Pred A ℓ₃} _≐′_ _≐′_ _≐′_
    ≐′-trans = zip′ (λ P⊆Q Q⊆R x x∈P → Q⊆R x (P⊆Q x x∈P)) λ Q⊆P R⊆Q x x∈R → Q⊆P x (R⊆Q x x∈R)

    ≐⇒≐′ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐_ _≐′_
    ≐⇒≐′ = Product.map ⊆⇒⊆′ ⊆⇒⊆′

    ≐′⇒≐ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≐′_ _≐_
    ≐′⇒≐ = Product.map ⊆′⇒⊆ ⊆′⇒⊆

    ------------------------------------------------------------------------
    -- Between/Disjoint properties

    ≬-symmetric : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≬_ _≬_
    ≬-symmetric = Product.map₂ swap

    ⊥-symmetric : Sym {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ _⊥_
    ⊥-symmetric = _∘ swap

    ≬-sym : Symmetric {A = Pred A ℓ₁} _≬_
    ≬-sym = ≬-symmetric

    ⊥-sym : Symmetric {A = Pred A ℓ₁} _⊥_
    ⊥-sym = ⊥-symmetric

    ≬⇒¬⊥ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _≬_ (¬_ ∘₂ _⊥_)
    ≬⇒¬⊥ P≬Q ¬P⊥Q = ¬P⊥Q (Product.proj₂ P≬Q)

    ⊥⇒¬≬ : Binary._⇒_ {A = Pred A ℓ₁} {B = Pred A ℓ₂} _⊥_ (¬_ ∘₂ _≬_)
    ⊥⇒¬≬ P⊥Q = P⊥Q ∘ Product.proj₂

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

    map : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} →
          P ≐ Q → Decidable P → Decidable Q
    map (P⊆Q , Q⊆P) P? x = map′ P⊆Q Q⊆P (P? x)

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

    infix 2 _×?_ _⊙?_
    infix 10 _~?
    infixr 1 _⊎?_
    infixr 7 _∩?_
    infixr 6 _∪?_

    _∪?_ : {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

    does-≡ : {P : Pred A ℓ} → (P? P?′ : Decidable P) →
             does ∘ P? ≗ does ∘ P?′
    does-≡ P? P?′ x = Dec.does-≡ (P? x) (P?′ x)

    does-≐ : {P : Pred A ℓ₁} {Q : Pred A ℓ₂} → P ≐ Q →
             (P? : Decidable P) → (Q? : Decidable Q) →
             does ∘ P? ≗ does ∘ Q?
    does-≐ P≐Q P? = does-≡ (map P≐Q P?)

    ------------------------------------------------------------------------
    -- Irrelevant properties

    U-irrelevant : Irrelevant {A = A} U
    U-irrelevant a b = refl

    ∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
    ∁-irrelevant P a b = refl