--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/RelOp.agda.replaced	Mon Mar 09 11:25:49 2020 +0900
@@ -0,0 +1,81 @@
+{-@$\#$@ 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)))