diff --git a/Algebra/Lattice.hs b/Algebra/Lattice.hs
--- a/Algebra/Lattice.hs
+++ b/Algebra/Lattice.hs
@@ -1,6 +1,10 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE FlexibleInstances #-}
+#if __GLASGOW_HASKELL__ >=710 && MIN_VERSION_unordered_containers(0,2,6)
+{-# LANGUAGE Safe #-}
+#else
 {-# LANGUAGE Trustworthy #-}
+#endif
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 #if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709
@@ -41,17 +45,13 @@
     gfp, gfpFrom, unsafeGfp,
   ) where
 
+import Prelude ()
+import Prelude.Compat
+
 import qualified Algebra.PartialOrd as PO
 
 import           Data.Universe.Class (Universe(..), Finite(..))
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import           Control.Applicative (Applicative(..))
-import           Data.Foldable       (Foldable, foldMap)
-import           Data.Monoid         (Monoid(..))
-#endif
-
 import           Control.Monad.Zip (MonadZip(..))
 import           Data.Data         (Data, Typeable)
 import           Data.Hashable     (Hashable(..))
@@ -70,9 +70,8 @@
 import qualified Data.HashMap.Lazy as HM
 
 import Control.Applicative (Const(..))
-#if MIN_VERSION_base(4,8,0)
 import Data.Functor.Identity (Identity(..))
-#endif
+import Data.Semigroup.Foldable (Foldable1 (..))
 
 infixr 6 /\ -- This comment needed because of CPP
 infixr 5 \/
@@ -98,10 +97,6 @@
 joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool
 joinLeq x y = (x \/ y) == y
 
--- | The join of at a list of join-semilattice elements (of length at least one)
-joins1 :: JoinSemiLattice a => [a] -> a
-joins1 = foldr1 (\/)
-
 -- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>
 --
 -- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z
@@ -123,10 +118,8 @@
 meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool
 meetLeq x y = (x /\ y) == x
 
--- | The meet of at a list of meet-semilattice elements (of length at least one)
-meets1 :: MeetSemiLattice a => [a] -> a
-meets1 = foldr1 (/\)
 
+
 -- | The combination of two semi lattices makes a lattice if the absorption law holds:
 -- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)>
 --
@@ -143,6 +136,10 @@
 joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a
 joins = getJoin . foldMap Join
 
+-- | The join of at a list of join-semilattice elements (of length at least one)
+joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a
+joins1 =  getJoin . foldMap1 Join
+
 -- | A meet-semilattice with some element |top| that /\ approaches.
 --
 -- > Identity: x /\ top == x
@@ -152,7 +149,10 @@
 -- | The meet of a list of meet-semilattice elements
 meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a
 meets = getMeet . foldMap Meet
-
+--
+-- | The meet of at a list of meet-semilattice elements (of length at least one)
+meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a
+meets1 = getMeet . foldMap1 Meet
 
 -- | Lattices with both bounds
 class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where
@@ -189,6 +189,11 @@
 instance JoinSemiLattice IS.IntSet where
     (\/) = IS.union
 
+instance MeetSemiLattice IS.IntSet where
+    (/\) = IS.intersection
+
+instance Lattice IS.IntSet
+
 instance BoundedJoinSemiLattice IS.IntSet where
     bottom = IS.empty
 
@@ -202,6 +207,8 @@
 instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where
     (/\) = HS.intersection
 
+instance (Eq a, Hashable a) => Lattice (HS.HashSet a)
+
 instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where
     bottom = HS.empty
 
@@ -234,6 +241,12 @@
 
 instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where
     bottom = IM.empty
+
+instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where
+    (/\) = IM.intersectionWith (/\)
+
+instance Lattice v => Lattice (IM.IntMap v)
+
 
 --
 -- HashMaps
diff --git a/Algebra/Lattice/Divisibility.hs b/Algebra/Lattice/Divisibility.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice/Divisibility.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+#if __GLASGOW_HASKELL__ < 709
+{-# LANGUAGE Trustworthy #-}
+#else
+{-# LANGUAGE Safe #-}
+#endif
+----------------------------------------------------------------------------
+-- |
+-- Module      :  Algebra.Lattice.Divisibility
+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus
+-- License     :  BSD-3-Clause (see the file LICENSE)
+--
+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
+--
+----------------------------------------------------------------------------
+module Algebra.Lattice.Divisibility (
+    Divisibility(..)
+  ) where
+
+import Prelude ()
+import Prelude.Compat
+
+import Algebra.Lattice
+import Algebra.PartialOrd
+
+import Control.DeepSeq
+import Control.Monad
+import Data.Data
+import Data.Hashable
+import GHC.Generics
+
+--
+-- Divisibility
+--
+
+-- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. 
+newtype Divisibility a = Divisibility { getDivisibility :: a }
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
+#if __GLASGOW_HASKELL__ >= 706
+           , Generic1
+#endif
+           )
+
+instance Applicative Divisibility where
+  pure = return
+  (<*>) = ap
+
+instance Monad Divisibility where
+  return           = Divisibility
+  Divisibility x >>= f  = f x
+
+instance NFData a => NFData (Divisibility a) where
+  rnf (Divisibility a) = rnf a
+
+instance Hashable a => Hashable (Divisibility a)
+
+instance Integral a => JoinSemiLattice (Divisibility a) where
+  Divisibility x \/ Divisibility y = Divisibility (lcm x y)
+
+instance Integral a => MeetSemiLattice (Divisibility a) where
+  Divisibility x /\ Divisibility y = Divisibility (gcd x y)
+
+instance Integral a => Lattice (Divisibility a) where
+
+instance Integral a => BoundedJoinSemiLattice (Divisibility a) where
+  bottom = Divisibility 1
+
+instance (Eq a, Integral a) => PartialOrd (Divisibility a) where
+    leq (Divisibility a) (Divisibility b) = b `mod` a == 0
diff --git a/Algebra/Lattice/Dropped.hs b/Algebra/Lattice/Dropped.hs
--- a/Algebra/Lattice/Dropped.hs
+++ b/Algebra/Lattice/Dropped.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -23,20 +26,11 @@
   , retractDropped
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Monoid (Monoid(..))
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -51,23 +45,11 @@
 -- As a bonus, the top will be an absorbing element for the join.
 data Dropped a = Top
                | Drop a
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
-
-instance Functor Dropped where
-  fmap _ Top      = Top
-  fmap f (Drop a) = Drop (f a)
-
-instance Foldable Dropped where
-  foldMap _ Top      = mempty
-  foldMap f (Drop a) = f a
-
-instance Traversable Dropped where
-  traverse _ Top      = pure Top
-  traverse f (Drop a) = Drop <$> f a
 
 instance Applicative Dropped where
   pure = return
diff --git a/Algebra/Lattice/Free.hs b/Algebra/Lattice/Free.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice/Free.hs
@@ -0,0 +1,148 @@
+{-# LANGUAGE RankNTypes #-}
+
+----------------------------------------------------------------------------
+-- |
+-- Module      :  Algebra.Lattice.Free
+-- License     :  BSD-3-Clause (see the file LICENSE)
+--
+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
+--
+----------------------------------------------------------------------------
+
+module Algebra.Lattice.Free
+  ( -- * Free join-semilattices
+    FreeJoinSemiLattice
+  , liftFreeJoinSemiLattice
+  , lowerFreeJoinSemiLattice
+  , retractFreeJoinSemiLattice
+
+   -- * Free meet-semilattices
+  , FreeMeetSemiLattice
+  , liftFreeMeetSemiLattice
+  , lowerFreeMeetSemiLattice
+  , retractFreeMeetSemiLattice
+
+   -- * Free lattices
+  , FreeLattice
+  , liftFreeLattice
+  , lowerFreeLattice
+  , retractFreeLattice
+  ) where
+
+import Prelude ()
+import Prelude.Compat
+
+import Algebra.Lattice
+import Data.Universe.Class
+
+--
+-- Free join-semilattices
+--
+
+newtype FreeJoinSemiLattice a = FreeJoinSemiLattice
+  { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b =>
+                                            (a -> b) -> b
+  }
+
+liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a
+liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a)
+
+retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a
+retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id
+
+instance Functor FreeJoinSemiLattice where
+  fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f))
+  a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a)))
+
+instance JoinSemiLattice (FreeJoinSemiLattice a) where
+  FreeJoinSemiLattice f \/ FreeJoinSemiLattice g =
+    FreeJoinSemiLattice (\inj -> f inj \/ g inj)
+
+instance BoundedJoinSemiLattice a =>
+         BoundedJoinSemiLattice (FreeJoinSemiLattice a) where
+  bottom = FreeJoinSemiLattice (\inj -> inj bottom)
+
+instance Universe a => Universe (FreeJoinSemiLattice a) where
+  universe = fmap liftFreeJoinSemiLattice universe
+
+instance Finite a => Finite (FreeJoinSemiLattice a) where
+  universeF = fmap liftFreeJoinSemiLattice universeF
+
+
+--
+-- Free meet-semilattices
+--
+
+newtype FreeMeetSemiLattice a = FreeMeetSemiLattice
+  { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b =>
+                                            (a -> b) -> b
+  }
+
+instance Functor FreeMeetSemiLattice where
+  fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f))
+  a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a)))
+
+liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a
+liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a)
+
+retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a
+retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id
+
+instance MeetSemiLattice (FreeMeetSemiLattice a) where
+  FreeMeetSemiLattice f /\ FreeMeetSemiLattice g =
+    FreeMeetSemiLattice (\inj -> f inj /\ g inj)
+
+instance BoundedMeetSemiLattice a =>
+         BoundedMeetSemiLattice (FreeMeetSemiLattice a) where
+  top = FreeMeetSemiLattice (\inj -> inj top)
+
+instance Universe a => Universe (FreeMeetSemiLattice a) where
+  universe = fmap liftFreeMeetSemiLattice universe
+
+instance Finite a => Finite (FreeMeetSemiLattice a) where
+  universeF = fmap liftFreeMeetSemiLattice universeF
+
+
+--
+-- Free lattices
+--
+
+newtype FreeLattice a = FreeLattice
+  { lowerFreeLattice :: forall b. Lattice b =>
+                                    (a -> b) -> b
+  }
+
+instance Functor FreeLattice where
+  fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f))
+  a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a)))
+
+liftFreeLattice :: a -> FreeLattice a
+liftFreeLattice a = FreeLattice (\inj -> inj a)
+
+retractFreeLattice :: Lattice a => FreeLattice a -> a
+retractFreeLattice a = lowerFreeLattice a id
+
+instance JoinSemiLattice (FreeLattice a) where
+  FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj)
+
+instance MeetSemiLattice (FreeLattice a) where
+  FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj)
+
+instance Lattice (FreeLattice a)
+
+instance BoundedJoinSemiLattice a =>
+         BoundedJoinSemiLattice (FreeLattice a) where
+  bottom = FreeLattice (\inj -> inj bottom)
+
+instance BoundedMeetSemiLattice a =>
+         BoundedMeetSemiLattice (FreeLattice a) where
+  top = FreeLattice (\inj -> inj top)
+
+instance BoundedLattice a =>
+         BoundedLattice (FreeLattice a)
+
+instance Universe a => Universe (FreeLattice a) where
+  universe = fmap liftFreeLattice universe
+
+instance Finite a => Finite (FreeLattice a) where
+  universeF = fmap liftFreeLattice universeF
diff --git a/Algebra/Lattice/Levitated.hs b/Algebra/Lattice/Levitated.hs
--- a/Algebra/Lattice/Levitated.hs
+++ b/Algebra/Lattice/Levitated.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -23,20 +26,11 @@
   , retractLevitated
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Monoid (Monoid(..))
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -53,25 +47,11 @@
 data Levitated a = Top
                  | Levitate a
                  | Bottom
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
-instance Functor Levitated where
-  fmap _ Bottom       = Bottom
-  fmap _ Top          = Top
-  fmap f (Levitate a) = Levitate (f a)
-
-instance Foldable Levitated where
-  foldMap _ Bottom       = mempty
-  foldMap _ Top          = mempty
-  foldMap f (Levitate a) = f a
-
-instance Traversable Levitated where
-  traverse _ Bottom       = pure Bottom
-  traverse _ Top          = pure Top
-  traverse f (Levitate a) = Levitate <$> f a
 
 instance Applicative Levitated where
   pure = return
diff --git a/Algebra/Lattice/Lexicographic.hs b/Algebra/Lattice/Lexicographic.hs
--- a/Algebra/Lattice/Lexicographic.hs
+++ b/Algebra/Lattice/Lexicographic.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -22,20 +25,12 @@
     Lexicographic(..)
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 import Algebra.PartialOrd
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -60,21 +55,12 @@
 -- 'Timestamps'.  Typically this is done in an arbitary, but
 -- deterministic manner.
 data Lexicographic k v = Lexicographic !k !v
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
 
-instance Foldable (Lexicographic k) where
-  foldMap f (Lexicographic _ v) = f v
-
-instance Traversable (Lexicographic k) where
-  traverse f (Lexicographic k v) = Lexicographic k <$> f v
-
-instance Functor (Lexicographic k) where
-  fmap f (Lexicographic k v) = Lexicographic k (f v)
-
 instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where
   pure = return
   (<*>) = ap
@@ -91,19 +77,40 @@
 
 instance (Hashable k, Hashable v) => Hashable (Lexicographic k v)
 
-instance (PartialOrd k, JoinSemiLattice k, JoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where
+-- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause?
+--
+-- For example what is the join of @(2, 1)@ and @(3, 2)@
+-- in lexicographic divisibility divisibility lattice.
+--
+-- With @v1 \\/ v2@, we get the upper bound, but not least!
+--
+-- @
+-- (2, 1) `leq` (6, 2)
+-- (3, 2) `leq` (6, 2)
+-- @
+--
+-- But @(6, 1) `leq` (6, 2)@, and
+--
+-- @
+-- (2, 1) `leq` (6, 1)
+-- (3, 2) `leq` (6, 1)
+-- @
+--
+instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where
   l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2)
+    | k1 == k2 = Lexicographic k1 (v1 \/ v2)
     | k1 `leq` k2 = r
     | k2 `leq` k1 = l
-    | otherwise   = Lexicographic (k1 \/ k2) (v1 \/ v2)
+    | otherwise   = Lexicographic (k1 \/ k2) bottom
 
-instance (PartialOrd k, MeetSemiLattice k, MeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where
+instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where
   l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2)
+    | k1 == k2 = Lexicographic k1 (v1 /\ v2)
     | k1 `leq` k2 = l
     | k2 `leq` k1 = r
-    | otherwise   = Lexicographic (k1 /\ k2) (v1 /\ v2)
+    | otherwise   = Lexicographic (k1 /\ k2) top
 
-instance (PartialOrd k, Lattice k, Lattice v) => Lattice (Lexicographic k v) where
+instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where
 
 instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where
   bottom = Lexicographic bottom bottom
@@ -115,6 +122,9 @@
 
 instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where
   Lexicographic k1 v1 `leq` Lexicographic k2 v2
+    | k1   ==  k2 = v1 `leq` v2
     | k1 `leq` k2 = True
-    | k1   ==  k1 = v1 `leq` v2
     | otherwise   = False -- Incomparable or k2 `leq` k1
+  comparable (Lexicographic k1 v1) (Lexicographic k2 v2)
+    | k1 == k2 = comparable v1 v2
+    | otherwise = comparable k1 k2
diff --git a/Algebra/Lattice/Lifted.hs b/Algebra/Lattice/Lifted.hs
--- a/Algebra/Lattice/Lifted.hs
+++ b/Algebra/Lattice/Lifted.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 #if __GLASGOW_HASKELL__ < 709
@@ -22,20 +25,11 @@
   , retractLifted
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Monoid (Monoid(..))
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -50,23 +44,11 @@
 -- As a bonus, the bottom will be an absorbing element for the meet.
 data Lifted a = Lift a
               | Bottom
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
-
-instance Functor Lifted where
-  fmap _ Bottom   = Bottom
-  fmap f (Lift a) = Lift (f a)
-
-instance Foldable Lifted where
-  foldMap _ Bottom   = mempty
-  foldMap f (Lift a) = f a
-
-instance Traversable Lifted where
-  traverse _ Bottom   = pure Bottom
-  traverse f (Lift a) = Lift <$> f a
 
 instance Applicative Lifted where
   pure = return
diff --git a/Algebra/Lattice/Op.hs b/Algebra/Lattice/Op.hs
--- a/Algebra/Lattice/Op.hs
+++ b/Algebra/Lattice/Op.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -22,20 +25,12 @@
     Op(..)
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 import Algebra.PartialOrd
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -49,21 +44,12 @@
 -- | The opposite lattice of a given lattice.  That is, switch
 -- meets and joins.
 newtype Op a = Op { getOp :: a }
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
 
-instance Foldable Op where
-  foldMap f (Op a) = f a
-
-instance Traversable Op where
-  traverse f (Op a) = Op <$> f a
-
-instance Functor Op where
-  fmap f (Op a) = Op (f a)
-
 instance Applicative Op where
   pure = return
   (<*>) = ap
@@ -83,7 +69,7 @@
 instance JoinSemiLattice a => MeetSemiLattice (Op a) where
   Op x /\ Op y = Op (x \/ y)
 
-instance (Lattice a, Ord a) => Lattice (Op a) where
+instance Lattice a => Lattice (Op a) where
 
 instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where
   bottom = Op top
@@ -91,7 +77,8 @@
 instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where
   top = Op bottom
 
-instance (BoundedLattice a, Ord a, Bounded a) => BoundedLattice (Op a) where
+instance BoundedLattice a => BoundedLattice (Op a) where
 
 instance PartialOrd a => PartialOrd (Op a) where
     Op a `leq` Op b = b `leq` a -- Note swap.
+    comparable (Op a) (Op b) = comparable a b
diff --git a/Algebra/Lattice/Ordered.hs b/Algebra/Lattice/Ordered.hs
--- a/Algebra/Lattice/Ordered.hs
+++ b/Algebra/Lattice/Ordered.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE DeriveFoldable #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -22,20 +25,12 @@
     Ordered(..)
   ) where
 
-#ifndef MIN_VERSION_base
-#define MIN_VERSION_base(x,y,z) 1
-#endif
+import Prelude ()
+import Prelude.Compat
 
 import Algebra.Lattice
 import Algebra.PartialOrd
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Foldable
-import Data.Traversable
-#endif
-
 import Control.DeepSeq
 import Control.Monad
 import Data.Data
@@ -49,21 +44,12 @@
 -- | A total order gives rise to a lattice. Join is
 -- max, meet is min.
 newtype Ordered a = Ordered { getOrdered :: a }
-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic
+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable
 #if __GLASGOW_HASKELL__ >= 706
            , Generic1
 #endif
            )
 
-instance Foldable Ordered where
-  foldMap f (Ordered a) = f a
-
-instance Traversable Ordered where
-  traverse f (Ordered a) = Ordered <$> f a
-
-instance Functor Ordered where
-  fmap f (Ordered a) = Ordered (f a)
-
 instance Applicative Ordered where
   pure = return
   (<*>) = ap
@@ -83,7 +69,7 @@
 instance Ord a => MeetSemiLattice (Ordered a) where
   Ordered x /\ Ordered y = Ordered (min x y)
 
-instance (Lattice a, Ord a) => Lattice (Ordered a) where
+instance Ord a => Lattice (Ordered a) where
 
 instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where
   bottom = Ordered minBound
@@ -91,7 +77,8 @@
 instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where
   top = Ordered maxBound
 
-instance (BoundedLattice a, Ord a, Bounded a) => BoundedLattice (Ordered a) where
+instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where
 
 instance Ord a => PartialOrd (Ordered a) where
     leq = (<=)
+    comparable _ _ = True
diff --git a/Algebra/PartialOrd.hs b/Algebra/PartialOrd.hs
--- a/Algebra/PartialOrd.hs
+++ b/Algebra/PartialOrd.hs
@@ -18,37 +18,82 @@
     gfpFrom, unsafeGfpFrom
   ) where
 
-import qualified Data.Set as S
+import qualified Data.IntMap as IM
 import qualified Data.IntSet as IS
 import qualified Data.Map as M
-import qualified Data.IntMap as IM
-
+import qualified Data.Set as S
 
--- | A partial ordering on sets: <http://en.wikipedia.org/wiki/Partially_ordered_set>
+-- | A partial ordering on sets
+-- (<http://en.wikipedia.org/wiki/Partially_ordered_set>) is a set equipped
+-- with a binary relation, `leq`, that obeys the following laws
 --
--- This can be defined using either 'joinLeq' or 'meetLeq', or a more efficient definition
--- can be derived directly.
+-- @
+-- Reflexive:     a ``leq`` a
+-- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b
+-- Transitive:    a ``leq`` b && b ``leq`` c ==> a ``leq`` c
+-- @
 --
+-- Two elements of the set are said to be `comparable` when they are are
+-- ordered with respect to the `leq` relation. So
+--
 -- @
--- Reflexive:     a `leq` a
--- Antisymmetric: a `leq` b && b `leq` a ==> a == b
--- Transitive:    a `leq` b && b `leq` c ==> a `leq` c
+-- `comparable` a b ==> a ``leq`` b || b ``leq`` a
 -- @
 --
--- The superclass equality (which can be defined using 'partialOrdEq') must obey these laws:
+-- If `comparable` always returns true then the relation `leq` defines a
+-- total ordering (and an `Ord` instance may be defined). Any `Ord` instance is
+-- trivially an instance of `PartialOrd`. 'Algebra.Lattice.Ordered' provides a
+-- convenient wrapper to satisfy 'PartialOrd' given 'Ord'.
 --
+-- As an example consider the partial ordering on sets induced by set
+-- inclusion.  Then for sets `a` and `b`,
+--
 -- @
--- Reflexive:  a == a
--- Transitive: a == b && b == c ==> a == b
+-- a ``leq`` b
 -- @
+--
+-- is true when `a` is a subset of `b`.  Two sets are `comparable` if one is a
+-- subset of the other. Concretely
+--
+-- @
+-- a = {1, 2, 3}
+-- b = {1, 3, 4}
+-- c = {1, 2}
+--
+-- a ``leq`` a = `True`
+-- a ``leq`` b = `False`
+-- a ``leq`` c = `False`
+-- b ``leq`` a = `False`
+-- b ``leq`` b = `True`
+-- b ``leq`` c = `False`
+-- c ``leq`` a = `True`
+-- c ``leq`` b = `False`
+-- c ``leq`` c = `True`
+--
+-- `comparable` a b = `False`
+-- `comparable` a c = `True`
+-- `comparable` b c = `False`
+-- @
 class Eq a => PartialOrd a where
+    -- | The relation that induces the partial ordering
     leq :: a -> a -> Bool
 
--- | The equality relation induced by the partial-order structure
+    -- | Whether two elements are ordered with respect to the relation. A
+    -- default implementation is given by
+    --
+    -- > comparable x y = leq x y || leq y x
+    comparable :: a -> a -> Bool
+    comparable x y = leq x y || leq y x
+
+-- | The equality relation induced by the partial-order structure. It must obey
+-- the laws
+-- @
+-- Reflexive:  a == a
+-- Transitive: a == b && b == c ==> a == c
+-- @
 partialOrdEq :: PartialOrd a => a -> a -> Bool
 partialOrdEq x y = leq x y && leq y x
 
-
 instance Ord a => PartialOrd (S.Set a) where
     leq = S.isSubsetOf
 
@@ -56,16 +101,15 @@
     leq = IS.isSubsetOf
 
 instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where
-    m1 `leq` m2 = m1 `M.isSubmapOf` m2 && M.fold (\(x1, x2) b -> b && x1 `leq` x2) True (M.intersectionWith (,) m1 m2)
+    leq = M.isSubmapOfBy leq
 
 instance PartialOrd v => PartialOrd (IM.IntMap v) where
-    im1 `leq` im2 = im1 `IM.isSubmapOf` im2 && IM.fold (\(x1, x2) b -> b && x1 `leq` x2) True (IM.intersectionWith (,) im1 im2)
+    leq = IM.isSubmapOfBy leq
 
 instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
     -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical
     -- ordering is incompatible with the transitivity axiom we require for the derived partial order
     (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2
-
 
 -- | Least point of a partially ordered monotone function. Checks that the function is monotone.
 lfpFrom :: PartialOrd a => a -> (a -> a) -> a
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,13 @@
+# 1.6.0 (2017-06-26)
+
+- Correct PartialOrd Map and IntMap instances
+- Add Lattice instance for `containers` types.
+- Change `meets1` and `joins1` to use `Foldable1`
+- Add `comparable` to `PartialOrd`
+- Add `Algebra.Lattice.Free` module
+- Add `Divisibility` lattice.
+- Fix `Lexicographic`.
+
 # 1.5.0 (2015-12-18)
 
 - Move `PartialOrd (k -> v)` instance into own module
diff --git a/lattices.cabal b/lattices.cabal
--- a/lattices.cabal
+++ b/lattices.cabal
@@ -1,5 +1,5 @@
 name:               lattices
-version:            1.5.0
+version:            1.6.0
 cabal-version:      >= 1.10
 category:           Math
 license:            BSD3
@@ -7,14 +7,19 @@
 author:             Maximilian Bolingbroke <batterseapower@hotmail.com>
 maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
 homepage:           http://github.com/phadej/lattices/
-bug-reports:        http://github.com/phadej/lattices.git/issues
+bug-reports:        http://github.com/phadej/lattices/issues
 copyright:          (C) 2010-2015 Maximilian Bolingbroke
 build-type:         Simple
 extra-source-files: README.md CHANGELOG.md
-tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.2
+tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.3, GHC==8.0.2, GHC==8.2.1
 synopsis:           Fine-grained library for constructing and manipulating lattices
 description:
-  In mathematics, a lattice is a partially ordered set in which every two elements have a unique supremum (also called a least upper bound or @join@) and a unique infimum (also called a greatest lower bound or @meet@).
+  In mathematics, a lattice is a partially ordered set in which every two
+  elements @x@ and @y@ have a unique supremum (also called a least upper bound, join, or @x /\\ y@)
+  and a unique infimum (also called a greatest lower bound, meet, or @x \\/ y@).
+  .
+  This package provide type-classes for different lattice types, as well
+  as a class for the partial order.
 
 source-repository head
   type: git
@@ -23,7 +28,9 @@
 library
   exposed-modules:  Algebra.Enumerable,
                     Algebra.Lattice,
+                    Algebra.Lattice.Divisibility,
                     Algebra.Lattice.Dropped,
+                    Algebra.Lattice.Free,
                     Algebra.Lattice.Levitated,
                     Algebra.Lattice.Lexicographic,
                     Algebra.Lattice.Lifted,
@@ -32,19 +39,26 @@
                     Algebra.PartialOrd,
                     Algebra.PartialOrd.Instances
 
-  build-depends:    base                       >= 4.5  && < 4.9,
+  build-depends:    base                       >= 4.5  && < 4.11,
+                    base-compat                >= 0.9.3 && < 0.10,
                     containers                 >= 0.3  && < 0.6,
                     deepseq                    >= 1.1  && < 1.5,
                     hashable                   >= 1.2  && < 1.3,
-                    semigroups                 >= 0.16 && < 0.19,
                     tagged                     >= 0.7  && < 0.9,
-                    void                       >= 0.7  && < 0.8,
                     unordered-containers       >= 0.2  && < 0.3,
+                    semigroupoids              >= 5.2  && < 5.3,
                     universe-base              >= 1.0  && < 1.1,
                     universe-reverse-instances >= 1.0  && < 1.1
   ghc-options:      -Wall
   default-language: Haskell2010
 
+  if !impl(ghc >= 8.0)
+    build-depends:  semigroups                 >= 0.16 && < 0.19
+
+  if !impl(ghc >= 7.10)
+    build-depends:   void                       >= 0.7  && < 0.8,
+                     transformers               >= 0.3  && < 0.6
+
   if impl(ghc >= 7.4 && < 7.5)
     build-depends:  ghc-prim
 
@@ -54,9 +68,14 @@
   hs-source-dirs:      test
   ghc-options:         -Wall
   default-language:    Haskell2010
-  build-depends:       base              >= 4.5  && < 4.9,
-                       tasty             >= 0.10 && < 0.12,
-                       tasty-quickcheck  >= 0.8  && < 0.9,
+  build-depends:       base,
+                       base-compat          >= 0.9.3 && <0.10,
+                       tasty                >= 0.10  && < 0.12,
+                       tasty-quickcheck     >= 0.8   && < 0.10,
+                       QuickCheck           >= 2.10  && <2.11,
+                       quickcheck-instances >=0.3.16 && <0.4,
+                       universe-instances-base >= 1.0 && <1.1,
                        lattices,
+                       containers,
                        transformers,
-                       QuickCheck
+                       unordered-containers
diff --git a/test/Tests.hs b/test/Tests.hs
--- a/test/Tests.hs
+++ b/test/Tests.hs
@@ -5,21 +5,20 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Main (main) where
 
-#if MIN_VERSION_base(4,8,0)
-#else
-import Control.Applicative
-import Data.Foldable
-#endif
+import Prelude ()
+import Prelude.Compat
 
-import Data.Functor.Compose
-import Data.Functor.Identity
-import Data.Monoid
-import Data.Traversable
-import Control.Monad (ap)
+import Data.Maybe (listToMaybe, isJust)
+import Data.Monoid ((<>))
+import Control.Monad (ap, guard)
 import Test.QuickCheck.Function
 import Test.Tasty
 import Test.Tasty.QuickCheck as QC
 
+import Algebra.Lattice
+import Algebra.PartialOrd
+
+import qualified Algebra.Lattice.Divisibility as Div
 import qualified Algebra.Lattice.Dropped as D
 import qualified Algebra.Lattice.Levitated as L
 import qualified Algebra.Lattice.Lexicographic as LO
@@ -27,81 +26,44 @@
 import qualified Algebra.Lattice.Op as Op
 import qualified Algebra.Lattice.Ordered as O
 
+import Data.IntMap (IntMap)
+import Data.IntSet (IntSet)
+import Data.Map (Map)
+import Data.Set (Set)
+
+import Data.Universe.Instances.Base ()
+import Test.QuickCheck.Instances ()
+
 -- For old GHC to work
+data Proxy (a :: *) = Proxy
 data Proxy1 (a :: * -> *) = Proxy1
 
 main :: IO ()
 main = defaultMain tests
 
 tests :: TestTree
-tests = testGroup "Tests" [theseProps]
-
-theseProps :: TestTree
-theseProps = testGroup "These"
-  [ functorLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
-  , functorLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)
-  , functorLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))
-  , functorLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
-  , functorLaws "Op" (Proxy1 :: Proxy1 Op.Op)
-  , functorLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)
+tests = testGroup "Tests"
+  [ latticeLaws "M3" False (Proxy :: Proxy M3) -- non distributive lattice!
+  , latticeLaws "M2" True (Proxy :: Proxy M2) -- M2
+  , latticeLaws "Map" True (Proxy :: Proxy (Map Int (O.Ordered Int)))
+  , latticeLaws "IntMap" True (Proxy :: Proxy (IntMap (O.Ordered Int)))
+  , latticeLaws "Set" True (Proxy :: Proxy (Set Int))
+  , latticeLaws "IntSet" True (Proxy :: Proxy IntSet)
+  , latticeLaws "Ordered" True (Proxy :: Proxy (O.Ordered Int))
+  , latticeLaws "Divisibility" True (Proxy :: Proxy (Div.Divisibility Int))
+  , latticeLaws "LexOrdered" True (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int)))
+  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool)))
+  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive!
+  , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $
+      isJust searchM3LexM2
   , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
   , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)
   , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))
   , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
   , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op)
   , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)
-  , traversableLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)
-  , traversableLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)
-  , traversableLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))
-  , traversableLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)
-  , traversableLaws "Op" (Proxy1 :: Proxy1 Op.Op)
-  , traversableLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)
   ]
 
-functorLaws :: forall (f :: * -> *). ( Functor f
-                                     , Arbitrary (f Int)
-                                     , Eq (f Int)
-                                     , Show (f Int))
-            => String
-            -> Proxy1 f
-            -> TestTree
-functorLaws name _ = testGroup ("Functor laws: " <> name)
-  [ QC.testProperty "identity" identityProp
-  , QC.testProperty "composition" compositionProp
-  ]
-  where
-    identityProp :: f Int -> Property
-    identityProp x = fmap id x === x
-
-    compositionProp :: f Int -> Fun Int Int -> Fun Int Int -> Property
-    compositionProp x (Fun _ f) (Fun _ g) = fmap g (fmap f x) === fmap (g . f) x
-
-traversableLaws :: forall (t :: * -> *). ( Traversable t
-                                         , Arbitrary (t Int)
-                                         , Eq (t Int)
-                                         , Show (t Int))
-                => String
-                -> Proxy1 t
-                -> TestTree
-traversableLaws name _ = testGroup ("Traversable laws: " <> name)
-  [ QC.testProperty "identity" identityProp
-  , QC.testProperty "composition" compositionProp
-  , QC.testProperty "functor" functorProp
-  , QC.testProperty "foldable" foldableProp
-  ]
-  where
-    identityProp :: t Int -> Property
-    identityProp x = traverse Identity x === Identity x
-
-    compositionProp :: t Int -> Fun Int (Maybe Int) -> Fun Int ([] Int) -> Property
-    compositionProp x (Fun _ f) (Fun _ g) = traverse (Compose . fmap g . f) x === (Compose . fmap (traverse g) . traverse f $ x)
-
-    functorProp :: t Int -> Fun Int Int -> Property
-    functorProp x (Fun _ f) = fmap f x === fmapDefault f x
-
-    foldableProp :: t Int -> Fun Int [Int] -> Property
-    foldableProp x (Fun _ f) = foldMap f x === foldMapDefault f x
-
 monadLaws :: forall (m :: * -> *). ( Monad m
 #if !MIN_VERSION_base(4, 8, 0)
                                    , Applicative m
@@ -138,9 +100,95 @@
     apProp f x = (f' <*> x) === ap f' x
        where f' = apply <$> f
 
+-------------------------------------------------------------------------------
+-- Lattice distributive
+-------------------------------------------------------------------------------
 
--- Orphan instances
+latticeLaws
+    :: forall a. (Eq a, Show a, Arbitrary a,  Lattice a, PartialOrd a)
+    => String
+    -> Bool -- ^ distributive
+    -> Proxy a
+    -> TestTree
+latticeLaws name distr _ = testGroup ("Lattice laws: " <> name) $
+    [ QC.testProperty "leq = joinLeq" joinLeqProp
+    , QC.testProperty "leq = meetLeq" meetLeqProp
+    , QC.testProperty "meet is lower bound" meetLower
+    , QC.testProperty "join is upper bound" joinUpper
+    , QC.testProperty "meet commutes" meetComm
+    , QC.testProperty "join commute" joinComm
+    , QC.testProperty "meet associative" meetAssoc
+    , QC.testProperty "join associative" joinAssoc
+    , QC.testProperty "absorbtion 1" meetAbsorb
+    , QC.testProperty "absorbtion 2" joinAbsorb
+    , QC.testProperty "meet idempontent" meetIdemp
+    , QC.testProperty "join idempontent" joinIdemp
+    , QC.testProperty "comparableDef" comparableDef
+    ] ++ if not distr then [] else
+    -- Not all lattices are distributive!
+    [ QC.testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp
+    , QC.testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop
+    ]
+  where
+    joinLeqProp :: a -> a -> Property
+    joinLeqProp x y = leq x y === joinLeq x y
 
+    meetLeqProp :: a -> a -> Property
+    meetLeqProp x y = leq x y === meetLeq x y
+
+    meetLower :: a -> a -> Property
+    meetLower x y = (m `leq` x) QC..&&. (m `leq` y)
+      where
+        m = x /\ y
+
+    joinUpper :: a -> a -> Property
+    joinUpper x y = (x `leq` j) QC..&&. (y `leq` j)
+      where
+        j = x \/ y
+
+    meetComm :: a -> a -> Property
+    meetComm x y = x /\ y === y /\ x
+
+    joinComm :: a -> a -> Property
+    joinComm x y = x \/ y === y \/ x
+
+    meetAssoc :: a -> a -> a -> Property
+    meetAssoc x y z = x /\ (y /\ z) === (x /\ y) /\ z
+
+    joinAssoc :: a -> a -> a -> Property
+    joinAssoc x y z = x \/ (y \/ z) === (x \/ y) \/ z
+
+    meetAbsorb :: a -> a -> Property
+    meetAbsorb x y = x /\ (x \/ y) === x
+
+    joinAbsorb :: a -> a -> Property
+    joinAbsorb x y = x \/ (x /\ y) === x
+
+    meetIdemp :: a -> Property
+    meetIdemp x = x /\ x === x
+
+    joinIdemp :: a -> Property
+    joinIdemp x = x \/ x === x
+
+    comparableDef :: a -> a -> Property
+    comparableDef x y = (leq x y || leq y x) === comparable x y
+
+    distrProp :: a -> a -> a -> Property
+    distrProp x y z = lhs === rhs
+      where
+        lhs = x /\ (y \/ z)
+        rhs = (x /\ y) \/ (x /\ z)
+
+    distr2Prop :: a -> a -> a -> Property
+    distr2Prop x y z = lhs === rhs
+      where
+        lhs = x \/ (y /\ z)
+        rhs = (x \/ y) /\ (x \/ z)
+
+-------------------------------------------------------------------------------
+-- Orphans
+-------------------------------------------------------------------------------
+
 instance Arbitrary a => Arbitrary (D.Dropped a) where
   arbitrary = frequency [ (1, pure D.Top)
                         , (9, D.Drop <$> arbitrary)
@@ -159,9 +207,143 @@
 
 instance Arbitrary a => Arbitrary (O.Ordered a) where
   arbitrary = O.Ordered <$> arbitrary
+  shrink = map O.Ordered . shrink . O.getOrdered
 
+instance (Arbitrary a, Num a, Ord a) => Arbitrary (Div.Divisibility a) where
+  arbitrary = divisibility <$> arbitrary
+  shrink d = filter (<d) . map divisibility . shrink . Div.getDivisibility $ d
+
+divisibility :: (Ord a, Num a) => a -> Div.Divisibility a
+divisibility x | x < (-1)  = Div.Divisibility (abs x)
+               | x < 1     = Div.Divisibility 1
+               | otherwise = Div.Divisibility x
+
+
 instance Arbitrary a => Arbitrary (Op.Op a) where
   arbitrary = Op.Op <$> arbitrary
 
 instance (Arbitrary k, Arbitrary v) => Arbitrary (LO.Lexicographic k v) where
-  arbitrary = LO.Lexicographic <$> arbitrary <*> arbitrary
+    arbitrary = uncurry LO.Lexicographic <$> arbitrary
+    shrink (LO.Lexicographic k v) = uncurry LO.Lexicographic <$> shrink (k, v)
+
+-------------------------------------------------------------------------------
+-- Examples
+-------------------------------------------------------------------------------
+
+-- | Non-distributive lattice
+data M3 = M3_0 | M3_a | M3_b | M3_c | M3_1
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+instance Arbitrary M3 where
+    arbitrary = QC.arbitraryBoundedEnum
+
+instance PartialOrd M3 where
+    x    `leq` y    | x == y = True
+    M3_0 `leq` _             = True
+    _    `leq` M3_1          = True
+    _    `leq` _             = False
+
+instance JoinSemiLattice M3 where
+    x    \/ M3_0          = x
+    M3_0 \/ y             = y
+    _    \/ M3_1          = M3_1
+    M3_1 \/ _             = M3_1
+    x    \/ y | x == y    = x
+              | otherwise = M3_1
+
+instance MeetSemiLattice M3 where
+    x    /\ M3_1          = x
+    M3_1 /\ y             = y
+    _    /\ M3_0          = M3_0
+    M3_0 /\ _             = M3_0
+    x    /\ y | x == y    = x
+              | otherwise = M3_0
+
+instance Lattice M3 where
+
+-- | Set Bool, M2
+data M2 = M2_0 | M2_T | M2_F | M2_1
+  deriving (Eq, Ord, Show, Enum, Bounded)
+
+instance Arbitrary M2 where
+    arbitrary = QC.arbitraryBoundedEnum
+
+instance PartialOrd M2 where
+    x    `leq` y   | x == y  = True
+    M2_0 `leq` _             = True
+    _    `leq` M2_1          = True
+    _    `leq` _             = False
+
+instance JoinSemiLattice M2 where
+    x    \/ M2_0          = x
+    M2_0 \/ y             = y
+    _    \/ M2_1          = M2_1
+    M2_1 \/ _             = M2_1
+    x    \/ y | x == y    = x
+              | otherwise = M2_1
+
+instance MeetSemiLattice M2 where
+    x    /\ M2_1          = x
+    M2_1 /\ y             = y
+    _    /\ M2_0          = M2_0
+    M2_0 /\ _             = M2_0
+    x    /\ y | x == y    = x
+              | otherwise = M2_0
+
+instance Lattice M2 where
+
+instance BoundedJoinSemiLattice M2 where
+    bottom = M2_0
+
+instance BoundedMeetSemiLattice M2 where
+    top = M2_1
+
+instance BoundedLattice M2 where
+
+-------------------------------------------------------------------------------
+-- Lexicographic M2 search
+-------------------------------------------------------------------------------
+
+searchM3 :: (Eq a, PartialOrd a, Lattice a) => [a] -> Maybe (a,a,a,a,a)
+searchM3 xs = listToMaybe $ do
+    x0 <- xs
+    xa <- xs
+    guard (xa `notElem` [x0])
+    guard (x0 `leq` xa)
+    xb <- xs
+    guard (xb `notElem` [x0,xa])
+    guard (x0 `leq` xb)
+    guard (not $ comparable xa xb)
+    xc <- xs
+    guard (xc `notElem` [x0,xa,xb])
+    guard (x0 `leq` xc)
+    guard (not $ comparable xa xc)
+    guard (not $ comparable xb xc)
+    x1 <- xs
+    guard (x1 `notElem` [x0,xa,xb,xc])
+    guard (x0 `leq` x1)
+    guard (xa `leq` x1)
+    guard (xb `leq` x1)
+    guard (xc `leq` x1)
+
+    -- homomorphism
+    let f M3_0 = x1
+        f M3_a = xa
+        f M3_b = xb
+        f M3_c = xc
+        f M3_1 = x1
+
+    ma <- [minBound .. maxBound]
+    mb <- [minBound .. maxBound]
+    guard (f (ma /\ mb) == f ma /\ f mb)
+    guard (f (ma \/ mb) == f ma \/ f mb)
+
+    return (x0,xa,xb,xc,x1)
+
+type L2 = LO.Lexicographic M2 M2
+
+searchM3LexM2 :: Maybe (L2,L2,L2,L2,L2)
+searchM3LexM2 = searchM3 xs
+  where
+    xs = [ LO.Lexicographic x y | x <- ys, y <- ys ]
+    ys = [minBound .. maxBound]