{-@$\#$@ OPTIONS --universe-polymorphism @$\#$@-}

open import Level
open import Data.Empty
open import Data.Product
open import Data.Nat.Base
open import Data.Sum
open import Data.Unit
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary
open import utilities

module RelOp (S : Set) where

data Id {l} {X : Set} : Rel X l where
  ref : {x : X} @$\rightarrow$@ Id x x

-- substId1 | x == y & P(x) => P(y)
substId1 :  @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@
           Id {l} x y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P x @$\rightarrow$@ P y
substId1 ref P q = q

-- substId2 | x == y & P(y) => P(x)
substId2 :  @$\forall$@ {l} @$\rightarrow$@ {X : Set} @$\rightarrow$@ {x y : X} @$\rightarrow$@
           Id {l} x  y @$\rightarrow$@ (P : Pred X) @$\rightarrow$@ P y @$\rightarrow$@ P x
substId2 ref P q = q

-- for X ⊆ S (formally, X : Pred S)
-- delta X = { (a, a) | a ∈ X }
delta : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l
delta X a b = X a @$\times$@ Id a b 

-- deltaGlob = delta S
deltaGlob : @$\forall$@ {l} @$\rightarrow$@ Rel S l
deltaGlob = delta (@$\lambda$@ (s : S) @$\rightarrow$@ @$\top$@)

-- emptyRel = \varnothing
emptyRel : Rel S Level.zero
emptyRel a b = @$\bot$@

-- comp R1 R2 = R2 ∘ R1 (= R1; R2)
comp : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
comp R1 R2 a b = ∃ (@$\lambda$@ (a' : S) @$\rightarrow$@ R1 a a' @$\times$@ R2 a' b)

-- union R1 R2 = R1 ∪ R2
union : @$\forall$@ {l} @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
union R1 R2 a b = R1 a b ⊎ R2 a b

-- repeat n R = R^n
repeat : @$\forall$@ {l} @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
repeat @$\mathbb{N}$@.zero R = deltaGlob
repeat (@$\mathbb{N}$@.suc m) R = comp (repeat m R) R

-- unionInf f = ⋃_{n ∈ ω} f(n)
unionInf : @$\forall$@ {l} @$\rightarrow$@ (@$\mathbb{N}$@ @$\rightarrow$@ Rel S l) @$\rightarrow$@ Rel S l
unionInf f a b = ∃ (@$\lambda$@ (n : @$\mathbb{N}$@) @$\rightarrow$@ f n a b)
-- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
restPre : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
restPre X R a b = X a @$\times$@ R a b

-- restPost X R = { (s1,s2) ∈ R | s2 ∈ X }
restPost : @$\forall$@ {l} @$\rightarrow$@ Pred S @$\rightarrow$@ Rel S l @$\rightarrow$@ Rel S l
restPost X R a b = R a b @$\times$@ X b

deltaRestPre : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@
               Iff (restPre X R a b) (comp (delta X) R a b)
deltaRestPre X R a b
  = (@$\lambda$@ (h : restPre X R a b) @$\rightarrow$@ a , (proj@$\_{1}$@ h , ref) , proj@$\_{2}$@ h) ,
     @$\lambda$@ (h : comp (delta X) R a b) @$\rightarrow$@ proj@$\_{1}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h)) ,
       substId2
         (proj@$\_{2}$@ (proj@$\_{1}$@ (proj@$\_{2}$@ h)))
         (@$\lambda$@ z @$\rightarrow$@ R z b) (proj@$\_{2}$@ (proj@$\_{2}$@ h))

deltaRestPost : (X : Pred S) @$\rightarrow$@ (R : Rel S Level.zero) @$\rightarrow$@ (a b : S) @$\rightarrow$@
                Iff (restPost X R a b) (comp R (delta X) a b)
deltaRestPost X R a b
  = (@$\lambda$@ (h : restPost X R a b) @$\rightarrow$@ b , proj@$\_{1}$@ h , proj@$\_{2}$@ h , ref) ,
     @$\lambda$@ (h : comp R (delta X) a b) @$\rightarrow$@
       substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) (R a) (proj@$\_{1}$@ (proj@$\_{2}$@ h)) ,
       substId1 (proj@$\_{2}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h))) X (proj@$\_{1}$@ (proj@$\_{2}$@ (proj@$\_{2}$@ h)))