{-# OPTIONS --without-K --safe #-}
module Relation.Unary where
open import Data.Empty
open import Data.Unit.Base using (⊤)
open import Data.Product
open import Data.Sum.Base using (_⊎_; [_,_])
open import Function.Base
open import Level
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable.Core using (True)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
private
variable
a b c ℓ ℓ₁ ℓ₂ : Level
A : Set a
B : Set b
C : Set c
Pred : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
Pred A ℓ = A → Set ℓ
∅ : Pred A 0ℓ
∅ = λ _ → ⊥
｛_｝ : A → Pred A _
｛ x ｝ = x ≡_
U : Pred A 0ℓ
U = λ _ → ⊤
infix 4 _∈_ _∉_
_∈_ : A → Pred A ℓ → Set _
x ∈ P = P x
_∉_ : A → Pred A ℓ → Set _
x ∉ P = ¬ x ∈ P
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)
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)
infix 10 Satisfiable Universal IUniversal
Empty : Pred A ℓ → Set _
Empty P = ∀ x → x ∉ P
Satisfiable : Pred A ℓ → Set _
Satisfiable P = ∃ λ x → x ∈ P
syntax Satisfiable P = ∃⟨ P ⟩
Universal : Pred A ℓ → Set _
Universal P = ∀ x → x ∈ P
syntax Universal P = Π[ P ]
IUniversal : Pred A ℓ → Set _
IUniversal P = ∀ {x} → x ∈ P
syntax IUniversal P = ∀[ P ]
Decidable : Pred A ℓ → Set _
Decidable P = ∀ x → Dec (P x)
⌊_⌋ : {P : Pred A ℓ} → Decidable P → Pred A ℓ
⌊ P? ⌋ a = Lift _ (True (P? a))
Irrelevant : Pred A ℓ → Set _
Irrelevant P = ∀ {x} (a : P x) (b : P x) → a ≡ b
Recomputable : Pred A ℓ → Set _
Recomputable P = ∀ {x} → .(P x) → P x
infix 10 ⋃ ⋂
infixr 9 _⊢_
infixr 8 _⇒_
infixr 7 _∩_
infixr 6 _∪_
infix 4 _≬_
∁ : Pred A ℓ → Pred A ℓ
∁ P = λ x → x ∉ P
_⇒_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ⇒ Q = λ x → x ∈ P → x ∈ Q
_∪_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∪ Q = λ x → x ∈ P ⊎ x ∈ Q
_∩_ : Pred A ℓ₁ → Pred A ℓ₂ → Pred A _
P ∩ Q = λ x → x ∈ P × x ∈ Q
⋃ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
⋃ I P = λ x → Σ[ i ∈ I ] P i x
syntax ⋃ I (λ i → P) = ⋃[ i ∶ I ] P
⋂ : ∀ {i} (I : Set i) → (I → Pred A ℓ) → Pred A _
⋂ I P = λ x → (i : I) → P i x
syntax ⋂ I (λ i → P) = ⋂[ i ∶ I ] P
_≬_ : Pred A ℓ₁ → Pred A ℓ₂ → Set _
P ≬ Q = ∃ λ x → x ∈ P × x ∈ Q
_⊢_ : (A → B) → Pred B ℓ → Pred A ℓ
f ⊢ P = λ x → P (f x)
infixr 2 _⟨×⟩_
infixr 2 _⟨⊙⟩_
infixr 1 _⟨⊎⟩_
infixr 0 _⟨→⟩_
infixl 9 _⟨·⟩_
infix 10 _~
infixr 9 _⟨∘⟩_
infixr 2 _//_ _\\_
_⟨×⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨×⟩ Q) (x , y) = x ∈ P × y ∈ Q
_⟨⊎⟩_ : Pred A ℓ → Pred B ℓ → Pred (A ⊎ B) _
P ⟨⊎⟩ Q = [ P , Q ]
_⟨⊙⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A × B) _
(P ⟨⊙⟩ Q) (x , y) = x ∈ P ⊎ y ∈ Q
_⟨→⟩_ : Pred A ℓ₁ → Pred B ℓ₂ → Pred (A → B) _
(P ⟨→⟩ Q) f = P ⊆ Q ∘ f
_⟨·⟩_ : (P : Pred A ℓ₁) (Q : Pred B ℓ₂) →
(P ⟨×⟩ (P ⟨→⟩ Q)) ⊆ Q ∘ uncurry (flip _$_)
(P ⟨·⟩ Q) (p , f) = f p
_~ : Pred (A × B) ℓ → Pred (B × A) ℓ
P ~ = P ∘ swap
_⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q
_//_ : Pred (A × C) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × B) _
(P // Q) (x , y) = Q ∘ (y ,_) ⊆ P ∘ (x ,_)
_\\_ : Pred (A × C) ℓ₁ → Pred (A × B) ℓ₂ → Pred (B × C) _
P \\ Q = (P ~ // Q ~) ~