diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,5 @@
+# Revision history for properties
+
+## 0.0.1  -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019, Chris McKinlay
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Chris McKinlay nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/lawz.cabal b/lawz.cabal
new file mode 100644
--- /dev/null
+++ b/lawz.cabal
@@ -0,0 +1,46 @@
+name:                lawz
+version:             0.0.1
+synopsis:            Common mathematical laws.
+description:         Library of predicates for property testing.
+homepage:            https://github.com/cmk/lawz
+license:             BSD3
+license-file:        LICENSE
+author:              Chris McKinlay
+maintainer:          chris.mckinlay@gmail.com
+category:            Testing, Math
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+
+library
+  exposed-modules:
+     Test.Relation
+     Test.Relation.Connex
+     Test.Relation.Reflexive
+     Test.Relation.Symmetric
+     Test.Relation.Transitive
+     Test.Function
+     Test.Function.Equivalent
+     Test.Function.Idempotent
+     Test.Function.Injective
+     Test.Function.Invertible
+     Test.Function.Monotone
+     Test.Operation
+     Test.Operation.Annihilative
+     Test.Operation.Associative
+     Test.Operation.Commutative
+     Test.Operation.Distributive
+     Test.Operation.Neutral
+     Test.Util
+
+  default-extensions:
+     FlexibleInstances
+     RankNTypes
+     ScopedTypeVariables
+     TypeApplications
+
+  build-depends:       
+      base <5.0
+
+  hs-source-dirs:      src
+  default-language:    Haskell2010
diff --git a/src/Test/Function.hs b/src/Test/Function.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function.hs
@@ -0,0 +1,7 @@
+module Test.Function (module Export) where
+
+import Test.Function.Equivalent as Export
+import Test.Function.Idempotent as Export
+import Test.Function.Injective  as Export
+import Test.Function.Invertible as Export
+import Test.Function.Monotone   as Export
diff --git a/src/Test/Function/Equivalent.hs b/src/Test/Function/Equivalent.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function/Equivalent.hs
@@ -0,0 +1,16 @@
+module Test.Function.Equivalent where
+
+import Test.Util
+
+
+
+-- | \( \forall a: f a \equiv g a \)
+--
+equivalent :: Eq r => (r -> r) -> (r -> r) -> (r -> Bool)
+equivalent = equivalent_on (==)
+
+
+-- | \( \forall a: f a \doteq g a \)
+--
+equivalent_on :: Rel r -> (r -> r) -> (r -> r) -> (r -> Bool)
+equivalent_on (~~) f g a = f a ~~ g a
diff --git a/src/Test/Function/Idempotent.hs b/src/Test/Function/Idempotent.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function/Idempotent.hs
@@ -0,0 +1,29 @@
+module Test.Function.Idempotent where
+
+import Data.List (unfoldr)
+import Numeric.Natural (Natural(..))
+import Test.Util
+
+-- | \( \forall a: g \circ f (a) = f (a) \)
+--
+projective :: Eq r => (r -> r) -> (r -> r) -> r -> Bool
+projective = projective_on (==)
+
+-- | \( \forall a: g \circ f (a) \sim f (a) \)
+--
+projective_on :: Rel s -> (r -> s) -> (s -> s) -> r -> Bool
+projective_on (~~) f g r = g (f r) ~~ f r
+
+-- | \( \forall a: f \circ f(a) = f(a) \)
+--
+idempotent :: Eq r => (r -> r) -> r -> Bool
+idempotent f = idempotent_on (==) f
+
+-- | \( \forall a: f \circ f(a) \sim f(a) \)
+--
+idempotent_on :: Rel r -> (r -> r) -> r -> Bool
+idempotent_on (~~) f = projective_on (~~) f f
+
+idempotent_k :: Eq r => Natural -> (r -> r) -> r -> Bool
+idempotent_k k f r = k >= 1 ==> foldr (.) id fs r == f r
+  where fs = (`unfoldr` k) $ \m -> if m==1 then Nothing else Just (f,m-1)
diff --git a/src/Test/Function/Injective.hs b/src/Test/Function/Injective.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function/Injective.hs
@@ -0,0 +1,14 @@
+module Test.Function.Injective where
+
+import Test.Util
+
+-- | \( \forall a: f a \equiv f b \Rightarrow a \equiv b \)
+--
+injective :: Eq r => (r -> r) -> r -> r -> Bool
+injective = injective_on (==)
+
+
+-- | \( \forall a: f a \doteq f b \Rightarrow a \doteq b \)
+--
+injective_on :: Rel r -> (r -> r) -> r -> r -> Bool
+injective_on (~~) f a b = (f a ~~ f b) ==> (a ~~ b)
diff --git a/src/Test/Function/Invertible.hs b/src/Test/Function/Invertible.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function/Invertible.hs
@@ -0,0 +1,21 @@
+module Test.Function.Invertible where
+
+import Test.Util
+
+
+-- | \( \forall a: f a \# b \Leftrightarrow a \# g b \)
+--
+-- For example, a Galois connection is defined by @adjoint_on (<=)@.
+--
+adjoint_on :: Rel r -> Rel s -> (s -> r) -> (r -> s) -> (s -> r -> Bool)
+adjoint_on (#) (%) f g a b = f a # b <==> a % g b
+
+-- | \( \forall a: f (g a) \equiv a \)
+--
+invertible :: Eq r => (r -> s) -> (s -> r) -> (r -> Bool)
+invertible = invertible_on (==)
+
+-- | \( \forall a: f (g a) \doteq a \)
+--
+invertible_on :: Rel s -> (s -> r) -> (r -> s) -> (s -> Bool)
+invertible_on (~~) f g a = g (f a) ~~ a
diff --git a/src/Test/Function/Monotone.hs b/src/Test/Function/Monotone.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Function/Monotone.hs
@@ -0,0 +1,20 @@
+module Test.Function.Monotone where
+
+import Test.Util
+
+monotone :: Ord r => (r -> r) -> r -> r -> Bool
+monotone = monotone_on (<=) (<=)
+
+-- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \)
+--
+monotone_on :: Rel r -> Rel s -> (r -> s) -> r -> r -> Bool
+monotone_on (#) (%) f a b = a # b ==> f a % f b
+
+antitone :: Ord r => (r -> r) -> r -> r -> Bool
+antitone = antitone_on (<=) (<=)
+
+-- | \( \forall a, b: a \leq b \Rightarrow f(b) \leq f(a) \)
+--
+antitone_on :: Rel r -> Rel s -> (r -> s) -> r -> r -> Bool
+antitone_on (#) (%) f a b = a # b ==> f b % f a
+
diff --git a/src/Test/Operation.hs b/src/Test/Operation.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation.hs
@@ -0,0 +1,7 @@
+module Test.Operation (module Export) where
+
+import Test.Operation.Annihilative as Export
+import Test.Operation.Associative  as Export
+import Test.Operation.Commutative  as Export
+import Test.Operation.Distributive as Export
+import Test.Operation.Neutral      as Export
diff --git a/src/Test/Operation/Annihilative.hs b/src/Test/Operation/Annihilative.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation/Annihilative.hs
@@ -0,0 +1,28 @@
+module Test.Operation.Annihilative where
+
+import Test.Util
+
+
+-- | \( \forall a: (u \# a) \equiv u \)
+--
+-- Right annihilativity of an element /u/ with respect to an operator /#/.
+--
+-- For example, @False@ is a right annihilative element of @||@.
+--
+annihilative :: Eq r => (r -> r -> r) -> r -> (r -> Bool)
+annihilative = annihilative_on (==)
+
+-- | \( \forall a: (a \# u) \equiv u \)
+--
+-- Left annihilativity of an element /u/ with respect to an operator /#/.
+--
+-- For example, @Nothing@ is a right annihilative element of @*>@.
+--
+annihilative' :: Eq r => (r -> r -> r) -> r -> (r -> Bool)
+annihilative' = annihilative_on' (==)
+
+annihilative_on :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)
+annihilative_on (~~) (#) u a = (u # a) ~~ u
+
+annihilative_on' :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)
+annihilative_on' (~~) (#) u a = (a # u) ~~ u
diff --git a/src/Test/Operation/Associative.hs b/src/Test/Operation/Associative.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation/Associative.hs
@@ -0,0 +1,15 @@
+module Test.Operation.Associative where
+
+import Test.Util
+
+
+-- | \( \forall a, b, c: (a \# b) \# c \equiv a \# (b \# c) \)
+--
+associative :: Eq r => (r -> r -> r) -> (r -> r -> r -> Bool)
+associative = associative_on (==)
+
+
+-- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \)
+--
+associative_on :: Rel r -> (r -> r -> r) -> (r -> r -> r -> Bool)
+associative_on (~~) (#) a b c = ((a # b) # c) ~~ (a # (b # c)) 
diff --git a/src/Test/Operation/Commutative.hs b/src/Test/Operation/Commutative.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation/Commutative.hs
@@ -0,0 +1,14 @@
+module Test.Operation.Commutative where
+
+import Test.Util
+
+-- | \( \forall a, b: a \# b \equiv b \# a \)
+--
+commutative :: Eq r => (r -> r -> r) -> r -> r -> Bool
+commutative = commutative_on (==)
+
+-- | \( \forall a, b: a \# b \doteq b \# a \)
+--
+commutative_on :: Rel r -> (r -> r -> r) -> r -> r -> Bool
+commutative_on (~~) (#) a b = (a # b) ~~ (b # a)
+
diff --git a/src/Test/Operation/Distributive.hs b/src/Test/Operation/Distributive.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation/Distributive.hs
@@ -0,0 +1,20 @@
+module Test.Operation.Distributive where
+
+import Test.Util
+
+
+-- | \( \forall a, b, c: (a \# b) \% c \equiv (a \% c) \# (b \% c) \)
+--
+distributive :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
+distributive = distributive_on (==)
+
+-- | \( \forall a, b, c: c \% (a \# b) \equiv (c \% a) \# (c \% b) \)
+--
+distributive' :: Eq r => (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
+distributive' = distributive_on' (==)
+
+distributive_on :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
+distributive_on (~~) (#) (%) a b c = ((a # b) % c) ~~ ((a % c) # (b % c))
+
+distributive_on' :: Rel r -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> Bool)
+distributive_on' (~~) (#) (%) a b c = (c % (a # b)) ~~ ((c % a) # (c % b))
diff --git a/src/Test/Operation/Neutral.hs b/src/Test/Operation/Neutral.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Operation/Neutral.hs
@@ -0,0 +1,27 @@
+module Test.Operation.Neutral where
+
+import Test.Util
+
+-- | \( \forall a: (u \# a) \equiv a \)
+--
+-- Right neutrality of a unit /u/ with respect to an operator /#/.
+--
+-- For example, an implementation of 'Monoid' must satisfy @neutral (<>) mempty@
+--
+neutral :: Eq r => (r -> r -> r) -> r -> (r -> Bool)
+neutral = neutral_on (==)
+
+-- | \( \forall a: (a \# u) \equiv a \)
+--
+-- Left neutrality of a unit /u/ with respect to an operator /#/.
+--
+-- For example, an implementation of 'Monoid' must satisfy @neutral (<>) mempty@
+--
+neutral' :: Eq r => (r -> r -> r) -> r -> (r -> Bool)
+neutral' = neutral_on' (==)
+
+neutral_on :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)
+neutral_on (~~) (#) u a = (u # a) ~~ a
+
+neutral_on' :: Rel r -> (r -> r -> r) -> r -> (r -> Bool)
+neutral_on' (~~) (#) u a = (a # u) ~~ a
diff --git a/src/Test/Relation.hs b/src/Test/Relation.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Relation.hs
@@ -0,0 +1,6 @@
+module Test.Relation (module Export) where
+
+import Test.Relation.Connex     as Export
+import Test.Relation.Reflexive  as Export
+import Test.Relation.Symmetric  as Export
+import Test.Relation.Transitive as Export
diff --git a/src/Test/Relation/Connex.hs b/src/Test/Relation/Connex.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Relation/Connex.hs
@@ -0,0 +1,47 @@
+-- | See <https://en.wikipedia.org/wiki/Connex_relation>.
+module Test.Relation.Connex where
+
+import Test.Util
+
+-- | \( \forall a, b: ((a \# b) \vee (b \# a)) \)
+--
+-- For example, ≥ is a connex relation, while 'divides evenly' is not.
+-- 
+-- A connex relation cannot be symmetric, except for the universal relation.
+--
+connex :: (r -> r -> Bool) -> r -> r -> Bool
+connex (#) a b = (a # b) || (b # a)
+
+
+-- | \( \forall a, b: \neg (a \equiv b) \Rightarrow ((a \# b) \vee (b \# a)) \)
+--
+-- A binary relation is semiconnex if it relates all pairs of _distinct_ elements in some way.
+--
+-- A relation is connex if and only if it is semiconnex and reflexive.
+--
+semiconnex :: Eq r => (r -> r -> Bool) -> r -> r -> Bool
+semiconnex = semiconnex_on (==)
+
+
+-- | \( \forall a, b: \neg (a \doteq b) \Rightarrow ((a \# b) \vee (b \# a)) \)
+--
+semiconnex_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
+semiconnex_on (~~) (#) a b = not (a ~~ b) ==> connex (#) a b
+
+
+-- | \( \forall a, b, c: ((a \# b) \vee (a \equiv b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \equiv b) \wedge (b \# a)) \)
+--
+-- Note that @ trichotomous (>) @ should hold for any 'Ord' instance.
+--
+trichotomous :: Eq r => (r -> r -> Bool) -> r -> r -> Bool
+trichotomous = trichotomous_on (==)
+
+
+-- | \( \forall a, b, c: ((a \# b) \vee (a \doteq b) \vee (b \# a)) \wedge \neg ((a \# b) \wedge (a \doteq b) \wedge (b \# a)) \)
+--
+-- In other words, exactly one of \(a \# b\), \(a \doteq b\), or \(b \# a\) holds.
+-- 	
+-- For example, > is a trichotomous relation, while ≥ is not.
+--
+trichotomous_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
+trichotomous_on (~~) (#) a b = xor3 (a # b) (a ~~ b) (b # a)
diff --git a/src/Test/Relation/Reflexive.hs b/src/Test/Relation/Reflexive.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Relation/Reflexive.hs
@@ -0,0 +1,51 @@
+-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.
+-- 
+-- Note that these properties do not exhaust all of the possibilities.
+--
+-- For example, the relation \( y = x^2 \) is neither irreflexive, 
+-- nor coreflexive, nor reflexive, since it contains the pairs
+-- \( (0, 0) \) and \( (2, 4) \), but not \( (2, 2) \).
+--
+--  The latter two facts also rule out quasi-reflexivity.
+module Test.Relation.Reflexive where
+
+import Test.Util
+
+
+-- | \( \forall a: (a \# a) \)
+--
+-- For example, ≥ is a reflexive relation but > is not.
+--
+reflexive :: (r -> r -> Bool) -> (r ->  Bool)
+reflexive (#) a = a # a 
+
+
+-- | \( \forall a: \neg (a \# a) \)
+--
+-- For example, > is an irreflexive relation, but ≥ is not.
+--
+irreflexive :: (r -> r -> Bool) -> (r ->  Bool)
+irreflexive (#) a = not $ a # a
+
+
+-- | \( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \equiv b) \)
+--
+-- For example, the relation over the integers in which each odd number is 
+-- related to itself is a coreflexive relation. The equality relation is the 
+-- only example of a relation that is both reflexive and coreflexive, and any 
+-- coreflexive relation is a subset of the equality relation.
+--
+coreflexive :: Eq r => (r -> r -> Bool) -> (r -> r -> Bool)
+coreflexive = coreflexive_on (==)
+
+
+-- | \( \forall a, b: ((a \# b) \wedge (b \# a)) \Rightarrow (a \doteq b) \)
+--
+coreflexive_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> (r -> r -> Bool)
+coreflexive_on (~~) (#) a b = (a # b) && (b # a) ==> (a ~~ b)
+
+
+-- | \( \forall a, b: (a \# b) \Rightarrow ((a \# a) \wedge (b \# b)) \)
+--
+quasireflexive :: (r -> r -> Bool) -> (r -> r -> Bool)
+quasireflexive (#) a b = (a # b) ==> (a # a) && (b # b)
diff --git a/src/Test/Relation/Symmetric.hs b/src/Test/Relation/Symmetric.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Relation/Symmetric.hs
@@ -0,0 +1,43 @@
+-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.
+--
+-- Note that these properties do not exhaust all of the possibilities.
+--
+-- As an example over the natural numbers, the relation \(a \# b \) defined by 
+-- \( a > 2 \) is neither symmetric nor antisymmetric, let alone asymmetric.
+module Test.Relation.Symmetric where
+
+import Test.Util
+
+
+-- | \( \forall a, b: (a \# b) \Leftrightarrow (b \# a) \)
+--
+-- For example, "is a blood relative of" is a symmetric relation, because 
+-- A is a blood relative of B if and only if B is a blood relative of A.
+--
+symmetric :: (r -> r -> Bool) -> r -> r -> Bool
+symmetric (#) a b = (a # b) <==> (b # a)
+
+
+-- | \( \forall a, b: (a \# b) \Rightarrow \neg (b \# a) \)
+--
+-- For example, > is an asymmetric relation, but ≥ is not.
+--
+-- A relation is asymmetric if and only if it is both antisymmetric and irreflexive.
+-- 
+asymmetric :: (r -> r -> Bool) -> r -> r -> Bool
+asymmetric (#) a b = (a # b) ==> not (b # a)
+
+
+-- | \( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \equiv b \)
+--
+-- For example, ≥ is an antisymmetric relation; so is >, but vacuously 
+-- (the condition in the definition is always false).
+-- 
+antisymmetric :: Eq r => (r -> r -> Bool) -> r -> r -> Bool
+antisymmetric = antisymmetric_on (==)
+
+
+-- | \( \forall a, b: (a \# b) \wedge (b \# a) \Rightarrow a \doteq b \)
+-- 
+antisymmetric_on :: (r -> r -> Bool) -> (r -> r -> Bool) -> r -> r -> Bool
+antisymmetric_on (~~) (#) a b = (a # b) && (b # a) ==> (a ~~ b)
diff --git a/src/Test/Relation/Transitive.hs b/src/Test/Relation/Transitive.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Relation/Transitive.hs
@@ -0,0 +1,27 @@
+module Test.Relation.Transitive where
+
+import Test.Util
+
+
+-- | \( \forall a, b, c: ((a \# b) \wedge (b \# c)) \Rightarrow (a \# c) \)
+--
+-- For example, "is ancestor of" is a transitive relation, while "is parent of" is not.
+--
+transitive :: (r -> r -> Bool) -> r -> r -> r -> Bool
+transitive (#) a b c = (a # b) && (b # c) ==> a # c
+
+
+-- | \( \forall a, b, c: ((a \# b) \wedge (a \# c)) \Rightarrow (b \# c) \)
+--
+-- For example, /=/ is an right Euclidean relation because if /x = y/ and /x = z/ then /y = z/.
+--
+euclidean :: (r -> r -> Bool) -> r -> r -> r -> Bool
+euclidean (#) a b c = (a # b) && (a # c) ==> b # c
+
+
+-- |  \( \forall a, b, c: ((b \# a) \wedge (c \# a)) \Rightarrow (b \# c) \)
+--
+-- For example, /=/ is a left Euclidean relation because if /x = y/ and /x = z/ then /y = z/.
+--
+euclidean' :: (r -> r -> Bool) -> r -> r -> r -> Bool
+euclidean' (#) a b c = (b # a) && (c # a) ==> b # c
diff --git a/src/Test/Util.hs b/src/Test/Util.hs
new file mode 100644
--- /dev/null
+++ b/src/Test/Util.hs
@@ -0,0 +1,22 @@
+module Test.Util where
+
+type Rel r = r -> r -> Bool
+
+xor :: Bool -> Bool -> Bool
+xor a b = (a || b) && not (a && b)
+
+xor3 :: Bool -> Bool -> Bool -> Bool
+xor3 a b c = (a `xor` (b `xor` c)) && not (a && b && c)
+
+infixr 0 ==>
+
+(==>) :: Bool -> Bool -> Bool
+(==>) a b = not a || b
+
+iff :: Bool -> Bool -> Bool
+iff a b = a ==> b && b ==> a
+
+infixr 1 <==>
+
+(<==>) :: Bool -> Bool -> Bool
+(<==>) = iff