{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Unary.PredicateTransformer where
open import Data.Product.Base using (∃)
open import Function.Base using (_∘_)
open import Level hiding (_⊔_)
open import Relation.Nullary
open import Relation.Unary
open import Relation.Binary.Core using (REL)
private
variable
a b c i ℓ ℓ₁ ℓ₂ ℓ₃ : Level
A : Set a
B : Set b
C : Set c
PT : Set a → Set b → (ℓ₁ ℓ₂ : Level) → Set _
PT A B ℓ₁ ℓ₂ = Pred A ℓ₁ → Pred B ℓ₂
Pt : Set a → (ℓ : Level) → Set _
Pt A ℓ = PT A A ℓ ℓ
infixr 9 _⍮_
_⍮_ : PT B C ℓ₂ ℓ₃ → PT A B ℓ₁ ℓ₂ → PT A C ℓ₁ _
S ⍮ T = S ∘ T
skip : PT A A ℓ ℓ
skip P = P
abort : PT A B 0ℓ 0ℓ
abort = λ _ → ∅
magic : PT A B 0ℓ 0ℓ
magic = λ _ → U
infix 8 ∼_
∼_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
∼ T = ∁ ∘ T
infix 4 _⊑_ _⊒_ _⊑′_ _⊒′_
_⊑_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⊑ T = ∀ {X} → S X ⊆ T X
_⊑′_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⊑′ T = ∀ X → S X ⊆ T X
_⊒_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
T ⊒ S = T ⊑ S
_⊒′_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
T ⊒′ S = S ⊑′ T
infix 4 _⋢_
_⋢_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → Set _
S ⋢ T = ∃ λ X → S X ≬ T X
infixl 6 _⊓_
_⊓_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⊓ T = λ X → S X ∪ T X
infixl 7 _⊔_
_⊔_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⊔ T = λ X → S X ∩ T X
infixl 8 _⇛_
_⇛_ : PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂ → PT A B ℓ₁ ℓ₂
S ⇛ T = λ X → S X ⇒ T X
infix 9 ⨆ ⨅
⨆ : ∀ (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
⨆ I T = λ X → ⋃[ i ∶ I ] T i X
syntax ⨆ I (λ i → T) = ⨆[ i ∶ I ] T
⨅ : ∀ (I : Set i) → (I → PT A B ℓ₁ ℓ₂) → PT A B ℓ₁ _
⨅ I T = λ X → ⋂[ i ∶ I ] T i X
syntax ⨅ I (λ i → T) = ⨅[ i ∶ I ] T
⟨_⟩ : REL A B ℓ → PT B A ℓ _
⟨ R ⟩ P = λ x → R x ≬ P
[_] : REL A B ℓ → PT B A ℓ _
[ R ] P = λ x → R x ⊆ P