------------------------------------------------------------------------
-- The Agda standard library
--
-- Predicate transformers
------------------------------------------------------------------------

{-# 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

------------------------------------------------------------------------
-- Heterogeneous and homogeneous predicate transformers

PT : Set a  Set b  (ℓ₁ ℓ₂ : Level)  Set _
PT A B ℓ₁ ℓ₂ = Pred A ℓ₁  Pred B ℓ₂

Pt : Set a  ( : Level)  Set _
Pt A  = PT A A  

------------------------------------------------------------------------
-- Composition and identity

infixr 9 _⍮_

_⍮_ : PT B C ℓ₂ ℓ₃  PT A B ℓ₁ ℓ₂  PT A C ℓ₁ _
S  T = S  T

skip : PT A A  
skip P = P

------------------------------------------------------------------------
-- Operations on predicates extend pointwise to predicate transformers

-- The bottom and the top of the predicate transformer lattice.

abort : PT A B 0ℓ 0ℓ
abort = λ _  

magic : PT A B 0ℓ 0ℓ
magic = λ _  U

-- Negation.

infix 8 ∼_

∼_ : PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂
 T =   T

-- Refinement.

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

-- The dual of refinement.

infix 4 _⋢_

_⋢_ : PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂  Set _
S  T =  λ X  S X  T X

-- Union.

infixl 6 _⊓_

_⊓_ : PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂
S  T = λ X  S X  T X

-- Intersection.

infixl 7 _⊔_

_⊔_ : PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂
S  T = λ X  S X  T X

-- Implication.

infixl 8 _⇛_

_⇛_ : PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂  PT A B ℓ₁ ℓ₂
S  T = λ X  S X  T X

-- Infinitary union and intersection.

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

-- Angelic and demonic update.

⟨_⟩ : REL A B   PT B A  _
 R  P = λ x  R x  P

[_] : REL A B   PT B A  _
[ R ] P = λ x  R x  P