------------------------------------------------------------------------
-- 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 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.Unary
open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?)
open import Function.Base using (id; _$_; _∘_)
 
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 ⊆′⇒⊆ ⊆′⇒⊆
 
------------------------------------------------------------------------
-- Decidability properties
 
∁? : {P : Pred A ℓ} → Decidable P → Decidable (∁ P)
∁? P? x = ¬? (P? x)
 
infix  _×?_ _⊙?_
infix  _~?
infixr  _⊎?_
infixr  _∩?_
infixr  _∪?_
 
_∪?_ : {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
 
------------------------------------------------------------------------
-- Irrelevant properties
 
U-irrelevant : Irrelevant {A = A} U
U-irrelevant a b = refl
 
∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
∁-irrelevant P a b = refl