diff --git a/Algebra/Enumerable.hs b/Algebra/Enumerable.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Enumerable.hs
@@ -0,0 +1,40 @@
+module Algebra.Enumerable (
+    Enumerable(..), universeBounded,
+    Enumerated(..)
+  ) where
+
+-- | Finitely enumerable things
+class Enumerable a where
+    universe :: [a]
+
+universeBounded :: (Enum a, Bounded a) => [a]
+universeBounded = enumFromTo minBound maxBound
+
+
+-- | Wrapper used to mark where we expect to use the fact that something is Enumerable
+newtype Enumerated a = Enumerated { unEnumerated :: a }
+                     deriving (Eq, Ord)
+
+instance Enumerable a => Enumerable (Enumerated a) where
+    universe = map Enumerated universe
+
+
+-- TODO: add to this rather sorry little set of instances. Can we exploit commonality with lazy-smallcheck?
+
+instance Enumerable Bool where
+    universe = universeBounded
+
+instance Enumerable Int where
+    universe = universeBounded
+
+instance Enumerable a => Enumerable (Maybe a) where
+    universe = Nothing : map Just universe
+
+instance (Enumerable a, Enumerable b) => Enumerable (Either a b) where
+    universe = map Left universe ++ map Right universe
+
+instance Enumerable () where
+    universe = [()]
+
+instance (Enumerable a, Enumerable b) => Enumerable (a, b) where
+    universe = [(a, b) | a <- universe, b <- universe]
diff --git a/Algebra/Lattice.hs b/Algebra/Lattice.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice.hs
@@ -0,0 +1,210 @@
+{-# LANGUAGE FlexibleInstances #-}
+module Algebra.Lattice (
+    -- * Unbounded lattices
+    JoinSemiLattice(..), MeetSemiLattice(..), Lattice,
+    joinLeq, joins1, meetLeq, meets1,
+    
+    -- * Bounded lattices
+    BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..), BoundedLattice,
+    joins, meets,
+    
+    -- * Fixed points of chains in lattices
+    lfp, unsafeLfp,
+    gfp, unsafeGfp,
+  ) where
+
+import Algebra.Enumerable
+import Algebra.PartialOrd
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+
+-- | A algebraic structure with element joins: <http://en.wikipedia.org/wiki/Semilattice>
+--
+-- Associativity: x `join` (y `join` z) == (x `join` y) `join` z
+-- Commutativity: x `join` y == y `join` x
+-- Idempotency:   x `join` x == x
+class JoinSemiLattice a where
+    join :: a -> a -> a
+
+-- | The partial ordering induced by the join-semilattice structure
+joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool
+joinLeq x y = x `join` y == y
+
+-- | The join of at a list of join-semilattice elements (of length at least one)
+joins1 :: JoinSemiLattice a => [a] -> a
+joins1 = foldr1 join
+
+-- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice>
+--
+-- Associativity: x `meet` (y `meet` z) == (x `meet` y) `meet` z
+-- Commutativity: x `meet` y == y `meet` x
+-- Idempotency:   x `meet` x == x
+class MeetSemiLattice a where
+    meet :: a -> a -> a
+
+-- | The partial ordering induced by the meet-semilattice structure
+meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool
+meetLeq x y = x `meet` y == x
+
+-- | The meet of at a list of meet-semilattice elements (of length at least one)
+meets1 :: MeetSemiLattice a => [a] -> a
+meets1 = foldr1 meet
+
+-- | 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)>
+--
+-- Absorption: a `join` (a `meet` b) == a `meet` (a `join` b) == a
+class (JoinSemiLattice a, MeetSemiLattice a) => Lattice a where
+
+-- | A join-semilattice with some element |bottom| that `join` approaches.
+--
+-- Identity: x `join` bottom == x
+class JoinSemiLattice a => BoundedJoinSemiLattice a where
+    bottom :: a
+
+-- | The join of a list of join-semilattice elements
+joins :: BoundedJoinSemiLattice a => [a] -> a
+joins = foldr join bottom
+
+-- | A meet-semilattice with some element |top| that `meet` approaches.
+--
+-- Identity: x `meet` top == x
+class MeetSemiLattice a => BoundedMeetSemiLattice a where
+    top :: a
+
+-- | The meet of a list of meet-semilattice elements
+meets :: BoundedMeetSemiLattice a => [a] -> a
+meets = foldr meet top
+
+
+-- | Lattices with both bounds
+class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where
+
+
+--
+-- Sets
+--
+
+instance Ord a => JoinSemiLattice (S.Set a) where
+    join = S.union
+
+instance (Ord a, Enumerable a) => MeetSemiLattice (S.Set (Enumerated a)) where
+    meet = S.intersection
+
+instance (Ord a, Enumerable a) => Lattice (S.Set (Enumerated a)) where
+
+instance Ord a => BoundedJoinSemiLattice (S.Set a) where
+    bottom = S.empty
+
+instance (Ord a, Enumerable a) => BoundedMeetSemiLattice (S.Set (Enumerated a)) where
+    top = S.fromList universe
+
+instance (Ord a, Enumerable a) => BoundedLattice (S.Set (Enumerated a)) where
+
+--
+-- Maps
+--
+
+instance (Ord k, JoinSemiLattice v) => JoinSemiLattice (M.Map k v) where
+    join = M.unionWith join
+
+instance (Ord k, Enumerable k, MeetSemiLattice v) => MeetSemiLattice (M.Map (Enumerated k) v) where
+    meet = M.intersectionWith meet
+
+instance (Ord k, Enumerable k, Lattice v) => Lattice (M.Map (Enumerated k) v) where
+
+instance (Ord k, JoinSemiLattice v) => BoundedJoinSemiLattice (M.Map k v) where
+    bottom = M.empty
+
+instance (Ord k, Enumerable k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (M.Map (Enumerated k) v) where
+    top = M.fromList (universe `zip` repeat top)
+
+instance (Ord k, Enumerable k, BoundedLattice v) => BoundedLattice (M.Map (Enumerated k) v) where
+
+--
+-- Functions
+--
+
+instance JoinSemiLattice v => JoinSemiLattice (k -> v) where
+    f `join` g = \x -> f x `join` g x
+
+instance MeetSemiLattice v => MeetSemiLattice (k -> v) where
+    f `meet` g = \x -> f x `meet` g x
+
+instance Lattice v => Lattice (k -> v) where
+
+instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where
+    bottom = const bottom
+
+instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where
+    top = const top
+
+instance BoundedLattice v => BoundedLattice (k -> v) where
+
+--
+-- Tuples
+--
+
+instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (a, b) where
+    (x1, y1) `join` (x2, y2) = (x1 `join` x2, y1 `join` y2)
+
+instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (a, b) where
+    (x1, y1) `meet` (x2, y2) = (x1 `meet` x2, y1 `meet` y2)
+
+instance (Lattice a, Lattice b) => Lattice (a, b) where
+
+instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where
+    bottom = (bottom, bottom)
+
+instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where
+    top = (top, top)
+
+instance (BoundedLattice a, BoundedLattice b) => BoundedLattice (a, b) where
+
+--
+-- Bools
+--
+
+instance JoinSemiLattice Bool where
+    join = (||)
+
+instance MeetSemiLattice Bool where
+    meet = (&&)
+
+instance Lattice Bool where
+
+instance BoundedJoinSemiLattice Bool where
+    bottom = False
+
+instance BoundedMeetSemiLattice Bool where
+    top = True
+
+instance BoundedLattice Bool where
+
+
+-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
+-- Assumes that the function is monotone and does not check if that is correct.
+{-# INLINE unsafeLfp #-}
+unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
+unsafeLfp = unsafeLfpFrom bottom
+
+-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
+-- Forces the function to be monotone.
+{-# INLINE lfp #-}
+lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
+lfp f = unsafeLfpFrom bottom (\x -> f x `join` x)
+
+
+-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
+-- Assumes that the function is antinone and does not check if that is correct.
+{-# INLINE unsafeGfp #-}
+unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
+unsafeGfp = unsafeGfpFrom top
+
+-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
+-- Forces the function to be antinone.
+{-# INLINE gfp #-}
+gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
+gfp f = unsafeGfpFrom top (\x -> f x `meet` x)
diff --git a/Algebra/Lattice/Dropped.hs b/Algebra/Lattice/Dropped.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice/Dropped.hs
@@ -0,0 +1,34 @@
+module Algebra.Lattice.Dropped (
+    Dropped(..)
+  ) where
+
+import Algebra.Lattice
+
+--
+-- Dropped
+--
+
+-- | Graft a distinct top onto an otherwise unbounded lattice.
+-- As a bonus, the top will be an absorbing element for the join.
+data Dropped a = Top
+               | Drop a
+
+instance JoinSemiLattice a => JoinSemiLattice (Dropped a) where
+    Top    `join` _      = Top
+    _      `join` Top    = Top
+    Drop x `join` Drop y = Drop (x `join` y)
+
+instance MeetSemiLattice a => MeetSemiLattice (Dropped a) where
+    Top    `meet` drop_y = drop_y
+    drop_x `meet` Top    = drop_x
+    Drop x `meet` Drop y = Drop (x `meet` y)
+
+instance Lattice a => Lattice (Dropped a) where
+
+instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Dropped a) where
+    bottom = Drop bottom
+
+instance MeetSemiLattice a => BoundedMeetSemiLattice (Dropped a) where
+    top = Top
+
+instance BoundedLattice a => BoundedLattice (Dropped a) where
diff --git a/Algebra/Lattice/Levitated.hs b/Algebra/Lattice/Levitated.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice/Levitated.hs
@@ -0,0 +1,40 @@
+module Algebra.Lattice.Levitated (
+    Levitated(..)
+  ) where
+
+import Algebra.Lattice
+
+--
+-- Levitated
+--
+
+-- | Graft a distinct top and bottom onto an otherwise unbounded lattice.
+-- The top is the absorbing element for the join, and the bottom is the absorbing
+-- element for the meet.
+data Levitated a = Top
+                 | Levitate a
+                 | Bottom
+
+instance JoinSemiLattice a => JoinSemiLattice (Levitated a) where
+    Top        `join` _          = Top
+    _          `join` Top        = Top
+    Levitate x `join` Levitate y = Levitate (x `join` y)
+    Bottom     `join` lev_y      = lev_y
+    lev_x      `join` Bottom     = lev_x
+
+instance MeetSemiLattice a => MeetSemiLattice (Levitated a) where
+    Top        `meet` lev_y      = lev_y
+    lev_x      `meet` Top        = lev_x
+    Levitate x `meet` Levitate y = Levitate (x `meet` y)
+    Bottom     `meet` _          = Bottom
+    _          `meet` Bottom     = Bottom
+
+instance Lattice a => Lattice (Levitated a) where
+
+instance JoinSemiLattice a => BoundedJoinSemiLattice (Levitated a) where
+    bottom = Bottom
+
+instance MeetSemiLattice a => BoundedMeetSemiLattice (Levitated a) where
+    top = Top
+
+instance BoundedLattice a => BoundedLattice (Levitated a) where
diff --git a/Algebra/Lattice/Lifted.hs b/Algebra/Lattice/Lifted.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/Lattice/Lifted.hs
@@ -0,0 +1,34 @@
+module Algebra.Lattice.Lifted (
+    Lifted(..)
+  ) where
+
+import Algebra.Lattice
+
+--
+-- Lifted
+--
+
+-- | Graft a distinct bottom onto an otherwise unbounded lattice.
+-- As a bonus, the bottom will be an absorbing element for the meet.
+data Lifted a = Lift a
+              | Bottom
+
+instance JoinSemiLattice a => JoinSemiLattice (Lifted a) where
+    Lift x `join` Lift y = Lift (x `join` y)
+    Bottom `join` lift_y = lift_y
+    lift_x `join` Bottom = lift_x
+
+instance MeetSemiLattice a => MeetSemiLattice (Lifted a) where
+    Lift x `meet` Lift y = Lift (x `meet` y)
+    Bottom `meet` _      = Bottom
+    _      `meet` Bottom = Bottom
+
+instance Lattice a => Lattice (Lifted a) where
+
+instance JoinSemiLattice a => BoundedJoinSemiLattice (Lifted a) where
+    bottom = Bottom
+
+instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Lifted a) where
+    top = Lift top
+
+instance BoundedLattice a => BoundedLattice (Lifted a) where
diff --git a/Algebra/PartialOrd.hs b/Algebra/PartialOrd.hs
new file mode 100644
--- /dev/null
+++ b/Algebra/PartialOrd.hs
@@ -0,0 +1,89 @@
+module Algebra.PartialOrd (
+    -- * Partial orderings
+    PartialOrd(..),
+    partialOrdEq,
+    
+    -- * Fixed points of chains in partial orders
+    lfpFrom, unsafeLfpFrom,
+    gfpFrom, unsafeGfpFrom
+  ) where
+
+import Algebra.Enumerable
+
+import qualified Data.Set as S
+import qualified Data.Map as M
+
+
+-- | A partial ordering on sets: <http://en.wikipedia.org/wiki/Partially_ordered_set>
+--
+-- 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
+--
+-- The superclass equality (which can be defined using |partialOrdEq|) must obey these laws:
+--
+-- Reflexive:  a == a
+-- Transitive: a == b && b == c ==> a == b
+class Eq a => PartialOrd a where
+    leq :: a -> a -> Bool
+
+-- | The equality relation induced by the partial-order structure
+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
+
+instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where
+    leq = M.isSubmapOf
+
+instance (Eq v, Enumerable k) => Eq (k -> v) where
+    f == g = all (\k -> f k == g k) universe
+
+instance (PartialOrd v, Enumerable k) => PartialOrd (k -> v) where
+    f `leq` g = all (\k -> f k `leq` g k) universe
+
+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
+lfpFrom = lfpFrom' leq
+
+-- | Least point of a partially ordered monotone function. Does not checks that the function is monotone.
+unsafeLfpFrom :: Eq a => a -> (a -> a) -> a
+unsafeLfpFrom = lfpFrom' (\_ _ -> True)
+
+{-# INLINE lfpFrom' #-}
+lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
+lfpFrom' check init_x f = go init_x
+  where go x | x' == x      = x
+             | x `check` x' = go x'
+             | otherwise    = error "lfpFrom: non-monotone function"
+          where x' = f x
+
+
+-- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone.
+{-# INLINE gfpFrom #-}
+gfpFrom :: PartialOrd a => a -> (a -> a) -> a
+gfpFrom = gfpFrom' leq
+
+-- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone.
+{-# INLINE unsafeGfpFrom #-}
+unsafeGfpFrom :: Eq a => a -> (a -> a) -> a
+unsafeGfpFrom = gfpFrom' (\_ _ -> True)
+
+{-# INLINE gfpFrom' #-}
+gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
+gfpFrom' check init_x f = go init_x
+  where go x | x' == x      = x
+             | x' `check` x = go x'
+             | otherwise    = error "gfpFrom: non-antinone function"
+          where x' = f x
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,22 @@
+Copyright (c) 2010, Maximilian Bolingbroke
+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 Maximilian Bolingbroke 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/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,4 @@
+#! /usr/bin/env runhaskell
+
+> import Distribution.Simple
+> main = defaultMain
diff --git a/lattices.cabal b/lattices.cabal
new file mode 100644
--- /dev/null
+++ b/lattices.cabal
@@ -0,0 +1,21 @@
+Name:               lattices
+Version:            1.0
+Cabal-Version:      >= 1.2
+Category:           Math
+Synopsis:           Fine-grained library for constructing and manipulating lattices
+License:            BSD3
+License-File:       LICENSE
+Author:             Max Bolingbroke <batterseapower@hotmail.com>
+Maintainer:         Max Bolingbroke <batterseapower@hotmail.com>
+Build-Type:         Simple
+
+Library
+        Exposed-Modules: Algebra.Enumerable,
+                         Algebra.Lattice,
+                         Algebra.Lattice.Dropped,
+                         Algebra.Lattice.Levitated,
+                         Algebra.Lattice.Lifted,
+                         Algebra.PartialOrd
+                         
+        Build-Depends:   base >= 3 && < 5,
+                         containers >= 0.3 && < 0.4