{-# 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 as Dec using (yes; no; _⊎-dec_; _×-dec_; ¬?; map′; does)
open import Function.Base using (id; _$_; _∘_)
private
variable
a b ℓ ℓ₁ ℓ₂ ℓ₃ : Level
A : Set a
B : Set b
∅? : Decidable {A = A} ∅
∅? _ = no λ()
∅-Empty : Empty {A = A} ∅
∅-Empty x ()
∁∅-Universal : Universal {A = A} (∁ ∅)
∁∅-Universal = λ x x∈∅ → x∈∅
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 _
∅-⊆ : (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 ⊆′⇒⊆ (_∘ ⊆⇒⊆′)
≐-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 ⊆′⇒⊆ ⊆′⇒⊆
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?)
U-irrelevant : Irrelevant {A = A} U
U-irrelevant a b = refl
∁-irrelevant : (P : Pred A ℓ) → Irrelevant (∁ P)
∁-irrelevant P a b = refl