diff --git a/LICENCE b/LICENCE
new file mode 100644
--- /dev/null
+++ b/LICENCE
@@ -0,0 +1,27 @@
+Copyright 2026 Tony Morris
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. 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.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE REGENTS 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 AUTHORS 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.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+main = defaultMain
+
diff --git a/changelog.md b/changelog.md
new file mode 100644
--- /dev/null
+++ b/changelog.md
@@ -0,0 +1,3 @@
+0.0.1
+
+* This change log starts
diff --git a/src/Data/Valuation.hs b/src/Data/Valuation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation.hs
@@ -0,0 +1,206 @@
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- |
+-- A Haskell library providing reified algebraic structures for valuations,
+-- based on the valuation algebra framework of Shenoy & Shafer (1990),
+-- Kohlas (2003), and Abramsky & Carù (2019).
+--
+-- == Type Hierarchy
+--
+-- === Data Types
+--
+-- @
+-- 'BinaryFunctionT' f a b        -- a -> a -> f b
+--   |
+--   +-- 'BinaryFunction' a b     -- a -> a -> b          (f ~ 'Data.Functor.Identity.Identity')
+--   |     |
+--   |     +-- 'Magma' a          -- a -> a -> a          (a ~ b)
+--   |
+--   +-- 'MagmaT' f a             -- a -> a -> f a        (a ~ b)
+--
+-- 'Semigroup' a                   -- a -> a -> a
+--
+-- 'PartialOrder' a                -- a -> a -> 'Maybe' 'Ordering'
+--
+-- 'ProjectValuation' v set var    -- set var -> v -> v
+--
+-- 'SemiValuationAlgebra' v set var
+--   = 'SemiValuationAlgebra'
+--       ('Semigroup' v)                   -- how to combine values
+--       ('ProjectValuation' v set var)    -- how to project over a domain
+--
+-- 'ValuationAlgebraOp' set var v      -- set var -> v
+--
+-- 'ValuationAlgebra' v set var
+--   = 'ValuationAlgebra'
+--       ('SemiValuationAlgebra' v set var)
+--       ('ValuationAlgebraOp' set var v)  -- unit: identity value for a domain
+--       ('ValuationAlgebraOp' set var v)  -- zero: annihilating value for a domain
+--
+-- 'DomainLattice' sg p
+--   = 'DomainLattice'
+--       ('Semigroup' sg)                  -- join (∨ \/ supremum)
+--       ('Semigroup' sg)                  -- meet (∧ \/ infimum)
+--       ('PartialOrder' p)               -- partial order
+--
+-- 'Valuation' set var a
+--   = 'Valuation'
+--       (set var)                       -- domain
+--       a                               -- information
+--
+-- 'PresheafValuationAlgebra' v set var
+--   = 'PresheafValuationAlgebra'
+--       ('DomainLattice' (set var) (set var))   -- lattice on domains
+--       ('ValuationAlgebra' v set var)          -- the valuation algebra
+-- @
+--
+-- === Relationships
+--
+-- @
+-- 'BinaryFunctionT' ──specialises──> 'Magma' ──iso──> 'Semigroup'
+--                                                         |
+--                          'ProjectValuation' ────────────+──> 'SemiValuationAlgebra'
+--                                                                       |
+--                            'ValuationAlgebraOp' ──────────────────────+──> 'ValuationAlgebra'
+--                                                                                    |
+--         'PartialOrder' ──> 'DomainLattice' ────────────────────────────────────────+──> 'PresheafValuationAlgebra'
+-- @
+--
+-- == Core Concepts
+--
+-- === BinaryFunctionT
+--
+-- 'BinaryFunctionT' @f a b@ wraps @a -> a -> f b@ — a binary function from two @a@ values to an effectful @b@. It has instances for 'Data.Profunctor.Profunctor', 'Data.Profunctor.Strong', 'Data.Profunctor.Choice', 'Functor', 'Applicative', 'Monad', and more.
+--
+-- When @f ~ 'Data.Functor.Identity.Identity'@ and @a ~ b@, this specialises to 'Magma' @a@ — a binary operation on @a@.
+--
+-- === Semigroup
+--
+-- A reified semigroup: a @newtype@ over @a -> a -> a@ representing an associative binary operation. Unlike 'Prelude.Semigroup' which is a type class (one instance per type), this is a value — multiple semigroups can exist for the same type.
+--
+-- 'Semigroup' is isomorphic to 'Magma' (and hence @'BinaryFunctionT' 'Data.Functor.Identity.Identity' a a@) via 'HasBinaryFunctionT' \/ 'AsBinaryFunctionT'.
+--
+-- @
+-- import qualified "Data.Valuation.Semigroup" as S
+--
+-- S.'Data.Valuation.Semigroup.sum'      :: 'Num' a => 'Semigroup' a       -- (+)
+-- S.'Data.Valuation.Semigroup.product'  :: 'Num' a => 'Semigroup' a       -- (*)
+-- S.'Data.Valuation.Semigroup.min'      :: 'Ord' a => 'Semigroup' a
+-- S.'Data.Valuation.Semigroup.max'      :: 'Ord' a => 'Semigroup' a
+-- S.'Data.Valuation.Semigroup.list'     :: 'Semigroup' [a]              -- (++)
+-- S.'Data.Valuation.Semigroup.ordering' :: 'Semigroup' 'Ordering'         -- lexicographic
+-- S.'Data.Valuation.Semigroup.first'    :: 'Semigroup' a                -- const
+-- S.'Data.Valuation.Semigroup.second'   :: 'Semigroup' a                -- const id
+-- @
+--
+-- Semigroups compose:
+--
+-- @
+-- S.'Data.Valuation.Semigroup.pair'     :: 'Semigroup' a -> 'Semigroup' b -> 'Semigroup' (a, b)
+-- S.'Data.Valuation.Semigroup.maybe'    :: 'Semigroup' a -> 'Semigroup' ('Maybe' a)
+-- S.'Data.Valuation.Semigroup.function' :: 'Semigroup' b -> 'Semigroup' (a -> b)
+-- S.'Data.Valuation.Semigroup.dual'     :: 'Semigroup' a -> 'Semigroup' a     -- flip
+-- @
+--
+-- === PartialOrder
+--
+-- 'PartialOrder' @a@ wraps @a -> a -> 'Maybe' 'Ordering'@ — a partial order comparison. Unlike 'Ord' which is total, this supports incomparable elements via 'Nothing'. It is 'Data.Functor.Contravariant.Contravariant', 'Data.Functor.Contravariant.Divisible.Divisible', 'Data.Functor.Contravariant.Divisible.Decidable', and has a lexicographic 'Semigroup'.
+--
+-- 'PartialOrder' is isomorphic to @'BinaryFunctionT' 'Maybe' a 'Ordering'@ via 'HasBinaryFunctionT' \/ 'AsBinaryFunctionT'.
+--
+-- === ProjectValuation
+--
+-- 'ProjectValuation' @v set var@ wraps @set var -> v -> v@. Given a domain of variables and a current value, it produces a new value. It is 'Data.Functor.Contravariant.Contravariant' in @var@, and has 'Data.Functor.Contravariant.Divisible.Divisible' and 'Data.Functor.Contravariant.Divisible.Decidable' instances for combining projections.
+--
+-- === Valuation
+--
+-- 'Valuation' @set var a@ pairs a domain @set var@ with information @a@. It is a 'Functor', 'Applicative', 'Monad', 'Control.Comonad.Comonad', 'Data.Bifunctor.Bifunctor', 'Control.Monad.Writer.Class.MonadWriter', and more in its type parameters.
+--
+-- === SemiValuationAlgebra
+--
+-- Bundles a 'Semigroup' @v@ with a 'ProjectValuation' @v set var@. This provides everything needed to combine valuations: a way to merge information and a way to project information over a domain.
+--
+-- === ValuationAlgebra
+--
+-- Extends 'SemiValuationAlgebra' with two additional 'ValuationAlgebraOp' functions:
+--
+-- * __unit__ (@set var -> v@): produces an identity value for a given domain
+-- * __zero__ (@set var -> v@): produces an annihilating value for a given domain
+--
+-- === DomainLattice
+--
+-- 'DomainLattice' @sg p@ packages a lattice structure on domains: join (∨) and meet (∧) as 'Semigroup' values, plus a 'PartialOrder'. The type alias @'DomainLattice'' x = 'DomainLattice' x x@ is provided for the common case where the semigroup and partial order operate on the same type.
+--
+-- The canonical instance is 'setDomainLattice' using 'Data.Set.union', 'Data.Set.intersection', and 'Data.Set.isSubsetOf'.
+--
+-- === PresheafValuationAlgebra
+--
+-- The presheaf formulation of a valuation algebra, following Shenoy & Shafer (1990), Kohlas (2003), and Abramsky & Carù (2019). A 'PresheafValuationAlgebra' bundles a 'DomainLattice' with a 'ValuationAlgebra', providing the full structure needed for local computation on valuations:
+--
+-- * 'marginalise' — the presheaf restriction map: project a valuation to a subdomain
+-- * 'combine' — the combination operation: merge two valuations over the joined domain
+-- * 'neutralValuation' — identity element for combination on a given domain
+-- * 'nullValuation' — annihilating element for combination on a given domain
+--
+-- The module also provides law-checking functions for the valuation algebra axioms.
+--
+-- == Combining Valuations
+--
+-- The library provides three levels of combination, each using more algebraic structure:
+--
+-- @
+-- -- Combine domains and information independently using two Semigroups
+-- 'combineVar'
+--   :: 'Semigroup' (set var) -> 'Semigroup' v
+--   -> 'Valuation' set var v -> 'Valuation' set var v
+--   -> 'Valuation' set var v
+--
+-- -- Combine using a 'SemiValuationAlgebra': merge domains, combine information,
+-- -- then project through the merged domain
+-- 'combineSemiValuation'
+--   :: 'Semigroup' (set var) -> 'SemiValuationAlgebra' v set var
+--   -> 'Valuation' set var v -> 'Valuation' set var v
+--   -> 'Valuation' set var v
+--
+-- -- Combine using a 'ValuationAlgebra': like 'combineSemiValuation', but also
+-- -- folds in the unit value for the merged domain
+-- 'combineValuation'
+--   :: 'Semigroup' (set var) -> 'ValuationAlgebra' v set var
+--   -> 'Valuation' set var v -> 'Valuation' set var v
+--   -> 'Valuation' set var v
+-- @
+--
+-- At the highest level, 'PresheafValuationAlgebra' provides 'combine' which uses the bundled 'DomainLattice' to join domains automatically.
+--
+-- == Classy Optics
+--
+-- Every data type provides @Has*@ (classy lens) and @As*@ (classy prism) type classes, allowing generic programming over any type that contains or can be constructed from the given structure. For example, 'HasSemigroup' @c a@ provides a lens to a 'Semigroup' @a@ inside any @c@, and 'PresheafValuationAlgebra' has instances for 'HasDomainLattice', 'HasValuationAlgebra', 'HasSemiValuationAlgebra', 'HasSemigroup', and 'HasProjectValuation'.
+--
+-- == Modules
+--
+-- * "Data.Valuation" — Re-exports everything
+-- * "Data.Valuation.BinaryFunction" — 'BinaryFunctionT' and type aliases
+-- * "Data.Valuation.DomainLattice" — Lattice structure on domains (join, meet, partial order)
+-- * "Data.Valuation.PartialOrder" — Partial order comparison (@a -> a -> 'Maybe' 'Ordering'@)
+-- * "Data.Valuation.PresheafValuationAlgebra" — Presheaf formulation: marginalise, combine, and axiom laws
+-- * "Data.Valuation.ProjectValuation" — Domain projection
+-- * "Data.Valuation.Semigroup" — Reified semigroups
+-- * "Data.Valuation.SemiValuationAlgebra" — Semigroup + projection
+-- * "Data.Valuation.Valuation" — Domain-information pairs
+-- * "Data.Valuation.ValuationAlgebra" — Full algebra with unit and zero
+-- * "Data.Valuation.ValuationAlgebraOp" — Operations on valuation algebras (@set var -> v@)
+module Data.Valuation
+  ( module V,
+  )
+where
+
+import Data.Valuation.BinaryFunction as V
+import Data.Valuation.DomainLattice as V
+import Data.Valuation.PartialOrder as V
+import Data.Valuation.PresheafValuationAlgebra as V
+import Data.Valuation.ProjectValuation as V
+import Data.Valuation.SemiValuationAlgebra as V
+import Data.Valuation.Semigroup as V
+import Data.Valuation.Valuation as V
+import Data.Valuation.ValuationAlgebra as V
+import Data.Valuation.ValuationAlgebraOp as V
diff --git a/src/Data/Valuation/BinaryFunction.hs b/src/Data/Valuation/BinaryFunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/BinaryFunction.hs
@@ -0,0 +1,335 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | Binary functions over a functor, generalising magmas and semigroups.
+module Data.Valuation.BinaryFunction
+  ( BinaryFunctionT (..),
+    BinaryFunction,
+    MagmaT,
+    Magma,
+
+    -- * optics
+    HasBinaryFunctionT (..),
+    AsBinaryFunctionT (..),
+
+    -- * combinators
+    binaryFunction,
+    semigroupBinaryFunctionT,
+  )
+where
+
+import Control.Applicative (Alternative (..))
+import Control.Lens
+  ( Iso,
+    Lens',
+    Prism',
+    Rewrapped,
+    Wrapped (..),
+    from,
+    iso,
+    over,
+    review,
+    view,
+    _Wrapped,
+  )
+import Control.Monad.Fix (MonadFix (..))
+import Control.Monad.IO.Class (MonadIO (..))
+import Control.Monad.Zip (MonadZip (..))
+import Control.Selective (Selective (..), selectM)
+import Data.Distributive (Distributive (..))
+import Data.Functor.Alt (Alt (..))
+import Data.Functor.Apply (Apply (..))
+import Data.Functor.Bind (Bind (..))
+import Data.Functor.Identity (Identity (..))
+import Data.Functor.Plus (Plus (..))
+import Data.Profunctor (Choice (..), Profunctor (..), Strong (..))
+import Data.Profunctor.Closed (Closed (..))
+import Data.Valuation.Semigroup
+  ( Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Prelude hiding (Semigroup)
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+
+-- |
+-- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int
+-- >>> f 3 5
+-- [8]
+--
+-- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> Just (x ++ y)) :: BinaryFunctionT Maybe String String
+-- >>> f "hello" " world"
+-- Just "hello world"
+newtype BinaryFunctionT f a b
+  = BinaryFunctionT (a -> a -> f b)
+
+instance
+  (BinaryFunctionT f a b ~ t) =>
+  Rewrapped (BinaryFunctionT f' a' b') t
+
+instance Wrapped (BinaryFunctionT f a b) where
+  type Unwrapped (BinaryFunctionT f a b) = a -> a -> f b
+  _Wrapped' =
+    iso (\(BinaryFunctionT x) -> x) BinaryFunctionT
+
+-- | A 'BinaryFunctionT' specialised to 'Identity'.
+type BinaryFunction a b =
+  BinaryFunctionT Identity a b
+
+-- | A 'BinaryFunctionT' where the input and output types coincide.
+type MagmaT f x =
+  BinaryFunctionT f x x
+
+-- | A 'BinaryFunction' where the input and output types coincide.
+type Magma x =
+  BinaryFunction x x
+
+-- | Classy lens for types that contain a 'BinaryFunctionT'.
+class HasBinaryFunctionT c f a b | c -> f a b where
+  binaryFunctionT ::
+    Lens' c (BinaryFunctionT f a b)
+
+instance HasBinaryFunctionT (BinaryFunctionT f a b) f a b where
+  binaryFunctionT = id
+
+-- | Classy prism for types that can be constructed from a 'BinaryFunctionT'.
+class AsBinaryFunctionT c f a b | c -> f a b where
+  _BinaryFunctionT ::
+    Prism' c (BinaryFunctionT f a b)
+
+instance AsBinaryFunctionT (BinaryFunctionT f a b) f a b where
+  _BinaryFunctionT = id
+
+instance HasBinaryFunctionT (Semigroup a) Identity a a where
+  binaryFunctionT = applySemigroup . from binaryFunction
+
+instance AsBinaryFunctionT (Semigroup a) Identity a a where
+  _BinaryFunctionT = applySemigroup . from binaryFunction
+
+-- | Iso between a 'BinaryFunction' and its underlying binary function.
+binaryFunction :: Iso (BinaryFunction a b) (BinaryFunction a' b') (a -> a -> b) (a' -> a' -> b')
+binaryFunction = _Wrapped . iso (\k a1 a2 -> runIdentity (k a1 a2)) (\k a1 a2 -> Identity (k a1 a2))
+
+-- |
+-- >>> let BinaryFunctionT f = fmap (*2) (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f 3 5
+-- [16]
+--
+-- >>> let BinaryFunctionT f = fmap show (BinaryFunctionT (\x y -> Just (x + y)) :: BinaryFunctionT Maybe Int Int)
+-- >>> f 3 5
+-- Just "8"
+instance (Functor f) => Functor (BinaryFunctionT f a) where
+  fmap g = over _Wrapped (\h a1 a2 -> fmap g (h a1 a2))
+
+-- |
+-- >>> import Data.Functor.Apply ((<.>))
+-- >>> let BinaryFunctionT f = (BinaryFunctionT (\x y -> [(*x), (*y)]) :: BinaryFunctionT [] Int (Int -> Int)) <.> BinaryFunctionT (\x y -> [x + y, x * y])
+-- >>> f 3 5
+-- [24,45,40,75]
+apBFT :: (f (b -> c) -> f b -> f c) -> BinaryFunctionT f a (b -> c) -> BinaryFunctionT f a b -> BinaryFunctionT f a c
+apBFT ap' (BinaryFunctionT hf) (BinaryFunctionT ha) = BinaryFunctionT (\a1 a2 -> ap' (hf a1 a2) (ha a1 a2))
+
+instance (Apply f) => Apply (BinaryFunctionT f a) where
+  (<.>) = apBFT (<.>)
+
+-- |
+-- >>> let BinaryFunctionT f = pure 42 :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- [42]
+--
+-- >>> let BinaryFunctionT f = (BinaryFunctionT (\x y -> [(*x), (*y)]) :: BinaryFunctionT [] Int (Int -> Int)) <*> BinaryFunctionT (\x y -> [x + y, x * y])
+-- >>> f 3 5
+-- [24,45,40,75]
+instance (Applicative f) => Applicative (BinaryFunctionT f a) where
+  pure b = BinaryFunctionT (\_ _ -> pure b)
+  (<*>) = apBFT (<*>)
+
+-- |
+-- >>> import Data.Functor.Bind ((>>-))
+-- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y, x * y]) >>- (\b -> BinaryFunctionT (\x y -> [b + x, b + y])) :: BinaryFunctionT [] Int Int
+-- >>> f 3 5
+-- [11,13,18,20]
+bindBFT :: (f b -> (b -> f c) -> f c) -> BinaryFunctionT f a b -> (b -> BinaryFunctionT f a c) -> BinaryFunctionT f a c
+bindBFT bnd (BinaryFunctionT h) k = BinaryFunctionT (\a1 a2 -> bnd (h a1 a2) (\b -> view _Wrapped (k b) a1 a2))
+
+instance (Bind f) => Bind (BinaryFunctionT f a) where
+  (>>-) = bindBFT (>>-)
+
+-- |
+-- >>> let BinaryFunctionT f = BinaryFunctionT (\x y -> [x + y, x * y]) >>= (\b -> BinaryFunctionT (\x y -> [b + x, b + y])) :: BinaryFunctionT [] Int Int
+-- >>> f 3 5
+-- [11,13,18,20]
+--
+-- >>> let BinaryFunctionT f = return 42 :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- [42]
+instance (Monad f) => Monad (BinaryFunctionT f a) where
+  (>>=) = bindBFT (>>=)
+
+-- |
+-- >>> import Data.Profunctor (dimap, lmap, rmap)
+-- >>> let BinaryFunctionT f = dimap (+1) (*2) (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f 3 5
+-- [20]
+--
+-- >>> import Data.Profunctor (lmap)
+-- >>> let BinaryFunctionT f = lmap (*10) (BinaryFunctionT (\x y -> [x, y]) :: BinaryFunctionT [] Int Int)
+-- >>> f 3 5
+-- [30,50]
+--
+-- >>> import Data.Profunctor (rmap)
+-- >>> let BinaryFunctionT f = rmap show (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f 3 5
+-- ["8"]
+instance (Functor f) => Profunctor (BinaryFunctionT f) where
+  dimap f g = over _Wrapped (\h a1 a2 -> fmap g (h (f a1) (f a2)))
+  lmap f = over _Wrapped (\h a1 a2 -> h (f a1) (f a2))
+  rmap g = over _Wrapped (\h a1 a2 -> fmap g (h a1 a2))
+
+-- |
+-- >>> import Data.Profunctor (Strong(..))
+-- >>> let BinaryFunctionT f = first' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f (1, "hello") (2, "world")
+-- [(3,"hello")]
+--
+-- >>> import Data.Profunctor (Strong(..))
+-- >>> let BinaryFunctionT f = second' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f ("hello", 1) ("world", 2)
+-- [("hello",3)]
+instance (Functor f) => Strong (BinaryFunctionT f) where
+  first' = over _Wrapped (\h (a1, c) (a2, _) -> fmap (,c) (h a1 a2))
+  second' = over _Wrapped (\h (c, a1) (_, a2) -> fmap (c,) (h a1 a2))
+
+-- |
+-- >>> import Data.Profunctor (Choice(..))
+-- >>> let BinaryFunctionT f = left' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f (Left 1) (Left 2)
+-- [Left 3]
+-- >>> f (Left 1) (Right "hi")
+-- [Right "hi"]
+-- >>> f (Right "hi") (Left 2)
+-- [Right "hi"]
+-- >>> f (Right "a") (Right "b")
+-- [Right "a"]
+--
+-- >>> import Data.Profunctor (Choice(..))
+-- >>> let BinaryFunctionT f = right' (BinaryFunctionT (\x y -> [x + y]) :: BinaryFunctionT [] Int Int)
+-- >>> f (Right 1) (Right 2)
+-- [Right 3]
+-- >>> f (Left "hi") (Right 2)
+-- [Left "hi"]
+instance (Applicative f) => Choice (BinaryFunctionT f) where
+  left' = over _Wrapped $ \h ea1 ea2 -> case (ea1, ea2) of
+    (Left a1, Left a2) -> fmap Left (h a1 a2)
+    (Right c, _) -> pure (Right c)
+    (_, Right c) -> pure (Right c)
+  right' = over _Wrapped $ \h ea1 ea2 -> case (ea1, ea2) of
+    (Right a1, Right a2) -> fmap Right (h a1 a2)
+    (Left c, _) -> pure (Left c)
+    (_, Left c) -> pure (Left c)
+
+-- |
+-- >>> import Control.Monad.Fix (mfix)
+-- >>> let BinaryFunctionT f = mfix (\x -> BinaryFunctionT (\a _ -> [const 42 x + a])) :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- [43]
+instance (MonadFix f) => MonadFix (BinaryFunctionT f a) where
+  mfix g = BinaryFunctionT (\a1 a2 -> mfix (\b -> view _Wrapped (g b) a1 a2))
+
+-- |
+-- >>> import Control.Selective (select)
+-- >>> let BinaryFunctionT f = select (BinaryFunctionT (\_ _ -> [Left 1, Right 2]) :: BinaryFunctionT [] Int (Either Int Int)) (BinaryFunctionT (\_ _ -> [(+10)]))
+-- >>> f 0 0
+-- [11,2]
+instance (Monad f) => Selective (BinaryFunctionT f a) where
+  select = selectM
+
+-- |
+-- >>> import Control.Monad.Zip (mzip)
+-- >>> let BinaryFunctionT f = mzip (BinaryFunctionT (\x y -> [x + y, x * y]) :: BinaryFunctionT [] Int Int) (BinaryFunctionT (\x y -> [x - y]))
+-- >>> f 5 3
+-- [(8,2)]
+instance (MonadZip f) => MonadZip (BinaryFunctionT f a) where
+  mzipWith g (BinaryFunctionT h1) (BinaryFunctionT h2) = BinaryFunctionT (\a1 a2 -> mzipWith g (h1 a1 a2) (h2 a1 a2))
+
+-- |
+-- >>> let BinaryFunctionT f = liftIO (putStrLn "hello") :: BinaryFunctionT IO Int ()
+-- >>> f 1 2
+-- hello
+instance (MonadIO f) => MonadIO (BinaryFunctionT f a) where
+  liftIO io = BinaryFunctionT (\_ _ -> liftIO io)
+
+-- |
+-- >>> import Data.Functor.Alt ((<!>))
+-- >>> let BinaryFunctionT f = (BinaryFunctionT (\_ _ -> Nothing) :: BinaryFunctionT Maybe Int Int) <!> BinaryFunctionT (\x y -> Just (x + y))
+-- >>> f 3 5
+-- Just 8
+instance (Alt f) => Alt (BinaryFunctionT f a) where
+  BinaryFunctionT h1 <!> BinaryFunctionT h2 = BinaryFunctionT (\a1 a2 -> h1 a1 a2 <!> h2 a1 a2)
+
+-- |
+-- >>> import Data.Functor.Plus (zero)
+-- >>> let BinaryFunctionT f = zero :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- []
+instance (Plus f) => Plus (BinaryFunctionT f a) where
+  zero = BinaryFunctionT (\_ _ -> zero)
+
+-- |
+-- >>> import Control.Applicative (empty, (<|>))
+-- >>> let BinaryFunctionT f = (BinaryFunctionT (\_ _ -> Nothing) :: BinaryFunctionT Maybe Int Int) <|> BinaryFunctionT (\x y -> Just (x + y))
+-- >>> f 3 5
+-- Just 8
+--
+-- >>> import Control.Applicative (empty)
+-- >>> let BinaryFunctionT f = empty :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- []
+instance (Alternative f) => Alternative (BinaryFunctionT f a) where
+  empty = BinaryFunctionT (\_ _ -> empty)
+  BinaryFunctionT h1 <|> BinaryFunctionT h2 = BinaryFunctionT (\a1 a2 -> h1 a1 a2 <|> h2 a1 a2)
+
+-- |
+-- >>> let BinaryFunctionT f = runSemigroup semigroupBinaryFunctionT (BinaryFunctionT (\_ _ -> [1, 2]) :: BinaryFunctionT [] Int Int) (BinaryFunctionT (\_ _ -> [10, 20])) in f 0 0
+-- [1,2,10,20]
+semigroupBinaryFunctionT :: (Prelude.Semigroup (f b)) => Semigroup (BinaryFunctionT f a b)
+semigroupBinaryFunctionT = review applySemigroup (\(BinaryFunctionT h1) (BinaryFunctionT h2) -> BinaryFunctionT (\a1 a2 -> h1 a1 a2 <> h2 a1 a2))
+
+-- |
+-- >>> let BinaryFunctionT f = BinaryFunctionT (\_ _ -> [1, 2]) <> (BinaryFunctionT (\_ _ -> [3, 4]) :: BinaryFunctionT [] Int Int)
+-- >>> f 0 0
+-- [1,2,3,4]
+instance (Prelude.Semigroup (f b)) => Prelude.Semigroup (BinaryFunctionT f a b) where
+  (<>) = runSemigroup semigroupBinaryFunctionT
+
+-- |
+-- >>> let BinaryFunctionT f = mempty :: BinaryFunctionT [] Int Int
+-- >>> f 1 2
+-- []
+instance (Prelude.Monoid (f b)) => Prelude.Monoid (BinaryFunctionT f a b) where
+  mempty = BinaryFunctionT (\_ _ -> mempty)
+
+-- |
+-- >>> import Data.Distributive (distribute)
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> let BinaryFunctionT f = distribute [BinaryFunctionT (\x y -> Identity (x + y)), BinaryFunctionT (\x y -> Identity (x * y))] :: BinaryFunctionT Identity Int [Int]
+-- >>> f 3 5
+-- Identity [8,15]
+instance (Distributive f) => Distributive (BinaryFunctionT f a) where
+  distribute gs = BinaryFunctionT (\a1 a2 -> distribute (fmap (\(BinaryFunctionT h) -> h a1 a2) gs))
+
+-- |
+-- >>> import Data.Profunctor.Closed (Closed(..))
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> let BinaryFunctionT f = closed (BinaryFunctionT (\x y -> Identity (x + y)) :: BinaryFunctionT Identity Int Int)
+-- >>> runIdentity (f (*2) (*3)) 10
+-- 50
+instance (Distributive f) => Closed (BinaryFunctionT f) where
+  closed (BinaryFunctionT h) = BinaryFunctionT (\xa1 xa2 -> distribute (\x -> h (xa1 x) (xa2 x)))
diff --git a/src/Data/Valuation/DomainLattice.hs b/src/Data/Valuation/DomainLattice.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/DomainLattice.hs
@@ -0,0 +1,248 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A lattice structure on domains, as required by the presheaf formulation
+-- of valuation algebras (Shenoy & Shafer, Kohlas, Abramsky & Carù).
+--
+-- A domain lattice provides:
+--
+-- * Join (\/) — combining domains (supremum)
+-- * Meet (/\) — intersecting domains (infimum)
+-- * Partial order — domain inclusion, with incomparable elements
+module Data.Valuation.DomainLattice
+  ( DomainLattice (..),
+    DomainLattice',
+    HasDomainLattice (..),
+    AsDomainLattice (..),
+    runDomainJoin,
+    runDomainMeet,
+    runDomainCompare,
+    runDomainLeq,
+    setDomainLattice,
+
+    -- * laws
+    lawJoinAssociative,
+    lawMeetAssociative,
+    lawJoinCommutative,
+    lawMeetCommutative,
+    lawAbsorption1,
+    lawAbsorption2,
+    lawJoinIdempotent,
+    lawMeetIdempotent,
+    lawLeqFromJoin,
+  )
+where
+
+import Control.Lens (Lens', Prism', review, view)
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Valuation.PartialOrder
+  ( HasPartialOrder (..),
+    PartialOrder,
+    fromLeq,
+    partialOrderLeq,
+    runPartialOrder,
+  )
+import Data.Valuation.Semigroup
+  ( Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Prelude hiding (Semigroup)
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+
+-- |
+-- >>> import qualified Data.Set as Set
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> runDomainJoin lat (Set.fromList [1,2]) (Set.fromList [2,3])
+-- fromList [1,2,3]
+-- >>> runDomainMeet lat (Set.fromList [1,2]) (Set.fromList [2,3])
+-- fromList [2]
+-- >>> runDomainLeq lat (Set.fromList [1]) (Set.fromList [1,2])
+-- True
+-- >>> runDomainLeq lat (Set.fromList [1,3]) (Set.fromList [1,2])
+-- False
+-- >>> runDomainCompare lat (Set.fromList [1,2]) (Set.fromList [2,3])
+-- Nothing
+data DomainLattice sg p
+  = DomainLattice
+      -- | join (\/ / supremum)
+      (Semigroup sg)
+      -- | meet (/\ / infimum)
+      (Semigroup sg)
+      -- | partial order
+      (PartialOrder p)
+
+type DomainLattice' x =
+  DomainLattice x x
+
+-- | Classy lens for types that contain a 'DomainLattice'.
+class HasDomainLattice c sg p | c -> sg p where
+  domainLattice :: Lens' c (DomainLattice sg p)
+  domainLatticeJoin :: Lens' c (Semigroup sg)
+  domainLatticeJoin = domainLattice . domainLatticeJoin
+  domainLatticeMeet :: Lens' c (Semigroup sg)
+  domainLatticeMeet = domainLattice . domainLatticeMeet
+
+instance HasDomainLattice (DomainLattice sg p) sg p where
+  domainLattice = id
+  domainLatticeJoin f (DomainLattice j m o) = fmap (\j' -> DomainLattice j' m o) (f j)
+  domainLatticeMeet f (DomainLattice j m o) = fmap (\m' -> DomainLattice j m' o) (f m)
+
+-- | Classy prism for types that can be constructed from a 'DomainLattice'.
+class AsDomainLattice c sg p | c -> sg p where
+  _DomainLattice :: Prism' c (DomainLattice sg p)
+
+instance AsDomainLattice (DomainLattice sg p) sg p where
+  _DomainLattice = id
+
+instance HasPartialOrder (DomainLattice sg p) p where
+  partialOrder f (DomainLattice j m o) = fmap (DomainLattice j m) (f o)
+
+-- | Apply the domain join (\/): the supremum of two domains.
+{-# SPECIALIZE runDomainJoin ::
+  DomainLattice sg p -> sg -> sg -> sg
+  #-}
+runDomainJoin :: (HasDomainLattice lat sg p) => lat -> sg -> sg -> sg
+runDomainJoin = runSemigroup . view domainLatticeJoin
+
+-- | Apply the domain meet (/\): the infimum of two domains.
+{-# SPECIALIZE runDomainMeet ::
+  DomainLattice sg p -> sg -> sg -> sg
+  #-}
+runDomainMeet :: (HasDomainLattice lat sg p) => lat -> sg -> sg -> sg
+runDomainMeet = runSemigroup . view domainLatticeMeet
+
+-- | Compare two domains using the partial order.
+-- Returns 'Nothing' for incomparable elements.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> runDomainCompare (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
+-- Just LT
+-- >>> runDomainCompare (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [1,2])
+-- Just EQ
+-- >>> runDomainCompare (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- Nothing
+{-# SPECIALIZE runDomainCompare ::
+  DomainLattice sg p -> p -> p -> Maybe Ordering
+  #-}
+runDomainCompare :: (HasPartialOrder lat p) => lat -> p -> p -> Maybe Ordering
+runDomainCompare = runPartialOrder . view partialOrder
+
+-- | Test the domain partial order: @runDomainLeq lat d1 d2@ is 'True' iff @d1 <= d2@.
+-- Returns 'False' for incomparable elements.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> runDomainLeq (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
+-- True
+-- >>> runDomainLeq (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- False
+{-# SPECIALIZE runDomainLeq ::
+  DomainLattice sg p -> p -> p -> Bool
+  #-}
+runDomainLeq :: (HasPartialOrder lat p) => lat -> p -> p -> Bool
+runDomainLeq = partialOrderLeq . view partialOrder
+
+-- | The canonical 'DomainLattice' for 'Set', with union as join,
+-- intersection as meet, and subset as the partial order.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> let lat = setDomainLattice :: DomainLattice (Set String) (Set String)
+-- >>> runDomainJoin lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
+-- fromList ["x","y","z"]
+-- >>> runDomainMeet lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
+-- fromList ["y"]
+-- >>> runDomainLeq lat (Set.fromList ["x"]) (Set.fromList ["x","y"])
+-- True
+-- >>> runDomainCompare lat (Set.fromList ["x","y"]) (Set.fromList ["y","z"])
+-- Nothing
+setDomainLattice :: (Ord a) => DomainLattice' (Set a)
+setDomainLattice =
+  DomainLattice
+    (review applySemigroup Set.union)
+    (review applySemigroup Set.intersection)
+    (fromLeq Set.isSubsetOf)
+
+-- |
+-- >>> import qualified Data.Set as Set
+-- >>> lawJoinAssociative (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4])
+-- True
+lawJoinAssociative :: (Eq sg) => DomainLattice sg p -> sg -> sg -> sg -> Bool
+lawJoinAssociative lat a b c =
+  let j = runDomainJoin lat
+   in j (j a b) c == j a (j b c)
+
+-- |
+-- >>> import qualified Data.Set as Set
+-- >>> lawMeetAssociative (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3]) (Set.fromList [3,4])
+-- True
+lawMeetAssociative :: (Eq sg) => DomainLattice sg p -> sg -> sg -> sg -> Bool
+lawMeetAssociative lat a b c =
+  let m = runDomainMeet lat
+   in m (m a b) c == m a (m b c)
+
+-- |
+-- >>> import qualified Data.Set as Set
+-- >>> lawJoinCommutative (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- True
+lawJoinCommutative :: (Eq sg) => DomainLattice sg p -> sg -> sg -> Bool
+lawJoinCommutative lat a b =
+  runDomainJoin lat a b == runDomainJoin lat b a
+
+-- |
+-- >>> import qualified Data.Set as Set
+-- >>> lawMeetCommutative (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- True
+lawMeetCommutative :: (Eq sg) => DomainLattice sg p -> sg -> sg -> Bool
+lawMeetCommutative lat a b =
+  runDomainMeet lat a b == runDomainMeet lat b a
+
+-- | Absorption law 1: @a \/ (a /\ b) = a@.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> lawAbsorption1 (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- True
+lawAbsorption1 :: (Eq sg) => DomainLattice sg p -> sg -> sg -> Bool
+lawAbsorption1 lat a b =
+  runDomainJoin lat a (runDomainMeet lat a b) == a
+
+-- | Absorption law 2: @a /\ (a \/ b) = a@.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> lawAbsorption2 (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2]) (Set.fromList [2,3])
+-- True
+lawAbsorption2 :: (Eq sg) => DomainLattice sg p -> sg -> sg -> Bool
+lawAbsorption2 lat a b =
+  runDomainMeet lat a (runDomainJoin lat a b) == a
+
+-- | Join idempotence: @a \/ a = a@.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> lawJoinIdempotent (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2])
+-- True
+lawJoinIdempotent :: (Eq sg) => DomainLattice sg p -> sg -> Bool
+lawJoinIdempotent lat a =
+  runDomainJoin lat a a == a
+
+-- | Meet idempotence: @a /\ a = a@.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> lawMeetIdempotent (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,2])
+-- True
+lawMeetIdempotent :: (Eq sg) => DomainLattice sg p -> sg -> Bool
+lawMeetIdempotent lat a =
+  runDomainMeet lat a a == a
+
+-- | Consistency of partial order with join: @a <= b@ iff @a \/ b = b@.
+--
+-- >>> import qualified Data.Set as Set
+-- >>> lawLeqFromJoin (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1]) (Set.fromList [1,2])
+-- True
+-- >>> lawLeqFromJoin (setDomainLattice :: DomainLattice (Set Int) (Set Int)) (Set.fromList [1,3]) (Set.fromList [1,2])
+-- True
+lawLeqFromJoin :: (Eq d) => DomainLattice' d -> d -> d -> Bool
+lawLeqFromJoin lat a b =
+  runDomainLeq lat a b == (runDomainJoin lat a b == b)
diff --git a/src/Data/Valuation/PartialOrder.hs b/src/Data/Valuation/PartialOrder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/PartialOrder.hs
@@ -0,0 +1,297 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A partial order on a type, wrapping @a -> a -> 'Maybe' 'Ordering'@.
+--
+-- This is the partial order analogue of 'Data.Functor.Contravariant.Comparison'
+-- (which represents total orders via @a -> a -> 'Ordering'@).
+-- The 'Nothing' case represents incomparable elements.
+--
+-- @
+-- 'Just' 'LT'  — a < b
+-- 'Just' 'EQ'  — a = b
+-- 'Just' 'GT'  — a > b
+-- 'Nothing'  — a and b are incomparable
+-- @
+module Data.Valuation.PartialOrder
+  ( PartialOrder (..),
+
+    -- * optics
+    HasPartialOrder (..),
+    AsPartialOrder (..),
+    isBinaryFunctionT,
+
+    -- * combinators
+    semigroupPartialOrder,
+    runPartialOrder,
+    partialOrderLeq,
+    totalOrder,
+    fromLeq,
+  )
+where
+
+import Control.Lens
+  ( Iso,
+    Lens',
+    Prism',
+    Rewrapped,
+    Wrapped (..),
+    from,
+    iso,
+    review,
+    _Wrapped,
+  )
+import Data.Functor.Contravariant (Contravariant (..))
+import Data.Functor.Contravariant.Conclude (Conclude (..))
+import Data.Functor.Contravariant.Decide (Decide (..))
+import Data.Functor.Contravariant.Divise (Divise (..))
+import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..))
+import Data.Valuation.BinaryFunction
+  ( AsBinaryFunctionT (..),
+    BinaryFunctionT,
+    HasBinaryFunctionT (..),
+  )
+import Data.Valuation.Semigroup
+  ( Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Data.Void (absurd)
+import Prelude hiding (Semigroup)
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+-- >>> import Data.Void (Void)
+
+-- |
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2
+-- Just LT
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2
+-- Just EQ
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2
+-- Just GT
+--
+-- >>> import qualified Data.Set as Set
+-- >>> runPartialOrder (fromLeq Set.isSubsetOf) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int])
+-- Nothing
+newtype PartialOrder a
+  = PartialOrder (a -> a -> Maybe Ordering)
+
+instance (PartialOrder a ~ t) => Rewrapped (PartialOrder a') t
+
+instance Wrapped (PartialOrder a) where
+  type Unwrapped (PartialOrder a) = a -> a -> Maybe Ordering
+  _Wrapped' = iso (\(PartialOrder x) -> x) PartialOrder
+
+-- | Classy lens for types that contain a 'PartialOrder'.
+class HasPartialOrder c a | c -> a where
+  partialOrder :: Lens' c (PartialOrder a)
+
+instance HasPartialOrder (PartialOrder a) a where
+  partialOrder = id
+
+-- | Classy prism for types that can be constructed from a 'PartialOrder'.
+class AsPartialOrder c a | c -> a where
+  _PartialOrder :: Prism' c (PartialOrder a)
+
+instance AsPartialOrder (PartialOrder a) a where
+  _PartialOrder = id
+
+instance HasBinaryFunctionT (PartialOrder a) Maybe a Ordering where
+  binaryFunctionT = isBinaryFunctionT
+
+instance AsBinaryFunctionT (PartialOrder a) Maybe a Ordering where
+  _BinaryFunctionT = isBinaryFunctionT
+
+isBinaryFunctionT :: Iso (PartialOrder a) (PartialOrder a') (BinaryFunctionT Maybe a Ordering) (BinaryFunctionT Maybe a' Ordering)
+isBinaryFunctionT = _Wrapped . from _Wrapped
+
+-- | Apply the partial order comparison.
+--
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2
+-- Just LT
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2
+-- Just EQ
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2
+-- Just GT
+runPartialOrder :: PartialOrder a -> a -> a -> Maybe Ordering
+runPartialOrder (PartialOrder f) = f
+
+-- | Test whether @a <= b@ in the partial order.
+-- Returns 'True' iff the comparison yields 'Just' 'LT' or 'Just' 'EQ'.
+-- Returns 'False' for incomparable elements.
+--
+-- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 1 2
+-- True
+-- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 2 2
+-- True
+-- >>> partialOrderLeq (totalOrder :: PartialOrder Int) 3 2
+-- False
+--
+-- >>> import qualified Data.Set as Set
+-- >>> partialOrderLeq (fromLeq Set.isSubsetOf) (Set.fromList [1,2]) (Set.fromList [2,3 :: Int])
+-- False
+partialOrderLeq :: PartialOrder a -> a -> a -> Bool
+partialOrderLeq po a b = case runPartialOrder po a b of
+  Just LT -> True
+  Just EQ -> True
+  _ -> False
+
+-- | Construct a 'PartialOrder' from a total order ('Ord' instance).
+-- The result never yields 'Nothing' since all elements are comparable.
+--
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 1 2
+-- Just LT
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 2 2
+-- Just EQ
+-- >>> runPartialOrder (totalOrder :: PartialOrder Int) 3 2
+-- Just GT
+totalOrder :: (Ord a) => PartialOrder a
+totalOrder = PartialOrder (\a b -> Just (compare a b))
+
+-- | Construct a 'PartialOrder' from a less-than-or-equal predicate.
+--
+-- The predicate should satisfy the partial order laws
+-- (reflexive, antisymmetric, transitive).
+-- Elements where neither @leq a b@ nor @leq b a@ holds are incomparable ('Nothing').
+--
+-- >>> import qualified Data.Set as Set
+-- >>> let po = fromLeq Set.isSubsetOf :: PartialOrder (Set.Set Int)
+-- >>> runPartialOrder po (Set.fromList [1]) (Set.fromList [1,2])
+-- Just LT
+-- >>> runPartialOrder po (Set.fromList [1,2]) (Set.fromList [1,2])
+-- Just EQ
+-- >>> runPartialOrder po (Set.fromList [1,2]) (Set.fromList [1])
+-- Just GT
+-- >>> runPartialOrder po (Set.fromList [1,2]) (Set.fromList [2,3])
+-- Nothing
+fromLeq :: (a -> a -> Bool) -> PartialOrder a
+fromLeq leq = PartialOrder $ \a b ->
+  case (leq a b, leq b a) of
+    (True, True) -> Just EQ
+    (True, False) -> Just LT
+    (False, True) -> Just GT
+    (False, False) -> Nothing
+
+-- |
+-- >>> import Data.Functor.Contravariant (contramap)
+-- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder Int)) 1 2
+-- Just GT
+-- >>> runPartialOrder (contramap negate (totalOrder :: PartialOrder Int)) 2 1
+-- Just LT
+instance Contravariant PartialOrder where
+  contramap f (PartialOrder g) = PartialOrder (\a b -> g (f a) (f b))
+
+-- | Lexicographic composition as a first-class 'Semigroup': compare by the
+-- first partial order; if equal ('Just' 'EQ'), compare by the second.
+-- If the first yields 'Nothing' (incomparable), the result is 'Nothing'.
+--
+-- >>> let po = totalOrder :: PartialOrder Int
+-- >>> runPartialOrder (runSemigroup semigroupPartialOrder po po) 1 2
+-- Just LT
+-- >>> runPartialOrder (runSemigroup semigroupPartialOrder po po) 2 2
+-- Just EQ
+semigroupPartialOrder :: Semigroup (PartialOrder a)
+semigroupPartialOrder = review applySemigroup $ \(PartialOrder f) (PartialOrder g) -> PartialOrder $ \a b ->
+  case f a b of
+    Just EQ -> g a b
+    r -> r
+
+-- |
+-- >>> let po = totalOrder :: PartialOrder Int
+-- >>> runPartialOrder (po <> po) 1 2
+-- Just LT
+-- >>> runPartialOrder (po <> po) 2 2
+-- Just EQ
+instance Prelude.Semigroup (PartialOrder a) where
+  (<>) = runSemigroup semigroupPartialOrder
+
+-- | The trivial partial order where all elements are equal.
+--
+-- >>> runPartialOrder (mempty :: PartialOrder Int) 1 2
+-- Just EQ
+-- >>> runPartialOrder (mempty :: PartialOrder Int) 42 99
+-- Just EQ
+instance Monoid (PartialOrder a) where
+  mempty = PartialOrder (\_ _ -> Just EQ)
+
+-- | Lexicographic product: split @a@ into @(b, c)@, compare by @b@ first,
+-- if equal then compare by @c@. @conquer@ treats all elements as equal.
+--
+-- >>> import Data.Functor.Contravariant.Divisible (divide, conquer)
+-- >>> let po = divide id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder Int)
+-- >>> runPartialOrder po (1, 2) (1, 3)
+-- Just LT
+-- >>> runPartialOrder po (1, 2) (2, 1)
+-- Just LT
+-- >>> runPartialOrder po (1, 2) (1, 2)
+-- Just EQ
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer)
+-- >>> runPartialOrder (conquer :: PartialOrder Int) 1 2
+-- Just EQ
+instance Divisible PartialOrder where
+  conquer = mempty
+  divide f pb pc = contramap (fst . f) pb <> contramap (snd . f) pc
+
+-- | Disjoint sum: classify @a@ as 'Left' @b@ or 'Right' @c@.
+-- Elements on the same side are compared by that side's order.
+-- Elements on different sides are incomparable ('Nothing').
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose, lose)
+-- >>> import Data.Void (Void, absurd)
+-- >>> let po = choose id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder String)
+-- >>> runPartialOrder po (Left 1) (Left 2)
+-- Just LT
+-- >>> runPartialOrder po (Right "a") (Right "b")
+-- Just LT
+-- >>> runPartialOrder po (Left 1) (Right "a")
+-- Nothing
+-- >>> runPartialOrder po (Right "a") (Left 1)
+-- Nothing
+--
+-- >>> import Data.Functor.Contravariant.Divisible (lose)
+-- >>> import Data.Void (Void, absurd)
+-- >>> let po = lose absurd :: PartialOrder Void
+-- >>> seq po ()
+-- ()
+instance Decidable PartialOrder where
+  lose f = PartialOrder (\a _ -> absurd (f a))
+  choose f pb pc = PartialOrder $ \a1 a2 ->
+    case (f a1, f a2) of
+      (Left b1, Left b2) -> runPartialOrder pb b1 b2
+      (Right c1, Right c2) -> runPartialOrder pc c1 c2
+      _ -> Nothing
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divise (divise)
+-- >>> let po = divise id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder Int)
+-- >>> runPartialOrder po (1, 2) (1, 3)
+-- Just LT
+-- >>> runPartialOrder po (1, 2) (1, 2)
+-- Just EQ
+instance Divise PartialOrder where
+  divise = divide
+
+-- |
+-- >>> import Data.Functor.Contravariant.Decide (decide)
+-- >>> let po = decide id (totalOrder :: PartialOrder Int) (totalOrder :: PartialOrder String)
+-- >>> runPartialOrder po (Left 1) (Left 2)
+-- Just LT
+-- >>> runPartialOrder po (Left 1) (Right "a")
+-- Nothing
+instance Decide PartialOrder where
+  decide = choose
+
+-- |
+-- >>> import Data.Functor.Contravariant.Conclude (conclude)
+-- >>> import Data.Void (absurd)
+-- >>> let po = conclude absurd :: PartialOrder Void
+-- >>> seq po ()
+-- ()
+instance Conclude PartialOrder where
+  conclude = lose
diff --git a/src/Data/Valuation/PresheafValuationAlgebra.hs b/src/Data/Valuation/PresheafValuationAlgebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/PresheafValuationAlgebra.hs
@@ -0,0 +1,341 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | The presheaf formulation of a valuation algebra, following
+-- Shenoy & Shafer (1990), Kohlas (2003), and Abramsky & Carù (2019).
+--
+-- In this formulation, valuations form a presheaf F over a domain lattice:
+--
+-- * For each domain d, F(d) is the set of valuations with domain d
+-- * For d' <= d, the restriction map rho_{d,d'}: F(d) -> F(d') implements marginalisation
+-- * Combination is a family of maps: F(d1) x F(d2) -> F(d1 \/ d2)
+--
+-- A 'PresheafValuationAlgebra' bundles a 'DomainLattice' with a 'ValuationAlgebra',
+-- providing all the structure needed for the presheaf formulation with
+-- operations that work directly on 'Valuation' values.
+module Data.Valuation.PresheafValuationAlgebra
+  ( PresheafValuationAlgebra (..),
+    SetPresheafValuationAlgebra,
+    HasPresheafValuationAlgebra (..),
+    AsPresheafValuationAlgebra (..),
+    marginalise,
+    combine,
+    neutralValuation,
+    nullValuation,
+    presheafCombineSemigroup,
+
+    -- * laws
+    lawTransitivity,
+    lawCombinationDomain,
+    lawMarginalisationIdentity,
+    lawNeutralCombination,
+    lawNullCombination,
+    lawCombinationCommutative,
+  )
+where
+
+import Control.Lens (Lens', Prism', review, view, _Wrapped)
+import Data.Set (Set)
+import Data.Valuation.DomainLattice
+  ( DomainLattice (..),
+    HasDomainLattice (..),
+    runDomainJoin,
+    runDomainLeq,
+  )
+import Data.Valuation.ProjectValuation (HasProjectValuation (..))
+import Data.Valuation.SemiValuationAlgebra
+  ( HasSemiValuationAlgebra (..),
+  )
+import Data.Valuation.Semigroup
+  ( HasSemigroup (..),
+    Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Data.Valuation.Valuation
+  ( HasValuation (valuationDomain, valuationInformation),
+    Valuation (..),
+  )
+import Data.Valuation.ValuationAlgebra
+  ( HasValuationAlgebra (..),
+    ValuationAlgebra (..),
+  )
+import Prelude hiding (Semigroup)
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+-- >>> import qualified Data.Set as Set
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (applySemigroup, runSemigroup)
+-- >>> import Data.Valuation.DomainLattice (setDomainLattice, runDomainJoin)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Prelude hiding (Semigroup)
+
+-- |
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> let v1 = Valuation (Set.fromList [1,2]) 10 :: Valuation Set Int Int
+-- >>> let v2 = Valuation (Set.fromList [2,3]) 20
+-- >>> combine pva v1 v2
+-- Valuation (fromList [1,2,3]) 30
+data PresheafValuationAlgebra v set var
+  = PresheafValuationAlgebra
+      -- | lattice structure on domains
+      (DomainLattice (set var) (set var))
+      -- | the valuation algebra
+      (ValuationAlgebra v set var)
+
+-- | A 'PresheafValuationAlgebra' specialised to 'Set'.
+type SetPresheafValuationAlgebra v var =
+  PresheafValuationAlgebra v Set var
+
+-- | Classy lens for types that contain a 'PresheafValuationAlgebra'.
+class HasPresheafValuationAlgebra c v set var | c -> v set var where
+  presheafValuationAlgebra :: Lens' c (PresheafValuationAlgebra v set var)
+
+instance HasPresheafValuationAlgebra (PresheafValuationAlgebra v set var) v set var where
+  presheafValuationAlgebra = id
+
+-- | Classy prism for types that can be constructed from a 'PresheafValuationAlgebra'.
+class AsPresheafValuationAlgebra c v set var | c -> v set var where
+  _PresheafValuationAlgebra :: Prism' c (PresheafValuationAlgebra v set var)
+
+instance AsPresheafValuationAlgebra (PresheafValuationAlgebra v set var) v set var where
+  _PresheafValuationAlgebra = id
+
+instance HasDomainLattice (PresheafValuationAlgebra v set var) (set var) (set var) where
+  domainLattice f (PresheafValuationAlgebra l a) = fmap (`PresheafValuationAlgebra` a) (f l)
+
+instance HasValuationAlgebra (PresheafValuationAlgebra v set var) v set var where
+  valuationAlgebra f (PresheafValuationAlgebra l a) = fmap (PresheafValuationAlgebra l) (f a)
+
+instance HasSemiValuationAlgebra (PresheafValuationAlgebra v set var) v set var where
+  semiValuationAlgebra = valuationAlgebra . semiValuationAlgebra
+
+instance HasSemigroup (PresheafValuationAlgebra v set var) v where
+  semigroup = semiValuationAlgebra . semigroup
+
+instance HasProjectValuation (PresheafValuationAlgebra v set var) v set var where
+  projectValuation = semiValuationAlgebra . projectValuation
+
+-- | Marginalise a valuation to a subdomain: the restriction map of the presheaf.
+--
+-- Given a target domain @d'@ and a valuation phi with domain @d@,
+-- computes @phi↓d'@ with @d(phi↓d') = d'@.
+--
+-- This is the presheaf restriction map: @rho_{d,d'}: F(d) -> F(d')@.
+--
+-- The caller should ensure @d' <= d(phi)@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + Set.size s))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> marginalise pva (Set.fromList [1]) (Valuation (Set.fromList [1,2]) 10)
+-- Valuation (fromList [1]) 11
+{-# SPECIALIZE marginalise ::
+  PresheafValuationAlgebra v set var -> set var -> Valuation set var v -> Valuation set var v
+  #-}
+marginalise :: (HasProjectValuation algebra v set var, HasValuation valuation set' var' v) => algebra -> set var -> valuation -> Valuation set var v
+marginalise algebra targetDomain =
+  Valuation targetDomain . view (projectValuation . _Wrapped) algebra targetDomain . view valuationInformation
+
+-- | Combine two valuations: the combination operation of the valuation algebra.
+--
+-- Computes @phi ⊗ psi@ with @d(phi ⊗ psi) = d(phi) \/ d(psi)@.
+--
+-- The information values are combined using the algebra's semigroup,
+-- and the result has the joined domain.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> combine pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20)
+-- Valuation (fromList [1,2,3]) 30
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> combine pva (Valuation (Set.fromList [1]) 3) (Valuation (Set.fromList [2]) 4)
+-- Valuation (fromList [1,2]) 12
+{-# SPECIALIZE combine ::
+  PresheafValuationAlgebra v set var -> Valuation set var v -> Valuation set var v -> Valuation set var v
+  #-}
+combine ::
+  (HasSemigroup s1 a, HasDomainLattice s1 (set var) p, HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Valuation set var a
+combine alg phi =
+  Valuation . runSemigroup (view domainLatticeJoin alg) (view valuationDomain phi) . view valuationDomain <*> runSemigroup (view semigroup alg) (view valuationInformation phi) . view valuationInformation
+
+-- | The neutral valuation for a domain: @e_d@ such that @e_d ⊗ phi = phi@
+-- for all phi with @d(phi) <= d@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> neutralValuation pva (Set.fromList [1,2])
+-- Valuation (fromList [1,2]) 0
+{-# SPECIALIZE neutralValuation ::
+  PresheafValuationAlgebra v set var -> set var -> Valuation set var v
+  #-}
+neutralValuation :: (HasValuationAlgebra s a set var) => s -> set var -> Valuation set var a
+neutralValuation algebra =
+  Valuation <*> view (valuationAlgebra . valuationAlgebraUnit . _Wrapped) algebra
+
+-- | The null/zero valuation for a domain: @z_d@ such that @z_d ⊗ phi = z_{d \/ d(phi)}@
+-- for all phi.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 99)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> nullValuation pva (Set.fromList [1,2])
+-- Valuation (fromList [1,2]) 99
+{-# SPECIALIZE nullValuation ::
+  PresheafValuationAlgebra v set var -> set var -> Valuation set var v
+  #-}
+nullValuation :: (HasValuationAlgebra s a set var) => s -> set var -> Valuation set var a
+nullValuation algebra =
+  Valuation <*> view (valuationAlgebra . valuationAlgebraZero . _Wrapped) algebra
+
+-- | A first-class 'Semigroup' on 'Valuation' derived from the presheaf algebra's
+-- combination operation.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> let sg = presheafCombineSemigroup pva
+-- >>> runSemigroup sg (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20)
+-- Valuation (fromList [1,2]) 30
+{-# SPECIALIZE presheafCombineSemigroup ::
+  PresheafValuationAlgebra v set var -> Semigroup (Valuation set var v)
+  #-}
+presheafCombineSemigroup :: (HasSemigroup algebra v, HasDomainLattice algebra (set var) p) => algebra -> Semigroup (Valuation set var v)
+presheafCombineSemigroup = review applySemigroup . combine
+
+-- | Transitivity of marginalisation: @(phi↓d')↓d'' = phi↓d''@ for @d'' <= d' <= d(phi)@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> let phi = Valuation (Set.fromList [1,2,3]) 10
+-- >>> lawTransitivity pva (Set.fromList [1,2]) (Set.fromList [1]) phi
+-- True
+{-# SPECIALIZE lawTransitivity ::
+  (Eq v) => PresheafValuationAlgebra v set var -> set var -> set var -> Valuation set var v -> Bool
+  #-}
+lawTransitivity :: (Eq a, HasProjectValuation p a set var, HasValuation q set' var' a) => p -> set var -> set var -> q -> Bool
+lawTransitivity pva d' d'' phi =
+  let step = marginalise pva d'' (marginalise pva d' phi)
+      direct = marginalise pva d'' phi
+      valuationInfo = view valuationInformation
+   in valuationInfo step == valuationInfo direct
+
+-- | Domain of combination: @d(phi ⊗ psi) = d(phi) \/ d(psi)@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> lawCombinationDomain pva (Valuation (Set.fromList [1,2]) 10) (Valuation (Set.fromList [2,3]) 20)
+-- True
+{-# SPECIALIZE lawCombinationDomain ::
+  (Eq (set var)) => PresheafValuationAlgebra v set var -> Valuation set var v -> Valuation set var v -> Bool
+  #-}
+lawCombinationDomain :: (HasSemigroup s1 a, Eq (set var), HasValuation s2 set var a, HasValuation s3 set var a, HasDomainLattice s1 (set var) p) => s1 -> s2 -> s3 -> Bool
+lawCombinationDomain pva val1 val2 =
+  let lat = view domainLattice pva
+      d1 = view valuationDomain val1
+      d2 = view valuationDomain val2
+      d = view valuationDomain (combine pva val1 val2)
+   in d == runDomainJoin lat d1 d2
+
+-- | Marginalisation identity: @phi↓d(phi) = phi@ (marginalising to own domain is identity).
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> lawMarginalisationIdentity pva (Valuation (Set.fromList [1,2]) 42)
+-- True
+{-# SPECIALIZE lawMarginalisationIdentity ::
+  (Eq (set var), Eq v) => PresheafValuationAlgebra v set var -> Valuation set var v -> Bool
+  #-}
+lawMarginalisationIdentity :: (Eq a, Eq (set var), HasValuation s set var a, HasProjectValuation p a set var) => p -> s -> Bool
+lawMarginalisationIdentity pva val =
+  let d = view valuationDomain val
+      v = view valuationInformation val
+      Valuation d' v' = marginalise pva d val
+   in d' == d && v' == v
+
+-- | Neutral element axiom: @combine pva (neutralValuation pva d) phi = phi@
+-- when @d(phi) <= d@ (the neutral valuation is an identity for combination).
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> let phi = Valuation (Set.fromList [1]) 42
+-- >>> lawNeutralCombination pva (Set.fromList [1,2]) phi
+-- True
+{-# SPECIALIZE lawNeutralCombination ::
+  (Eq (set var), Eq v) => PresheafValuationAlgebra v set var -> set var -> Valuation set var v -> Bool
+  #-}
+lawNeutralCombination :: (HasSemigroup s1 a, Eq a, Eq (set var), HasDomainLattice s1 (set var) (set var), HasValuation s2 set var a, HasValuationAlgebra s1 a set var) => s1 -> set var -> s2 -> Bool
+lawNeutralCombination pva d phi =
+  let lat = view domainLattice pva
+      dPhi = view valuationDomain phi
+      vPhi = view valuationInformation phi
+   in not (runDomainLeq lat dPhi d)
+        || let Valuation d' v' = combine pva (neutralValuation pva d) phi
+               expectedDomain = runDomainJoin lat d dPhi
+            in d' == expectedDomain && v' == vPhi
+
+-- | Null element axiom: @combine pva (nullValuation pva d) phi = nullValuation pva (d \/ d(phi))@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (*)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> let phi = Valuation (Set.fromList [1]) 42
+-- >>> lawNullCombination pva (Set.fromList [2]) phi
+-- True
+{-# SPECIALIZE lawNullCombination ::
+  (Eq (set var), Eq v) => PresheafValuationAlgebra v set var -> set var -> Valuation set var v -> Bool
+  #-}
+lawNullCombination :: (HasSemigroup s1 a, Eq a, Eq (set var), HasValuation s2 set var a, HasDomainLattice s1 (set var) p, HasValuationAlgebra s1 a set var) => s1 -> set var -> s2 -> Bool
+lawNullCombination pva d phi =
+  let lat = view domainLattice pva
+      dPhi = view valuationDomain phi
+      lhs = combine pva (nullValuation pva d) phi
+      expectedDomain = runDomainJoin lat d dPhi
+      rhs = nullValuation pva expectedDomain
+      valuationDom = view valuationDomain
+      valuationInfo = view valuationInformation
+   in valuationDom lhs == valuationDom rhs && valuationInfo lhs == valuationInfo rhs
+
+-- | Combination is commutative: @phi ⊗ psi = psi ⊗ phi@.
+--
+-- >>> let lat = setDomainLattice :: DomainLattice (Set Int) (Set Int)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\_ v -> v))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 0)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int Set Int
+-- >>> let pva = PresheafValuationAlgebra lat va
+-- >>> lawCombinationCommutative pva (Valuation (Set.fromList [1]) 10) (Valuation (Set.fromList [2]) 20)
+-- True
+{-# SPECIALIZE lawCombinationCommutative ::
+  (Eq (set var), Eq v) => PresheafValuationAlgebra v set var -> Valuation set var v -> Valuation set var v -> Bool
+  #-}
+lawCombinationCommutative :: (HasSemigroup s1 a, Eq a, Eq (set var), HasDomainLattice s1 (set var) p, HasValuation s2 set var a, HasValuation s3 set var a) => s1 -> s2 -> s3 -> Bool
+lawCombinationCommutative pva phi psi =
+  let Valuation d1 v1 = combine pva phi psi
+      Valuation d2 v2 = combine pva psi phi
+   in d1 == d2 && v1 == v2
diff --git a/src/Data/Valuation/ProjectValuation.hs b/src/Data/Valuation/ProjectValuation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/ProjectValuation.hs
@@ -0,0 +1,210 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A projection function that updates a value given a set of variables.
+module Data.Valuation.ProjectValuation
+  ( ProjectValuation (..),
+    SetProjectValuation,
+
+    -- * optics
+    HasProjectValuation (..),
+    AsProjectValuation (..),
+
+    -- * combinators
+    semigroupProjectValuation,
+    applyHasProjectValuation,
+    applyAsProjectValuation,
+  )
+where
+
+import Control.Lens
+  ( Lens',
+    Prism',
+    Rewrapped,
+    Wrapped (..),
+    iso,
+    review,
+    _Wrapped,
+  )
+import Data.Functor.Contravariant (Contravariant (..))
+import Data.Functor.Contravariant.Conclude (Conclude (..))
+import Data.Functor.Contravariant.Decide (Decide (..))
+import Data.Functor.Contravariant.Divise (Divise (..))
+import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..))
+import Data.Set (Set)
+import Data.Valuation.Semigroup
+  ( Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Witherable (Filterable (mapMaybe))
+import Prelude hiding (Semigroup)
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+-- >>> import Data.Void (Void)
+
+-- |
+-- >>> let ProjectValuation f = ProjectValuation (\s v -> v + sum s) in f [1,2,3] (10 :: Int)
+-- 16
+--
+-- >>> let ProjectValuation f = ProjectValuation (\s v -> v + length s) in f [1,2,3] (10 :: Int)
+-- 13
+newtype ProjectValuation v set var
+  = ProjectValuation (set var -> v -> v)
+
+instance
+  (ProjectValuation v set var ~ t) =>
+  Rewrapped (ProjectValuation v' set' var') t
+
+instance Wrapped (ProjectValuation v set var) where
+  type Unwrapped (ProjectValuation v set var) = set var -> v -> v
+  _Wrapped' = iso (\(ProjectValuation x) -> x) ProjectValuation
+
+-- | Classy lens for types that contain a 'ProjectValuation'.
+class HasProjectValuation c v set var | c -> v set var where
+  projectValuation :: Lens' c (ProjectValuation v set var)
+
+instance HasProjectValuation (ProjectValuation v set var) v set var where
+  projectValuation = id
+
+-- | Classy prism for types that can be constructed from a 'ProjectValuation'.
+class AsProjectValuation c v set var | c -> v set var where
+  _ProjectValuation :: Prism' c (ProjectValuation v set var)
+
+instance AsProjectValuation (ProjectValuation v set var) v set var where
+  _ProjectValuation = id
+
+-- | Lens to the underlying function of a 'HasProjectValuation'.
+applyHasProjectValuation :: (HasProjectValuation pv v set var) => Lens' pv (set var -> v -> v)
+applyHasProjectValuation = projectValuation . _Wrapped
+
+-- | Prism to the underlying function of an 'AsProjectValuation'.
+applyAsProjectValuation :: (AsProjectValuation pv v set var) => Prism' pv (set var -> v -> v)
+applyAsProjectValuation = _ProjectValuation . _Wrapped
+
+-- |
+-- >>> import Data.Functor.Contravariant (contramap)
+-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = contramap (*2) pv in f [1,2,3] 10
+-- 22
+--
+-- >>> import Data.Functor.Contravariant (contramap)
+-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = contramap negate pv in f [1,2,3] 0
+-- -6
+instance (Functor set) => Contravariant (ProjectValuation v set) where
+  contramap f (ProjectValuation g) = ProjectValuation (g . fmap f)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let ProjectValuation f = conquer :: ProjectValuation Int [] Int in f [1,2,3] 42
+-- 42
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let ProjectValuation f = conquer :: ProjectValuation String [] Char in f "abc" "hello"
+-- "hello"
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = divide (\x -> (x, x * 10)) pvB pvC in f [1,2,3] 5
+-- 21
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = divide (\x -> (x, x)) pvB pvC in f [1,2,3] 5
+-- 21
+instance (Functor set) => Divisible (ProjectValuation v set) where
+  conquer = ProjectValuation (const id)
+  divide split (ProjectValuation pb) (ProjectValuation pc) =
+    ProjectValuation (\fa v -> pb (fmap (fst . split) fa) (pc (fmap (snd . split) fa) v))
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (choose, lose)
+-- >>> import Data.Void (Void, absurd)
+-- >>> let ProjectValuation f = lose absurd :: ProjectValuation Int [] Void in f [] 42
+-- 42
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = choose (\x -> if even x then Left x else Right x) pvB pvC in f [1,2,3,4] 10
+-- 26
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = choose Left pvB pvC in f [1,2,3] 10
+-- 6
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = choose Right pvB pvC in f [1,2,3] 10
+-- 30
+instance (Filterable set) => Decidable (ProjectValuation v set) where
+  lose _ = ProjectValuation (const id)
+  choose ch (ProjectValuation pb) (ProjectValuation pc) =
+    ProjectValuation
+      ( \fa v ->
+          let fb = mapMaybe (either Just (const Nothing) . ch) fa
+              fc = mapMaybe (either (const Nothing) Just . ch) fa
+           in pb fb (pc fc v)
+      )
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divise (divise)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = divise (\x -> (x, x * 10)) pvB pvC in f [1,2,3] 5
+-- 21
+instance (Functor set) => Divise (ProjectValuation v set) where
+  divise = divide
+
+-- |
+-- >>> import Data.Functor.Contravariant.Decide (decide)
+-- >>> let pvB = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let pvC = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = decide (\x -> if even x then Left x else Right x) pvB pvC in f [1,2,3,4] 10
+-- 26
+instance (Filterable set) => Decide (ProjectValuation v set) where
+  decide = choose
+
+-- |
+-- >>> import Data.Functor.Contravariant.Conclude (conclude)
+-- >>> import Data.Void (absurd)
+-- >>> let ProjectValuation f = conclude absurd :: ProjectValuation Int [] Void in f [] 42
+-- 42
+instance (Filterable set) => Conclude (ProjectValuation v set) where
+  conclude _ = ProjectValuation (const id)
+
+-- |
+-- >>> let ProjectValuation f = runSemigroup semigroupProjectValuation (ProjectValuation (\_ v -> v + 1)) (ProjectValuation (\_ v -> v * 2)) in f [] (3 :: Int)
+-- 7
+semigroupProjectValuation :: Semigroup (ProjectValuation v set var)
+semigroupProjectValuation = review applySemigroup (\(ProjectValuation p1) (ProjectValuation p2) -> ProjectValuation (\s -> p1 s . p2 s))
+
+-- |
+-- >>> let p1 = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let p2 = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = p1 <> p2 in f [1,2,3] 5
+-- 21
+instance Prelude.Semigroup (ProjectValuation v set var) where
+  (<>) = runSemigroup semigroupProjectValuation
+
+-- |
+-- >>> let p = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> let ProjectValuation f = mempty <> p in f [1,2,3] 5
+-- 11
+instance Monoid (ProjectValuation v set var) where
+  mempty = ProjectValuation (const id)
+
+-- | A 'ProjectValuation' specialised to 'Set'.
+type SetProjectValuation v var =
+  ProjectValuation v Set var
diff --git a/src/Data/Valuation/SemiValuationAlgebra.hs b/src/Data/Valuation/SemiValuationAlgebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/SemiValuationAlgebra.hs
@@ -0,0 +1,183 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A semi-valuation algebra: a semigroup paired with a projection.
+module Data.Valuation.SemiValuationAlgebra
+  ( SemiValuationAlgebra (..),
+    SetSemiValuationAlgebra,
+
+    -- * optics
+    HasSemiValuationAlgebra (..),
+    AsSemiValuationAlgebra (..),
+
+    -- * combinators
+    projectValuation',
+  )
+where
+
+import Control.Lens
+  ( Lens,
+    Lens',
+    Prism',
+    review,
+  )
+import Data.Functor.Contravariant (Contravariant (..))
+import Data.Functor.Contravariant.Conclude (Conclude (..))
+import Data.Functor.Contravariant.Decide (Decide (..))
+import Data.Functor.Contravariant.Divise (Divise (..))
+import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..))
+import Data.Set (Set)
+import Data.Valuation.ProjectValuation
+  ( HasProjectValuation (..),
+    ProjectValuation (..),
+  )
+import Data.Valuation.Semigroup
+  ( HasSemigroup (..),
+    Semigroup,
+    applySemigroup,
+  )
+import Witherable (Filterable)
+import Prelude hiding (Semigroup)
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (applySemigroup, runSemigroup)
+-- >>> import Data.Void (Void)
+-- >>> import Prelude hiding (Semigroup)
+
+-- |
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra Int [] Int
+-- >>> runSemigroup sg 3 4
+-- 7
+-- >>> p [1,2,3] 10
+-- 16
+data SemiValuationAlgebra v set var
+  = SemiValuationAlgebra
+      -- | algebra combine
+      (Semigroup v)
+      -- | algebra project
+      (ProjectValuation v set var)
+
+-- | Type-changing lens to the 'ProjectValuation' component.
+projectValuation' :: Lens (SemiValuationAlgebra v set var) (SemiValuationAlgebra v set' var') (ProjectValuation v set var) (ProjectValuation v set' var')
+projectValuation' f (SemiValuationAlgebra s p) = fmap (SemiValuationAlgebra s) (f p)
+
+-- | Classy lens for types that contain a 'SemiValuationAlgebra'.
+class HasSemiValuationAlgebra c v set var | c -> v set var where
+  semiValuationAlgebra ::
+    Lens' c (SemiValuationAlgebra v set var)
+
+instance HasSemiValuationAlgebra (SemiValuationAlgebra v set var) v set var where
+  semiValuationAlgebra = id
+
+-- | Classy prism for types that can be constructed from a 'SemiValuationAlgebra'.
+class AsSemiValuationAlgebra c v set var | c -> v set var where
+  _SemiValuationAlgebra ::
+    Prism' c (SemiValuationAlgebra v set var)
+
+instance AsSemiValuationAlgebra (SemiValuationAlgebra v set var) v set var where
+  _SemiValuationAlgebra = id
+
+instance HasSemigroup (SemiValuationAlgebra v set var) v where
+  semigroup f (SemiValuationAlgebra s p) = fmap (`SemiValuationAlgebra` p) (f s)
+
+instance HasProjectValuation (SemiValuationAlgebra v set var) v set var where
+  projectValuation = projectValuation'
+
+-- |
+-- >>> import Data.Functor.Contravariant (contramap)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra Int [] Int
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = contramap (*2) sva
+-- >>> runSemigroup sg 3 4
+-- 7
+-- >>> p [1,2,3] 10
+-- 22
+instance (Functor set) => Contravariant (SemiValuationAlgebra v set) where
+  contramap f (SemiValuationAlgebra s p) = SemiValuationAlgebra s (contramap f p)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conquer :: SemiValuationAlgebra [Int] [] Int
+-- >>> runSemigroup sg [1,2] [3,4]
+-- [1,2,3,4]
+-- >>> p [10,20,30] [42]
+-- [42]
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = divide (\x -> (x, x + 10)) sva1 sva2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [1,2,3] [0]
+-- [0,13,12,11,1,2,3]
+instance (Functor set, Prelude.Semigroup v) => Divisible (SemiValuationAlgebra v set) where
+  conquer = SemiValuationAlgebra (review applySemigroup (<>)) conquer
+  divide f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) =
+    SemiValuationAlgebra s (divide f p1 p2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (choose, lose)
+-- >>> import Data.Void (Void, absurd)
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = lose absurd :: SemiValuationAlgebra [Int] [] Void
+-- >>> runSemigroup sg [1,2] [3,4]
+-- [1,2,3,4]
+-- >>> p [] [42]
+-- [42]
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = choose (\x -> if even x then Left x else Right x) sva1 sva2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [1,2,3,4] [0]
+-- [0,-1,-3,2,4]
+instance (Filterable set, Prelude.Semigroup v) => Decidable (SemiValuationAlgebra v set) where
+  lose f = SemiValuationAlgebra (review applySemigroup (<>)) (lose f)
+  choose f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) =
+    SemiValuationAlgebra s (choose f p1 p2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divise (divise)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = divise (\x -> (x, x + 10)) sva1 sva2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [1,2,3] [0]
+-- [0,13,12,11,1,2,3]
+instance (Functor set) => Divise (SemiValuationAlgebra v set) where
+  divise f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) =
+    SemiValuationAlgebra s (divise f p1 p2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Decide (decide)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ map negate s)) :: SemiValuationAlgebra [Int] [] Int
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = decide (\x -> if even x then Left x else Right x) sva1 sva2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [1,2,3,4] [0]
+-- [0,-1,-3,2,4]
+instance (Filterable set) => Decide (SemiValuationAlgebra v set) where
+  decide f (SemiValuationAlgebra s p1) (SemiValuationAlgebra _ p2) =
+    SemiValuationAlgebra s (decide f p1 p2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Conclude (conclude)
+-- >>> import Data.Void (absurd)
+-- >>> let SemiValuationAlgebra sg (ProjectValuation p) = conclude absurd :: SemiValuationAlgebra [Int] [] Void
+-- >>> runSemigroup sg [1,2] [3,4]
+-- [1,2,3,4]
+-- >>> p [] [42]
+-- [42]
+instance (Filterable set, Prelude.Semigroup v) => Conclude (SemiValuationAlgebra v set) where
+  conclude f = SemiValuationAlgebra (review applySemigroup (<>)) (conclude f)
+
+-- | A 'SemiValuationAlgebra' specialised to 'Set'.
+type SetSemiValuationAlgebra v var =
+  SemiValuationAlgebra v Set var
diff --git a/src/Data/Valuation/Semigroup.hs b/src/Data/Valuation/Semigroup.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/Semigroup.hs
@@ -0,0 +1,672 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | First-class semigroup values, independent of the 'Prelude.Semigroup' type class.
+module Data.Valuation.Semigroup
+  ( Semigroup (..),
+
+    -- * optics
+    HasSemigroup (..),
+    AsSemigroup (..),
+
+    -- * combinators
+    applySemigroup,
+    applyHasSemigroup,
+    applyAsSemigroup,
+    semigroup',
+    runSemigroup,
+    liftSemigroup,
+    liftRunSemigroup,
+
+    -- * semigroup values
+    first,
+    second,
+    dual,
+    min,
+    max,
+    sum,
+    product,
+    Data.Valuation.Semigroup.all,
+    Data.Valuation.Semigroup.any,
+    endo,
+    endoDual,
+    unit,
+    pair,
+    ordering,
+    Data.Valuation.Semigroup.maybe,
+    list,
+    nonEmpty,
+    io,
+    Data.Valuation.Semigroup.either,
+    void,
+    byteArray,
+    event,
+    comparison,
+    equivalence,
+    predicate,
+    op,
+    Data.Valuation.Semigroup.and,
+    ior,
+    Data.Valuation.Semigroup.xor,
+    iff,
+    wrappedMonoid,
+    identity,
+    down,
+    dualM,
+    solo,
+    stm,
+    st,
+    function,
+    const',
+    alt,
+    proxy,
+    lifetime,
+    tuple3,
+    tuple4,
+    tuple5,
+    u1,
+    v1,
+    par1,
+    rec1,
+    k1,
+    m1,
+    productG,
+    composeG,
+    productF,
+    composeF,
+
+    -- * laws
+    lawAssociative,
+  )
+where
+
+-- \$setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults -XTypeOperators
+-- >>> import Prelude hiding (Semigroup, min, max, sum, product, all, any, and, either, maybe)
+
+import Control.Applicative (Alternative ((<|>)))
+import Control.Lens
+  ( Iso,
+    Lens',
+    Prism',
+    Rewrapped,
+    Wrapped (..),
+    iso,
+    review,
+    _Wrapped,
+  )
+import Control.Monad.ST (ST)
+import Data.Array.Byte (ByteArray)
+import Data.Bits (Bits (complement, xor, (.&.), (.|.)), FiniteBits)
+import Data.Functor.Compose (Compose (..))
+import Data.Functor.Const (Const (..))
+import Data.Functor.Contravariant
+  ( Comparison,
+    Equivalence,
+    Predicate,
+  )
+import Data.Functor.Identity (Identity)
+import Data.Functor.Product (Product (..))
+import Data.List.NonEmpty (NonEmpty (..))
+import Data.Ord (Down (..))
+import Data.Proxy (Proxy (..))
+import Data.Tuple (Solo)
+import Data.Void (Void, absurd)
+import GHC.Conc (STM)
+import GHC.Event (Event, Lifetime)
+import GHC.Generics (K1 (..), M1 (..), Par1 (..), Rec1 (..), U1 (..), V1, type (:*:) (..), type (:.:) (..))
+import Prelude hiding (Semigroup, max, min, product, sum)
+import qualified Prelude
+
+-- | A first-class semigroup: an associative binary operation on @a@.
+newtype Semigroup a
+  = Semigroup (a -> a -> a)
+
+instance (Semigroup a ~ t) => Rewrapped (Semigroup a') t
+
+instance Wrapped (Semigroup a) where
+  type Unwrapped (Semigroup a) = a -> a -> a
+  _Wrapped' = iso (\(Semigroup x) -> x) Semigroup
+
+-- | Classy lens for types that contain a 'Semigroup'.
+class HasSemigroup c a | c -> a where
+  semigroup :: Lens' c (Semigroup a)
+
+instance HasSemigroup (Semigroup a) a where
+  semigroup = id
+
+-- | Classy prism for types that can be constructed from a 'Semigroup'.
+class AsSemigroup c a | c -> a where
+  _Semigroup :: Prism' c (Semigroup a)
+
+instance AsSemigroup (Semigroup a) a where
+  _Semigroup = id
+
+-- | Iso between a 'Semigroup' and its underlying binary operation.
+applySemigroup :: Iso (Semigroup a) (Semigroup a') (a -> a -> a) (a' -> a' -> a')
+applySemigroup = _Wrapped
+
+-- | Lens to the underlying binary operation of a 'HasSemigroup'.
+applyHasSemigroup :: (HasSemigroup s a) => Lens' s (a -> a -> a)
+applyHasSemigroup = semigroup . applySemigroup
+
+-- | Prism to the underlying binary operation of an 'AsSemigroup'.
+applyAsSemigroup :: (AsSemigroup s a) => Prism' s (a -> a -> a)
+applyAsSemigroup = _Semigroup . applySemigroup
+
+-- |
+-- >>> lawAssociative sum (1 :: Int) 2 3
+-- True
+--
+-- >>> lawAssociative product (2 :: Int) 3 4
+-- True
+--
+-- >>> lawAssociative list [1,2] [3,4] [5 :: Int,6]
+-- True
+--
+-- >>> lawAssociative min (3 :: Int) 1 2
+-- True
+--
+-- >>> lawAssociative max (3 :: Int) 1 2
+-- True
+--
+-- >>> lawAssociative ordering LT EQ GT
+-- True
+--
+-- >>> lawAssociative (review applySemigroup (&&)) True False True
+-- True
+--
+-- >>> lawAssociative (review applySemigroup (||)) True False True
+-- True
+--
+-- >>> lawAssociative (pair sum product) (1,2) (3,4) (5 :: Int,6 :: Int)
+-- True
+--
+-- >>> lawAssociative (Data.Valuation.Semigroup.maybe sum) (Just 1) Nothing (Just 3 :: Maybe Int)
+-- True
+--
+-- >>> lawAssociative nonEmpty (1 :| [2]) (3 :| []) (4 :| [5 :: Int])
+-- True
+--
+-- >>> lawAssociative first (1 :: Int) 2 3
+-- True
+--
+-- >>> lawAssociative second (1 :: Int) 2 3
+-- True
+lawAssociative :: (Eq a) => Semigroup a -> a -> a -> a -> Bool
+lawAssociative s a b c =
+  let f = runSemigroup s
+   in f (f a b) c == f a (f b c)
+
+-- |
+-- >>> runSemigroup semigroup' "ab" "cd" :: String
+-- "abcd"
+semigroup' :: (Prelude.Semigroup a) => Semigroup a
+semigroup' = review applySemigroup (<>)
+
+-- |
+-- >>> runSemigroup sum 3 4 :: Int
+-- 7
+runSemigroup :: Semigroup a -> a -> a -> a
+runSemigroup (Semigroup f) = f
+
+-- | Map a 'Semigroup' through an isomorphism (unwrap, wrap).
+mapSemigroup :: (b -> a) -> (a -> b) -> Semigroup a -> Semigroup b
+mapSemigroup unwrap wrap s = review applySemigroup (\b1 b2 -> wrap (runSemigroup s (unwrap b1) (unwrap b2)))
+
+-- |
+-- >>> runSemigroup (liftSemigroup sum) [1, 2] [10, 20] :: [Int]
+-- [11,21,12,22]
+--
+-- >>> runSemigroup (liftSemigroup sum) (Just 3) (Just 4) :: Maybe Int
+-- Just 7
+liftSemigroup :: (Applicative f) => Semigroup a -> Semigroup (f a)
+liftSemigroup = review applySemigroup . liftA2 . runSemigroup
+
+-- |
+-- >>> liftRunSemigroup sum [1, 2] [10, 20] :: [Int]
+-- [11,21,12,22]
+liftRunSemigroup :: (Applicative f) => Semigroup a -> f a -> f a -> f a
+liftRunSemigroup = liftA2 . runSemigroup
+
+-- |
+-- >>> runSemigroup first 1 2 :: Int
+-- 1
+--
+-- >>> runSemigroup first "a" "b"
+-- "a"
+first :: Semigroup a
+first = review applySemigroup const
+
+-- |
+-- >>> runSemigroup second 1 2 :: Int
+-- 2
+--
+-- >>> runSemigroup second "a" "b"
+-- "b"
+second :: Semigroup a
+second = review applySemigroup (const id)
+
+-- |
+-- >>> runSemigroup (dual first) 1 2 :: Int
+-- 2
+--
+-- >>> runSemigroup (dual second) 1 2 :: Int
+-- 1
+dual :: Semigroup a -> Semigroup a
+dual = review applySemigroup . flip . runSemigroup
+
+-- |
+-- >>> runSemigroup min 3 5 :: Int
+-- 3
+--
+-- >>> runSemigroup min 5 3 :: Int
+-- 3
+min :: (Ord a) => Semigroup a
+min = review applySemigroup Prelude.min
+
+-- |
+-- >>> runSemigroup max 3 5 :: Int
+-- 5
+--
+-- >>> runSemigroup max 5 3 :: Int
+-- 5
+max :: (Ord a) => Semigroup a
+max = review applySemigroup Prelude.max
+
+-- |
+-- >>> runSemigroup sum 3 4 :: Int
+-- 7
+--
+-- >>> runSemigroup sum 0 5 :: Int
+-- 5
+sum :: (Num a) => Semigroup a
+sum = review applySemigroup (+)
+
+-- |
+-- >>> runSemigroup product 3 4 :: Int
+-- 12
+--
+-- >>> runSemigroup product 1 5 :: Int
+-- 5
+product :: (Num a) => Semigroup a
+product = review applySemigroup (*)
+
+-- |
+-- >>> runSemigroup Data.Valuation.Semigroup.all True True
+-- True
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.all True False
+-- False
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.all False False
+-- False
+all :: Semigroup Bool
+all = review applySemigroup (&&)
+
+-- |
+-- >>> runSemigroup Data.Valuation.Semigroup.any True False
+-- True
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.any False False
+-- False
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.any False True
+-- True
+any :: Semigroup Bool
+any = review applySemigroup (||)
+
+-- |
+-- >>> runSemigroup endo (+1) (*2) 3 :: Int
+-- 7
+--
+-- >>> runSemigroup endo (*2) (+1) 3 :: Int
+-- 8
+endo :: Semigroup (a -> a)
+endo = review applySemigroup (.)
+
+-- |
+-- >>> runSemigroup endoDual (+1) (*2) 3 :: Int
+-- 8
+endoDual :: Semigroup (a -> a)
+endoDual = dual endo
+
+-- |
+-- >>> runSemigroup unit () ()
+-- ()
+unit :: Semigroup ()
+unit = review applySemigroup (\() () -> ())
+
+-- |
+-- >>> runSemigroup (pair sum product) (1, 2) (3, 4) :: (Int, Int)
+-- (4,8)
+--
+-- >>> runSemigroup (pair min max) (1, 2) (3, 4) :: (Int, Int)
+-- (1,4)
+pair :: Semigroup a -> Semigroup b -> Semigroup (a, b)
+pair sa sb = review applySemigroup (\(a1, b1) (a2, b2) -> (runSemigroup sa a1 a2, runSemigroup sb b1 b2))
+
+-- |
+-- >>> runSemigroup ordering LT EQ
+-- LT
+--
+-- >>> runSemigroup ordering EQ GT
+-- GT
+--
+-- >>> runSemigroup ordering EQ EQ
+-- EQ
+--
+-- >>> runSemigroup ordering GT LT
+-- GT
+ordering :: Semigroup Ordering
+ordering = review applySemigroup (\a b -> if a /= EQ then a else b)
+
+-- |
+-- >>> runSemigroup (Data.Valuation.Semigroup.maybe sum) (Just 1) (Just 2) :: Maybe Int
+-- Just 3
+--
+-- >>> runSemigroup (Data.Valuation.Semigroup.maybe sum) (Just 1) Nothing :: Maybe Int
+-- Just 1
+--
+-- >>> runSemigroup (Data.Valuation.Semigroup.maybe sum) Nothing (Just 2) :: Maybe Int
+-- Just 2
+--
+-- >>> runSemigroup (Data.Valuation.Semigroup.maybe sum) Nothing Nothing :: Maybe Int
+-- Nothing
+maybe :: Semigroup a -> Semigroup (Maybe a)
+maybe s = review applySemigroup (\a1 a2 -> Prelude.maybe a2 (\a1' -> Prelude.maybe a1 (Just . runSemigroup s a1') a2) a1)
+
+-- |
+-- >>> runSemigroup list [1, 2] [3, 4] :: [Int]
+-- [1,2,3,4]
+--
+-- >>> runSemigroup list "ab" "cd"
+-- "abcd"
+list :: Semigroup [a]
+list = review applySemigroup (<>)
+
+-- |
+-- >>> runSemigroup nonEmpty (1 :| [2]) (3 :| [4]) :: NonEmpty Int
+-- 1 :| [2,3,4]
+nonEmpty :: Semigroup (NonEmpty a)
+nonEmpty = review applySemigroup (\(a :| as) (b :| bs) -> a :| (as <> (b : bs)))
+
+-- |
+-- >>> runSemigroup (io sum) (pure 3) (pure 4) :: IO Int
+-- 7
+io :: Semigroup a -> Semigroup (IO a)
+io = liftSemigroup
+
+-- |
+-- >>> runSemigroup Data.Valuation.Semigroup.either (Right 1) (Right 2) :: Either String Int
+-- Right 1
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.either (Left "a") (Right 2) :: Either String Int
+-- Right 2
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.either (Right 1) (Left "b") :: Either String Int
+-- Right 1
+--
+-- >>> runSemigroup Data.Valuation.Semigroup.either (Left "a") (Left "b") :: Either String String
+-- Left "b"
+either :: Semigroup (Either a b)
+either = review applySemigroup (\a b -> case a of Right _ -> a; Left _ -> b)
+
+-- | Vacuous semigroup on 'Void'.
+void :: Semigroup Void
+void = review applySemigroup (pure . absurd)
+
+-- | Semigroup on 'ByteArray' via concatenation.
+byteArray :: Semigroup ByteArray
+byteArray = semigroup'
+
+-- | Semigroup on 'Event' via bitwise OR.
+event :: Semigroup Event
+event = semigroup'
+
+-- |
+-- >>> import Data.Functor.Contravariant (Comparison(..), getComparison)
+-- >>> let cmp1 = Comparison (compare :: Int -> Int -> Ordering)
+-- >>> let cmp2 = Comparison (\a b -> compare (a `mod` 2) (b `mod` 2))
+-- >>> getComparison (runSemigroup comparison cmp1 cmp2) 1 2
+-- LT
+--
+-- >>> import Data.Functor.Contravariant (Comparison(..), getComparison)
+-- >>> let cmp1 = Comparison (\_ _ -> EQ) :: Comparison Int
+-- >>> let cmp2 = Comparison compare
+-- >>> getComparison (runSemigroup comparison cmp1 cmp2) 1 2
+-- LT
+comparison :: Semigroup (Comparison a)
+comparison = semigroup'
+
+-- |
+-- >>> import Data.Functor.Contravariant (Equivalence(..), getEquivalence)
+-- >>> let eq1 = Equivalence ((==) :: Int -> Int -> Bool)
+-- >>> let eq2 = Equivalence (\a b -> even a == even b)
+-- >>> getEquivalence (runSemigroup equivalence eq1 eq2) 2 2
+-- True
+--
+-- >>> import Data.Functor.Contravariant (Equivalence(..), getEquivalence)
+-- >>> let eq1 = Equivalence ((==) :: Int -> Int -> Bool)
+-- >>> let eq2 = Equivalence (\a b -> even a == even b)
+-- >>> getEquivalence (runSemigroup equivalence eq1 eq2) 2 4
+-- False
+equivalence :: Semigroup (Equivalence a)
+equivalence = semigroup'
+
+-- |
+-- >>> import Data.Functor.Contravariant (Predicate(..), getPredicate)
+-- >>> let p1 = Predicate even :: Predicate Int
+-- >>> let p2 = Predicate (> 0)
+-- >>> getPredicate (runSemigroup predicate p1 p2) 4
+-- True
+--
+-- >>> import Data.Functor.Contravariant (Predicate(..), getPredicate)
+-- >>> let p1 = Predicate even :: Predicate Int
+-- >>> let p2 = Predicate (> 0)
+-- >>> getPredicate (runSemigroup predicate p1 p2) 3
+-- False
+--
+-- >>> import Data.Functor.Contravariant (Predicate(..), getPredicate)
+-- >>> let p1 = Predicate even :: Predicate Int
+-- >>> let p2 = Predicate (> 0)
+-- >>> getPredicate (runSemigroup predicate p1 p2) (-2)
+-- False
+predicate :: Semigroup (Predicate a)
+predicate = semigroup'
+
+-- |
+-- >>> runSemigroup (Data.Valuation.Semigroup.op sum) (+ 1) (+ 2) 10 :: Int
+-- 23
+op :: Semigroup b -> Semigroup (a -> b)
+op = liftSemigroup
+
+-- |
+-- >>> runSemigroup Data.Valuation.Semigroup.and (0xFF :: Int) (0x0F :: Int) :: Int
+-- 15
+and :: (Bits a) => Semigroup a
+and = review applySemigroup (.&.)
+
+-- |
+-- >>> runSemigroup ior (0xF0 :: Int) (0x0F :: Int) :: Int
+-- 255
+ior :: (Bits a) => Semigroup a
+ior = review applySemigroup (.|.)
+
+-- |
+-- >>> runSemigroup Data.Valuation.Semigroup.xor (0xFF :: Int) (0x0F :: Int) :: Int
+-- 240
+xor :: (Bits a) => Semigroup a
+xor = review applySemigroup Data.Bits.xor
+
+-- |
+-- >>> import Data.Word (Word8)
+-- >>> runSemigroup iff (0xFF :: Word8) (0x0F :: Word8)
+-- 15
+iff :: (FiniteBits a) => Semigroup a
+iff = review applySemigroup (\a b -> complement (Data.Bits.xor a b))
+
+-- |
+-- >>> runSemigroup wrappedMonoid "ab" "cd"
+-- "abcd"
+wrappedMonoid :: (Prelude.Monoid a) => Semigroup a
+wrappedMonoid = review applySemigroup mappend
+
+-- |
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> runSemigroup (identity sum) (Identity 3) (Identity 4)
+-- Identity 7
+identity :: Semigroup a -> Semigroup (Identity a)
+identity = liftSemigroup
+
+-- |
+-- >>> runSemigroup (down sum) (Down 3) (Down 4)
+-- Down 7
+down :: Semigroup a -> Semigroup (Down a)
+down = liftSemigroup
+
+-- |
+-- >>> runSemigroup (dualM sum) (1, 2) (3, 4) :: (Int, Int)
+-- (4,6)
+dualM :: Semigroup a -> Semigroup (a, a)
+dualM s = pair s s
+
+-- |
+-- >>> runSemigroup (solo sum) (pure 3) (pure 4) :: Solo Int
+-- MkSolo 7
+solo :: Semigroup a -> Semigroup (Solo a)
+solo = liftSemigroup
+
+-- | Lift a 'Semigroup' through 'STM'.
+stm :: Semigroup a -> Semigroup (STM a)
+stm = liftSemigroup
+
+-- | Lift a 'Semigroup' through 'ST'.
+st :: Semigroup a -> Semigroup (ST s a)
+st = liftSemigroup
+
+-- |
+-- >>> runSemigroup (function sum) (+ 1) (+ 2) 10 :: Int
+-- 23
+--
+-- >>> runSemigroup (function list) words lines "hello world"
+-- ["hello","world","hello world"]
+function :: Semigroup b -> Semigroup (a -> b)
+function = liftSemigroup
+
+-- |
+-- >>> runSemigroup (const' sum) (Const 3) (Const 4) :: Const Int String
+-- Const 7
+const' :: Semigroup a -> Semigroup (Const a b)
+const' = mapSemigroup getConst Const
+
+-- |
+-- >>> runSemigroup alt [1, 2] [3, 4] :: [Int]
+-- [1,2,3,4]
+--
+-- >>> runSemigroup alt Nothing (Just 1) :: Maybe Int
+-- Just 1
+alt :: (Alternative f) => Semigroup (f a)
+alt = review applySemigroup (<|>)
+
+-- |
+-- >>> runSemigroup proxy Proxy Proxy
+-- Proxy
+proxy :: Semigroup (Proxy s)
+proxy = review applySemigroup (\_ _ -> Proxy)
+
+-- | Semigroup on 'Lifetime'.
+lifetime :: Semigroup Lifetime
+lifetime = semigroup'
+
+-- |
+-- >>> runSemigroup (tuple3 sum product min) (1, 2, 3) (4, 5, 6) :: (Int, Int, Int)
+-- (5,10,3)
+tuple3 :: Semigroup a -> Semigroup b -> Semigroup c -> Semigroup (a, b, c)
+tuple3 sa sb sc =
+  let f = runSemigroup sa; g = runSemigroup sb; h = runSemigroup sc
+   in review applySemigroup (\(a1, b1, c1) (a2, b2, c2) -> (f a1 a2, g b1 b2, h c1 c2))
+
+-- |
+-- >>> runSemigroup (tuple4 sum sum sum sum) (1, 2, 3, 4) (5, 6, 7, 8) :: (Int, Int, Int, Int)
+-- (6,8,10,12)
+tuple4 :: Semigroup a -> Semigroup b -> Semigroup c -> Semigroup d -> Semigroup (a, b, c, d)
+tuple4 sa sb sc sd =
+  let f = runSemigroup sa; g = runSemigroup sb; h = runSemigroup sc; i = runSemigroup sd
+   in review applySemigroup (\(a1, b1, c1, d1) (a2, b2, c2, d2) -> (f a1 a2, g b1 b2, h c1 c2, i d1 d2))
+
+-- |
+-- >>> runSemigroup (tuple5 sum sum sum sum sum) (1, 2, 3, 4, 5) (6, 7, 8, 9, 10) :: (Int, Int, Int, Int, Int)
+-- (7,9,11,13,15)
+tuple5 :: Semigroup a -> Semigroup b -> Semigroup c -> Semigroup d -> Semigroup e -> Semigroup (a, b, c, d, e)
+tuple5 sa sb sc sd se =
+  let f = runSemigroup sa; g = runSemigroup sb; h = runSemigroup sc; i = runSemigroup sd; j = runSemigroup se
+   in review applySemigroup (\(a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2) -> (f a1 a2, g b1 b2, h c1 c2, i d1 d2, j e1 e2))
+
+-- |
+-- >>> runSemigroup u1 U1 U1
+-- U1
+u1 :: Semigroup (U1 p)
+u1 = review applySemigroup (\_ _ -> U1)
+
+-- | Vacuous semigroup on 'V1' (uninhabited type).
+v1 :: Semigroup (V1 p)
+v1 = review applySemigroup const
+
+-- |
+-- >>> runSemigroup (par1 sum) (Par1 3) (Par1 4)
+-- Par1 {unPar1 = 7}
+par1 :: Semigroup p -> Semigroup (Par1 p)
+par1 = mapSemigroup unPar1 Par1
+
+-- |
+-- >>> runSemigroup (rec1 list) (Rec1 [1, 2]) (Rec1 [3, 4]) :: Rec1 [] Int
+-- Rec1 {unRec1 = [1,2,3,4]}
+rec1 :: Semigroup (f p) -> Semigroup (Rec1 f p)
+rec1 = mapSemigroup unRec1 Rec1
+
+-- |
+-- >>> runSemigroup (k1 sum) (K1 3) (K1 4) :: K1 () Int ()
+-- K1 {unK1 = 7}
+k1 :: Semigroup c -> Semigroup (K1 i c p)
+k1 = mapSemigroup unK1 K1
+
+-- |
+-- >>> :set -XDataKinds
+-- >>> runSemigroup (m1 (k1 sum)) (M1 (K1 3)) (M1 (K1 4)) :: M1 () ('GHC.Generics.MetaData "" "" "" 'False) (K1 () Int) ()
+-- M1 {unM1 = K1 {unK1 = 7}}
+m1 :: Semigroup (f p) -> Semigroup (M1 i c f p)
+m1 = mapSemigroup unM1 M1
+
+-- |
+-- >>> :set -XTypeOperators
+-- >>> runSemigroup (productG (par1 sum) (par1 product)) (Par1 1 :*: Par1 2) (Par1 3 :*: Par1 4) :: (Par1 :*: Par1) Int
+-- Par1 {unPar1 = 4} :*: Par1 {unPar1 = 8}
+productG :: Semigroup (f p) -> Semigroup (g p) -> Semigroup ((f :*: g) p)
+productG sf sg =
+  let f = runSemigroup sf; g = runSemigroup sg
+   in review applySemigroup (\(a :*: b) (c :*: d) -> f a c :*: g b d)
+
+-- |
+-- >>> :set -XTypeOperators
+-- >>> runSemigroup (composeG (par1 list)) (Comp1 (Par1 [1, 2])) (Comp1 (Par1 [3, 4])) :: (Par1 :.: []) Int
+-- Comp1 {unComp1 = Par1 {unPar1 = [1,2,3,4]}}
+composeG :: Semigroup (f (g p)) -> Semigroup ((f :.: g) p)
+composeG = mapSemigroup unComp1 Comp1
+
+-- |
+-- >>> runSemigroup (productF list list) (Pair [1] [2]) (Pair [3] [4]) :: Product [] [] Int
+-- Pair [1,3] [2,4]
+productF :: Semigroup (f a) -> Semigroup (g a) -> Semigroup (Product f g a)
+productF sf sg =
+  let f = runSemigroup sf; g = runSemigroup sg
+   in review applySemigroup (\(Pair a b) (Pair c d) -> Pair (f a c) (g b d))
+
+-- |
+-- >>> runSemigroup (composeF list) (Compose [[1, 2]]) (Compose [[3, 4]]) :: Compose [] [] Int
+-- Compose [[1,2],[3,4]]
+composeF :: Semigroup (f (g a)) -> Semigroup (Compose f g a)
+composeF = mapSemigroup getCompose Compose
diff --git a/src/Data/Valuation/Valuation.hs b/src/Data/Valuation/Valuation.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/Valuation.hs
@@ -0,0 +1,581 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A valuation: a domain paired with information. Isomorphic to @(set var, a)@.
+module Data.Valuation.Valuation
+  ( Valuation (..),
+    SetValuation,
+
+    -- * optics
+    HasValuation (..),
+    AsValuation (..),
+
+    -- * combinators
+    valuationDomain',
+    valuationInformation',
+    projectVar,
+    combineVar,
+    combineSemiValuation,
+    combineValuation,
+    semigroupValuation,
+  )
+where
+
+import Control.Comonad (Comonad (..), ComonadApply (..))
+import Control.Comonad.Env.Class (ComonadEnv (..))
+import Control.Lens
+  ( Lens,
+    Lens',
+    Prism',
+    review,
+  )
+import Control.Monad.Fix (MonadFix (..))
+import Control.Monad.Writer.Class (MonadWriter (..))
+import Control.Monad.Zip (MonadZip (..))
+import Control.Selective (Selective (..), selectM)
+import Data.Biapplicative (Biapplicative (..))
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifoldable1 (Bifoldable1 (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bifunctor.Apply (Biapply (..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Foldable1 (Foldable1 (..))
+import Data.Functor.Apply (Apply (..))
+import Data.Functor.Bind (Bind (..))
+import Data.Functor.Classes (Eq1 (..), Eq2 (..), Ord1 (..), Ord2 (..), Show1 (..), Show2 (..))
+import Data.Functor.Extend (Extend (..))
+import Data.Semigroup.Traversable.Class (Bitraversable1 (..), Traversable1 (..))
+import Data.Set (Set)
+import Data.Valuation.ProjectValuation (ProjectValuation (..))
+import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra (..))
+import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup, semigroup')
+import Data.Valuation.ValuationAlgebra (ValuationAlgebra (..))
+import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp (..))
+import GHC.Generics (Generic, Generic1)
+import Prelude hiding (Semigroup)
+import qualified Prelude (Semigroup (..))
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+
+-- |
+-- >>> Valuation [1,2,3] "hello"
+-- Valuation [1,2,3] "hello"
+--
+-- >>> let Valuation d a = Valuation [1,2,3] "hello" :: Valuation [] Int String in (d, a)
+-- ([1,2,3],"hello")
+data Valuation set var a
+  = Valuation
+      -- | valuation domain
+      (set var)
+      -- | valuation information
+      a
+  deriving (Generic, Generic1)
+
+-- | A 'Valuation' specialised to 'Set'.
+type SetValuation var a =
+  Valuation Set var a
+
+-- | Type-changing lens to the domain component.
+valuationDomain' ::
+  Lens (Valuation set var a) (Valuation set' var' a) (set var) (set' var')
+valuationDomain' f (Valuation d i) =
+  fmap (`Valuation` i) (f d)
+
+-- | Type-changing lens to the information component.
+valuationInformation' ::
+  Lens (Valuation set var a) (Valuation set var a') a a'
+valuationInformation' f (Valuation d i) =
+  fmap (Valuation d) (f i)
+
+-- | Classy lens for types that contain a 'Valuation'.
+class HasValuation c set var a | c -> set var a where
+  valuation ::
+    Lens' c (Valuation set var a)
+  valuationDomain ::
+    Lens' c (set var)
+  valuationDomain =
+    valuation . valuationDomain
+  valuationInformation ::
+    Lens' c a
+  valuationInformation =
+    valuation . valuationInformation
+
+instance HasValuation (Valuation set var a) set var a where
+  valuation =
+    id
+  valuationDomain =
+    valuationDomain'
+  valuationInformation =
+    valuationInformation'
+
+-- | Classy prism for types that can be constructed from a 'Valuation'.
+class AsValuation c set var a | c -> set var a where
+  _Valuation ::
+    Prism' c (Valuation set var a)
+
+instance AsValuation (Valuation set var a) set var a where
+  _Valuation =
+    id
+
+-- |
+-- >>> (Valuation [1,2] "ab" :: Valuation [] Int String) <> Valuation [3,4] "cd"
+-- Valuation [1,2,3,4] "abcd"
+instance (Prelude.Semigroup (set var), Prelude.Semigroup a) => Prelude.Semigroup (Valuation set var a) where
+  (<>) =
+    runSemigroup (semigroupValuation semigroup' semigroup')
+
+-- |
+-- >>> mempty :: Valuation [] Int String
+-- Valuation [] ""
+--
+-- >>> mempty <> Valuation [1,2] "ab" :: Valuation [] Int String
+-- Valuation [1,2] "ab"
+instance (Monoid (set var), Monoid a) => Monoid (Valuation set var a) where
+  mempty =
+    Valuation mempty mempty
+
+-- |
+-- >>> Valuation [1,2] "a" == (Valuation [1,2] "a" :: Valuation [] Int String)
+-- True
+--
+-- >>> Valuation [1,2] "a" == (Valuation [1,2] "b" :: Valuation [] Int String)
+-- False
+--
+-- >>> Valuation [1,2] "a" == (Valuation [3,4] "a" :: Valuation [] Int String)
+-- False
+instance (Eq (set var), Eq a) => Eq (Valuation set var a) where
+  Valuation d1 a1 == Valuation d2 a2 =
+    d1 == d2 && a1 == a2
+
+-- |
+-- >>> compare (Valuation [1] "a") (Valuation [2] "a" :: Valuation [] Int String)
+-- LT
+--
+-- >>> compare (Valuation [1] "a") (Valuation [1] "b" :: Valuation [] Int String)
+-- LT
+--
+-- >>> compare (Valuation [1] "b") (Valuation [1] "a" :: Valuation [] Int String)
+-- GT
+instance (Ord (set var), Ord a) => Ord (Valuation set var a) where
+  compare (Valuation d1 a1) (Valuation d2 a2) =
+    compare d1 d2 <> compare a1 a2
+
+-- |
+-- >>> show (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- "Valuation [1,2,3] \"hello\""
+--
+-- >>> show (Valuation [1] (42 :: Int) :: Valuation [] Int Int)
+-- "Valuation [1] 42"
+instance (Show (set var), Show a) => Show (Valuation set var a) where
+  showsPrec d (Valuation dom info) =
+    showParen (d > 10) $
+      showString "Valuation " . showsPrec 11 dom . showChar ' ' . showsPrec 11 info
+
+-- |
+-- >>> import Data.Functor.Classes (eq1)
+-- >>> eq1 (Valuation [1,2] "a") (Valuation [1,2] "a" :: Valuation [] Int String)
+-- True
+--
+-- >>> import Data.Functor.Classes (eq1)
+-- >>> eq1 (Valuation [1,2] "a") (Valuation [1,2] "b" :: Valuation [] Int String)
+-- False
+instance (Eq (set var)) => Eq1 (Valuation set var) where
+  liftEq eq (Valuation d1 a1) (Valuation d2 a2) =
+    d1 == d2 && eq a1 a2
+
+-- |
+-- >>> import Data.Functor.Classes (compare1)
+-- >>> compare1 (Valuation [1] "a") (Valuation [2] "a" :: Valuation [] Int String)
+-- LT
+instance (Ord (set var)) => Ord1 (Valuation set var) where
+  liftCompare cmp (Valuation d1 a1) (Valuation d2 a2) =
+    compare d1 d2 <> cmp a1 a2
+
+-- |
+-- >>> import Data.Functor.Classes (showsPrec1)
+-- >>> showsPrec1 0 (Valuation [1] "hi" :: Valuation [] Int String) ""
+-- "Valuation [1] \"hi\""
+instance (Show (set var)) => Show1 (Valuation set var) where
+  liftShowsPrec sp _ d (Valuation dom info) =
+    showParen (d > 10) $
+      showString "Valuation " . showsPrec 11 dom . showChar ' ' . sp 11 info
+
+-- |
+-- >>> import Data.Functor.Classes (liftEq2)
+-- >>> liftEq2 (==) (==) (Valuation [1,2] "a") (Valuation [1,2] "a" :: Valuation [] Int String)
+-- True
+--
+-- >>> import Data.Functor.Classes (liftEq2)
+-- >>> liftEq2 (\_ _ -> True) (==) (Valuation [1] "a") (Valuation [2] "a" :: Valuation [] Int String)
+-- True
+instance (Eq1 set) => Eq2 (Valuation set) where
+  liftEq2 eqV eqA (Valuation d1 a1) (Valuation d2 a2) = liftEq eqV d1 d2 && eqA a1 a2
+
+-- |
+-- >>> import Data.Functor.Classes (liftCompare2)
+-- >>> liftCompare2 compare compare (Valuation [1] "a") (Valuation [2] "b" :: Valuation [] Int String)
+-- LT
+instance (Ord1 set) => Ord2 (Valuation set) where
+  liftCompare2 cmpV cmpA (Valuation d1 a1) (Valuation d2 a2) =
+    liftCompare cmpV d1 d2 <> cmpA a1 a2
+
+-- |
+-- >>> import Data.Functor.Classes (liftShowsPrec2)
+-- >>> liftShowsPrec2 showsPrec showList showsPrec showList 0 (Valuation [1] "hi" :: Valuation [] Int String) ""
+-- "Valuation [1] \"hi\""
+instance (Show1 set) => Show2 (Valuation set) where
+  liftShowsPrec2 spV slV spA _ d (Valuation dom info) =
+    showParen (d > 10) $
+      showString "Valuation " . liftShowsPrec spV slV 11 dom . showChar ' ' . spA 11 info
+
+-- |
+-- >>> fmap (*2) (Valuation [1,2,3] 10 :: Valuation [] Int Int)
+-- Valuation [1,2,3] 20
+--
+-- >>> fmap length (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- Valuation [1,2,3] 5
+instance Functor (Valuation set var) where
+  fmap f (Valuation dom info) =
+    Valuation dom (f info)
+
+-- |
+-- >>> import Data.Semigroup (Sum(..))
+-- >>> foldMap Sum (Valuation [1,2,3] 42 :: Valuation [] Int Int)
+-- Sum {getSum = 42}
+--
+-- >>> foldr (:) [] (Valuation [1,2,3] 42 :: Valuation [] Int Int)
+-- [42]
+instance Foldable (Valuation set var) where
+  foldMap f (Valuation _ info) =
+    f info
+
+-- |
+-- >>> traverse Just (Valuation [1,2,3] 42 :: Valuation [] Int Int)
+-- Just (Valuation [1,2,3] 42)
+--
+-- >>> sequenceA (Valuation [1,2,3] (Just 42) :: Valuation [] Int (Maybe Int))
+-- Just (Valuation [1,2,3] 42)
+--
+-- >>> sequenceA (Valuation [1,2,3] Nothing :: Valuation [] Int (Maybe Int))
+-- Nothing
+instance Traversable (Valuation set var) where
+  traverse f (Valuation dom info) =
+    Valuation dom <$> f info
+
+-- |
+-- >>> import Data.Foldable1 (foldMap1)
+-- >>> import Data.Semigroup (Sum(..))
+-- >>> foldMap1 Sum (Valuation [1,2,3] 42 :: Valuation [] Int Int)
+-- Sum {getSum = 42}
+instance Foldable1 (Valuation set var) where
+  foldMap1 f (Valuation _ info) =
+    f info
+
+-- |
+-- >>> import Data.Semigroup.Traversable.Class (traverse1)
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> traverse1 (Identity . (*2)) (Valuation [1,2,3] 5 :: Valuation [] Int Int)
+-- Identity (Valuation [1,2,3] 10)
+instance Traversable1 (Valuation set var) where
+  traverse1 f (Valuation dom info) =
+    Valuation dom <$> f info
+
+-- |
+-- >>> import Data.Functor.Apply ((<.>))
+-- >>> (Valuation [1,2] (*2) :: Valuation [] Int (Int -> Int)) <.> Valuation [3,4] 5
+-- Valuation [1,2,3,4] 10
+instance (Prelude.Semigroup (set var)) => Apply (Valuation set var) where
+  Valuation d1 f <.> Valuation d2 a =
+    Valuation (d1 <> d2) (f a)
+
+-- |
+-- >>> import Data.Functor.Bind ((>>-))
+-- >>> (Valuation [1,2] 3 :: Valuation [] Int Int) >>- (\x -> Valuation [4,5] (x * 10))
+-- Valuation [1,2,4,5] 30
+instance (Prelude.Semigroup (set var)) => Bind (Valuation set var) where
+  Valuation d1 a >>- f =
+    let Valuation d2 b = f a
+     in Valuation (d1 <> d2) b
+
+-- |
+-- >>> pure 42 :: Valuation [] Int Int
+-- Valuation [] 42
+--
+-- >>> Valuation [1,2] (*2) <*> Valuation [3,4] (5 :: Int)
+-- Valuation [1,2,3,4] 10
+instance (Monoid (set var)) => Applicative (Valuation set var) where
+  pure =
+    Valuation mempty
+  (<*>) =
+    (<.>)
+
+-- |
+-- >>> Valuation [1,2] 3 >>= (\x -> Valuation [4,5] (x * 10)) :: Valuation [] Int Int
+-- Valuation [1,2,4,5] 30
+--
+-- >>> return 42 :: Valuation [] Int Int
+-- Valuation [] 42
+instance (Monoid (set var)) => Monad (Valuation set var) where
+  (>>=) =
+    (>>-)
+
+-- |
+-- >>> import Control.Monad.Writer.Class (writer, tell, listen, pass)
+-- >>> writer ("hello", [1,2,3]) :: Valuation [] Int String
+-- Valuation [1,2,3] "hello"
+-- >>> tell [1,2,3] :: Valuation [] Int ()
+-- Valuation [1,2,3] ()
+-- >>> listen (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- Valuation [1,2,3] ("hello",[1,2,3])
+-- >>> pass (Valuation [1,2,3] ("hello", map (*2)) :: Valuation [] Int (String, [Int] -> [Int]))
+-- Valuation [2,4,6] "hello"
+instance (Monoid (set var)) => MonadWriter (set var) (Valuation set var) where
+  writer (a, w) =
+    Valuation w a
+  tell w =
+    Valuation w ()
+  listen (Valuation dom info) =
+    Valuation dom (info, dom)
+  pass (Valuation dom (info, f)) =
+    Valuation (f dom) info
+
+-- |
+-- >>> import Data.Functor.Extend (duplicated)
+-- >>> duplicated (Valuation [1,2] "hello" :: Valuation [] Int String)
+-- Valuation [1,2] (Valuation [1,2] "hello")
+instance Extend (Valuation set var) where
+  duplicated =
+    duplicate
+
+-- |
+-- >>> import Control.Comonad (extract, duplicate)
+-- >>> extract (Valuation [1,2] "hello" :: Valuation [] Int String)
+-- "hello"
+-- >>> duplicate (Valuation [1,2] "hello" :: Valuation [] Int String)
+-- Valuation [1,2] (Valuation [1,2] "hello")
+instance Comonad (Valuation set var) where
+  extract (Valuation _ info) =
+    info
+  duplicate (Valuation dom info) =
+    Valuation dom (Valuation dom info)
+
+-- |
+-- >>> import Control.Comonad ((<@>))
+-- >>> (Valuation [1,2] (*2) :: Valuation [] Int (Int -> Int)) <@> Valuation [3,4] 5
+-- Valuation [1,2,3,4] 10
+instance (Prelude.Semigroup (set var)) => ComonadApply (Valuation set var) where
+  (<@>) =
+    (<.>)
+
+-- |
+-- >>> import Control.Comonad.Env.Class (ask)
+-- >>> ask (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- [1,2,3]
+instance ComonadEnv (set var) (Valuation set var) where
+  ask (Valuation dom _) =
+    dom
+
+-- |
+-- >>> import Control.Selective (select)
+-- >>> select (Valuation [1] (Right 42) :: Valuation [] Int (Either String Int)) (Valuation [2] read)
+-- Valuation [1] 42
+--
+-- >>> import Control.Selective (select)
+-- >>> select (Valuation [1] (Left "42") :: Valuation [] Int (Either String Int)) (Valuation [2] read)
+-- Valuation [1,2] 42
+instance (Monoid (set var)) => Selective (Valuation set var) where
+  select =
+    selectM
+
+-- |
+-- >>> import Control.Monad.Fix (mfix)
+-- >>> mfix (\x -> Valuation [1,2] (const 42 x)) :: Valuation [] Int Int
+-- Valuation [1,2] 42
+instance (Monoid (set var)) => MonadFix (Valuation set var) where
+  mfix f =
+    let Valuation d a = f a
+     in Valuation d a
+
+-- |
+-- >>> import Control.Monad.Zip (mzip, mzipWith)
+-- >>> mzip (Valuation [1,2] 3) (Valuation [3,4] "hi" :: Valuation [] Int String)
+-- Valuation [1,2,3,4] (3,"hi")
+--
+-- >>> import Control.Monad.Zip (mzipWith)
+-- >>> mzipWith (+) (Valuation [1,2] 3) (Valuation [3,4] 4 :: Valuation [] Int Int)
+-- Valuation [1,2,3,4] 7
+instance (Monoid (set var)) => MonadZip (Valuation set var) where
+  mzip (Valuation d1 a) (Valuation d2 b) =
+    Valuation (d1 <> d2) (a, b)
+  mzipWith f (Valuation d1 a) (Valuation d2 b) =
+    Valuation (d1 <> d2) (f a b)
+
+-- |
+-- >>> import Data.Bifunctor (bimap, first, second)
+-- >>> bimap (*2) length (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- Valuation [2,4,6] 5
+--
+-- >>> import Data.Bifunctor (bimap, first, second)
+-- >>> first (*2) (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- Valuation [2,4,6] "hello"
+--
+-- >>> import Data.Bifunctor (bimap, first, second)
+-- >>> second length (Valuation [1,2,3] "hello" :: Valuation [] Int String)
+-- Valuation [1,2,3] 5
+instance (Functor set) => Bifunctor (Valuation set) where
+  bimap f g (Valuation dom info) =
+    Valuation (fmap f dom) (g info)
+
+-- |
+-- >>> import Data.Bifoldable (bifoldMap)
+-- >>> import Data.Semigroup (Sum(..))
+-- >>> bifoldMap (Sum . (*10)) Sum (Valuation [1,2,3] 4 :: Valuation [] Int Int)
+-- Sum {getSum = 64}
+instance (Foldable set) => Bifoldable (Valuation set) where
+  bifoldMap f g (Valuation dom info) =
+    foldMap f dom <> g info
+
+-- |
+-- >>> import Data.Bitraversable (bitraverse)
+-- >>> bitraverse (\x -> [x, x*2]) (\s -> [s, s ++ "!"]) (Valuation [1] "hi" :: Valuation [] Int String)
+-- [Valuation [1] "hi",Valuation [1] "hi!",Valuation [2] "hi",Valuation [2] "hi!"]
+instance (Traversable set) => Bitraversable (Valuation set) where
+  bitraverse f g (Valuation dom info) =
+    Valuation <$> traverse f dom <*> g info
+
+-- |
+-- >>> import Data.Bifoldable1 (bifoldMap1)
+-- >>> import Data.Semigroup (Sum(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> bifoldMap1 Sum Sum (Valuation (1 :| [2,3]) 4 :: Valuation NonEmpty Int Int)
+-- Sum {getSum = 10}
+instance (Foldable1 set) => Bifoldable1 (Valuation set) where
+  bifoldMap1 f g (Valuation dom info) =
+    foldMap1 f dom <> g info
+
+-- |
+-- >>> import Data.Semigroup.Traversable.Class (bitraverse1)
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> bitraverse1 (Identity . (*2)) (Identity . (*3)) (Valuation (1 :| [2]) 3 :: Valuation NonEmpty Int Int)
+-- Identity (Valuation (2 :| [4]) 9)
+instance (Traversable1 set) => Bitraversable1 (Valuation set) where
+  bitraverse1 f g (Valuation dom info) =
+    Valuation <$> traverse1 f dom <.> g info
+
+-- |
+-- >>> let pv = ProjectValuation (\s v -> v + sum s) :: ProjectValuation Int [] Int
+-- >>> projectVar pv (Valuation [1,2,3] 10)
+-- 16
+--
+-- >>> let pv = ProjectValuation (\s v -> v * length s) :: ProjectValuation Int [] Int
+-- >>> projectVar pv (Valuation [1,2,3] 5)
+-- 15
+projectVar ::
+  ProjectValuation v set var ->
+  Valuation set var v ->
+  v
+projectVar (ProjectValuation p) (Valuation dom info) =
+  p dom info
+
+-- |
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> combineVar S.list S.sum (Valuation [1,2] 10) (Valuation [3,4] 20 :: Valuation [] Int Int)
+-- Valuation [1,2,3,4] 30
+--
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> combineVar S.list S.product (Valuation [1,2] 10) (Valuation [3,4] 20 :: Valuation [] Int Int)
+-- Valuation [1,2,3,4] 200
+combineVar ::
+  Semigroup (set var) ->
+  Semigroup v ->
+  Valuation set var v ->
+  Valuation set var v ->
+  Valuation set var v
+combineVar sd sv (Valuation d1 a1) (Valuation d2 a2) =
+  Valuation (runSemigroup sd d1 d2) (runSemigroup sv a1 a2)
+
+-- |
+-- >>> import Control.Lens (review)
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (+)) (ProjectValuation (\s v -> v + sum s)) :: SemiValuationAlgebra Int [] Int
+-- >>> combineSemiValuation S.list sva (Valuation [1,2] 10) (Valuation [3,4] 20)
+-- Valuation [1,2,3,4] 40
+--
+-- >>> import Control.Lens (review)
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (*)) (ProjectValuation (\s v -> v + length s)) :: SemiValuationAlgebra Int [] Int
+-- >>> combineSemiValuation S.list sva (Valuation [1,2] 3) (Valuation [3] 4)
+-- Valuation [1,2,3] 15
+combineSemiValuation ::
+  Semigroup (set var) ->
+  SemiValuationAlgebra v set var ->
+  Valuation set var v ->
+  Valuation set var v ->
+  Valuation set var v
+combineSemiValuation sd (SemiValuationAlgebra sg (ProjectValuation p)) (Valuation d1 v1) (Valuation d2 v2) =
+  let d = runSemigroup sd d1 d2
+   in Valuation d (p d (runSemigroup sg v1 v2))
+
+-- |
+-- >>> import Control.Lens (review)
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (+)) (ProjectValuation (\s v -> v + sum s))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int [] Int
+-- >>> combineValuation S.list va (Valuation [1,2] 10) (Valuation [3,4] 20)
+-- Valuation [1,2,3,4] 50
+--
+-- >>> import Control.Lens (review)
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> let sva = SemiValuationAlgebra (review S.applySemigroup (*)) (ProjectValuation (\s v -> v + length s))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp (const 1)) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int [] Int
+-- >>> combineValuation S.list va (Valuation [1,2] 3) (Valuation [3] 4)
+-- Valuation [1,2,3] 15
+combineValuation ::
+  Semigroup (set var) ->
+  ValuationAlgebra v set var ->
+  Valuation set var v ->
+  Valuation set var v ->
+  Valuation set var v
+combineValuation sd (ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) _) (Valuation d1 v1) (Valuation d2 v2) =
+  let d = runSemigroup sd d1 d2
+      v = runSemigroup sg (u d) (runSemigroup sg v1 v2)
+   in Valuation d (p d v)
+
+-- |
+-- >>> import Data.Bifunctor.Apply ((<<.>>))
+-- >>> Valuation [(*2), (+10)] length <<.>> (Valuation [3] "hi" :: Valuation [] Int String)
+-- Valuation [6,13] 2
+instance (Apply set) => Biapply (Valuation set) where
+  Valuation d1 f <<.>> Valuation d2 a =
+    Valuation (d1 <.> d2) (f a)
+
+-- |
+-- >>> import Data.Biapplicative (bipure, (<<*>>))
+-- >>> bipure 1 "hello" :: Valuation [] Int String
+-- Valuation [1] "hello"
+--
+-- >>> import Data.Biapplicative (bipure, (<<*>>))
+-- >>> Valuation [(*2), (+10)] length <<*>> (Valuation [3] "hi" :: Valuation [] Int String)
+-- Valuation [6,13] 2
+instance (Applicative set) => Biapplicative (Valuation set) where
+  bipure =
+    Valuation . pure
+  Valuation d1 f <<*>> Valuation d2 a =
+    Valuation (d1 <*> d2) (f a)
+
+-- |
+-- >>> import qualified Data.Valuation.Semigroup as S
+-- >>> runSemigroup (semigroupValuation S.list S.sum) (Valuation [1,2] 10) (Valuation [3,4] 20 :: Valuation [] Int Int)
+-- Valuation [1,2,3,4] 30
+semigroupValuation ::
+  Semigroup (set var) ->
+  Semigroup a ->
+  Semigroup (Valuation set var a)
+semigroupValuation sd sa =
+  review applySemigroup (\(Valuation d1 a1) (Valuation d2 a2) -> Valuation (runSemigroup sd d1 d2) (runSemigroup sa a1 a2))
diff --git a/src/Data/Valuation/ValuationAlgebra.hs b/src/Data/Valuation/ValuationAlgebra.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/ValuationAlgebra.hs
@@ -0,0 +1,265 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | A valuation algebra: a semi-valuation algebra with unit and zero operations.
+module Data.Valuation.ValuationAlgebra
+  ( ValuationAlgebra (..),
+    SetValuationAlgebra,
+
+    -- * optics
+    HasValuationAlgebra (..),
+    AsValuationAlgebra (..),
+  )
+where
+
+import Control.Lens (Lens', Prism')
+import Data.Functor.Contravariant (Contravariant (..))
+import Data.Functor.Contravariant.Conclude (Conclude (..))
+import Data.Functor.Contravariant.Decide (Decide (..))
+import Data.Functor.Contravariant.Divise (Divise (..))
+import Data.Functor.Contravariant.Divisible (Decidable (..), Divisible (..))
+import Data.Set (Set)
+import Data.Valuation.ProjectValuation (HasProjectValuation (..))
+import Data.Valuation.SemiValuationAlgebra
+  ( HasSemiValuationAlgebra (..),
+    SemiValuationAlgebra,
+  )
+import Data.Valuation.Semigroup (HasSemigroup (..))
+import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp (..))
+import Witherable (Filterable (mapMaybe))
+import Prelude hiding (Semigroup)
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+-- >>> import Data.Void (Void)
+
+-- |
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = va
+-- >>> runSemigroup sg 3 4
+-- 7
+-- >>> p [1,2,3] 10
+-- 16
+-- >>> u [1,2,3]
+-- 6
+-- >>> z [1,2,3]
+-- 0
+data ValuationAlgebra v set var
+  = ValuationAlgebra
+      (SemiValuationAlgebra v set var)
+      -- | algebra unit
+      (ValuationAlgebraOp set var v)
+      -- | algebra zero
+      (ValuationAlgebraOp set var v)
+
+-- | Classy lens for types that contain a 'ValuationAlgebra'.
+class HasValuationAlgebra c v set var | c -> v set var where
+  valuationAlgebra :: Lens' c (ValuationAlgebra v set var)
+  valuationAlgebraUnit :: Lens' c (ValuationAlgebraOp set var v)
+  valuationAlgebraUnit = valuationAlgebra . valuationAlgebraUnit
+  valuationAlgebraZero :: Lens' c (ValuationAlgebraOp set var v)
+  valuationAlgebraZero = valuationAlgebra . valuationAlgebraZero
+
+instance HasValuationAlgebra (ValuationAlgebra v set var) v set var where
+  valuationAlgebra = id
+  valuationAlgebraUnit f (ValuationAlgebra s u z) = fmap (\u' -> ValuationAlgebra s u' z) (f u)
+  valuationAlgebraZero f (ValuationAlgebra s u z) = fmap (ValuationAlgebra s u) (f z)
+
+-- | Classy prism for types that can be constructed from a 'ValuationAlgebra'.
+class AsValuationAlgebra c v set var | c -> v set var where
+  _ValuationAlgebra :: Prism' c (ValuationAlgebra v set var)
+
+instance AsValuationAlgebra (ValuationAlgebra v set var) v set var where
+  _ValuationAlgebra = id
+
+instance HasSemiValuationAlgebra (ValuationAlgebra v set var) v set var where
+  semiValuationAlgebra f (ValuationAlgebra a u z) = fmap (\a' -> ValuationAlgebra a' u z) (f a)
+
+instance HasSemigroup (ValuationAlgebra v set var) v where
+  semigroup = semiValuationAlgebra . semigroup
+
+instance HasProjectValuation (ValuationAlgebra v set var) v set var where
+  projectValuation = semiValuationAlgebra . projectValuation
+
+-- |
+-- >>> import Data.Functor.Contravariant (contramap)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva = SemiValuationAlgebra (review applySemigroup (+)) (ProjectValuation (\s v -> v + sum s))
+-- >>> let va = ValuationAlgebra sva (ValuationAlgebraOp sum) (ValuationAlgebraOp (const 0)) :: ValuationAlgebra Int [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = contramap (*2) va
+-- >>> runSemigroup sg 3 4
+-- 7
+-- >>> p [1,2,3] 10
+-- 22
+-- >>> u [1,2,3]
+-- 12
+-- >>> z [1,2,3]
+-- 0
+instance (Functor set) => Contravariant (ValuationAlgebra v set) where
+  contramap f (ValuationAlgebra s (ValuationAlgebraOp u) (ValuationAlgebraOp z)) =
+    ValuationAlgebra (contramap f s) (ValuationAlgebraOp (u . fmap f)) (ValuationAlgebraOp (z . fmap f))
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conquer :: ValuationAlgebra [Int] [] Int
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [10,20] [42]
+-- [42]
+-- >>> u [10,20]
+-- []
+-- >>> z [10,20]
+-- []
+--
+-- >>> import Data.Functor.Contravariant.Divisible (conquer, divide)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s))
+-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s))
+-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra [Int] [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = divide (\x -> (x, x + 10)) va1 va2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> u [1,2,3]
+-- [1,2,3,13,12,11]
+-- >>> z [1,2,3]
+-- [-1,-2,-3]
+instance (Functor set, Prelude.Semigroup v, Prelude.Monoid v) => Divisible (ValuationAlgebra v set) where
+  conquer = ValuationAlgebra conquer (ValuationAlgebraOp (const mempty)) (ValuationAlgebraOp (const mempty))
+  divide f (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) =
+    let combine g1 g2 = ValuationAlgebraOp (\fa -> g1 (fmap (fst . f) fa) <> g2 (fmap (snd . f) fa))
+     in ValuationAlgebra (divide f s1 s2) (combine u1 u2) (combine z1 z2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divisible (choose, lose)
+-- >>> import Data.Void (Void, absurd)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = lose absurd :: ValuationAlgebra [Int] [] Void
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> p [] [42]
+-- [42]
+-- >>> u []
+-- []
+-- >>> z []
+-- []
+--
+-- >>> import Data.Functor.Contravariant.Divisible (choose)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s))
+-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s))
+-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra [Int] [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = choose (\x -> if even x then Left x else Right x) va1 va2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> u [1,2,3,4]
+-- [2,4,3,1]
+-- >>> z [1,2,3,4]
+-- [-2,-4]
+instance (Filterable set, Prelude.Semigroup v, Prelude.Monoid v) => Decidable (ValuationAlgebra v set) where
+  lose f = ValuationAlgebra (lose f) (ValuationAlgebraOp (const mempty)) (ValuationAlgebraOp (const mempty))
+  choose ch (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) =
+    let lefts = mapMaybe (either Just (const Nothing) . ch)
+        rights = mapMaybe (either (const Nothing) Just . ch)
+        combine g1 g2 = ValuationAlgebraOp (\fa -> g1 (lefts fa) <> g2 (rights fa))
+     in ValuationAlgebra (choose ch s1 s2) (combine u1 u2) (combine z1 z2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Divise (divise)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s))
+-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s))
+-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra [Int] [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = divise (\x -> (x, x + 10)) va1 va2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> u [1,2,3]
+-- [1,2,3,13,12,11]
+-- >>> z [1,2,3]
+-- [-1,-2,-3]
+instance (Functor set, Prelude.Semigroup v) => Divise (ValuationAlgebra v set) where
+  divise f (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) =
+    let combine g1 g2 = ValuationAlgebraOp (\fa -> g1 (fmap (fst . f) fa) <> g2 (fmap (snd . f) fa))
+     in ValuationAlgebra (divise f s1 s2) (combine u1 u2) (combine z1 z2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Decide (decide)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let sva1 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ s))
+-- >>> let va1 = ValuationAlgebra sva1 (ValuationAlgebraOp id) (ValuationAlgebraOp (map negate)) :: ValuationAlgebra [Int] [] Int
+-- >>> let sva2 = SemiValuationAlgebra (review applySemigroup (++)) (ProjectValuation (\s v -> v ++ reverse s))
+-- >>> let va2 = ValuationAlgebra sva2 (ValuationAlgebraOp reverse) (ValuationAlgebraOp (const [])) :: ValuationAlgebra [Int] [] Int
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = decide (\x -> if even x then Left x else Right x) va1 va2
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> u [1,2,3,4]
+-- [2,4,3,1]
+-- >>> z [1,2,3,4]
+-- [-2,-4]
+instance (Filterable set, Prelude.Semigroup v) => Decide (ValuationAlgebra v set) where
+  decide ch (ValuationAlgebra s1 (ValuationAlgebraOp u1) (ValuationAlgebraOp z1)) (ValuationAlgebra s2 (ValuationAlgebraOp u2) (ValuationAlgebraOp z2)) =
+    let lefts = mapMaybe (either Just (const Nothing) . ch)
+        rights = mapMaybe (either (const Nothing) Just . ch)
+        combine g1 g2 = ValuationAlgebraOp (\fa -> g1 (lefts fa) <> g2 (rights fa))
+     in ValuationAlgebra (decide ch s1 s2) (combine u1 u2) (combine z1 z2)
+
+-- |
+-- >>> import Data.Functor.Contravariant.Conclude (conclude)
+-- >>> import Data.Void (absurd)
+-- >>> import Data.Valuation.SemiValuationAlgebra (SemiValuationAlgebra(..))
+-- >>> import Data.Valuation.ProjectValuation (ProjectValuation(..))
+-- >>> import Data.Valuation.ValuationAlgebraOp (ValuationAlgebraOp(..))
+-- >>> import Control.Lens (review)
+-- >>> import Data.Valuation.Semigroup (Semigroup, applySemigroup, runSemigroup)
+-- >>> let ValuationAlgebra (SemiValuationAlgebra sg (ProjectValuation p)) (ValuationAlgebraOp u) (ValuationAlgebraOp z) = conclude absurd :: ValuationAlgebra [Int] [] Void
+-- >>> runSemigroup sg [1] [2]
+-- [1,2]
+-- >>> u []
+-- []
+-- >>> z []
+-- []
+instance (Filterable set, Prelude.Semigroup v, Prelude.Monoid v) => Conclude (ValuationAlgebra v set) where
+  conclude f = ValuationAlgebra (conclude f) (ValuationAlgebraOp (const mempty)) (ValuationAlgebraOp (const mempty))
+
+-- | A 'ValuationAlgebra' specialised to 'Set'.
+type SetValuationAlgebra v var =
+  ValuationAlgebra v Set var
diff --git a/src/Data/Valuation/ValuationAlgebraOp.hs b/src/Data/Valuation/ValuationAlgebraOp.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Valuation/ValuationAlgebraOp.hs
@@ -0,0 +1,373 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+-- | An operation on a valuation algebra, a function from a set of variables to a value.
+module Data.Valuation.ValuationAlgebraOp
+  ( ValuationAlgebraOp (..),
+
+    -- * optics
+    HasValuationAlgebraOp (..),
+    AsValuationAlgebraOp (..),
+
+    -- * combinators
+    semigroupValuationAlgebraOp,
+    valuationAlgebraOpProjectValuation,
+    applyHasValuationAlgebraOp,
+    applyAsValuationAlgebraOp,
+  )
+where
+
+import Control.Arrow (Arrow (..), ArrowApply (..), ArrowChoice (..), ArrowLoop (..))
+import Control.Category (Category (..))
+import Control.Comonad (Comonad (..), ComonadApply (..))
+import Control.Lens
+  ( Iso,
+    Lens',
+    Prism',
+    Rewrapped,
+    Wrapped (..),
+    iso,
+    review,
+    _Wrapped,
+  )
+import Control.Monad.Fix (MonadFix (..))
+import Control.Monad.Reader.Class (MonadReader (..))
+import Control.Monad.Zip (MonadZip (..))
+import Control.Selective (Selective (..), selectM)
+import Data.Distributive (Distributive (..))
+import Data.Either (fromLeft, fromRight)
+import Data.Function (fix)
+import Data.Functor.Apply (Apply (..))
+import Data.Functor.Bind (Bind (..))
+import Data.Functor.Extend (Extend (..))
+import Data.Functor.Rep (Representable (..))
+import Data.Profunctor (Choice (..), Profunctor (..), Strong (..))
+import Data.Profunctor.Closed (Closed (..))
+import Data.Profunctor.Sieve (Cosieve (..))
+import Data.Semigroupoid (Semigroupoid (..))
+import Data.Valuation.ProjectValuation (ProjectValuation (..))
+import Data.Valuation.Semigroup
+  ( Semigroup,
+    applySemigroup,
+    runSemigroup,
+  )
+import Prelude hiding (Semigroup, id, (.))
+import qualified Prelude
+
+-- $setup
+-- >>> :set -Wno-name-shadowing -Wno-type-defaults
+
+-- | A function from a set of variables to a value. Isomorphic to @set var -> v@.
+newtype ValuationAlgebraOp set var v
+  = ValuationAlgebraOp (set var -> v)
+
+instance (ValuationAlgebraOp set var v ~ t) => Rewrapped (ValuationAlgebraOp set' var' v') t
+
+instance Wrapped (ValuationAlgebraOp set var v) where
+  type Unwrapped (ValuationAlgebraOp set var v) = set var -> v
+  _Wrapped' =
+    iso (\(ValuationAlgebraOp x) -> x) ValuationAlgebraOp
+
+-- | Classy lens for types that contain a 'ValuationAlgebraOp'.
+class HasValuationAlgebraOp c set var v | c -> set var v where
+  valuationAlgebraOp ::
+    Lens' c (ValuationAlgebraOp set var v)
+
+instance HasValuationAlgebraOp (ValuationAlgebraOp set var v) set var v where
+  valuationAlgebraOp = id
+
+-- | Classy prism for types that can be constructed from a 'ValuationAlgebraOp'.
+class AsValuationAlgebraOp c set var v | c -> set var v where
+  _ValuationAlgebraOp ::
+    Prism' c (ValuationAlgebraOp set var v)
+
+instance AsValuationAlgebraOp (ValuationAlgebraOp set var v) set var v where
+  _ValuationAlgebraOp = id
+
+-- | Iso between a 'ValuationAlgebraOp' producing an endomorphism and a 'ProjectValuation'.
+valuationAlgebraOpProjectValuation :: Iso (ValuationAlgebraOp set var (v -> v)) (ValuationAlgebraOp set' var' (v' -> v')) (ProjectValuation v set var) (ProjectValuation v' set' var')
+valuationAlgebraOpProjectValuation =
+  iso
+    (\(ValuationAlgebraOp k) -> ProjectValuation k)
+    (\(ProjectValuation k) -> ValuationAlgebraOp k)
+
+-- | Lens to the underlying function of a 'HasValuationAlgebraOp'.
+applyHasValuationAlgebraOp :: (HasValuationAlgebraOp op set var v) => Lens' op (set var -> v)
+applyHasValuationAlgebraOp = valuationAlgebraOp . _Wrapped
+
+-- | Prism to the underlying function of an 'AsValuationAlgebraOp'.
+applyAsValuationAlgebraOp :: (AsValuationAlgebraOp op set var v) => Prism' op (set var -> v)
+applyAsValuationAlgebraOp = _ValuationAlgebraOp . _Wrapped
+
+-- |
+-- >>> let ValuationAlgebraOp f = fmap (*2) (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- 12
+instance Functor (ValuationAlgebraOp set a) where
+  fmap f (ValuationAlgebraOp g) = ValuationAlgebraOp (f . g)
+
+-- |
+-- >>> import Data.Functor.Apply ((<.>))
+-- >>> let ValuationAlgebraOp f = (ValuationAlgebraOp (\s -> (+ sum s)) :: ValuationAlgebraOp [] Int (Int -> Int)) <.> ValuationAlgebraOp product
+-- >>> f [1,2,3]
+-- 12
+instance Apply (ValuationAlgebraOp set a) where
+  ValuationAlgebraOp f <.> ValuationAlgebraOp g = ValuationAlgebraOp (\sa -> f sa (g sa))
+
+-- |
+-- >>> let ValuationAlgebraOp f = pure 42 :: ValuationAlgebraOp [] Int Int
+-- >>> f [1,2,3]
+-- 42
+--
+-- >>> let ValuationAlgebraOp f = (ValuationAlgebraOp (\s -> (+ sum s)) :: ValuationAlgebraOp [] Int (Int -> Int)) <*> ValuationAlgebraOp product
+-- >>> f [1,2,3]
+-- 12
+instance Applicative (ValuationAlgebraOp set a) where
+  pure b = ValuationAlgebraOp (const b)
+  (<*>) = (<.>)
+
+-- |
+-- >>> import Data.Functor.Bind ((>>-))
+-- >>> let ValuationAlgebraOp f = (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int) >>- (\n -> ValuationAlgebraOp (\s -> n + product s))
+-- >>> f [1,2,3]
+-- 12
+instance Bind (ValuationAlgebraOp set a) where
+  ValuationAlgebraOp f >>- k = ValuationAlgebraOp (\sa -> let ValuationAlgebraOp g = k (f sa) in g sa)
+
+-- |
+-- >>> let ValuationAlgebraOp f = (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int) >>= (\n -> ValuationAlgebraOp (\s -> n * length s))
+-- >>> f [1,2,3]
+-- 18
+--
+-- >>> let ValuationAlgebraOp f = return 42 :: ValuationAlgebraOp [] Int Int
+-- >>> f [1,2,3]
+-- 42
+instance Monad (ValuationAlgebraOp set a) where
+  (>>=) = (>>-)
+
+-- |
+-- >>> import Data.Semigroupoid (o)
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = o (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int) (ValuationAlgebraOp sum)
+-- >>> f (1 :| [2, 3])
+-- 14
+instance (Extend set) => Semigroupoid (ValuationAlgebraOp set) where
+  o (ValuationAlgebraOp g) (ValuationAlgebraOp f) = ValuationAlgebraOp (g . extended f)
+
+-- |
+-- >>> import Control.Category (id, (.))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = id :: ValuationAlgebraOp NonEmpty Int Int
+-- >>> f (1 :| [2, 3])
+-- 1
+--
+-- >>> import Control.Category ((.))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int) . ValuationAlgebraOp sum
+-- >>> f (1 :| [2, 3])
+-- 14
+instance (Comonad set) => Category (ValuationAlgebraOp set) where
+  id = ValuationAlgebraOp extract
+  ValuationAlgebraOp g . ValuationAlgebraOp f = ValuationAlgebraOp (g . extend f)
+
+-- |
+-- >>> import Control.Arrow (arr, first)
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = arr (*2) :: ValuationAlgebraOp NonEmpty Int Int
+-- >>> f (3 :| [4, 5])
+-- 6
+--
+-- >>> import Control.Arrow (first)
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = first (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f ((1, "a") :| [(2, "b"), (3, "c")])
+-- (6,"a")
+instance (Comonad set) => Arrow (ValuationAlgebraOp set) where
+  arr f = ValuationAlgebraOp (f . extract)
+  first = first'
+
+-- |
+-- >>> import Control.Arrow (left)
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = left (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f (Left 1 :| [Left 2, Left 3])
+-- Left 6
+-- >>> f (Right "hi" :| [Left 2])
+-- Right "hi"
+instance (Comonad set) => ArrowChoice (ValuationAlgebraOp set) where
+  left = left'
+
+-- |
+-- >>> import Control.Arrow (app)
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = app :: ValuationAlgebraOp NonEmpty (ValuationAlgebraOp NonEmpty Int Int, Int) Int
+-- >>> f ((ValuationAlgebraOp sum, 99) :| [(ValuationAlgebraOp product, 1)])
+-- 100
+instance (Comonad set) => ArrowApply (ValuationAlgebraOp set) where
+  app = ValuationAlgebraOp $ \wpair ->
+    let (ValuationAlgebraOp f, _) = extract wpair
+     in f (fmap snd wpair)
+
+-- |
+-- >>> import Control.Arrow (loop)
+-- >>> import Data.Functor.Identity (Identity(..))
+-- >>> let ValuationAlgebraOp f = loop (ValuationAlgebraOp (\(Identity (b, _)) -> (b * 2, 0))) :: ValuationAlgebraOp Identity Int Int
+-- >>> f (Identity 3)
+-- 6
+instance (ComonadApply set) => ArrowLoop (ValuationAlgebraOp set) where
+  loop (ValuationAlgebraOp f) = ValuationAlgebraOp $ \wa ->
+    fst . extract $ fix $ \wbd -> extend f ((,) <$> wa <@> fmap snd wbd)
+
+-- |
+-- >>> import Control.Monad.Fix (mfix)
+-- >>> let ValuationAlgebraOp f = mfix (\x -> ValuationAlgebraOp (\s -> const 42 x + sum s)) :: ValuationAlgebraOp [] Int Int
+-- >>> f [1,2,3]
+-- 48
+instance MonadFix (ValuationAlgebraOp set var) where
+  mfix f = ValuationAlgebraOp (\s -> fix (\a -> let ValuationAlgebraOp g = f a in g s))
+
+-- |
+-- >>> import Control.Monad.Zip (mzipWith)
+-- >>> let ValuationAlgebraOp f = mzipWith (+) (ValuationAlgebraOp sum) (ValuationAlgebraOp product :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- 12
+instance MonadZip (ValuationAlgebraOp set var) where
+  mzipWith f (ValuationAlgebraOp g) (ValuationAlgebraOp h) = ValuationAlgebraOp (\s -> f (g s) (h s))
+
+-- |
+-- >>> import Control.Selective (select)
+-- >>> let ValuationAlgebraOp f = select (ValuationAlgebraOp (\s -> Left (sum s)) :: ValuationAlgebraOp [] Int (Either Int Int)) (ValuationAlgebraOp (\_ -> (+10)))
+-- >>> f [1,2,3]
+-- 16
+instance Selective (ValuationAlgebraOp set var) where
+  select = selectM
+
+-- |
+-- >>> import Control.Monad.Reader.Class (ask, local)
+-- >>> let ValuationAlgebraOp f = ask :: ValuationAlgebraOp [] Int [Int]
+-- >>> f [1,2,3]
+-- [1,2,3]
+--
+-- >>> import Control.Monad.Reader.Class (ask, local)
+-- >>> let ValuationAlgebraOp f = local (map (*2)) (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- 12
+instance MonadReader (set var) (ValuationAlgebraOp set var) where
+  ask = ValuationAlgebraOp id
+  local f (ValuationAlgebraOp g) = ValuationAlgebraOp (g . f)
+
+-- |
+-- >>> import Data.Profunctor (dimap, lmap, rmap)
+-- >>> let ValuationAlgebraOp f = dimap (+1) (*2) (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- 18
+--
+-- >>> import Data.Profunctor (lmap)
+-- >>> let ValuationAlgebraOp f = lmap (*10) (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- 60
+--
+-- >>> import Data.Profunctor (rmap)
+-- >>> let ValuationAlgebraOp f = rmap show (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [1,2,3]
+-- "6"
+instance (Functor set) => Profunctor (ValuationAlgebraOp set) where
+  dimap f g (ValuationAlgebraOp h) = ValuationAlgebraOp (g . h . fmap f)
+  lmap f (ValuationAlgebraOp h) = ValuationAlgebraOp (h . fmap f)
+  rmap g (ValuationAlgebraOp h) = ValuationAlgebraOp (g . h)
+
+-- |
+-- >>> import Data.Profunctor (Strong(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = first' (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f ((1, "a") :| [(2, "b"), (3, "c")])
+-- (6,"a")
+--
+-- >>> import Data.Profunctor (Strong(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = second' (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f (("a", 1) :| [("b", 2), ("c", 3)])
+-- ("a",6)
+instance (Comonad set) => Strong (ValuationAlgebraOp set) where
+  first' (ValuationAlgebraOp f) = ValuationAlgebraOp (\sac -> (f (fmap fst sac), snd (extract sac)))
+  second' (ValuationAlgebraOp f) = ValuationAlgebraOp (\sca -> (fst (extract sca), f (fmap snd sca)))
+
+-- |
+-- >>> import Data.Profunctor (Choice(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = left' (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f (Left 1 :| [Left 2, Left 3])
+-- Left 6
+-- >>> f (Right "hi" :| [Left 2])
+-- Right "hi"
+--
+-- >>> import Data.Profunctor (Choice(..))
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> let ValuationAlgebraOp f = right' (ValuationAlgebraOp sum :: ValuationAlgebraOp NonEmpty Int Int)
+-- >>> f (Right 1 :| [Right 2, Right 3])
+-- Right 6
+-- >>> f (Left "hi" :| [Right 2])
+-- Left "hi"
+instance (Comonad set) => Choice (ValuationAlgebraOp set) where
+  left' (ValuationAlgebraOp f) = ValuationAlgebraOp $ \seac ->
+    case extract seac of
+      Left a -> Left (f (fmap (fromLeft a) seac))
+      Right c -> Right c
+  right' (ValuationAlgebraOp f) = ValuationAlgebraOp $ \seca ->
+    case extract seca of
+      Right a -> Right (f (fmap (fromRight a) seca))
+      Left c -> Left c
+
+-- |
+-- >>> import Data.Profunctor.Closed (Closed(..))
+-- >>> let ValuationAlgebraOp f = closed (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int)
+-- >>> f [(*2), (*3)] 10
+-- 50
+instance (Functor set) => Closed (ValuationAlgebraOp set) where
+  closed (ValuationAlgebraOp f) = ValuationAlgebraOp (\sxa x -> f (fmap ($ x) sxa))
+
+-- |
+-- >>> import Data.Profunctor.Sieve (Cosieve(..))
+-- >>> cosieve (ValuationAlgebraOp sum :: ValuationAlgebraOp [] Int Int) [1,2,3]
+-- 6
+instance (Functor set) => Cosieve (ValuationAlgebraOp set) set where
+  cosieve (ValuationAlgebraOp f) = f
+
+-- |
+-- >>> import Data.Distributive (distribute)
+-- >>> let ValuationAlgebraOp f = distribute [ValuationAlgebraOp sum, ValuationAlgebraOp product] :: ValuationAlgebraOp [] Int [Int]
+-- >>> f [1,2,3]
+-- [6,6]
+instance Distributive (ValuationAlgebraOp set var) where
+  distribute fs = ValuationAlgebraOp (\s -> fmap (\(ValuationAlgebraOp g) -> g s) fs)
+
+-- |
+-- >>> import Data.Functor.Rep (tabulate, index)
+-- >>> let vao = tabulate (\s -> sum s * 2) :: ValuationAlgebraOp [] Int Int
+-- >>> index vao [1,2,3]
+-- 12
+instance Representable (ValuationAlgebraOp set var) where
+  type Rep (ValuationAlgebraOp set var) = set var
+  tabulate = ValuationAlgebraOp
+  index (ValuationAlgebraOp f) = f
+
+-- |
+-- >>> let ValuationAlgebraOp f = runSemigroup semigroupValuationAlgebraOp (ValuationAlgebraOp (const "hello")) (ValuationAlgebraOp (const " world") :: ValuationAlgebraOp [] Int String) in f []
+-- "hello world"
+semigroupValuationAlgebraOp :: (Prelude.Semigroup v) => Semigroup (ValuationAlgebraOp set var v)
+semigroupValuationAlgebraOp = review applySemigroup (\(ValuationAlgebraOp f) (ValuationAlgebraOp g) -> ValuationAlgebraOp (\s -> f s <> g s))
+
+-- |
+-- >>> let ValuationAlgebraOp f = ValuationAlgebraOp (const "hello") <> (ValuationAlgebraOp (const " world") :: ValuationAlgebraOp [] Int String) in f []
+-- "hello world"
+instance (Prelude.Semigroup v) => Prelude.Semigroup (ValuationAlgebraOp set var v) where
+  (<>) = runSemigroup semigroupValuationAlgebraOp
+
+-- |
+-- >>> let ValuationAlgebraOp f = mempty :: ValuationAlgebraOp [] Int String in f [1,2,3]
+-- ""
+instance (Prelude.Monoid v) => Prelude.Monoid (ValuationAlgebraOp set var v) where
+  mempty = ValuationAlgebraOp (const mempty)
diff --git a/valuations.cabal b/valuations.cabal
new file mode 100644
--- /dev/null
+++ b/valuations.cabal
@@ -0,0 +1,54 @@
+name:                 valuations
+version:              0.0.1
+synopsis:             Valuations
+description:          Valuations: Valuation and Valuation Algebra sdfgsdf
+license:              BSD3
+license-file:         LICENCE
+author:               Tony Morris <ʇǝu˙sıɹɹoɯʇ@ןןǝʞsɐɥ>
+maintainer:           Tony Morris <ʇǝu˙sıɹɹoɯʇ@ןןǝʞsɐɥ>
+copyright:            Copyright (C) 2026 Tony Morris
+category:             Test
+build-type:           Simple
+extra-source-files:   changelog.md
+cabal-version:        >=1.10
+homepage:             https://gitlab.com/tonymorris/valuations
+bug-reports:          https://gitlab.com/tonymorris/valuations/issues
+tested-with:          GHC == 9.6.7
+
+source-repository     head
+  type:               git
+  location:           git@gitlab.com:tonymorris/valuations.git
+
+library
+  exposed-modules:
+                      Data.Valuation
+                      Data.Valuation.BinaryFunction
+                      Data.Valuation.DomainLattice
+                      Data.Valuation.PartialOrder
+                      Data.Valuation.PresheafValuationAlgebra
+                      Data.Valuation.ProjectValuation
+                      Data.Valuation.Semigroup
+                      Data.Valuation.SemiValuationAlgebra
+                      Data.Valuation.Valuation
+                      Data.Valuation.ValuationAlgebra
+                      Data.Valuation.ValuationAlgebraOp
+
+  build-depends:        base >= 4.8 && < 6
+                      , adjunctions >= 4.4 && < 5
+                      , bifunctors >= 5 && < 6
+                      , comonad >= 5 && < 6
+                      , containers >= 0.5 && < 1
+                      , contravariant >= 1 && < 2
+                      , distributive >= 0.5 && < 1
+                      , lens >= 4 && < 6
+                      , mtl >= 2.2 && < 3
+                      , profunctors >= 5 && < 6
+                      , selective >= 0.7.0.1 && < 1
+                      , semigroupoids >= 5.2 && < 7
+                      , witherable >= 0.4 && < 1
+
+  hs-source-dirs:     src
+
+  default-language:   Haskell2010
+
+  ghc-options:        -Wall