diff RelOp.agda @ 21:5e4abc1919b4

fix module relation
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 24 Dec 2018 22:50:25 +0900 (2018-12-24)
parents 5001cda86c3d
children bfe7d83cf9ba
line wrap: on
line diff
--- a/RelOp.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/RelOp.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -9,22 +9,10 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 open import Relation.Nullary
-
+open import utilities
 
 module RelOp (S : Set) where
 
-Pred : Set -> Set₁
-Pred X = X -> Set
-
-Imply : Set -> Set -> Set
-Imply X Y = X -> Y
-
-Iff : Set -> Set -> Set
-Iff X Y = Imply X Y × Imply Y X
-
-NotP : {S : Set} -> Pred S -> Pred S
-NotP X s = ¬ X s
-
 data Id {l} {X : Set} : Rel X l where
   ref : {x : X} -> Id x x