--- a/utilities.agda	Mon Dec 24 17:53:22 2018 +0900
+++ b/utilities.agda	Mon Dec 24 22:50:25 2018 +0900
@@ -2,11 +2,20 @@
 
 open import Function
 open import Data.Nat
+open import Data.Product
 open import Data.Bool hiding ( _≟_ )
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
 
+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
 
 record _/\_ {n : Level } (a : Set n) (b : Set n): Set n where
   field