diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,7 @@
+# Change log
+
+noether uses [Semantic Versioning][].
+The change log is available through the [releases on GitHub][].
+
+[Semantic Versioning]: http://semver.org/spec/v2.0.0.html
+[releases on GitHub]: https://github.com/mrkgnao/noether/releases
diff --git a/LICENSE.md b/LICENSE.md
new file mode 100644
--- /dev/null
+++ b/LICENSE.md
@@ -0,0 +1,23 @@
+[The MIT License (MIT)][]
+
+Copyright (c) 2017 Soham Chowdhury
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+of the Software, and to permit persons to whom the Software is furnished to do
+so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+
+[The MIT License (MIT)]: https://opensource.org/licenses/MIT
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,108 @@
+[![ii](https://img.shields.io/badge/IncoherentInstances-%E2%9C%93-brightgreen.svg)]()
+
+# Noether
+
+A very WIP number theory / abstract algebra playground in Haskell. 
+
+The part I'm working on at present develops a highly polymorphic numeric hierarchy. Unlike almost every other project (including the great `subhask`, which is by far the biggest inspiration for this project), all typeclasses representing algebraic structures are "tagged" with the operations that the base type supports. The intention is to have, without newtyping, things like automatically specified *L*-vector space instances for any *K*-vector space with *K / L* a (nice) field extension.
+
+While it may not be inevitable, my inexperienced preliminary encoding of these ideas has delightful consequences like
+
+```haskell
+instance {-# INCOHERENT #-}
+         ( DotProductSpace' k v
+         , DotProductSpace' k w
+         , p ~ Add
+         , m ~ Mul
+         ) => InnerProductSpace DotProduct p m k Add (v, w) where
+```
+
+that I don't know how to "kill with fire".
+
+Obviously, I'm still exploring the design space to try and find a good balance between avoiding arbitrary choices (e.g. no privileged `Monoid` instances for `Double` and the like) and a useful level of type inference. In large part, this means that I'm trying not to run up against trouble with instance resolution and failing hard (see above), or discovering that associated types are sometimes less permissive than one would like.
+
+The numeric hierarchy, at present, extends to functions like this:
+
+```haskell
+(%<) :: LeftModule' r v => r -> v -> v
+r %< v = leftAct AddP AddP MulP r v
+
+-- | Linear interpolation.
+-- lerp λ v w = λv + (1 - λ)w
+lerp
+  :: VectorSpace' r v
+  => r -> v -> v -> v
+lerp lambda v w = lambda %< v + w >% (one - lambda)
+
+lol :: (Complex Double, Complex Double)
+lol =
+  (1, 3) * lerp lambda (3, 3) (4, 5) + (1, 0) >% lambda + v + lambda %< w +
+  (lambda, -lambda)
+
+  where
+    lambda :: Complex Double
+    lambda = 0.3 :+ 1
+
+    v = (3, 3)
+    w = (2, 7)
+```
+
+A preliminary implementation of linear maps between (what should be) free modules is being developed after the design in Conal Elliott's "Reimagining matrices". The added polymorphism and lack of fixed `Scalar a`-esque base fields is an interesting challenge, and Conal's basic GADT decomposition of linear maps changes in my case to
+
+```haskell
+data (\>) :: (* -> * -> * -> *) where
+```
+
+where the first "slot" is for the base field. With a nice `~>` type operator (which is basically `$`), a linear map between two *k*-vector space types `a` and `b` has the type 
+
+```haskell
+func :: k \> a ~> b
+```
+
+paving the way for the representation of the category _k_-**Vect** as `(\>) k :: (* -> * -> *)`.
+
+Some sample function signatures:
+
+```haskell
+
+-- | Converts a linear map into a function.
+apply :: k \> a ~> b -> a -> b
+
+compose
+  :: k \> a ~> b
+  -> k \>      b ~> c
+  -> k \> a ~>      c
+```
+
+Usage looks like this for now:
+
+```
+> apply (rotate (pi / 4 :: Double)) (1,1)
+(1.1102230246251565e-16,1.414213562373095)
+```
+
+# Other stuff
+
+Some other stuff I'm thinking about includes polymorphic numeric literals, possibly along the lines of this:
+
+```haskell
+type family NumericLit (n :: Nat) = (c :: * -> Constraint) where
+  NumericLit 0 = Neutral Add
+  NumericLit 1 = Neutral Mul
+  -- NumericLit 2 = Field Add Mul
+  -- NumericLit n = NumericLit (n - 1)
+  NumericLit n = Ring Add Mul
+
+fromIntegerP :: forall n a. (KnownNat n, NumericLit n a) => Proxy n -> a
+fromIntegerP p =
+  case sameNat p (Proxy :: Proxy 0) of
+    Just prf -> gcastWith prf zero'
+    Nothing -> case sameNat p (Proxy :: Proxy 1) of
+      Just prf -> gcastWith prf one'
+      Nothing -> undefined -- unsafeCoerce (val (Proxy :: Proxy a))
+        -- where
+        --   val :: (Field Add Mul b) => Proxy b -> b
+        --   val _ = one + undefined -- fromIntegerP (Proxy :: Proxy (n - 1))
+```
+
+The original core of the project is a short implementation of elliptic curve addition over Q, which I've put on hold temporarily as I try to work out the issues outlined above first. This part uses a Protolude "fork" called Lemmata that I expect will evolve over time.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,7 @@
+-- This script is used to build and install your package. Typically you don't
+-- need to change it. The Cabal documentation has more information about this
+-- file: <https://www.haskell.org/cabal/users-guide/installing-packages.html>.
+import qualified Distribution.Simple
+
+main :: IO ()
+main = Distribution.Simple.defaultMain
diff --git a/benchmark/Main.hs b/benchmark/Main.hs
new file mode 100644
--- /dev/null
+++ b/benchmark/Main.hs
@@ -0,0 +1,6 @@
+-- You can benchmark your code quickly and effectively with Criterion. See its
+-- website for help: <http://www.serpentine.com/criterion/>.
+import Criterion.Main
+
+main :: IO ()
+main = defaultMain [bench "const" (whnf const ())]
diff --git a/executable/Main.hs b/executable/Main.hs
new file mode 100644
--- /dev/null
+++ b/executable/Main.hs
@@ -0,0 +1,8 @@
+-- It is generally a good idea to keep all your business logic in your library
+-- and only use it in the executable. Doing so allows others to use what you
+-- wrote in their libraries.
+
+import           Lemmata
+
+main :: IO ()
+main = putText "cool and good"
diff --git a/library/Lemmata.hs b/library/Lemmata.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata.hs
@@ -0,0 +1,596 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+module Lemmata (
+  module X,
+  module Base,
+  identity,
+  map,
+  uncons,
+  unsnoc,
+  applyN,
+  print,
+  throwIO,
+  throwTo,
+  foreach,
+  show,
+  pass,
+  guarded,
+  guardedA,
+  LText,
+  LByteString,
+  liftIO1,
+  liftIO2,
+#if !MIN_VERSION_base(4,8,0)
+  (&),
+#endif
+) where
+
+-- Protolude module exports.
+import Lemmata.List as X
+import Lemmata.Show as X
+import Lemmata.Bool as X
+import Lemmata.Debug as X
+import Lemmata.Monad as X
+import Lemmata.Functor as X
+import Lemmata.Either as X
+import Lemmata.Applicative as X
+import Lemmata.Conv as X
+import Lemmata.Panic as X
+import Lemmata.Exceptions as X
+import Lemmata.Semiring as X
+
+import Lemmata.Base as Base hiding (
+    putStr           -- Overriden by Show.putStr
+  , putStrLn         -- Overriden by Show.putStrLn
+  , print            -- Overriden by Protolude.print
+  , error            -- Overriden by Debug.error
+  , undefined        -- Overriden by Debug.undefined
+  , show             -- Overriden by Protolude.show
+  , showFloat        -- Custom Show instances deprecated.
+  , showList         -- Custom Show instances deprecated.
+  , showSigned       -- Custom Show instances deprecated.
+  , showSignedFloat  -- Custom Show instances deprecated.
+  , showsPrec        -- Custom Show instances deprecated.
+  )
+import qualified Lemmata.Base as PBase
+
+-- Used for 'show', not exported.
+import Data.String (String)
+import Data.String as X (IsString)
+
+-- Maybe'ized version of partial functions
+import Safe as X (
+    headMay
+  , headDef
+  , initMay
+  , initDef
+  , initSafe
+  , tailMay
+  , tailDef
+  , tailSafe
+  , lastDef
+  , lastMay
+  , foldr1May
+  , foldl1May
+  , atMay
+  , atDef
+  )
+
+-- Applicatives
+import Control.Applicative as X (
+    Applicative(..)
+  , Alternative(..)
+  , Const(..)
+  , ZipList(..)
+  , (<**>)
+  , liftA
+  , liftA2
+  , liftA3
+  , optional
+  )
+
+-- Base typeclasses
+import Data.Eq as X (
+    Eq(..)
+  )
+import Data.Ord as X (
+    Ord(..)
+  , Ordering(..)
+  , Down(..)
+  , comparing
+  )
+import Data.Traversable as X
+import Data.Foldable as X hiding (
+    foldr1
+  , foldl1
+  , product
+  , sum
+  )
+import Data.Functor.Identity as X (
+    Identity(..)
+  )
+
+#if MIN_VERSION_base(4,9,0)
+import Data.List.NonEmpty as X (
+    NonEmpty(..)
+  , nonEmpty
+  )
+import Data.Semigroup as X (
+    Semigroup(sconcat, stimes)
+  , WrappedMonoid
+  , Option(..)
+  , option
+  , diff
+  , cycle1
+  , stimesMonoid
+  , stimesIdempotent
+  , stimesIdempotentMonoid
+  , mtimesDefault
+  )
+#endif
+
+import Data.Monoid  as X
+
+#if !MIN_VERSION_base(4,8,0)
+import Bifunctor as X (Bifunctor(..))
+#else
+import Data.Bifunctor as X (Bifunctor(..))
+#endif
+
+-- Deepseq
+import Control.DeepSeq as X (
+    NFData(..)
+  , ($!!)
+  , deepseq
+  , force
+  )
+
+-- Data structures
+import Data.Tuple as X (
+    fst
+  , snd
+  , curry
+  , uncurry
+  , swap
+  )
+
+import Data.List as X (
+    splitAt
+  , break
+  , intercalate
+  , isPrefixOf
+  , drop
+  , filter
+  , reverse
+  , replicate
+  , take
+  , sortBy
+  , sort
+  , intersperse
+  , transpose
+  , subsequences
+  , permutations
+  , scanl
+  , scanr
+  , iterate
+  , repeat
+  , cycle
+  , unfoldr
+  , takeWhile
+  , dropWhile
+  , group
+  , inits
+  , tails
+  , zipWith
+  , zip
+  , unzip
+  , genericLength
+  , genericTake
+  , genericDrop
+  , genericSplitAt
+  , genericReplicate
+  )
+
+-- Hashing
+import Data.Hashable as X (
+    Hashable
+  , hash
+  , hashWithSalt
+  , hashUsing
+  )
+
+import Data.Map as X (Map)
+import Data.Set as X (Set)
+import Data.Sequence as X (Seq)
+import Data.IntMap as X (IntMap)
+import Data.IntSet as X (IntSet)
+
+#if MIN_VERSION_base(4,7,0)
+import Data.Proxy as X (
+    Proxy(..)
+  )
+
+import Data.Typeable as X (
+    TypeRep
+  , Typeable
+  , typeRep
+  , cast
+  , eqT
+  )
+
+import Data.Type.Coercion as X (
+    Coercion(..)
+  , coerceWith
+  , repr
+  )
+
+import Data.Type.Equality as X (
+    (:~:)(..)
+  , type (==)
+  , sym
+  , trans
+  , castWith
+  , gcastWith
+  )
+
+#endif
+
+#if MIN_VERSION_base(4,8,0)
+import Data.Void as X (
+    Void
+  , absurd
+  , vacuous
+  )
+#endif
+
+-- Monad transformers
+import Control.Monad.State as X (
+    MonadState
+  , State
+  , StateT(StateT)
+  , put
+  , get
+  , gets
+  , modify
+  , state
+  , withState
+
+  , runState
+  , execState
+  , evalState
+
+  , runStateT
+  , execStateT
+  , evalStateT
+  )
+
+import Control.Monad.Reader as X (
+    MonadReader
+  , Reader
+  , ReaderT(ReaderT)
+  , ask
+  , asks
+  , local
+  , reader
+  , runReader
+  , runReaderT
+  )
+
+import Control.Monad.Except as X (
+    MonadError
+  , Except
+  , ExceptT(ExceptT)
+  , throwError
+  , catchError
+  , runExcept
+  , runExceptT
+  )
+
+import Control.Monad.Trans as X (
+    MonadIO
+  , lift
+  , liftIO
+  )
+
+-- Base types
+import Data.Int as X (
+    Int
+  , Int8
+  , Int16
+  , Int32
+   , Int64
+  )
+import Data.Bits as X hiding (
+    unsafeShiftL
+  , unsafeShiftR
+  )
+import Data.Word as X (
+    Word
+  , Word8
+  , Word16
+  , Word32
+  , Word64
+#if MIN_VERSION_base(4,7,0)
+  , byteSwap16
+  , byteSwap32
+  , byteSwap64
+#endif
+  )
+
+import Data.Either as X (
+    Either(..)
+  , either
+  , lefts
+  , rights
+  , partitionEithers
+#if MIN_VERSION_base(4,7,0)
+  , isLeft
+  , isRight
+#endif
+  )
+
+import Data.Complex as X (
+    Complex(..)
+  , realPart
+  , imagPart
+  , mkPolar
+  , cis
+  , polar
+  , magnitude
+  , phase
+  , conjugate
+  )
+import Data.Char as X (chr)
+import Data.Bool as X hiding (bool)
+import Data.Maybe as X hiding (fromJust)
+
+import Data.Function as X (
+    const
+  , (.)
+  , ($)
+  , flip
+  , fix
+  , on
+#if MIN_VERSION_base(4,8,0)
+  , (&)
+#endif
+  )
+
+-- Genericss
+import GHC.Generics as X (
+    Generic(..)
+  , Generic1
+  , Rep
+  , K1(..)
+  , M1(..)
+  , U1(..)
+  , V1
+  , D1
+  , C1
+  , S1
+  , (:+:)(..)
+  , (:*:)(..)
+  , (:.:)(..)
+  , Rec0
+  , Constructor(..)
+  , Datatype(..)
+  , Selector(..)
+  , Fixity(..)
+  , Associativity(..)
+#if ( __GLASGOW_HASKELL__ >= 800 )
+  , Meta(..)
+  , FixityI(..)
+  , URec
+#endif
+  )
+
+-- ByteString
+import qualified Data.ByteString.Lazy
+import Data.ByteString as X (ByteString)
+
+-- Text
+import Data.Text as X (Text)
+import qualified Data.Text.Lazy
+
+import Data.Text.IO as X (
+    getLine
+  , getContents
+  , interact
+  , readFile
+  , writeFile
+  , appendFile
+  )
+
+import Data.Text.Lazy as X (
+    toStrict
+  , fromStrict
+  )
+
+import Data.Text.Encoding as X (
+    encodeUtf8
+  , decodeUtf8
+  , decodeUtf8'
+  , decodeUtf8With
+  )
+
+import Data.Text.Encoding.Error as X (
+    OnDecodeError
+  , OnError
+  , UnicodeException
+  , lenientDecode
+  , strictDecode
+  , ignore
+  , replace
+  )
+
+-- IO
+import System.Environment as X (getArgs)
+import System.Exit as X (
+    ExitCode(..)
+  , exitWith
+  , exitFailure
+  , exitSuccess
+#if MIN_VERSION_base(4,8,0)
+  , die
+#endif
+  )
+import System.IO as X (
+    Handle
+  , FilePath
+  , IOMode(..)
+  , stdin
+  , stdout
+  , stderr
+  , withFile
+  , openFile
+  )
+
+-- ST
+import Control.Monad.ST as X (
+    ST
+  , runST
+  , fixST
+  )
+
+-- Concurrency and Parallelism
+import Control.Exception as X hiding (
+    throw    -- Impure throw is forbidden.
+  , throwIO
+  , throwTo
+  , assert
+  , Handler(..)
+  )
+
+import qualified Control.Exception
+
+import Control.Monad.STM as X (
+    STM
+  , atomically
+  , always
+  , alwaysSucceeds
+  , retry
+  , orElse
+  , check
+  , throwSTM
+  , catchSTM
+  )
+import Control.Concurrent as X hiding (
+    throwTo
+  , yield
+  )
+import Control.Concurrent.Async as X (
+    Async(..)
+  , Concurrently(..)
+  , async
+  , asyncBound
+  , asyncOn
+  , withAsync
+  , withAsyncBound
+  , withAsyncOn
+  , wait
+  , poll
+  , waitCatch
+  , cancel
+  , cancelWith
+  , asyncThreadId
+  , waitAny
+  , waitAnyCatch
+  , waitAnyCancel
+  , waitAnyCatchCancel
+  , waitEither
+  , waitEitherCatch
+  , waitEitherCancel
+  , waitEitherCatchCancel
+  , waitEither_
+  , waitBoth
+  , link
+  , link2
+  , race
+  , race_
+  , concurrently
+  )
+
+import Foreign.Storable as X (Storable)
+
+-- Read instances hiding unsafe builtins (read)
+import Text.Read as X (
+    Read
+  , reads
+  , readMaybe
+  , readEither
+  )
+
+-- Type synonymss for lazy texts
+type LText = Data.Text.Lazy.Text
+type LByteString = Data.ByteString.Lazy.ByteString
+
+
+#if !MIN_VERSION_base(4,8,0)
+infixl 1 &
+
+(&) :: a -> (a -> b) -> b
+x & f = f x
+#endif
+
+identity :: a -> a
+identity x = x
+
+map :: Functor f => (a -> b) -> f a -> f b
+map = fmap
+
+uncons :: [a] -> Maybe (a, [a])
+uncons [] = Nothing
+uncons (x:xs) = Just (x, xs)
+
+unsnoc :: [x] -> Maybe ([x],x)
+unsnoc = foldr go Nothing
+  where
+    go x mxs = Just (case mxs of
+       Nothing -> ([], x)
+       Just (xs, e) -> (x:xs, e))
+
+applyN :: Int -> (a -> a) -> a -> a
+applyN n f = X.foldr (.) identity (X.replicate n f)
+
+print :: (X.MonadIO m, PBase.Show a) => a -> m ()
+print = liftIO . PBase.print
+
+throwIO :: (X.MonadIO m, Exception e) => e -> m a
+throwIO = liftIO . Control.Exception.throwIO
+
+throwTo :: (X.MonadIO m, Exception e) => ThreadId -> e -> m ()
+throwTo tid e = liftIO (Control.Exception.throwTo tid e)
+
+foreach :: Functor f => f a -> (a -> b) -> f b
+foreach = flip fmap
+
+-- | Do nothing returning unit inside applicative.
+pass :: Applicative f => f ()
+pass = pure ()
+
+guarded :: (Alternative f) => (a -> Bool) -> a -> f a
+guarded p x = X.bool empty (pure x) (p x)
+
+guardedA :: (Functor f, Alternative t) => (a -> f Bool) -> a -> f (t a)
+guardedA p x = X.bool empty (pure x) <$> p x
+
+-- | Lift an 'IO' operation with 1 argument into another monad
+liftIO1 :: MonadIO m => (a -> IO b) -> a -> m b
+liftIO1 = (.) liftIO
+
+-- | Lift an 'IO' operation with 2 arguments into another monad
+liftIO2 :: MonadIO m => (a -> b -> IO c) -> a -> b -> m c
+liftIO2 = ((.).(.)) liftIO
+
+show :: (Show a, StringConv String b) => a -> b
+show x = toS (PBase.show x)
+{-# SPECIALIZE show :: Show  a => a -> Text  #-}
+{-# SPECIALIZE show :: Show  a => a -> LText  #-}
+{-# SPECIALIZE show :: Show  a => a -> ByteString  #-}
+{-# SPECIALIZE show :: Show  a => a -> LByteString  #-}
+{-# SPECIALIZE show :: Show  a => a -> String  #-}
diff --git a/library/Lemmata/Applicative.hs b/library/Lemmata/Applicative.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Applicative.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Applicative (
+  orAlt,
+  orEmpty,
+  eitherA,
+  purer,
+  liftAA2,
+  (<<*>>),
+) where
+
+import           Control.Applicative
+import           Data.Bool           (Bool)
+import           Data.Either         (Either (..))
+import           Data.Function       ((.))
+import           Data.Monoid         (Monoid (..))
+
+orAlt :: (Alternative f, Monoid a) => f a -> f a
+orAlt f = f <|> pure mempty
+
+orEmpty :: Alternative f => Bool -> a -> f a
+orEmpty b a = if b then pure a else empty
+
+eitherA :: (Alternative f) => f a -> f b -> f (Either a b)
+eitherA a b = (Left <$> a) <|> (Right <$> b)
+
+purer :: (Applicative f, Applicative g) => a -> f (g a)
+purer = pure . pure
+
+liftAA2 :: (Applicative f, Applicative g) => (a -> b -> c) -> f (g a) -> f (g b) -> f (g c)
+liftAA2 = liftA2 . liftA2
+
+(<<*>>) :: (Applicative f, Applicative g)  => f (g (a -> b)) -> f (g a) -> f (g b)
+(<<*>>) = liftA2 (<*>)
diff --git a/library/Lemmata/Base.hs b/library/Lemmata/Base.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Base.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE Unsafe #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+
+module Lemmata.Base (
+  module X,
+  ($!),
+) where
+
+-- Glorious Glasgow Haskell Compiler
+#if defined(__GLASGOW_HASKELL__) && ( __GLASGOW_HASKELL__ >= 600 )
+
+-- Base GHC types
+import GHC.Num as X (
+    Num(..)
+  , Integer
+  , subtract
+  )
+import GHC.Enum as X (
+    Bounded(..)
+  , Enum(..)
+  , boundedEnumFrom
+  , boundedEnumFromThen
+  )
+import GHC.Real as X
+import GHC.Float as X (
+    Float(..)
+  , Double(..)
+  , Floating (..)
+  , showFloat
+  , showSignedFloat
+  )
+import GHC.Err as X (
+    undefined
+  , error
+  )
+import GHC.Show as X (
+    Show(..)
+  )
+import GHC.Exts as X (
+    Constraint
+  , Ptr
+  , FunPtr
+  )
+import GHC.Base as X (
+    (++)
+  , seq
+  , asTypeOf
+  , ord
+  , maxInt
+  , minInt
+  )
+
+-- Exported for lifting into new functions.
+import System.IO as X (
+    print
+  , putStr
+  , putStrLn
+  )
+
+import GHC.Types as X (
+    Bool
+  , Char
+  , Int
+  , Word
+  , Ordering
+  , IO
+#if ( __GLASGOW_HASKELL__ >= 710 )
+  , Coercible
+#endif
+  )
+
+#if ( __GLASGOW_HASKELL__ >= 710 )
+import GHC.StaticPtr as X (StaticPtr)
+#endif
+
+#if ( __GLASGOW_HASKELL__ >= 800 )
+import GHC.OverloadedLabels as X (
+    IsLabel(..)
+  )
+
+import GHC.ExecutionStack as X (
+    Location(..)
+  , SrcLoc(..)
+  , getStackTrace
+  , showStackTrace
+  )
+
+import GHC.Stack as X (
+    CallStack
+  , type HasCallStack
+  , callStack
+  , prettySrcLoc
+  , currentCallStack
+  , getCallStack
+  , prettyCallStack
+  , withFrozenCallStack
+  )
+
+#if ( __GLASGOW_HASKELL__ >= 710 )
+import GHC.TypeLits as X (
+    Symbol
+  , SomeSymbol(..)
+  , Nat
+  , SomeNat(..)
+  , CmpNat
+  , KnownSymbol
+  , KnownNat
+  , natVal
+  , someNatVal
+  , symbolVal
+  , someSymbolVal
+  )
+#endif
+
+-- Pending GHC 8.2 we'll expose these.
+
+{-
+import GHC.Records as X (
+    HasField(..)
+  )
+
+import Data.Kind as X (
+    type (*)
+  , type Type
+  )
+-}
+
+#endif
+
+-- Default Prelude defines this at the toplevel module, so we do as well.
+infixr 0 $!
+
+($!) :: (a -> b) -> a -> b
+f $! x  = let !vx = x in f vx
+
+#endif
diff --git a/library/Lemmata/Bifunctor.hs b/library/Lemmata/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Bifunctor.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Bifunctor (
+  Bifunctor(..)
+) where
+
+import           Control.Applicative (Const (..))
+import           Data.Either         (Either (..))
+import           Data.Function       (id, (.))
+
+class Bifunctor p where
+  {-# MINIMAL bimap | first, second #-}
+
+  bimap :: (a -> b) -> (c -> d) -> p a c -> p b d
+  bimap f g = first f . second g
+
+  first :: (a -> b) -> p a c -> p b c
+  first f = bimap f id
+
+  second :: (b -> c) -> p a b -> p a c
+  second = bimap id
+
+instance Bifunctor (,) where
+  bimap f g ~(a, b) = (f a, g b)
+
+instance Bifunctor ((,,) x1) where
+  bimap f g ~(x1, a, b) = (x1, f a, g b)
+
+instance Bifunctor ((,,,) x1 x2) where
+  bimap f g ~(x1, x2, a, b) = (x1, x2, f a, g b)
+
+instance Bifunctor ((,,,,) x1 x2 x3) where
+  bimap f g ~(x1, x2, x3, a, b) = (x1, x2, x3, f a, g b)
+
+instance Bifunctor ((,,,,,) x1 x2 x3 x4) where
+  bimap f g ~(x1, x2, x3, x4, a, b) = (x1, x2, x3, x4, f a, g b)
+
+instance Bifunctor ((,,,,,,) x1 x2 x3 x4 x5) where
+  bimap f g ~(x1, x2, x3, x4, x5, a, b) = (x1, x2, x3, x4, x5, f a, g b)
+
+instance Bifunctor Either where
+  bimap f _ (Left a)  = Left (f a)
+  bimap _ g (Right b) = Right (g b)
+
+instance Bifunctor Const where
+  bimap f _ (Const a) = Const (f a)
diff --git a/library/Lemmata/Bool.hs b/library/Lemmata/Bool.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Bool.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Bool (
+  whenM
+, unlessM
+, ifM
+, guardM
+, bool
+, (&&^)
+, (||^)
+, (<&&>)
+, (<||>)
+) where
+
+import           Control.Applicative (Applicative, liftA2)
+import           Control.Monad
+    ( Monad
+    , MonadPlus
+    , guard
+    , return
+    , unless
+    , when
+    , (=<<)
+    , (>>=)
+    )
+import           Data.Bool           (Bool (..), (&&), (||))
+import           Data.Function       (flip)
+
+bool :: a -> a -> Bool -> a
+bool f t p = if p then t else f
+
+whenM :: Monad m => m Bool -> m () -> m ()
+whenM p m =
+  p >>= flip when m
+
+unlessM :: Monad m => m Bool -> m () -> m ()
+unlessM p m =
+  p >>= flip unless m
+
+ifM :: Monad m => m Bool -> m a -> m a -> m a
+ifM p x y = p >>= \b -> if b then x else y
+
+guardM :: MonadPlus m => m Bool -> m ()
+guardM f = guard =<< f
+
+-- | The '||' operator lifted to a monad. If the first
+--   argument evaluates to 'True' the second argument will not
+--   be evaluated.
+infixr 2 ||^ -- same as (||)
+(||^) :: Monad m => m Bool -> m Bool -> m Bool
+(||^) a b = ifM a (return True) b
+
+infixr 2 <||>
+-- | '||' lifted to an Applicative.
+-- Unlike '||^' the operator is __not__ short-circuiting.
+(<||>) :: Applicative a => a Bool -> a Bool -> a Bool
+(<||>) = liftA2 (||)
+{-# INLINE (<||>) #-}
+
+-- | The '&&' operator lifted to a monad. If the first
+--   argument evaluates to 'False' the second argument will not
+--   be evaluated.
+infixr 3 &&^ -- same as (&&)
+(&&^) :: Monad m => m Bool -> m Bool -> m Bool
+(&&^) a b = ifM a b (return False)
+
+infixr 3 <&&>
+-- | '&&' lifted to an Applicative.
+-- Unlike '&&^' the operator is __not__ short-circuiting.
+(<&&>) :: Applicative a => a Bool -> a Bool -> a Bool
+(<&&>) = liftA2 (&&)
+{-# INLINE (<&&>) #-}
diff --git a/library/Lemmata/Conv.hs b/library/Lemmata/Conv.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Conv.hs
@@ -0,0 +1,126 @@
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Lemmata.Conv
+  ( StringConv(..)
+  , toS
+  , toSL
+  , Leniency(..)
+  ) where
+
+import Data.ByteString.Char8 as B
+import Data.ByteString.Lazy.Char8 as LB
+import Data.Text as T
+import Data.Text.Encoding as T
+import Data.Text.Encoding.Error as T
+import Data.Text.Lazy as LT
+import Data.Text.Lazy.Encoding as LT
+
+import Lemmata.Base
+import Control.Applicative (pure)
+import Data.Eq (Eq(..))
+import Data.Function ((.), id)
+import Data.Ord (Ord(..))
+import Data.String (String)
+
+data Leniency
+  = Lenient
+  | Strict
+  deriving (Eq, Show, Ord, Enum, Bounded)
+
+class StringConv a b where
+  strConv :: Leniency -> a -> b
+
+toS
+  :: StringConv a b
+  => a -> b
+toS = strConv Strict
+
+toSL
+  :: StringConv a b
+  => a -> b
+toSL = strConv Lenient
+
+instance StringConv String String where
+  strConv _ = id
+
+instance StringConv String B.ByteString where
+  strConv _ = B.pack
+
+instance StringConv String LB.ByteString where
+  strConv _ = LB.pack
+
+instance StringConv String T.Text where
+  strConv _ = T.pack
+
+instance StringConv String LT.Text where
+  strConv _ = LT.pack
+
+instance StringConv B.ByteString String where
+  strConv _ = B.unpack
+
+instance StringConv B.ByteString B.ByteString where
+  strConv _ = id
+
+instance StringConv B.ByteString LB.ByteString where
+  strConv _ = LB.fromChunks . pure
+
+instance StringConv B.ByteString T.Text where
+  strConv = decodeUtf8T
+
+instance StringConv B.ByteString LT.Text where
+  strConv l = strConv l . LB.fromChunks . pure
+
+instance StringConv LB.ByteString String where
+  strConv _ = LB.unpack
+
+instance StringConv LB.ByteString B.ByteString where
+  strConv _ = B.concat . LB.toChunks
+
+instance StringConv LB.ByteString LB.ByteString where
+  strConv _ = id
+
+instance StringConv LB.ByteString T.Text where
+  strConv l = decodeUtf8T l . strConv l
+
+instance StringConv LB.ByteString LT.Text where
+  strConv = decodeUtf8LT
+
+instance StringConv T.Text String where
+  strConv _ = T.unpack
+
+instance StringConv T.Text B.ByteString where
+  strConv _ = T.encodeUtf8
+
+instance StringConv T.Text LB.ByteString where
+  strConv l = strConv l . T.encodeUtf8
+
+instance StringConv T.Text LT.Text where
+  strConv _ = LT.fromStrict
+
+instance StringConv T.Text T.Text where
+  strConv _ = id
+
+instance StringConv LT.Text String where
+  strConv _ = LT.unpack
+
+instance StringConv LT.Text T.Text where
+  strConv _ = LT.toStrict
+
+instance StringConv LT.Text LT.Text where
+  strConv _ = id
+
+instance StringConv LT.Text LB.ByteString where
+  strConv _ = LT.encodeUtf8
+
+instance StringConv LT.Text B.ByteString where
+  strConv l = strConv l . LT.encodeUtf8
+
+decodeUtf8T :: Leniency -> B.ByteString -> T.Text
+decodeUtf8T Lenient = T.decodeUtf8With T.lenientDecode
+decodeUtf8T Strict = T.decodeUtf8With T.strictDecode
+
+decodeUtf8LT :: Leniency -> LB.ByteString -> LT.Text
+decodeUtf8LT Lenient = LT.decodeUtf8With T.lenientDecode
+decodeUtf8LT Strict = LT.decodeUtf8With T.strictDecode
diff --git a/library/Lemmata/Debug.hs b/library/Lemmata/Debug.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Debug.hs
@@ -0,0 +1,102 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Trustworthy       #-}
+
+module Lemmata.Debug
+  ( undefined
+  , error
+  , trace
+  , traceM
+  , traceId
+  , traceIO
+  , traceShow
+  , traceShowId
+  , traceShowM
+  , notImplemented
+  ) where
+
+import           Control.Monad    (Monad, return)
+import           Data.Text        (Text, unpack)
+
+import qualified Lemmata.Base     as P
+import           Lemmata.Show     (Print, putStrLn)
+
+import           System.IO.Unsafe (unsafePerformIO)
+
+{-# WARNING
+trace "'trace' remains in code"
+ #-}
+
+trace
+  :: Print b
+  => b -> a -> a
+trace string expr =
+  unsafePerformIO
+    (do putStrLn string
+        return expr)
+
+{-# WARNING
+traceIO "'traceIO' remains in code"
+ #-}
+
+traceIO
+  :: Print b
+  => b -> a -> P.IO a
+traceIO string expr = do
+  putStrLn string
+  return expr
+
+{-# WARNING
+error "'error' remains in code"
+ #-}
+
+error :: Text -> a
+error s = P.error (unpack s)
+
+{-# WARNING
+traceShow "'traceShow' remains in code"
+ #-}
+
+traceShow
+  :: P.Show a
+  => a -> b -> b
+traceShow a b = trace (P.show a) b
+
+{-# WARNING
+traceShowId "'traceShowId' remains in code"
+ #-}
+
+traceShowId
+  :: P.Show a
+  => a -> a
+traceShowId a = trace (P.show a) a
+
+{-# WARNING
+traceShowM "'traceShowM' remains in code"
+ #-}
+
+traceShowM
+  :: (P.Show a, Monad m)
+  => a -> m ()
+traceShowM a = trace (P.show a) (return ())
+
+{-# WARNING
+traceM "'traceM' remains in code"
+ #-}
+
+traceM
+  :: (Monad m)
+  => Text -> m ()
+traceM s = trace (unpack s) (return ())
+
+{-# WARNING
+traceId "'traceId' remains in code"
+ #-}
+
+traceId :: Text -> Text
+traceId s = trace s s
+
+notImplemented :: a
+notImplemented = P.error "Not implemented"
+
+undefined :: a
+undefined = P.undefined
diff --git a/library/Lemmata/Either.hs b/library/Lemmata/Either.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Either.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Either (
+  maybeToLeft
+, maybeToRight
+, leftToMaybe
+, rightToMaybe
+, maybeToEither
+) where
+
+import           Data.Either   (Either (..), either)
+import           Data.Function (const)
+import           Data.Maybe    (Maybe (..), maybe)
+import           Data.Monoid   (Monoid, mempty)
+
+leftToMaybe :: Either l r -> Maybe l
+leftToMaybe = either Just (const Nothing)
+
+rightToMaybe :: Either l r -> Maybe r
+rightToMaybe = either (const Nothing) Just
+
+maybeToRight :: l -> Maybe r -> Either l r
+maybeToRight l = maybe (Left l) Right
+
+maybeToLeft :: r -> Maybe l -> Either l r
+maybeToLeft r = maybe (Right r) Left
+
+maybeToEither :: Monoid b => (a -> b) -> Maybe a -> b
+maybeToEither = maybe mempty
diff --git a/library/Lemmata/Exceptions.hs b/library/Lemmata/Exceptions.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Exceptions.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Lemmata.Exceptions (
+  hush,
+  note,
+  tryIO,
+) where
+
+import Lemmata.Base (IO)
+import Data.Function ((.))
+import Control.Monad.Trans (liftIO)
+import Control.Monad.IO.Class (MonadIO)
+import Control.Monad.Except (ExceptT(..), MonadError, throwError)
+import Control.Exception as Exception
+import Control.Applicative
+import Data.Maybe (Maybe, maybe)
+import Data.Either (Either(..))
+
+hush :: Alternative m => Either e a -> m a
+hush (Left _)  = empty
+hush (Right x) = pure x
+
+-- To suppress redundant applicative constraint warning on GHC 8.0
+#if ( __GLASGOW_HASKELL__ >= 800 )
+note :: (MonadError e m) => e -> Maybe a -> m a
+note err = maybe (throwError err) pure
+#else
+note :: (MonadError e m, Applicative m) => e -> Maybe a -> m a
+note err = maybe (throwError err) pure
+#endif
+
+tryIO :: MonadIO m => IO a -> ExceptT IOException m a
+tryIO = ExceptT . liftIO . Exception.try
diff --git a/library/Lemmata/Functor.hs b/library/Lemmata/Functor.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Functor.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Functor (
+  Functor(..),
+  ($>),
+  (<$>),
+  (<<$>>),
+  void,
+) where
+
+import           Data.Function ((.))
+
+#if MIN_VERSION_base(4,7,0)
+import           Data.Functor  (Functor (..), void, ($>), (<$>))
+#else
+import           Data.Functor  (Functor (..), (<$>))
+
+import           Data.Function (flip)
+
+infixl 4 $>
+
+($>) :: Functor f => f a -> b -> f b
+($>) = flip (<$)
+
+void :: Functor f => f a -> f ()
+void x = () <$ x
+#endif
+
+infixl 4 <<$>>
+
+(<<$>>) :: (Functor f, Functor g) => (a -> b) -> f (g a) -> f (g b)
+(<<$>>) = fmap . fmap
diff --git a/library/Lemmata/List.hs b/library/Lemmata/List.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/List.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.List (
+  head,
+  ordNub,
+  sortOn,
+  list,
+  product,
+  sum
+) where
+
+import           Control.Applicative (pure)
+import           Data.Foldable       (Foldable, foldl', foldr)
+import           Data.Function       ((.))
+import           Data.Functor        (fmap)
+import           Data.List           (sortBy)
+import           Data.Maybe          (Maybe (..))
+import           Data.Ord            (Ord, comparing)
+import qualified Data.Set            as Set
+import           GHC.Num             (Num, (*), (+))
+
+head :: (Foldable f) => f a -> Maybe a
+head = foldr (\x _ -> pure x) Nothing
+
+sortOn :: (Ord o) => (a -> o) -> [a] -> [a]
+sortOn = sortBy . comparing
+
+-- O(n * log n)
+ordNub :: (Ord a) => [a] -> [a]
+ordNub l = go Set.empty l
+  where
+    go _ []     = []
+    go s (x:xs) =
+      if x `Set.member` s
+      then go s xs
+      else x : go (Set.insert x s) xs
+
+list :: [b] -> (a -> b) -> [a] -> [b]
+list def f xs = case xs of
+  [] -> def
+  _  -> fmap f xs
+
+{-# INLINE product #-}
+product :: (Foldable f, Num a) => f a -> a
+product = foldl' (*) 1
+
+{-# INLINE sum #-}
+sum :: (Foldable f, Num a) => f a -> a
+sum = foldl' (+) 0
diff --git a/library/Lemmata/Monad.hs b/library/Lemmata/Monad.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Monad.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Trustworthy       #-}
+
+module Lemmata.Monad (
+    Monad((>>=), return)
+  , MonadPlus(..)
+
+  , (=<<)
+  , (>=>)
+  , (<=<)
+  , (>>)
+  , forever
+
+  , join
+  , mfilter
+  , filterM
+  , mapAndUnzipM
+  , zipWithM
+  , zipWithM_
+  , foldM
+  , foldM_
+  , replicateM
+  , replicateM_
+  , concatMapM
+
+  , guard
+  , when
+  , unless
+
+  , liftM
+  , liftM2
+  , liftM3
+  , liftM4
+  , liftM5
+  , liftM'
+  , liftM2'
+  , ap
+
+  , (<$!>)
+  ) where
+
+import           Control.Monad
+import           Data.List     (concat)
+import           Lemmata.Base  (seq)
+
+concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]
+concatMapM f xs = fmap concat (mapM f xs)
+
+liftM' :: Monad m => (a -> b) -> m a -> m b
+liftM' = (<$!>)
+{-# INLINE liftM' #-}
+
+liftM2' :: (Monad m) => (a -> b -> c) -> m a -> m b -> m c
+liftM2' f a b = do
+  x <- a
+  y <- b
+  let z = f x y
+  z `seq` return z
+{-# INLINE liftM2' #-}
+
+#if !MIN_VERSION_base(4,8,0)
+(<$!>) :: Monad m => (a -> b) -> m a -> m b
+f <$!> m = do
+  x <- m
+  let z = f x
+  z `seq` return z
+{-# INLINE (<$!>) #-}
+#endif
diff --git a/library/Lemmata/Panic.hs b/library/Lemmata/Panic.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Panic.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE Trustworthy        #-}
+
+module Lemmata.Panic (
+  FatalError(..),
+  panic,
+) where
+
+import           Control.Exception as X
+import           Data.Text         (Text)
+import           Data.Typeable     (Typeable)
+import           Lemmata.Base      (Show)
+
+-- | Uncatchable exceptions thrown and never caught.
+data FatalError = FatalError { fatalErrorMessage :: Text }
+  deriving (Show, Typeable)
+
+instance Exception FatalError
+
+panic :: Text -> a
+panic a = throw (FatalError a)
diff --git a/library/Lemmata/Semiring.hs b/library/Lemmata/Semiring.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Semiring.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Safe              #-}
+
+module Lemmata.Semiring (
+  Semiring(..),
+  zero,
+) where
+
+import           Data.Monoid
+
+-- | Alias for 'mempty'
+zero :: Monoid m => m
+zero = mempty
+
+class Monoid m => Semiring m where
+  {-# MINIMAL one, (<.>) #-}
+
+  one :: m
+  (<.>) :: m -> m -> m
diff --git a/library/Lemmata/Show.hs b/library/Lemmata/Show.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Show.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE ExtendedDefaultRules #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE NoImplicitPrelude    #-}
+{-# LANGUAGE Trustworthy          #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+module Lemmata.Show (
+  Print(..),
+  putText,
+  putLText,
+  putByteString,
+  putLByteString,
+) where
+
+import           Data.Function              ((.))
+import qualified Lemmata.Base               as Base
+
+import           Control.Monad.IO.Class     (MonadIO, liftIO)
+import qualified Data.ByteString.Char8      as BS
+import qualified Data.ByteString.Lazy.Char8 as BL
+
+import qualified Data.Text                  as T
+import qualified Data.Text.IO               as T
+
+import qualified Data.Text.Lazy             as TL
+import qualified Data.Text.Lazy.IO          as TL
+
+
+class Print a where
+  putStr :: MonadIO m => a -> m ()
+  putStrLn :: MonadIO m => a -> m ()
+
+instance Print T.Text where
+  putStr = liftIO . T.putStr
+  putStrLn = liftIO . T.putStrLn
+
+instance Print TL.Text where
+  putStr = liftIO . TL.putStr
+  putStrLn = liftIO . TL.putStrLn
+
+instance Print BS.ByteString where
+  putStr = liftIO . BS.putStr
+  putStrLn = liftIO . BS.putStrLn
+
+instance Print BL.ByteString where
+  putStr = liftIO . BL.putStr
+  putStrLn = liftIO . BL.putStrLn
+
+instance Print [Base.Char] where
+  putStr = liftIO . Base.putStr
+  putStrLn = liftIO . Base.putStrLn
+
+-- For forcing type inference
+putText :: MonadIO m => T.Text -> m ()
+putText = putStrLn
+{-# SPECIALIZE putText :: T.Text -> Base.IO () #-}
+
+putLText :: MonadIO m => TL.Text -> m ()
+putLText = putStrLn
+{-# SPECIALIZE putLText :: TL.Text -> Base.IO () #-}
+
+putByteString :: MonadIO m => BS.ByteString -> m ()
+putByteString = putStrLn
+{-# SPECIALIZE putByteString :: BS.ByteString -> Base.IO () #-}
+
+putLByteString :: MonadIO m => BL.ByteString -> m ()
+putLByteString = putStrLn
+{-# SPECIALIZE putLByteString :: BL.ByteString -> Base.IO () #-}
diff --git a/library/Lemmata/Unsafe.hs b/library/Lemmata/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/library/Lemmata/Unsafe.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE Unsafe            #-}
+
+module Lemmata.Unsafe (
+  unsafeHead,
+  unsafeTail,
+  unsafeInit,
+  unsafeLast,
+  unsafeFromJust,
+  unsafeIndex,
+  unsafeThrow,
+) where
+
+import qualified Control.Exception as Exc
+import qualified Data.List         as List
+import qualified Data.Maybe        as Maybe
+import           Lemmata.Base      (Int)
+
+unsafeHead :: [a] -> a
+unsafeHead = List.head
+
+unsafeTail :: [a] -> [a]
+unsafeTail = List.tail
+
+unsafeInit :: [a] -> [a]
+unsafeInit = List.init
+
+unsafeLast :: [a] -> a
+unsafeLast = List.last
+
+unsafeFromJust :: Maybe.Maybe a -> a
+unsafeFromJust = Maybe.fromJust
+
+unsafeIndex :: [a] -> Int -> a
+unsafeIndex = (List.!!)
+
+unsafeThrow :: Exc.Exception e => e -> a
+unsafeThrow = Exc.throw
diff --git a/library/Noether/Algebra/Actions.hs b/library/Noether/Algebra/Actions.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+module Noether.Algebra.Actions
+  ( module Noether.Algebra.Actions.Acts
+  , module Noether.Algebra.Actions.Compatible
+  , module Noether.Algebra.Actions.Linearity
+  , module Noether.Algebra.Actions.API
+  , module Noether.Algebra.Actions.Strategies
+  ) where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Actions.Acts
+import           Noether.Algebra.Actions.Compatible
+import           Noether.Algebra.Actions.Linearity
+
+import           Noether.Algebra.Actions.API
+import           Noether.Algebra.Actions.Strategies
diff --git a/library/Noether/Algebra/Actions/API.hs b/library/Noether/Algebra/Actions/API.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/API.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications    #-}
+module Noether.Algebra.Actions.API where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Actions.Acts
+import           Noether.Algebra.Actions.Compatible
+import           Noether.Algebra.Actions.Linearity
+
+import           Noether.Algebra.Single
+
+type CompatibleC lr op act a b = CompatibleK lr op act a b (CompatibleS lr op act a b)
+
+type Compatible lr op act a b
+  = ( CompatibleC lr op act a b
+    , Semigroup op a
+    , Acts lr act a b)
+
+type LeftCompatible act ao a b = Compatible L act ao a b
+type RightCompatible act ao a b = Compatible R act ao a b
+
+type Acts lr op a b = ActsK lr op a b (ActsS lr op a b)
+
+type LeftActs  op a b = Acts L op a b
+type RightActs op a b = Acts R op a b
+
+type BiActs op a b = (LeftActs op a b, RightActs op a b)
+
+
+leftActK
+  :: forall op s a b. ActsK 'L op a b s => a -> b -> b
+leftActK = actK (Proxy @op) (Proxy @s) (Proxy @'L)
+
+rightActK
+  :: forall op s a b. ActsK 'R op a b s => a -> b -> b
+rightActK = actK (Proxy @op) (Proxy @s) (Proxy @'R)
+
+leftAct :: forall op a b. LeftActs op a b => a -> b -> b
+leftAct = leftActK @op @(ActsS 'L op a b)
+
+rightAct :: forall op a b. RightActs op a b => a -> b -> b
+rightAct = rightActK @op @(ActsS 'R op a b)
+
+-- | > (a1 `ao` a2) `act` b = (a1 `act` b) `bo` (a2 `act` b)
+type ActorLinearC lr act ao a bo b =
+  ActorLinearK lr act ao a bo b (ActorLinearS lr act ao a bo b)
+
+-- | > a `act` (b1 `bo` b2) = (a `act` b1) `bo` (a `act` b2)
+type ActeeLinearC lr act a bo b =
+  ActeeLinearK lr act a bo b (ActeeLinearS lr act a bo b)
+
+type LinearActsOn lr act ao a bo b
+  = ( ActorLinearC lr act ao a bo b
+    , ActeeLinearC lr act a bo b
+    , Acts lr act a b
+    , Semigroup ao a
+    , Semigroup bo b)
+
+type LinearActs act ao a bo b = (LinearActsOn L act ao a bo b, LinearActsOn R act ao a bo b)
+
+type LeftLinear act ao a bo b = LinearActsOn L act ao a bo b
+type RightLinear act ao a bo b = LinearActsOn R act ao a bo b
diff --git a/library/Noether/Algebra/Actions/Acts.hs b/library/Noether/Algebra/Actions/Acts.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/Acts.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Actions.Acts where
+
+import           Data.Complex
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+
+data ActsE
+  = Acts_Magma MagmaE
+  | ActsNamed Symbol ActsE
+  | ActsTagged Type ActsE
+
+class ActsK (lr :: Side) (op :: k) a b (s :: ActsE) where
+  actK :: Proxy op -> Proxy s -> Proxy lr -> a -> b -> b
+
+type family ActsS (lr :: Side) (op :: k) (a :: Type) (b :: Type) = (r :: ActsE)
+
+instance MagmaK op a zm => ActsK lr op a a (Acts_Magma zm) where
+  actK opP _ _ = binaryOpK opP (Proxy @zm)
+
diff --git a/library/Noether/Algebra/Actions/Compatible.hs b/library/Noether/Algebra/Actions/Compatible.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/Compatible.hs
@@ -0,0 +1,32 @@
+module Noether.Algebra.Actions.Compatible where
+
+import           Data.Complex
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Actions.Acts
+
+
+{-| A strategy-parameterized typeclass for a compatible action, where compatibility
+    is defined in the group action sense.
+
+    A compatible action satisfies
+    a `act` (a' `act` b) = (a `op` a') `act` b
+-}
+
+class CompatibleK (lr :: Side) (op :: k1) (act :: k2) a b (s :: CompatibleE)
+
+data CompatibleE = Compatible_Acts_Semigroup
+  { compatible_actor           :: Type
+  , compatible_action          :: ActsE
+  , compatible_actor_semigroup :: SemigroupE
+  }
+
+type family CompatibleS (lr :: Side) (op :: k1) (act :: k2) (a :: Type) (b :: Type) = (r :: CompatibleE)
+
+instance (ActsK lr act a b za, SemigroupK op a zs) =>
+         CompatibleK lr op act a b (Compatible_Acts_Semigroup a za zs)
diff --git a/library/Noether/Algebra/Actions/GroupActions.hs b/library/Noether/Algebra/Actions/GroupActions.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/GroupActions.hs
@@ -0,0 +1,18 @@
+module Noether.Algebra.Actions.GroupActions where
+-- --------------------------------------------------------------------------------
+-- -- Group actions
+-- --------------------------------------------------------------------------------
+
+-- type family GSetS (lr :: k1) (op :: k1) (g :: Type) (b :: Type) = (r :: Type)
+
+-- class GSetK lr op g b s
+
+-- type GSetC lr op g b = GSetK lr op g b (GSetS lr op g b)
+
+-- type GSet lr op g b
+--   = GSetC lr op g b
+--   & Compatible lr op g b
+--   & Group op g
+
+-- type LeftGSet  op g b = GSet L op g b
+-- type RightGSet op g b = GSet R op g b
diff --git a/library/Noether/Algebra/Actions/Linearity.hs b/library/Noether/Algebra/Actions/Linearity.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/Linearity.hs
@@ -0,0 +1,26 @@
+module Noether.Algebra.Actions.Linearity where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Actions.Acts
+import           Noether.Algebra.Actions.Compatible
+
+data ActorLinearE = ActorLinear_Acts_Semigroup_Semigroup ActsE SemigroupE SemigroupE
+data ActeeLinearE = ActeeLinear_Acts_Semigroup ActsE SemigroupE
+
+type family ActorLinearS (lr :: Side) (act :: k0) (ao :: k1) a (bo :: k2) b :: ActorLinearE
+type family ActeeLinearS (lr :: Side) (act :: k0) a (bo :: k2) b :: ActeeLinearE
+
+class ActorLinearK lr act ao a bo b (s :: ActorLinearE)
+class ActeeLinearK lr act a bo b (s :: ActeeLinearE)
+
+instance (ActsK lr act a b za, SemigroupK ao a zas, SemigroupK bo b zbs) =>
+         ActorLinearK lr act ao a bo b (ActorLinear_Acts_Semigroup_Semigroup za zas zbs)
+
+instance (ActsK lr act a b za, SemigroupK bo b zbs) =>
+         ActeeLinearK lr act a bo b (ActeeLinear_Acts_Semigroup za zbs)
+
diff --git a/library/Noether/Algebra/Actions/Strategies.hs b/library/Noether/Algebra/Actions/Strategies.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Actions/Strategies.hs
@@ -0,0 +1,60 @@
+module Noether.Algebra.Actions.Strategies where
+
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+import           Noether.Lemmata.Prelude
+
+import           Noether.Algebra.Actions.Acts
+import           Noether.Algebra.Actions.Compatible
+import           Noether.Algebra.Actions.Linearity
+
+import           Noether.Algebra.Actions.API
+
+type DeriveActs_Tagged tag lr op a b =
+  ActsTagged tag (ActsS lr op a b)
+
+type DeriveActs_Magma op a =
+  Acts_Magma (MagmaS op a)
+
+type DeriveCompatible_Acts_Semigroup lr op act a b =
+  Compatible_Acts_Semigroup a
+    (ActsS lr act a b)
+    (SemigroupS op a)
+
+-- | a + (b + c) = (a + b) + c
+type DeriveCompatible_Associativity lr op a =
+  DeriveCompatible_Acts_Semigroup lr op op a a
+
+type DeriveActorLinearActs_Acts_Semigroup_Semigroup lr act ao a bo b =
+  ActorLinear_Acts_Semigroup_Semigroup
+    (ActsS lr act a b)
+    (SemigroupS ao a)
+    (SemigroupS bo b)
+
+type DeriveActeeLinearActs_Acts_Semigroup lr act a bo b =
+  ActeeLinear_Acts_Semigroup
+    (ActsS lr act a b)
+    (SemigroupS bo b)
+
+-- | (a + b) * c = a * c + b * c
+type DeriveActorLinearActs_LeftDistributivity lr p m a =
+  DeriveActorLinearActs_Acts_Semigroup_Semigroup lr m p a p a
+
+-- | a * (b + c) = a * b + a * c
+type DeriveActeeLinearActs_RightDistributivity lr p m a =
+  DeriveActeeLinearActs_Acts_Semigroup lr m a p a
+
+type instance ActsS lr (op :: BinaryNumeric) Double Double = DeriveActs_Magma op Double
+type instance CompatibleS lr (op :: BinaryNumeric) op Double Double = DeriveCompatible_Associativity lr op Double
+type instance ActorLinearS lr Mul Add Double Add Double = DeriveActorLinearActs_LeftDistributivity lr Add Mul Double
+type instance ActeeLinearS lr Mul Double Add Double = DeriveActeeLinearActs_RightDistributivity lr Add Mul Double
+
+type instance ActsS lr (op :: BinaryNumeric) Rational Rational = DeriveActs_Magma op Rational
+type instance CompatibleS lr (op :: BinaryNumeric) op Rational Rational = DeriveCompatible_Associativity lr op Rational
+type instance ActorLinearS lr Mul Add Rational Add Rational = DeriveActorLinearActs_LeftDistributivity lr Add Mul Rational
+type instance ActeeLinearS lr Mul Rational Add Rational = DeriveActeeLinearActs_RightDistributivity lr Add Mul Rational
+
+type instance ActsS lr (op :: BinaryNumeric) (Complex Double) (Complex Double) = DeriveActs_Magma op (Complex Double)
+type instance CompatibleS lr (op :: BinaryNumeric) op (Complex Double) (Complex Double) = DeriveCompatible_Associativity lr op (Complex Double)
+type instance ActorLinearS lr Mul Add (Complex Double) Add (Complex Double) = DeriveActorLinearActs_LeftDistributivity lr Add Mul (Complex Double)
+type instance ActeeLinearS lr Mul (Complex Double) Add (Complex Double) = DeriveActeeLinearActs_RightDistributivity lr Add Mul (Complex Double)
diff --git a/library/Noether/Algebra/Derive.hs b/library/Noether/Algebra/Derive.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Derive.hs
@@ -0,0 +1,3 @@
+module Noether.Algebra.Derive where
+
+data Automatic
diff --git a/library/Noether/Algebra/Inference.hs b/library/Noether/Algebra/Inference.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Inference.hs
@@ -0,0 +1,30 @@
+module Noether.Algebra.Inference
+  ( Synergise
+  , Infer
+  , Prim
+  , DerivedFrom
+  , Strategy
+  , module TypeFu.Map
+  ) where
+
+import           Noether.Lemmata.TypeFu
+import           Noether.Lemmata.TypeFu.Map as TypeFu.Map
+
+-- bahahahaha
+data Synergise (a :: [k])
+
+type family Strategy (t :: k) (a :: Type) (hint :: Symbol) :: Type
+
+type family Infer_ (t :: k) (a :: Type) (hint :: [Symbol]) :: [Type] where
+  Infer_ t a '[] = '[]
+  Infer_ t a (x : xs) = (x := Strategy t a x) : Infer_ t a xs
+
+type Infer (t :: k) a (h :: [Symbol]) = Synergise (Nub (Sort (Infer_ t a h)))
+
+data family Sorted (t :: k)
+
+-- Tags
+
+data DerivedFrom (a :: k)
+
+data Prim
diff --git a/library/Noether/Algebra/Linear.hs b/library/Noether/Algebra/Linear.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Linear.hs
@@ -0,0 +1,12 @@
+module Noether.Algebra.Linear
+  ( module Noether.Algebra.Linear.Module
+  --
+  , module Noether.Algebra.Linear.API
+  , module Noether.Algebra.Linear.Strategies
+  ) where
+
+import           Noether.Algebra.Linear.Module
+
+import           Noether.Algebra.Linear.API
+import           Noether.Algebra.Linear.Strategies
+
diff --git a/library/Noether/Algebra/Linear/API.hs b/library/Noether/Algebra/Linear/API.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Linear/API.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Linear.API
+  (
+  -- * Basic actions
+    (%<)
+  , (>%)
+  -- * Using specialized actions
+  , (%<~)
+  , (~>%)
+  -- * Utility functions
+  , lerp
+  ) where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Multiple
+import           Noether.Algebra.Single
+import           Noether.Algebra.Single.Synonyms
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Linear.Module
+import           Noether.Algebra.Linear.Strategies
+
+type LeftModule' r v = LeftModule Mul Add Mul r Add v
+type RightModule' r v = RightModule Mul Add Mul r Add v
+
+(%<) :: LeftActs 'Mul r v => r -> v -> v
+r %< v = leftAct @Mul r v
+
+(>%) :: RightActs 'Mul r v => v -> r -> v
+v >% r = rightAct @Mul r v
+
+-- | Locally use the left self-action induced by the multiplicative magma
+-- structure of the ring, whatever structure the user may have chosen to use
+-- globally.
+--
+-- prop> a %<~ b = a * b
+(%<~) :: forall r. Ring Add Mul r => r -> r -> r
+a %<~ b = leftActK @Mul @(DeriveActs_Magma Mul r) a b
+
+-- | Locally use the right self-action induced by the multiplicative magma
+-- structure of the ring, whatever structure the user may have chosen to use
+-- globally.
+--
+-- prop> b ~>% a = a * b
+(~>%) :: forall r. Ring Add Mul r => r -> r -> r
+b ~>% a = rightActK @Mul @(DeriveActs_Magma Mul r) b a
+
+-- | Linear interpolation.
+--
+-- prop> lerp λ v w = λv + (1 - λ)w
+
+lerp ::
+  ( Neutral 'Mul r
+  , Cancellative 'Add r
+  , Magma 'Add r, Magma 'Add a
+  , Acts 'R 'Mul r a
+  , Acts 'L 'Mul r a
+  ) => r -> a -> a -> a
+lerp lambda v w = lambda %< v + w >% (one - lambda)
diff --git a/library/Noether/Algebra/Linear/Module.hs b/library/Noether/Algebra/Linear/Module.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Linear/Module.hs
@@ -0,0 +1,81 @@
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+module Noether.Algebra.Linear.Module where
+
+import           Data.Complex
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Multiple
+import           Noether.Algebra.Single
+
+import           Noether.Algebra.Tags
+
+data LeftModuleE
+  = LeftModule_Ring_AbelianGroup_Linear_Compatible
+    { leftModule_ring           :: RingE
+    , leftModule_abelianGroup   :: AbelianGroupE
+    , leftModule_actorLinearity :: ActorLinearE
+    , leftModule_acteeLinearity :: ActeeLinearE
+    , leftModule_compatibility  :: CompatibleE}
+  | LeftModule_Named Symbol
+                     LeftModuleE
+
+-- | A left module (v, a) over the ring (r, p, m).
+class LeftModuleK op p m r a v s
+
+type family LeftModuleS (op :: k0) (p :: k1) (m :: k2) r (a :: k3) v :: LeftModuleE
+
+type LeftModuleC op p m r a v = LeftModuleK op p m r a v (LeftModuleS op p m r a v)
+
+instance ( RingK p m r zr
+         , AbelianGroupK a v zag
+         , ActorLinearK L m p r a v zor
+         , ActeeLinearK L m r a v zee
+         , CompatibleK L op m r v zlc
+         ) =>
+         LeftModuleK op p m r a v
+           (LeftModule_Ring_AbelianGroup_Linear_Compatible zr zag zor zee zlc)
+
+type LeftModule op p m r a v =
+  ( LeftModuleC op p m r a v
+  , Ring p m r
+  , AbelianGroup a v
+  , LinearActsOn L m p r a v
+  , LeftCompatible op m r v
+  )
+
+data RightModuleE
+  = RightModule_Ring_AbelianGroup_Linear_Compatible
+    { rightModule_ring           :: RingE
+    , rightModule_abelianGroup   :: AbelianGroupE
+    , rightModule_actorLinearity :: ActorLinearE
+    , rightModule_acteeLinearity :: ActeeLinearE
+    , rightModule_compatibility  :: CompatibleE}
+  | RightModule_Named Symbol
+                     RightModuleE
+
+-- | A right module (v, a) over the ring (r, p, m).
+class RightModuleK op p m r a v s
+
+type family RightModuleS (op :: k0) (p :: k1) (m :: k2) r (a :: k3) v :: RightModuleE
+
+type RightModuleC op p m r a v = RightModuleK op p m r a v (RightModuleS op p m r a v)
+
+instance ( RingK p m r zr
+         , AbelianGroupK a v zag
+         , ActorLinearK R m p r a v zor
+         , ActeeLinearK R m r a v zee
+         , CompatibleK R op m r v zrc
+         ) => RightModuleK op p m r a v
+           (RightModule_Ring_AbelianGroup_Linear_Compatible zr zag zor zee zrc)
+
+type RightModule op p m r a v =
+  ( RightModuleC op p m r a v
+  , Ring p m r
+  , AbelianGroup a v
+  , LinearActsOn R m p r a v
+  , RightCompatible op m r v
+  )
diff --git a/library/Noether/Algebra/Linear/Strategies.hs b/library/Noether/Algebra/Linear/Strategies.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Linear/Strategies.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}
+module Noether.Algebra.Linear.Strategies where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Multiple
+import           Noether.Algebra.Single
+import           Noether.Algebra.Single.Synonyms
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Linear.Module
+
+type DeriveLeftModule_Ring_AbelianGroup op p m r a v =
+  LeftModule_Ring_AbelianGroup_Linear_Compatible
+    (RingS p m r)
+    (AbelianGroupS a v)
+    (ActorLinearS L m p r a v)
+    (ActeeLinearS L m r a v)
+    (CompatibleS L op m r v)
+
+type DeriveLeftModule_Self p m r = DeriveLeftModule_Ring_AbelianGroup m p m r p r
+
+type DeriveRightModule_Ring_AbelianGroup op p m r a v =
+  RightModule_Ring_AbelianGroup_Linear_Compatible
+    (RingS p m r)
+    (AbelianGroupS a v)
+    (ActorLinearS R m p r a v)
+    (ActeeLinearS R m r a v)
+    (CompatibleS R op m r v)
+
+type DeriveRightModule_Self p m r = DeriveRightModule_Ring_AbelianGroup m p m r p r
+
+type instance LeftModuleS Mul Add Mul Double Add Double =
+     DeriveLeftModule_Self Add Mul Double
+
+type instance RightModuleS Mul Add Mul Double Add Double =
+     DeriveRightModule_Self Add Mul Double
diff --git a/library/Noether/Algebra/Multiple.hs b/library/Noether/Algebra/Multiple.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Multiple.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RebindableSyntax #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+
+module Noether.Algebra.Multiple
+  ( module Noether.Algebra.Multiple.Semiring
+  , module Noether.Algebra.Multiple.Ring
+  , module Noether.Algebra.Multiple.Strategies
+  ) where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Multiple.Ring
+import           Noether.Algebra.Multiple.Semiring
+import           Noether.Algebra.Multiple.Strategies
diff --git a/library/Noether/Algebra/Multiple/Ring.hs b/library/Noether/Algebra/Multiple/Ring.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Multiple/Ring.hs
@@ -0,0 +1,29 @@
+module Noether.Algebra.Multiple.Ring where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Multiple.Semiring
+import           Noether.Algebra.Single
+
+type family RingS (add :: ka) (mul :: km) (a :: Type) = (r :: RingE)
+
+data RingE
+  = Ring_Semiring_Cancellative { ring_semiring              :: SemiringE
+                              ,  ring_addition_cancellative :: CancellativeE}
+  | Ring_AbelianGroup_Group { ring_additive_group       :: AbelianGroupE
+                           ,  ring_multiplicative_group :: GroupE}
+  | RingNamed Symbol
+              RingE
+
+class RingK (add :: ka) (mul :: km) a (s :: RingE)
+
+instance (SemiringK p m a zs, CancellativeK p a zpc) =>
+         RingK p m a (Ring_Semiring_Cancellative zs zpc)
+
+instance (AbelianGroupK p a zpab, GroupK m a zmg) =>
+         RingK p m a (Ring_AbelianGroup_Group zpab zmg)
+
+instance (KnownSymbol sym, RingK p m a s) =>
+         RingK p m a (RingNamed sym s)
+
+type RingC p m a = RingK p m a (RingS p m a)
diff --git a/library/Noether/Algebra/Multiple/Semiring.hs b/library/Noether/Algebra/Multiple/Semiring.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Multiple/Semiring.hs
@@ -0,0 +1,24 @@
+module Noether.Algebra.Multiple.Semiring where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single
+
+type family SemiringS (add :: ka) (mul :: km) (a :: Type) = (r :: SemiringE)
+
+data SemiringE
+  = Semiring_Commutative_Monoid_Monoid { semiring_commutative :: CommutativeE
+                                       , semiring_additive_monoid :: MonoidE
+                                       , semiring_multiplicative_monoid :: MonoidE}
+  | SemiringNamed Symbol
+                  SemiringE
+
+class SemiringK (add :: ka) (mul :: km) a (s :: SemiringE)
+
+instance (MonoidK p a zam, CommutativeK p a zac, MonoidK m a zbm) =>
+         SemiringK p m a (Semiring_Commutative_Monoid_Monoid zac zam zbm)
+
+instance (KnownSymbol sym, SemiringK p m a s) =>
+         SemiringK p m a (SemiringNamed sym s)
+
+type SemiringC p m a = (SemiringK $$> SemiringS) p m a
diff --git a/library/Noether/Algebra/Multiple/Strategies.hs b/library/Noether/Algebra/Multiple/Strategies.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Multiple/Strategies.hs
@@ -0,0 +1,63 @@
+{-# OPTIONS_GHC -fconstraint-solver-iterations=0 #-}
+module Noether.Algebra.Multiple.Strategies where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Multiple.Ring
+import           Noether.Algebra.Multiple.Semiring
+import           Noether.Algebra.Single
+
+type Ring p m a =
+  ( RingC p m a
+  , Group m a
+  , AbelianGroup p a
+  )
+
+type Semiring p m a =
+  ( SemiringC p m a
+  , Commutative p a
+  , Monoid p a
+  , Monoid m a
+  )
+
+-- Lifting strategies
+
+type DeriveSemiring_Commutative_Monoid_Monoid p m a =
+  Semiring_Commutative_Monoid_Monoid
+    (CommutativeS p a)
+    (MonoidS p a)
+    (MonoidS m a)
+
+type DeriveRing_Semiring_Cancellative p m a =
+  Ring_Semiring_Cancellative
+    (SemiringS p m a)
+    (CancellativeS p a)
+
+type DeriveRing_AbelianGroup_Group p m a =
+  Ring_AbelianGroup_Group
+    (AbelianGroupS p a)
+    (GroupS m a)
+
+type family RingNamedT a where
+  RingNamedT (Ring_AbelianGroup_Group ab grp) =
+    Ring_AbelianGroup_Group
+      (AbelianGroupNamed "Additive group" ab)
+      (GroupNamed "Multiplicative group" grp)
+
+type DeriveRingDoc_AbelianGroup_Group p m a =
+  RingNamedT (DeriveRing_AbelianGroup_Group p m a)
+
+type instance SemiringS Add Mul Double =
+     DeriveSemiring_Commutative_Monoid_Monoid Add Mul Double
+
+type instance RingS Add Mul Double =
+     DeriveRingDoc_AbelianGroup_Group Add Mul Double
+
+p :: Ring Add Mul a => a -> a -> a
+p a b = a + b / (b - a) * b + (b + a / b * b - a)
+
+q :: Double
+q = p 2 (p 3 4)
diff --git a/library/Noether/Algebra/Single.hs b/library/Noether/Algebra/Single.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single.hs
@@ -0,0 +1,31 @@
+module Noether.Algebra.Single
+  ( module Noether.Algebra.Single.API
+  -- $structures
+  , module Noether.Algebra.Single.Cancellative
+  , module Noether.Algebra.Single.Commutative
+  , module Noether.Algebra.Single.Neutral
+  , module Noether.Algebra.Single.Magma
+  , module Noether.Algebra.Single.Monoid
+  , module Noether.Algebra.Single.Semigroup
+  , module Noether.Algebra.Single.Group
+  , module Noether.Algebra.Single.AbelianGroup
+  -- $strategies
+  , module Noether.Algebra.Single.Strategies
+  , module Noether.Algebra.Single.Synonyms
+  ) where
+
+import           Noether.Algebra.Single.API
+
+import           Noether.Algebra.Single.Cancellative
+import           Noether.Algebra.Single.Commutative
+import           Noether.Algebra.Single.Neutral
+
+import           Noether.Algebra.Single.Magma
+import           Noether.Algebra.Single.Monoid
+import           Noether.Algebra.Single.Semigroup
+
+import           Noether.Algebra.Single.AbelianGroup
+import           Noether.Algebra.Single.Group
+
+import           Noether.Algebra.Single.Strategies
+import           Noether.Algebra.Single.Synonyms
diff --git a/library/Noether/Algebra/Single/API.hs b/library/Noether/Algebra/Single/API.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/API.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE RebindableSyntax    #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeInType          #-}
+
+module Noether.Algebra.Single.API where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+import           Prelude                             ((==))
+
+import           Noether.Algebra.Single.Cancellative
+import           Noether.Algebra.Single.Group
+import           Noether.Algebra.Single.Magma
+import           Noether.Algebra.Single.Monoid
+import           Noether.Algebra.Single.Neutral
+import           Noether.Algebra.Single.Semigroup
+
+import           Noether.Algebra.Single.Strategies
+
+import           Noether.Algebra.Single.Synonyms
+import           Noether.Algebra.Tags
+
+cancel :: forall op a. Cancellative op a => Proxy op -> a -> a
+cancel p = cancelK p (Proxy @(CancellativeS op a))
+
+binaryOp :: forall op a. Magma op a => Proxy op -> a -> a -> a
+binaryOp p = binaryOpK p (Proxy @(MagmaS op a))
+
+neutral :: forall op a. Neutral op a => Proxy op -> a
+neutral p = neutralK p (Proxy @(NeutralS op a))
+
+zero :: Neutral Add a => a
+zero = neutral AddP
+
+one :: Neutral Mul a => a
+one = neutral MulP
+
+true :: Neutral And a => a
+true = neutral AndP
+
+false :: Neutral Or a => a
+false = neutral OrP
+
+negate :: Cancellative Add a => a -> a
+negate = cancel AddP
+
+reciprocal :: Cancellative Mul a => a -> a
+reciprocal = cancel MulP
+
+-- Addition, multiplication
+
+infixl 6 +
+
+(+) :: Magma Add a => a -> a -> a
+(+) = binaryOp AddP
+
+infixl 7 *
+
+(*) :: Magma Mul a => a -> a -> a
+(*) = binaryOp MulP
+
+-- Groupy things
+
+infixl 6 -
+
+(-) :: (Magma Add a, Cancellative Add a) => a -> a -> a
+a - b = a + negate b
+
+infixl 7 /
+
+(/) :: (Magma Mul a, Cancellative Mul a) => a -> a -> a
+a / b = a * reciprocal b
+
+-- Binary operations
+
+infixl 3 &&
+
+(&&) :: Magma And a => a -> a -> a
+(&&) = binaryOp AndP
+
+infixl 2 ||
+
+(||) :: Magma Or a => a -> a -> a
+(||) = binaryOp OrP
diff --git a/library/Noether/Algebra/Single/AbelianGroup.hs b/library/Noether/Algebra/Single/AbelianGroup.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/AbelianGroup.hs
@@ -0,0 +1,22 @@
+module Noether.Algebra.Single.AbelianGroup where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single.Commutative
+import           Noether.Algebra.Single.Group
+
+type family AbelianGroupS (op :: k) (a :: Type) = (r :: AbelianGroupE)
+
+data AbelianGroupE
+  = AbelianGroup_Commutative_Group CommutativeE GroupE
+  | AbelianGroupNamed Symbol AbelianGroupE
+
+class AbelianGroupK (op :: k) a (s :: AbelianGroupE)
+
+instance (GroupK op a zm, CommutativeK op a zl) =>
+         AbelianGroupK op a (AbelianGroup_Commutative_Group zl zm)
+
+instance (KnownSymbol sym, AbelianGroupK op a s) =>
+         AbelianGroupK op a (AbelianGroupNamed sym s)
+
+type AbelianGroupC op a = AbelianGroupK op a (AbelianGroupS op a)
diff --git a/library/Noether/Algebra/Single/Cancellative.hs b/library/Noether/Algebra/Single/Cancellative.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Cancellative.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Single.Cancellative where
+
+import qualified Prelude                 as P
+
+import           Noether.Algebra.Tags
+import           Noether.Lemmata.Prelude hiding (Num)
+import           Noether.Lemmata.TypeFu
+
+data CancellativeE
+  = CancellativeNum
+  | CancellativeFractional
+  | CancellativeNamed Symbol CancellativeE
+  | CancellativeTagged Type CancellativeE
+
+class CancellativeK (op :: k) a (s :: CancellativeE) where
+  cancelK :: Proxy op -> Proxy s -> a -> a
+
+instance P.Num a => CancellativeK Add a CancellativeNum where
+  cancelK _ _ = (0 P.-)
+
+instance P.Fractional a => CancellativeK Mul a CancellativeFractional where
+  cancelK _ _ = (1 P./)
+
+instance (KnownSymbol sym, CancellativeK op a s) =>
+         CancellativeK op a (CancellativeNamed sym s) where
+  cancelK opP _ = cancelK opP (Proxy @s)
+
+instance CancellativeK op a s =>
+         CancellativeK op (i -> a) (CancellativeTagged FunctionLift s) where
+  cancelK o _ f = cancelK' . f
+    where
+      cancelK' = cancelK o (Proxy @s)
+
+type Cancellative op a = CancellativeK op a (CancellativeS op a)
+
+type family CancellativeS (op :: k) (a :: Type) = (r :: CancellativeE)
diff --git a/library/Noether/Algebra/Single/Commutative.hs b/library/Noether/Algebra/Single/Commutative.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Commutative.hs
@@ -0,0 +1,27 @@
+module Noether.Algebra.Single.Commutative where
+
+import qualified Prelude                 as P
+
+import           Noether.Algebra.Tags
+import           Noether.Lemmata.Prelude hiding (Num)
+import           Noether.Lemmata.TypeFu
+
+data CommutativeE
+  = CommutativeNum
+  | CommutativeNamed Symbol CommutativeE
+  | CommutativeTagged Type CommutativeE
+
+class CommutativeK (op :: k) a (s :: CommutativeE)
+
+instance P.Num a => CommutativeK Add a CommutativeNum
+instance P.Num a => CommutativeK Mul a CommutativeNum
+
+instance (KnownSymbol sym, CommutativeK op a s) =>
+         CommutativeK op a (CommutativeNamed sym s)
+
+instance (CommutativeK op a s) =>
+         CommutativeK op a (CommutativeTagged tag s)
+
+type Commutative op a = CommutativeK op a (CommutativeS op a)
+
+type family CommutativeS (op :: k) (a :: Type) = (r :: CommutativeE)
diff --git a/library/Noether/Algebra/Single/Group.hs b/library/Noether/Algebra/Single/Group.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Group.hs
@@ -0,0 +1,24 @@
+module Noether.Algebra.Single.Group where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single.Cancellative
+import           Noether.Algebra.Single.Commutative
+import           Noether.Algebra.Single.Magma
+import           Noether.Algebra.Single.Monoid
+
+type family GroupS (op :: k) (a :: Type) = (r :: GroupE)
+
+data GroupE
+  = Group_Monoid_Cancellative MonoidE CancellativeE
+  | GroupNamed Symbol GroupE
+
+class GroupK (op :: k) a (s :: GroupE)
+
+instance (MonoidK op a zm, CancellativeK op a zl) =>
+         GroupK op a (Group_Monoid_Cancellative zm zl)
+
+instance (KnownSymbol sym, GroupK op a s) =>
+         GroupK op a (GroupNamed sym s)
+
+type GroupC op a = GroupK op a (GroupS op a)
diff --git a/library/Noether/Algebra/Single/Magma.hs b/library/Noether/Algebra/Single/Magma.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Magma.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Single.Magma where
+
+import qualified Prelude                 as P
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+data MagmaE
+  = MagmaPrim
+  | MagmaNum
+  | MagmaNamed Symbol MagmaE
+  | MagmaTagged Type MagmaE
+
+class MagmaK (op :: k) a (s :: MagmaE) where
+  binaryOpK :: Proxy op -> Proxy s -> a -> a -> a
+
+instance P.Num a => MagmaK Add a MagmaNum where
+  binaryOpK _ _ = (P.+)
+
+instance P.Num a => MagmaK Mul a MagmaNum where
+  binaryOpK _ _ = (P.*)
+
+instance MagmaK And P.Bool MagmaPrim where
+  binaryOpK _ _ = (P.&&)
+
+instance MagmaK Or P.Bool MagmaPrim where
+  binaryOpK _ _ = (P.||)
+
+instance MagmaK op a s => MagmaK op a (MagmaNamed sym s) where
+  binaryOpK o _ = binaryOpK o (Proxy @(MagmaNamed sym s))
+
+instance MagmaK op a s => MagmaK op (i -> a) (MagmaTagged FunctionLift s) where
+  binaryOpK o _ f g = \x -> f x `binop` g x
+    where binop = binaryOpK o (Proxy @s)
+
+type Magma op a = MagmaK op a (MagmaS op a)
+
+type family MagmaS (op :: k) (a :: Type) = (r :: MagmaE)
diff --git a/library/Noether/Algebra/Single/Monoid.hs b/library/Noether/Algebra/Single/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Monoid.hs
@@ -0,0 +1,22 @@
+module Noether.Algebra.Single.Monoid where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single.Neutral
+import           Noether.Algebra.Single.Semigroup
+
+data MonoidE
+  = Monoid_Semigroup_Neutral SemigroupE NeutralE
+  | MonoidNamed Symbol MonoidE
+
+class MonoidK (op :: k) a (s :: MonoidE)
+
+instance (SemigroupK op a zs, NeutralK op a zn) =>
+         MonoidK op a (Monoid_Semigroup_Neutral zs zn)
+
+instance (KnownSymbol sym, MonoidK op a s) =>
+         MonoidK op a (MonoidNamed sym s)
+
+type MonoidC op a = MonoidK op a (MonoidS op a)
+
+type family MonoidS (op :: k) (a :: Type) = (r :: MonoidE)
diff --git a/library/Noether/Algebra/Single/Neutral.hs b/library/Noether/Algebra/Single/Neutral.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Neutral.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Single.Neutral where
+
+import qualified Prelude                 as P
+
+import           Noether.Lemmata.Prelude hiding (Num)
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+data NeutralE
+  = NeutralPrim
+  | NeutralNum
+  | NeutralNamed Symbol NeutralE
+  | NeutralTagged Type NeutralE
+
+class NeutralK (op :: k) a (s :: NeutralE) where
+  neutralK :: Proxy op -> Proxy s -> a
+
+instance P.Num a => NeutralK Add a NeutralNum where
+  neutralK _ _ = 0
+
+instance P.Num a => NeutralK Mul a NeutralNum where
+  neutralK _ _ = 1
+
+instance NeutralK And P.Bool NeutralPrim where
+  neutralK _ _ = True
+
+instance NeutralK Or P.Bool NeutralPrim where
+  neutralK _ _ = False
+
+instance (KnownSymbol sym, NeutralK op a s) => NeutralK op a (NeutralNamed sym s) where
+  neutralK opP _ = neutralK opP (Proxy @s)
+
+type family NeutralS (op :: k) (a :: Type) = (r :: NeutralE)
+
+type Neutral op a = NeutralK op a (NeutralS op a)
diff --git a/library/Noether/Algebra/Single/Semigroup.hs b/library/Noether/Algebra/Single/Semigroup.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Semigroup.hs
@@ -0,0 +1,22 @@
+module Noether.Algebra.Single.Semigroup where
+
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Single.Magma
+import           Noether.Algebra.Tags
+
+data SemigroupE
+  = Semigroup_Magma MagmaE
+  | SemigroupNamed Symbol SemigroupE
+
+class SemigroupK (op :: k) a (s :: SemigroupE)
+
+instance MagmaK op a s => SemigroupK op a (Semigroup_Magma s)
+
+instance (KnownSymbol sym, SemigroupK op a s) =>
+         SemigroupK op a (SemigroupNamed sym s)
+
+type SemigroupC op a = SemigroupK op a (SemigroupS op a)
+
+type family SemigroupS (op :: k) (a :: Type) = (r :: SemigroupE)
+
diff --git a/library/Noether/Algebra/Single/Strategies.hs b/library/Noether/Algebra/Single/Strategies.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Strategies.hs
@@ -0,0 +1,266 @@
+module Noether.Algebra.Single.Strategies where
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Single.Cancellative
+import           Noether.Algebra.Single.Commutative
+import           Noether.Algebra.Single.Neutral
+
+import           Noether.Algebra.Single.Magma
+import           Noether.Algebra.Single.Monoid
+import           Noether.Algebra.Single.Semigroup
+
+import           Noether.Algebra.Single.AbelianGroup
+import           Noether.Algebra.Single.Group
+
+type Semigroup op a = (SemigroupC op a, Magma op a)
+
+type Monoid op a = (MonoidC op a, Semigroup op a, Neutral op a)
+
+type Group op a = (GroupC op a, Monoid op a, Cancellative op a)
+
+type AbelianGroup op a = (AbelianGroupC op a, Group op a, Commutative op a)
+
+-- Lifting strategies
+
+type DeriveMagma_Tagged tag op a = MagmaTagged tag (MagmaS op a)
+type DeriveMagma_Named tag op a = MagmaNamed tag (MagmaS op a)
+type DeriveCommutative_Tagged tag op a = CommutativeTagged tag (CommutativeS op a)
+type DeriveCancellative_Tagged tag op a = CancellativeTagged tag (CancellativeS op a)
+type DeriveNeutral_Tagged tag op a = NeutralTagged tag (NeutralS op a)
+type DeriveSemigroup_Magma (t :: k) (a :: Type) = Semigroup_Magma (MagmaS t a)
+
+type DeriveMonoid_Semigroup_Neutral t a =
+  Monoid_Semigroup_Neutral (SemigroupS t a) (NeutralS t a)
+
+type DeriveGroup_Monoid_Cancellative t a =
+  Group_Monoid_Cancellative (MonoidS t a) (CancellativeS t a)
+
+type DeriveAbelianGroup_Commutative_Group t a =
+  AbelianGroup_Commutative_Group (CommutativeS t a) (GroupS t a)
+
+type DeriveAbelianGroup_Commutative_Monoid_Cancellative t a =
+  AbelianGroup_Commutative_Group
+    (CommutativeS t a)
+    (DeriveGroup_Monoid_Cancellative t a)
+
+-- Instances
+
+type instance MagmaS (_ :: BinaryBoolean) Bool = MagmaPrim
+type instance NeutralS (_ :: BinaryBoolean) Bool = NeutralPrim
+type instance CommutativeS (_ :: BinaryBoolean) Bool = CommutativeNum
+type instance SemigroupS (op :: BinaryBoolean) Bool =
+     DeriveSemigroup_Magma op Bool
+
+-- Int
+
+type instance MagmaS       (_ :: BinaryNumeric) Int = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Int = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Int = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Int = DeriveSemigroup_Magma          op Int
+type instance MonoidS     (op :: BinaryNumeric) Int = DeriveMonoid_Semigroup_Neutral op Int
+
+type instance CancellativeS Add Int = CancellativeNum
+type instance GroupS        Add Int = DeriveGroup_Monoid_Cancellative      Add Int
+type instance AbelianGroupS Add Int = DeriveAbelianGroup_Commutative_Group Add Int
+
+-- Integer
+
+type instance MagmaS       (_ :: BinaryNumeric) Integer = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Integer = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Integer = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Integer = DeriveSemigroup_Magma          op Integer
+type instance MonoidS     (op :: BinaryNumeric) Integer = DeriveMonoid_Semigroup_Neutral op Integer
+
+type instance CancellativeS Add Integer = CancellativeNum
+type instance GroupS        Add Integer = DeriveGroup_Monoid_Cancellative      Add Integer
+type instance AbelianGroupS Add Integer = DeriveAbelianGroup_Commutative_Group Add Integer
+
+-- Float
+
+type instance MagmaS       (_ :: BinaryNumeric) Float = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Float = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Float = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Float = DeriveSemigroup_Magma          op Float
+type instance MonoidS     (op :: BinaryNumeric) Float = DeriveMonoid_Semigroup_Neutral op Float
+
+type instance CancellativeS Add Float = CancellativeNum
+type instance CancellativeS Mul Float = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) Float = DeriveGroup_Monoid_Cancellative      op Float
+type instance AbelianGroupS (op :: BinaryNumeric) Float = DeriveAbelianGroup_Commutative_Group op Float
+
+-- Double
+
+type instance MagmaS       (_ :: BinaryNumeric) Double = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Double = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Double = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Double = DeriveSemigroup_Magma          op Double
+type instance MonoidS     (op :: BinaryNumeric) Double = DeriveMonoid_Semigroup_Neutral op Double
+
+type instance CancellativeS Add Double = CancellativeNum
+type instance CancellativeS Mul Double = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) Double = DeriveGroup_Monoid_Cancellative      op Double
+type instance AbelianGroupS (op :: BinaryNumeric) Double = DeriveAbelianGroup_Commutative_Group op Double
+
+-- Rational
+
+type instance MagmaS       (_ :: BinaryNumeric) Rational = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Rational = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Rational = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Rational = DeriveSemigroup_Magma          op Rational
+type instance MonoidS     (op :: BinaryNumeric) Rational = DeriveMonoid_Semigroup_Neutral op Rational
+
+type instance CancellativeS Add Rational = CancellativeNum
+type instance CancellativeS Mul Rational = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) Rational = DeriveGroup_Monoid_Cancellative      op Rational
+type instance AbelianGroupS (op :: BinaryNumeric) Rational = DeriveAbelianGroup_Commutative_Group op Rational
+
+type instance MagmaS       (_ :: BinaryNumeric) Rational = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) Rational = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) Rational = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) Rational = DeriveSemigroup_Magma          op Rational
+type instance MonoidS     (op :: BinaryNumeric) Rational = DeriveMonoid_Semigroup_Neutral op Rational
+
+-- Ratio Int8
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int8) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int8) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int8) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int8) = DeriveSemigroup_Magma          op (Ratio Int8)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int8) = DeriveMonoid_Semigroup_Neutral op (Ratio Int8)
+
+type instance CancellativeS Add (Ratio Int8) = CancellativeNum
+type instance CancellativeS Mul (Ratio Int8) = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) (Ratio Int8) = DeriveGroup_Monoid_Cancellative      op (Ratio Int8)
+type instance AbelianGroupS (op :: BinaryNumeric) (Ratio Int8) = DeriveAbelianGroup_Commutative_Group op (Ratio Int8)
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int8) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int8) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int8) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int8) = DeriveSemigroup_Magma          op (Ratio Int8)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int8) = DeriveMonoid_Semigroup_Neutral op (Ratio Int8)
+
+-- Ratio Int8
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int8) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int8) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int8) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int8) = DeriveSemigroup_Magma          op (Ratio Int8)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int8) = DeriveMonoid_Semigroup_Neutral op (Ratio Int8)
+
+type instance CancellativeS Add (Ratio Int8) = CancellativeNum
+type instance CancellativeS Mul (Ratio Int8) = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) (Ratio Int8) = DeriveGroup_Monoid_Cancellative      op (Ratio Int8)
+type instance AbelianGroupS (op :: BinaryNumeric) (Ratio Int8) = DeriveAbelianGroup_Commutative_Group op (Ratio Int8)
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int8) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int8) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int8) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int8) = DeriveSemigroup_Magma          op (Ratio Int8)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int8) = DeriveMonoid_Semigroup_Neutral op (Ratio Int8)
+
+-- Ratio Int16
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int16) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int16) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int16) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int16) = DeriveSemigroup_Magma          op (Ratio Int16)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int16) = DeriveMonoid_Semigroup_Neutral op (Ratio Int16)
+
+type instance CancellativeS Add (Ratio Int16) = CancellativeNum
+type instance CancellativeS Mul (Ratio Int16) = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) (Ratio Int16) = DeriveGroup_Monoid_Cancellative      op (Ratio Int16)
+type instance AbelianGroupS (op :: BinaryNumeric) (Ratio Int16) = DeriveAbelianGroup_Commutative_Group op (Ratio Int16)
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int16) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int16) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int16) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int16) = DeriveSemigroup_Magma          op (Ratio Int16)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int16) = DeriveMonoid_Semigroup_Neutral op (Ratio Int16)
+
+-- Ratio Int32
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int32) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int32) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int32) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int32) = DeriveSemigroup_Magma          op (Ratio Int32)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int32) = DeriveMonoid_Semigroup_Neutral op (Ratio Int32)
+
+type instance CancellativeS Add (Ratio Int32) = CancellativeNum
+type instance CancellativeS Mul (Ratio Int32) = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) (Ratio Int32) = DeriveGroup_Monoid_Cancellative      op (Ratio Int32)
+type instance AbelianGroupS (op :: BinaryNumeric) (Ratio Int32) = DeriveAbelianGroup_Commutative_Group op (Ratio Int32)
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int32) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int32) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int32) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int32) = DeriveSemigroup_Magma          op (Ratio Int32)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int32) = DeriveMonoid_Semigroup_Neutral op (Ratio Int32)
+
+
+-- Ratio Int64
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int64) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int64) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int64) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int64) = DeriveSemigroup_Magma          op (Ratio Int64)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int64) = DeriveMonoid_Semigroup_Neutral op (Ratio Int64)
+
+type instance CancellativeS Add (Ratio Int64) = CancellativeNum
+type instance CancellativeS Mul (Ratio Int64) = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) (Ratio Int64) = DeriveGroup_Monoid_Cancellative      op (Ratio Int64)
+type instance AbelianGroupS (op :: BinaryNumeric) (Ratio Int64) = DeriveAbelianGroup_Commutative_Group op (Ratio Int64)
+
+type instance MagmaS       (_ :: BinaryNumeric) (Ratio Int64) = MagmaNum
+type instance NeutralS     (_ :: BinaryNumeric) (Ratio Int64) = NeutralNum
+type instance CommutativeS (_ :: BinaryNumeric) (Ratio Int64) = CommutativeNum
+
+type instance SemigroupS  (op :: BinaryNumeric) (Ratio Int64) = DeriveSemigroup_Magma          op (Ratio Int64)
+type instance MonoidS     (op :: BinaryNumeric) (Ratio Int64) = DeriveMonoid_Semigroup_Neutral op (Ratio Int64)
+
+
+type instance CancellativeS Add Rational = CancellativeNum
+type instance CancellativeS Mul Rational = CancellativeFractional
+
+type instance GroupS        (op :: BinaryNumeric) Rational = DeriveGroup_Monoid_Cancellative      op Rational
+type instance AbelianGroupS (op :: BinaryNumeric) Rational = DeriveAbelianGroup_Commutative_Group op Rational
+
+data ComplexLift
+
+type instance MagmaS        (op :: BinaryNumeric) (Complex a) = MagmaNum
+type instance NeutralS      (op :: BinaryNumeric) (Complex a) = NeutralNum
+type instance CommutativeS  (op :: BinaryNumeric) (Complex a) = CommutativeNum
+type instance CancellativeS Add (Complex a) = CancellativeNum
+type instance CancellativeS Mul (Complex a) = CancellativeFractional
+
+type instance SemigroupS  (op :: BinaryNumeric) (Complex a) = DeriveSemigroup_Magma          op (Complex a)
+type instance MonoidS     (op :: BinaryNumeric) (Complex a) = DeriveMonoid_Semigroup_Neutral op (Complex a)
+
+type instance GroupS        (op :: BinaryNumeric) (Complex a) = DeriveGroup_Monoid_Cancellative      op (Complex a)
+type instance AbelianGroupS (op :: BinaryNumeric) (Complex a) = DeriveAbelianGroup_Commutative_Group op (Complex a)
diff --git a/library/Noether/Algebra/Single/Synonyms.hs b/library/Noether/Algebra/Single/Synonyms.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Single/Synonyms.hs
@@ -0,0 +1,22 @@
+module Noether.Algebra.Single.Synonyms where
+
+import           Noether.Lemmata.TypeFu (Proxy(..))
+
+import           Noether.Algebra.Tags
+
+-- Some proxy synonyms
+
+pattern AddP :: Proxy Add
+pattern AddP = Proxy
+
+pattern MulP :: Proxy Mul
+pattern MulP = Proxy
+
+pattern AndP :: Proxy And
+pattern AndP = Proxy
+
+pattern OrP :: Proxy Or
+pattern OrP = Proxy
+
+pattern XorP :: Proxy Xor
+pattern XorP = Proxy
diff --git a/library/Noether/Algebra/Subtyping.hs b/library/Noether/Algebra/Subtyping.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Subtyping.hs
@@ -0,0 +1,7 @@
+module Noether.Algebra.Subtyping
+  ( Subtype
+  , embed
+  ) where
+
+class Subtype a b where
+  embed :: a -> b
diff --git a/library/Noether/Algebra/Tags.hs b/library/Noether/Algebra/Tags.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Tags.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE InstanceSigs        #-}
+module Noether.Algebra.Tags where
+
+import           Data.Monoid
+import           Prelude
+
+data BinaryNumeric = Add | Mul
+data BinaryBoolean = And | Or | Xor
+
+-- | Oh, Either...
+data Side = L | R
+
+data FunctionLift = FunctionLift
+
diff --git a/library/Noether/Algebra/Vector/Boxed.hs b/library/Noether/Algebra/Vector/Boxed.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Vector/Boxed.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE DeriveAnyClass   #-}
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Vector.Boxed where
+
+import qualified Prelude                        as P
+
+import qualified Data.Vector                    as V
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Linear
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+
+import           Noether.Algebra.Vector.Generic
+import           Noether.Algebra.Vector.Tags
+
+{-| BVector n v ≅ v^n. -}
+
+newtype BVector (n :: k) v =
+  BVector (V.Vector v)
+  deriving (Show)
+
+unsafeFromList :: [a] -> BVector n a
+unsafeFromList as = BVector (V.fromList as)
+
+unsafeChangeDimension
+  :: forall k l (m :: k) (n :: l) a.
+     BVector m a -> BVector n a
+unsafeChangeDimension (BVector as) = BVector as
+
+{-| Lifting addition and multiplication coordinatewise (Hadamard?) -}
+
+instance (MagmaK op v s) =>
+         MagmaK op (BVector n v) (MagmaTagged BVectorLift s) where
+  binaryOpK o _ = gBinaryOpK @V.Vector @v @s o
+
+{-| Neutral elements for addition and multiplication. -}
+
+instance (KnownNat n, NeutralK op v s) =>
+         NeutralK op (BVector n v) (NeutralTagged BVectorLift s) where
+  neutralK o _ = gNeutralK @n @V.Vector @v @s o
+
+{-| Pointwise negation and inversion.
+
+    Note that v^n has (a lot of) nontrivial zerodivisors even if v does not.
+    The zerodivisors are all elements with a zero(divisor) in some coordinate,
+    e.g. (1,0) and (0,1) are zerodivisors in R^2.
+
+    (This corresponds to the idea that the Spec of a product ring is disconnected!)
+-}
+
+instance (CancellativeK op v s) =>
+         CancellativeK op (BVector n v) (CancellativeTagged BVectorLift s) where
+  cancelK o _ = gCancelK @V.Vector @v @s o
+
+{-| Actions of a on b extend to actions of a on 'BVector n b'. -}
+
+instance (ActsK lr op a b s) =>
+         ActsK lr op a (BVector n b) (ActsTagged BVectorLift s) where
+  actK o _ _ = gActK @V.Vector @a @b @s @lr o
+
+{- Instances of the "basic types". Everything else can be derived from these.
+   We're simply choosing the strategies we defined above, using the Derive*
+   synonyms to ease typing.
+-}
+
+type instance MagmaS        (op :: BinaryNumeric) (BVector n a) = DeriveMagma_Tagged        BVectorLift op a
+type instance NeutralS      (op :: BinaryNumeric) (BVector n a) = DeriveNeutral_Tagged      BVectorLift op a
+type instance CommutativeS  (op :: BinaryNumeric) (BVector n a) = DeriveCommutative_Tagged  BVectorLift op a
+
+-- Protecting the innocent from zerodivisors since 1998
+
+type instance CancellativeS  Add (BVector n a) = DeriveCancellative_Tagged BVectorLift Add a
+
+-- Like I said:
+
+type instance SemigroupS (op :: BinaryNumeric) (BVector n a) = DeriveSemigroup_Magma          op (BVector n a)
+type instance MonoidS    (op :: BinaryNumeric) (BVector n a) = DeriveMonoid_Semigroup_Neutral op (BVector n a)
+
+type instance GroupS        Add (BVector n a)  = DeriveGroup_Monoid_Cancellative      Add (BVector n a)
+type instance AbelianGroupS Add (BVector n a)  = DeriveAbelianGroup_Commutative_Group Add (BVector n a)
+
+type instance ActsS       lr Mul     a (BVector n b) = DeriveActs_Tagged BVectorLift   lr Mul a b
+type instance CompatibleS lr Mul Mul a (BVector n b) = DeriveCompatible_Acts_Semigroup lr Mul Mul a (BVector n b)
+
+type instance ActorLinearS lr Mul Add a Add (BVector n a) =
+     DeriveActorLinearActs_Acts_Semigroup_Semigroup lr Mul Add a Add (BVector n a)
+type instance ActeeLinearS lr Mul a Add (BVector n a) =
+     DeriveActeeLinearActs_Acts_Semigroup lr Mul a Add (BVector n a)
+
diff --git a/library/Noether/Algebra/Vector/Generic.hs b/library/Noether/Algebra/Vector/Generic.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Vector/Generic.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE TypeApplications    #-}
+module Noether.Algebra.Vector.Generic where
+
+import qualified Data.Vector.Generic      as G
+
+import           Noether.Lemmata.TypeFu
+import qualified Prelude                  as P
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Multiple
+import           Noether.Algebra.Single
+
+gBinaryOpK
+  :: forall v a s op z.
+     (MagmaK op a s, G.Vector v a, Coercible v z)
+  => Proxy op -> z a -> z a -> z a
+gBinaryOpK o x y = coerce (G.zipWith binop (coerce x :: v a) (coerce y :: v a))
+    where
+      binop = binaryOpK o (Proxy @s)
+
+gCancelK
+  :: forall v a s op z.
+     (CancellativeK op a s, G.Vector v a, Coercible v z)
+  => Proxy op -> z a -> z a
+gCancelK o x = coerce (G.map cancelK' (coerce x :: v a))
+    where
+      cancelK' = cancelK o (Proxy @s)
+
+gActK
+  :: forall v a b s lr op z.
+     (ActsK lr op a b s, G.Vector v b, Coercible v z)
+  => Proxy op -> a -> z b -> z b
+gActK o a x = coerce (G.map (actK' a) (coerce x :: v b))
+    where
+      actK' = actK o (Proxy @s) (Proxy @lr)
+
+gNeutralK
+  :: forall n v a s op b.
+     (NeutralK op a s, KnownNat n, G.Vector v a, Coercible v (b n))
+  => Proxy op -> b n a
+gNeutralK o = coerce (G.replicate count neutralValue :: v a)
+    where
+      count = P.fromIntegral (natVal (Proxy @n))
+      neutralValue = neutralK o (Proxy @s)
+
diff --git a/library/Noether/Algebra/Vector/Tags.hs b/library/Noether/Algebra/Vector/Tags.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Vector/Tags.hs
@@ -0,0 +1,12 @@
+module Noether.Algebra.Vector.Tags where
+
+import           Noether.Lemmata.TypeFu
+
+data VectorLift
+
+data UVectorLift
+data BVectorLift
+data SVectorLift
+data MVectorLift
+data SMVectorLift
+data UMVectorLift
diff --git a/library/Noether/Algebra/Vector/Tutorial.hs b/library/Noether/Algebra/Vector/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Vector/Tutorial.hs
@@ -0,0 +1,114 @@
+{-| A work-in-progress tutorial for Noether vectors.
+
+    This module demonstrates creating vectors, using simple operators to
+    transform them, and techniques that leverage type system features to provide
+    improved correctness guarantees.
+-}
+module Noether.Algebra.Vector.Tutorial
+  (
+  -- * Basics
+  -- $basics
+
+  -- * Computing with statically differentiable but unknown dimensions, a la subhask
+  -- $action
+
+  -- $sizedvectors
+  ) where
+
+import           Noether.Algebra.Tags
+import           Noether.Lemmata.Prelude
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Linear
+import           Noether.Algebra.Single
+
+import           Noether.Algebra.Vector.Boxed
+
+{- $basics
+
+  Vectors are constructed with 'unsafeFromList', which wraps
+  'Data.Vector.Generic.fromList' under the hood.
+
+> v :: BVector 10 (Complex Double)
+> v = unsafeFromList $ map (\x -> cis (x * pi / 10)) [1..10]
+
+> w :: BVector 10 (Complex Double)
+> w = unsafeFromList $ map (\x -> cis (-x * pi / 10)) [1..10]
+
+  The type annotations actually do nothing but bring the KnownNat constraint
+  into scope. (TODO demo with PartialTypeSignatures?)
+
+> func x = x + x - x * x + zero
+
+  The inferred type of @func@ is somewhat hairy:
+
+> func
+>   :: ( CancellativeK 'Add a (CancellativeS 'Add a)
+>      , MagmaK 'Add a (MagmaS 'Add a)
+>      , MagmaK 'Mul a (MagmaS 'Mul a)
+>      , NeutralK 'Add a (NeutralS 'Add a)
+>      ) => a -> a
+
+  which is an expanded version of
+
+> func
+>   :: ( Cancellative 'Add a
+>      , Magma 'Add a
+>      , Magma 'Mul a
+>      , Neutral 'Add a
+>      ) => a -> a
+
+  but can be understood as asking for a type @a@ that supports subtraction
+  ('Cancellative' 'Add'), addition ('Magma' 'Add'), and multiplication ('Magma'
+  'Mul'), and has a zero ('Neutral' 'Add').
+
+> g = map (\lambda -> lerp (lambda :+ 0) v (func w)) [0.0,0.1..1.0 :: Double]
+
+-}
+
+{- $action
+
+   Given an action of @a@ on @b@, @a %< b@ computes the result. Usually, this is
+   just multiplication. Other interesting examples exist: e.g. group actions,
+   where @b@ is just a set, and so on.
+
+   A particularly pervasive one is the action of Z on groups:
+
+prop> n %< a = a + a + ... + a
+
+   where the right side is a added to itself n times.
+-}
+
+{-
+
+> g :: [BVector 10 (Complex Double)]
+-}
+
+{- $sizedvectors
+
+> u1 :: BVector "a" Double
+> u1 = unsafeFromList [1..10]
+
+> u2 :: BVector "b" Double
+> u2 = unsafeFromList [1..10]
+
+> u3 :: BVector "a" Double
+> u3 = unsafeFromList [1..10]
+
+> s = u1 + x %< u3
+>   where
+>     x = 0.3 :: Double
+
+  This fails:
+
+> t = u1 + u2
+
+>   • Couldn't match type ‘"b"’ with ‘"a"’
+>     Expected type: BVector "a" Double
+>       Actual type: BVector "b" Double
+
+  You need to do the whole "I know what I'm doing":
+
+> t = u1 + unsafeChangeDimension u3
+
+-}
diff --git a/library/Noether/Algebra/Vector/Unboxed.hs b/library/Noether/Algebra/Vector/Unboxed.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Algebra/Vector/Unboxed.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE TypeApplications #-}
+module Noether.Algebra.Vector.Unboxed where
+
+import qualified Prelude                     as P
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Noether.Algebra.Actions
+import           Noether.Algebra.Linear
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+import           Noether.Algebra.Vector.Tags
+
+import qualified Data.Vector.Unboxed         as U
+
+{-| UVector n v ≅ v^n for 'Unbox' types 'v'. -}
+
+newtype UVector (n :: Nat) v =
+  UVector (U.Vector v)
+  deriving (Show)
+
+{-| Lifting addition and multiplication coordinatewise (Hadamard?) -}
+
+instance (U.Unbox v, MagmaK op v s) =>
+         MagmaK op (UVector n v) (MagmaTagged UVectorLift s) where
+  binaryOpK o _ (UVector x) (UVector y) = UVector (U.zipWith binop x y)
+    where
+      binop = binaryOpK o (Proxy @s)
+
+{-| Neutral elements for addition and multiplication. -}
+
+instance (U.Unbox v, KnownNat n, NeutralK op v s) =>
+         NeutralK op (UVector n v) (NeutralTagged UVectorLift s) where
+  neutralK o _ = UVector (U.replicate count neutralValue)
+    where
+      count = P.fromIntegral (natVal (Proxy @n))
+      neutralValue = neutralK o (Proxy @s)
+
+{-| Pointwise negation and inversion.
+
+    Note that v^n has (a lot of) nontrivial zerodivisors even if v does not.
+    The zerodivisors are all elements with a zero(divisor) in some coordinate,
+    e.g. (1,0) and (0,1) are zerodivisors in R^2.
+
+    (This corresponds to the idea that the Spec of a product ring is disconnected!)
+-}
+
+instance (U.Unbox v, KnownNat n, CancellativeK op v s) =>
+         CancellativeK op (UVector n v) (CancellativeTagged UVectorLift s) where
+  cancelK o _ (UVector vs) = UVector (U.map cancelK' vs)
+    where
+      cancelK' = cancelK o (Proxy @s)
+
+{-| Actions of a on b extend to actions of a on 'UVector n b'. -}
+
+instance (U.Unbox b, KnownNat n, ActsK lr op a b s) =>
+         ActsK lr op a (UVector n b) (ActsTagged UVectorLift s) where
+  actK o _ lr a (UVector bs) = UVector (U.map (actK' a) bs)
+    where
+      actK' = actK o (Proxy @s) lr
+
+{- Instances of the "basic types". Everything else can be derived from these.
+   We're simply choosing the strategies we defined above, using the Derive*
+   synonyms to ease typing.
+-}
+
+type instance MagmaS        (op :: BinaryNumeric) (UVector n a) = DeriveMagma_Tagged        UVectorLift op a
+type instance NeutralS      (op :: BinaryNumeric) (UVector n a) = DeriveNeutral_Tagged      UVectorLift op a
+type instance CommutativeS  (op :: BinaryNumeric) (UVector n a) = DeriveCommutative_Tagged  UVectorLift op a
+
+-- Protecting the innocent from zerodivisors since 1998
+
+type instance CancellativeS  Add (UVector n a) = DeriveCancellative_Tagged UVectorLift Add a
+
+{- Like I said: -}
+
+type instance SemigroupS (op :: BinaryNumeric) (UVector n a) = DeriveSemigroup_Magma          op (UVector n a)
+type instance MonoidS    (op :: BinaryNumeric) (UVector n a) = DeriveMonoid_Semigroup_Neutral op (UVector n a)
+
+type instance GroupS        Add (UVector n a)  = DeriveGroup_Monoid_Cancellative      Add (UVector n a)
+type instance AbelianGroupS Add (UVector n a)  = DeriveAbelianGroup_Commutative_Group Add (UVector n a)
+
+type instance ActsS       lr Mul     a (UVector n b) = DeriveActs_Tagged UVectorLift   lr Mul a b
+type instance CompatibleS lr Mul Mul a (UVector n b) = DeriveCompatible_Acts_Semigroup lr Mul Mul a (UVector n b)
+
+type instance ActorLinearS lr Mul Add a Add (UVector n a) =
+     DeriveActorLinearActs_Acts_Semigroup_Semigroup lr Mul Add a Add (UVector n a)
+type instance ActeeLinearS lr Mul a Add (UVector n a) =
+     DeriveActeeLinearActs_Acts_Semigroup lr Mul a Add (UVector n a)
+
+v :: UVector 10 Double
+v = UVector $ U.fromList [1..10]
+
+w :: UVector 10 Double
+w = UVector $ U.fromList [10,9..1]
+
+-- Inferred type:
+-- f ::
+--   (MagmaK 'Mul a (MagmaS 'Mul a), MagmaK 'Add a (MagmaS 'Add a),
+--    CancellativeK 'Add a (CancellativeS 'Add a)) =>
+--   a -> a
+
+f x = x + x - x * x
+
+-- | This is equal to
+-- > UVector [5.0,5.0,5.0,5.0,5.0,5.0,5.0,5.0,5.0,5.0]
+
+g :: [UVector 10 Double]
+g = map (\x -> lerp x v w) [0.0,0.1..1.0 :: Double]
diff --git a/library/Noether/Equality.hs b/library/Noether/Equality.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Equality.hs
@@ -0,0 +1,214 @@
+{-# LANGUAGE MagicHash #-}
+
+{-| Flexible, extensible notions of equality supporting "custom deriving strategies".
+
+    This module is, as of now, completely separate from the rest of the codebase
+    (which was developed later, using ideas first tested here).
+
+    There are no incoherent or even overlapping instances anywhere here.
+    The ideas are based off of the "Advanced Overlap" page on the Haskell wiki:
+    <https://wiki.haskell.org/GHC/AdvancedOverlap>, and were inspired by
+    the observation that the overlapping instances there could be completely
+    replaced with not-necessarily-closed type families.
+
+    This last point is crucial for Noether, which aspires to be a library that
+    people can use for their own work. The closed-TF approach of declaring how
+    a couple standard types are compared, putting a catch-all case after
+    those to handle everything else (all in the core library), and then calling it a day
+    isn't really sensible, then, for obvious reasons.
+
+    I have some prototype Oleg-style "guided resolution" in development that seems to
+    be promising, and I think this approach, together with the former, can be used
+    to handle (instances of typeclasses representing) algebraic structures on types
+    without the incoherent nonsense in place currently.
+-}
+
+module Noether.Equality where
+
+import           GHC.Prim
+
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+import           Prelude                 ((&&), (-))
+import qualified Prelude
+
+{-| This represents the unique "equality strategy" to be used for 'a'.
+
+    There may be many different notions of equality that can be applied to a
+    particular type, and instances of the 'Equality' family are used to disambiguate
+    those by specifying which one to use.
+-}
+
+type family Equality a
+
+{-| Different notions of equality can have different "results". For instance,
+    standard Eq-style "tired" equality returns Bool values, whereas a more
+    numerically "wired" implementation for floating-point numbers could instead
+    use tolerances/"epsilons" to compare things.
+
+    This is reminiscent of subhask-ish things (in particular, the all-pervasive
+    Logic type family).
+-}
+
+type family EquateResult s a
+
+type EquateResult' a = EquateResult (Equality a) a
+type EquateAs' a = EquateAs (Equality a) a
+
+{-| This is the user-facing 'Eq' replacement class.
+
+    The Eq a/EquateAs s a trick is straight off the GHC wiki, as I said, although
+    we can now use proxies instead of slinging 'undefined's around :)
+-}
+
+class Eq a where
+  (==) :: a -> a -> EquateResult' a
+
+instance (EquateAs s a, s ~ Equality a) => Eq a where
+  (==) = equateAs (proxy# :: Proxy# s)
+
+{-| An instance of this class defines a way to equate two terms of
+    a given type according to a given "strategy" 's'.
+-}
+
+class EquateAs s a where
+  equateAs :: Proxy# s -> a -> a -> EquateResult s a
+
+--------------------------------------------------------------------------------
+-- Instances
+--------------------------------------------------------------------------------
+
+-- Prelude equality.
+
+data PreludeEq
+
+type instance EquateResult PreludeEq a = Bool
+
+instance (Prelude.Eq a) => EquateAs PreludeEq a where
+  equateAs _ = (Prelude.==)
+
+{- "Numeric" equality.
+
+   This is obviously the same as Prelude equality. It makes for another example,
+   that's all.
+-}
+
+data Numeric
+
+type instance EquateResult Numeric a = Bool
+
+instance (Prelude.Eq a, Num a) => EquateAs Numeric a where
+  equateAs _ = (Prelude.==)
+
+{- "Approximate" equality defined only up to an epsilon.
+   (`reflection` could be considered if one wanted to defer the choice of tolerance.)
+-}
+
+data Approximate
+
+type instance EquateResult Approximate a = a -> Bool
+
+instance (Num a, Ord a) =>
+         EquateAs Approximate a where
+  equateAs _ x y epsilon = abs (x - y) < epsilon
+
+-- Maybe this is a good time to learn generics?
+
+type instance EquateResult (Common Approximate) (a, a) = a -> Bool
+
+instance (EquateAs Approximate a) =>
+         EquateAs (Common Approximate) (a, a) where
+  equateAs _ (x,y) (x',y') eps = equateAs p x x' eps && equateAs p y y' eps
+    where
+      p = proxy# :: Proxy# Approximate
+
+{- Ideally, all equality strategies with a 'Bool' equality result could've been
+   quantified over here, but I don't see how that can be done without replacing
+   EquateResult by a fundep of some sort or ending up with un-unifiable constraints
+   via the use of a type-level if, where the latter would lead to scary errors that
+   look like:
+
+   "No instance for <two pages of really helpfully expanded type synonyms>"
+-}
+
+data Common a
+
+type instance EquateResult (Common Numeric) (a, a) = Bool
+
+instance ( EquateAs Numeric a
+         , EquateAs Numeric a
+         ) => EquateAs (Common Numeric) (a, a) where
+
+  equateAs _ (x, y) (x', y') = equateAs p x x' && equateAs p y y'
+    where
+      p = proxy# :: Proxy# Numeric
+
+type instance EquateResult (Common PreludeEq) (a, a) = Bool
+
+instance ( EquateAs PreludeEq a
+         , EquateAs PreludeEq a
+         ) => EquateAs (Common PreludeEq) (a, a) where
+
+  equateAs _ (x, y) (x', y') = equateAs p x x' && equateAs p y y'
+    where
+      p = proxy# :: Proxy# PreludeEq
+
+{-| The 'Composite' strategy just uses the canonical strategies on each
+    "slot" of the tuple and returns a tuple of results.
+
+    It's ... sort of lazy.
+-}
+
+data Composite a b
+
+type instance EquateResult (Composite l r) (a, b) =
+     (EquateResult l a, EquateResult r b)
+
+instance (EquateAs l a, EquateAs r b) =>
+         EquateAs (Composite l r) (a, b) where
+  equateAs _ (x,y) (x',y') = (equateAs pl x x', equateAs pr y y')
+    where
+      pl = proxy# :: Proxy# l
+      pr = proxy# :: Proxy# r
+
+{- You can always define one-off 'Explicit' equality strategies.
+
+   If I can implement guided instance selection robustly, these can
+   be expected to have the highest priority (unless one thinks of attaching
+   priorities to the strategies themselves, like fixity annotations! TODO).
+-}
+
+data Explicit (s :: k)
+
+{- For instance, consider comparing integers for equality modulo
+   some number.
+-}
+
+data Modulo (n :: Nat)
+
+type instance EquateResult (Explicit (Modulo n)) Int = Bool
+
+instance KnownNat n => EquateAs (Explicit (Modulo n)) Int where
+  equateAs _ x y = x `div` n' Prelude.== y `div` n'
+    where
+      n' = fromInteger $ natVal' (proxy# :: Proxy# n)
+
+{-| Lightweight equality for newtypes using 'Coercible' from 'Data.Coerce'.
+
+    This is so, so wonderful. (Well, now that the complaints about differing
+    representations have gone away, anyway.)
+-}
+
+data CoerceFrom a s
+type CoerceFrom' a = CoerceFrom a (Equality a)
+
+type instance EquateResult (CoerceFrom a s) b = EquateResult s a
+
+instance ( EquateAs s a
+         , Coercible b a
+         ) => EquateAs (CoerceFrom a s) b where
+  equateAs _ x y = equateAs p (coerce x :: a) (coerce y :: a)
+    where
+      p = proxy# :: Proxy# s
+
diff --git a/library/Noether/Equality/Tutorial.hs b/library/Noether/Equality/Tutorial.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Equality/Tutorial.hs
@@ -0,0 +1,122 @@
+{-# LANGUAGE MagicHash              #-}
+
+module Noether.Equality.Tutorial where
+
+import           GHC.TypeLits
+import           Prelude          hiding (Eq, (==))
+
+import           Noether.Equality
+
+{- Library definitions would probably look like this.
+
+   (They might even be put in Backpack signature files or something, for, e.g.
+   a swap-in numerically sensible set of equality strategies that uses approximate
+   equality for everything floating-ish.)
+
+   These type instance definitions can be thought of as fine-grained applications of
+   custom deriving strategies, as alluded to in the opening wall of text. So we have
+   'Numeric', but also 'Composite Approximate Numeric', and so on. (More generics?)
+-}
+
+-- This might be read as
+-- | deriving instance Eq Int using strategy Numeric
+type instance Equality Int = Numeric
+
+testInt = 0 == (1 :: Int)
+
+-- | deriving instance Eq Double using strategy Approximate
+type instance Equality Double = Approximate
+
+testDouble = (t eps1, t eps2)
+  where
+    t = 0.0 == (0.01 :: Double)
+    eps1 = 0.001
+    eps2 = 0.1
+
+-- And so on.
+
+{- What follows are the specifications of (unique!) equality strategies for
+   a couple of types. A user would only interact with this bit, ideally, to define
+   equality for her own types.
+
+   The types of the test* functions have intentionally been left out. Inference stays
+   alive and well :)
+-}
+
+{-| 'Common' 'Approximate' is a strategy that uses the same epsilon for both
+    slots of the tuple, going
+
+    (a -> Bool, a -> Bool) ~> a -> (Bool, Bool) ~> a -> Bool
+
+    Note that I can replace this with Common Numeric and have that work just fine,
+    even though the concrete specification of equality on Double is Approximate.
+    Defining the Equality instance does not throw away the information of the other
+    possible equality tests, and bigger types like tuples and such can make use of
+    any equality that the components support.
+-}
+type instance Equality (Double, Double) = Common Approximate
+
+test1 = lhs == rhs
+  where
+    lhs, rhs :: (Double, Double)
+    lhs = (2.0, 2.0)
+    rhs = (2.00001, 2.0)
+
+{- Suppose I want a newtype that is equated differently.
+   For instance, consider a newtype-wrapped Double that compares according to Prelude
+   equality, not the funky tolerance-ish thing above.
+
+   In defining it,  I can skip making it support the operations that my choice
+   of equality strategy requires. The use of 'PreludeEq' demands an 'Eq' constraint,
+   but 'Dbl' does not need to derive that.
+
+   FIXME: Maybe the type family should make this available? The Advanced Overlap page
+   says that getting the class instances and the type instances to agree is "just
+   something you'll have to do", but does ConstraintKinds let us hack around that now?
+-}
+
+newtype Dbl = Dbl Double
+
+-- Now I can simply coerce the equality on the base type to the newtype.
+
+type instance Equality Dbl = CoerceFrom Double PreludeEq
+
+test2 = Dbl 2.0 == Dbl 2.01
+
+{- In case of 'Eq' on a newtype-wrapped Prelude numeric type, this is a parlor trick
+   at best, but not having to "derive" Num (or write a one-off partial implementation)
+   is awesome:
+-}
+
+newtype Dbl' = Dbl' Double
+
+-- et .. magic!
+type instance Equality Dbl' = CoerceFrom Double Numeric
+
+test3 = Dbl' 2.0 == Dbl' 2.01
+
+{- (I'm intentionally using 'Composite' instead of a tuple to leave that option open
+   for auto-deriving shenanigans.)
+-}
+
+type instance Equality (Dbl, Dbl') = Composite (Equality Dbl) (Equality Dbl')
+
+test4 = (Dbl 2, Dbl' 2) == (Dbl 2.001, Dbl' 2)
+
+-- Let's try the Z/n equality we defined above.
+
+-- As before, define the newtype...
+
+newtype Mod (n :: Nat) = Mod Int
+
+-- "derive" the equality strategy...
+
+type instance Equality (Mod n) = CoerceFrom Int (Explicit (Modulo n))
+
+--- and profit!
+
+test5 = a == b
+  where
+    a, b :: Mod 7
+    a = Mod 3
+    b = Mod 24
diff --git a/library/Noether/Lemmata/Prelude.hs b/library/Noether/Lemmata/Prelude.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Lemmata/Prelude.hs
@@ -0,0 +1,22 @@
+module Noether.Lemmata.Prelude
+  ( module X
+  , fromInteger
+  , fromString
+  ) where
+
+import           Data.Complex as X
+import           Data.Monoid  as X ((<>))
+import           Prelude      as X hiding (Eq, Monoid, fromInteger, negate,
+                                    recip, (&&), (*), (+), (-), (/), (==), (||))
+
+import           Data.Ratio   as X
+import           Data.Int     as X
+import qualified Data.String  as S
+import qualified Prelude      as P
+
+fromInteger :: Num a => Integer -> a
+fromInteger = P.fromInteger
+
+fromString :: S.IsString a => String -> a
+fromString = S.fromString
+
diff --git a/library/Noether/Lemmata/TypeFu.hs b/library/Noether/Lemmata/TypeFu.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Lemmata/TypeFu.hs
@@ -0,0 +1,46 @@
+module Noether.Lemmata.TypeFu
+  ( module X
+  , type ($$>)
+  ) where
+
+import           GHC.Exts           as X
+import           GHC.Prim           as X
+import           GHC.TypeLits       as X
+
+import           Data.Coerce        as X
+import           Data.Proxy         as X
+
+import           Data.Kind          as X hiding (type (*))
+import           Data.Type.Bool     as X
+import           Data.Type.Equality as X
+
+infixl 6 &
+type (&) (a :: Constraint) (b :: Constraint) = (a, b)
+
+infixl 6 &.
+type (&.)
+  (a :: k -> k' -> Constraint)
+  (b :: k -> k' -> Constraint)
+  (p :: k) (q :: k')
+  = (a p q, b p q)
+
+infixl 6 &&.
+type (&&.)
+  (a :: k1 -> k2 -> k3 -> Constraint)
+  (b :: k1 -> k2 -> k3 -> Constraint)
+  (p :: k1) (q :: k2) (r :: k3)
+  = (a p q r, b p q r)
+
+infixl 7 $>
+type ($>)
+  (a :: k1 -> k2 -> k3 -> k4)
+  (b :: k1 -> k2 -> k3)
+  (p :: k1) (q :: k2)
+  = a p q (b p q)
+
+infixl 7 $$>
+type ($$>)
+  (a :: k1 -> k2 -> k3 -> k4 -> k5)
+  (b :: k1 -> k2 -> k3 -> k4)
+  (p :: k1) (q :: k2) (r :: k3)
+  = a p q r (b p q r)
diff --git a/library/Noether/Lemmata/TypeFu/DList.hs b/library/Noether/Lemmata/TypeFu/DList.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Lemmata/TypeFu/DList.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE FunctionalDependencies #-}
+module Noether.Lemmata.TypeFu.DList where
+
+import           Noether.Lemmata.TypeFu
+import           Noether.Lemmata.TypeFu.Set
+
+data The k (x :: k) = The
+
+data Tagged (s :: Symbol) k (x :: k) = Tagged
+
+type instance Cmp (Tagged s1 _ _) (Tagged s2 _ _) = Cmp s1 s2
+
+data DList (xs :: [Type]) :: Type where
+  Nil :: DList '[]
+  Tag :: The Symbol s -> The k x -> DList xs -> DList (Tagged s k x : xs)
+
+nil :: DList '[]
+nil = Nil
+
+data Foo = Bar | Baz
+
+type (**) k (x :: k) = ('The :: The k x)
+
+infixr 5 ~>
+
+type (~>) (s :: Symbol) (the :: The k x) = Tag ('The :: The Symbol s) the
+
+infixr 0 |-|
+type (|-|) a b = a b
+
+infixr 0 |<|
+type (|<|) a b = a (b Nil)
+
+infixr 0 |>|
+type (|>|) a b = Conv (a b)
+
+type family Conv (a :: DList xs) where
+  Conv (_ :: DList xs) = Sort xs
+
+newtype DList_ xs = DList_ (Proxy (Sort xs))
+
+type B
+   =  "index"    ~> Nat    ** 1
+  |-| "type"     ~> Type   ** Type
+  |-| "afoo"     ~> Nat    ** 2
+  |-| "akoe"     ~> Nat    ** 2
+  |-| "pqr"      ~> Type   ** (Type -> Type)
+  |<| "aardvark" ~> [Type] ** '[Type]
+
+type A
+   =  "index"    ~> Nat    ** 1
+  |>| "type"     ~> Type   ** Type
+  |-| "afoo"     ~> Nat    ** 2
+  |-| "akoe"     ~> Nat    ** 2
+  |-| "pqr"      ~> Type   ** (Type -> Type)
+  |<| "aardvark" ~> [Type] **
+       (  "b"  ~> Type ** Nat
+      |>| "aa" ~> Type ** (Type, Type)
+      |<| "a"  ~> Nat  ** 1)
+
+class A__ (a :: [Type]) (b :: Type) | a -> b
+
+data ATag
+data BTag
+
+class A_ (a :: [Type])
+
+instance (a ~ A) => A_ a
+instance A_ a => A__ a ATag
+
+f :: A__ A ATag => Proxy Nat
+f = Proxy
+
+a :: Proxy A
+a = Proxy
diff --git a/library/Noether/Lemmata/TypeFu/Map.hs b/library/Noether/Lemmata/TypeFu/Map.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Lemmata/TypeFu/Map.hs
@@ -0,0 +1,57 @@
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+module Noether.Lemmata.TypeFu.Map
+  ( Nub
+  , Sort
+  , type (<+>)
+  , TMap
+  , TMap'
+  , (:=)
+  , type (\\)
+  , Lookup
+  , Lookup'
+  , Combine
+  , Member
+  ) where
+
+import           Noether.Lemmata.TypeFu
+import           Prelude                    (Bool (..), Maybe (..))
+
+import           Noether.Lemmata.TypeFu.Set hiding (Nub)
+
+infixr 4 :=
+
+data (:=) (k :: k1) (v :: k2)
+
+type TMap m = Nub (Sort m)
+type TMap' m = Sort m
+type (<+>) m n = TMap (m ++ n)
+
+type family Nub t where
+  Nub '[] = '[]
+  Nub '[x] = '[x]
+  Nub ((k := v) : (k := w) : m) = Nub ((k := Combine v w) : m)
+  Nub (x : y : s) = x : Nub (y : s)
+
+type family Combine (a :: v) (b :: v) :: v
+type instance Combine a a = a
+
+type family (m :: [k]) \\ (c :: Symbol) :: [k] where
+  '[] \\ _ = '[]
+  ((q := _) : m) \\ q = m \\ q
+  (p : m) \\ q = p : (m \\ q)
+
+type family Lookup (m :: [k']) (c :: k) :: Maybe v where
+  Lookup '[] k = Nothing
+  Lookup ((k := v) : _) k = Just v
+  Lookup (_ : m) k = Lookup m k
+
+type family Lookup' (m :: [k']) (c :: k) :: v where
+  Lookup' ((k := v) : _) k = v
+  Lookup' (_ : m) k = Lookup' m k
+
+type family Member (c :: k) (m :: [Type]) :: Bool where
+  Member _ '[] = False
+  Member k ((k := _) : _) = True
+  Member k (_ : m) = Member k m
+
+type instance Cmp (k := _) (k' := _) = CmpSymbol k k'
diff --git a/library/Noether/Lemmata/TypeFu/Set.hs b/library/Noether/Lemmata/TypeFu/Set.hs
new file mode 100644
--- /dev/null
+++ b/library/Noether/Lemmata/TypeFu/Set.hs
@@ -0,0 +1,39 @@
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+module Noether.Lemmata.TypeFu.Set where
+
+import           Noether.Lemmata.TypeFu
+import           Prelude                (Bool (..), Ordering (..))
+
+type TSet s = Nub (Sort s)
+type TSet' s = Sort s
+
+type family Cmp (a :: k) (b :: k) :: Ordering
+
+type family (++) (x :: [k]) (y :: [k]) :: [k] where
+  '[]       ++ xs = xs
+  (x : xs) ++ ys = x : (xs ++ ys)
+
+-- xor
+type family (^^) (a :: Bool) (b :: Bool) :: Bool where
+  x ^^ x = False
+  _ ^^ _ = True
+
+type family Nub t where
+  Nub '[] = '[]
+  Nub '[e] = '[e]
+  Nub (e : e : s) = Nub (e : s)
+  Nub (e : f : s) = e : Nub (f : s)
+
+type family Sort (xs :: [k]) :: [k] where
+  Sort '[] = '[]
+  Sort (x : xs) = Sort (Filter False x xs) ++ '[x] ++ Sort (Filter True x xs)
+
+type family Filter (f :: Bool) (p :: k) (xs :: [k]) :: [k] where
+  Filter _ _ '[] = '[]
+  Filter f p (x : xs) = IfCons (f ^^ (Cmp x p == LT)) x (Filter f p xs)
+
+type family IfCons (pred :: Bool) (x :: k) (xs :: [k]) :: [k] where
+  IfCons False _ xs = xs
+  IfCons True x xs = x : xs
+
+type instance Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k'
diff --git a/noether.cabal b/noether.cabal
new file mode 100644
--- /dev/null
+++ b/noether.cabal
@@ -0,0 +1,150 @@
+-- This file has been generated from package.yaml by hpack version 0.17.1.
+--
+-- see: https://github.com/sol/hpack
+
+name:           noether
+version:        0.0.1
+synopsis:       Math in Haskell.
+description:    TODO
+category:       Math
+homepage:       https://github.com/mrkgnao/noether#readme
+bug-reports:    https://github.com/mrkgnao/noether/issues
+maintainer:     Soham Chowdhury
+license:        MIT
+license-file:   LICENSE.md
+build-type:     Simple
+cabal-version:  >= 1.10
+
+extra-source-files:
+    CHANGELOG.md
+    LICENSE.md
+    package.yaml
+    README.md
+    stack.yaml
+
+source-repository head
+  type: git
+  location: https://github.com/mrkgnao/noether
+
+library
+  hs-source-dirs:
+      library
+  default-extensions: ConstraintKinds DataKinds PatternSynonyms EmptyDataDecls FlexibleContexts FlexibleInstances GADTs LiberalTypeSynonyms MultiParamTypeClasses NoImplicitPrelude OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TypeFamilies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses
+  ghc-options: -fwarn-implicit-prelude -fno-warn-unticked-promoted-constructors
+  build-depends:
+      base <= 5.1.0.0
+    , array
+    , ghc-prim
+    , async
+    , deepseq
+    , containers
+    , hashable
+    , transformers
+    , text
+    , stm
+    , bytestring
+    , mtl
+    , mtl-compat
+    , safe
+    , pretty-show
+    , vector
+  exposed-modules:
+      Lemmata
+      Lemmata.Applicative
+      Lemmata.Base
+      Lemmata.Bifunctor
+      Lemmata.Bool
+      Lemmata.Conv
+      Lemmata.Debug
+      Lemmata.Either
+      Lemmata.Exceptions
+      Lemmata.Functor
+      Lemmata.List
+      Lemmata.Monad
+      Lemmata.Panic
+      Lemmata.Semiring
+      Lemmata.Show
+      Lemmata.Unsafe
+      Noether.Algebra.Actions
+      Noether.Algebra.Actions.Acts
+      Noether.Algebra.Actions.API
+      Noether.Algebra.Actions.Compatible
+      Noether.Algebra.Actions.GroupActions
+      Noether.Algebra.Actions.Linearity
+      Noether.Algebra.Actions.Strategies
+      Noether.Algebra.Derive
+      Noether.Algebra.Inference
+      Noether.Algebra.Linear
+      Noether.Algebra.Linear.API
+      Noether.Algebra.Linear.Module
+      Noether.Algebra.Linear.Strategies
+      Noether.Algebra.Multiple
+      Noether.Algebra.Multiple.Ring
+      Noether.Algebra.Multiple.Semiring
+      Noether.Algebra.Multiple.Strategies
+      Noether.Algebra.Single
+      Noether.Algebra.Single.AbelianGroup
+      Noether.Algebra.Single.API
+      Noether.Algebra.Single.Cancellative
+      Noether.Algebra.Single.Commutative
+      Noether.Algebra.Single.Group
+      Noether.Algebra.Single.Magma
+      Noether.Algebra.Single.Monoid
+      Noether.Algebra.Single.Neutral
+      Noether.Algebra.Single.Semigroup
+      Noether.Algebra.Single.Strategies
+      Noether.Algebra.Single.Synonyms
+      Noether.Algebra.Subtyping
+      Noether.Algebra.Tags
+      Noether.Algebra.Vector.Boxed
+      Noether.Algebra.Vector.Generic
+      Noether.Algebra.Vector.Tags
+      Noether.Algebra.Vector.Tutorial
+      Noether.Algebra.Vector.Unboxed
+      Noether.Equality
+      Noether.Equality.Tutorial
+      Noether.Lemmata.Prelude
+      Noether.Lemmata.TypeFu
+      Noether.Lemmata.TypeFu.DList
+      Noether.Lemmata.TypeFu.Map
+      Noether.Lemmata.TypeFu.Set
+  default-language: Haskell2010
+
+executable noether
+  main-is: Main.hs
+  hs-source-dirs:
+      executable
+  default-extensions: ConstraintKinds DataKinds PatternSynonyms EmptyDataDecls FlexibleContexts FlexibleInstances GADTs LiberalTypeSynonyms MultiParamTypeClasses NoImplicitPrelude OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TypeFamilies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses
+  ghc-options: -fwarn-implicit-prelude -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N
+  build-depends:
+      base
+    , noether
+  default-language: Haskell2010
+
+test-suite noether-test-suite
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs:
+      test-suite
+  default-extensions: ConstraintKinds DataKinds PatternSynonyms EmptyDataDecls FlexibleContexts FlexibleInstances GADTs LiberalTypeSynonyms MultiParamTypeClasses NoImplicitPrelude OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TypeFamilies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses
+  ghc-options: -fwarn-implicit-prelude -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N
+  build-depends:
+      base
+    , noether
+    , hedgehog
+  other-modules:
+      Noether.Test.Algebra
+  default-language: Haskell2010
+
+benchmark noether-benchmarks
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs:
+      benchmark
+  default-extensions: ConstraintKinds DataKinds PatternSynonyms EmptyDataDecls FlexibleContexts FlexibleInstances GADTs LiberalTypeSynonyms MultiParamTypeClasses NoImplicitPrelude OverloadedStrings PolyKinds RankNTypes ScopedTypeVariables TypeFamilies TypeInType TypeOperators TypeSynonymInstances UndecidableInstances UndecidableSuperClasses
+  ghc-options: -fwarn-implicit-prelude -fno-warn-unticked-promoted-constructors -rtsopts -threaded -with-rtsopts=-N
+  build-depends:
+      base
+    , noether
+    , criterion
+  default-language: Haskell2010
diff --git a/package.yaml b/package.yaml
new file mode 100644
--- /dev/null
+++ b/package.yaml
@@ -0,0 +1,107 @@
+name: noether
+synopsis: Math in Haskell.
+version: '0.0.1'
+
+maintainer: Soham Chowdhury
+github: mrkgnao/noether
+
+category: Math
+license: MIT
+license-file: LICENSE.md
+description: TODO
+
+ghc-options:
+  - "-fwarn-implicit-prelude"
+  - "-fno-warn-unticked-promoted-constructors"
+default-extensions:
+  - ConstraintKinds
+  - DataKinds
+  - PatternSynonyms
+  - EmptyDataDecls
+  - FlexibleContexts
+  - FlexibleInstances
+  - GADTs
+  - LiberalTypeSynonyms
+  - MultiParamTypeClasses
+  - NoImplicitPrelude
+  - OverloadedStrings
+  - PolyKinds
+  - RankNTypes
+  - ScopedTypeVariables
+  - TypeFamilies
+  - TypeInType
+  - TypeOperators
+  - TypeSynonymInstances
+  - UndecidableInstances
+  - UndecidableSuperClasses
+
+library:
+  dependencies:
+  - base <= 5.1.0.0
+  - array
+  - ghc-prim
+  - async
+  - deepseq
+  - containers
+  - hashable
+  - transformers
+  - text
+  - stm
+  - bytestring
+  - mtl
+  - mtl-compat
+  - safe
+  - pretty-show
+  - vector
+
+    #- reflection
+    #- template-haskell
+  source-dirs:
+  - library
+
+executables:
+  noether:
+    dependencies:
+    - base
+    - noether
+    ghc-options:
+    - "-rtsopts"
+    - "-threaded"
+    - "-with-rtsopts=-N"
+    main: Main.hs
+    source-dirs: executable
+
+# Other stuff
+
+benchmarks:
+  noether-benchmarks:
+    dependencies:
+    - base
+    - noether
+    - criterion
+    ghc-options:
+    - "-rtsopts"
+    - "-threaded"
+    - "-with-rtsopts=-N"
+    main: Main.hs
+    source-dirs: benchmark
+
+tests:
+  noether-test-suite:
+    dependencies:
+    - base
+    - noether
+    - hedgehog
+    ghc-options:
+    - "-rtsopts"
+    - "-threaded"
+    - "-with-rtsopts=-N"
+    main: Main.hs
+    source-dirs: test-suite
+
+extra-source-files:
+- CHANGELOG.md
+- LICENSE.md
+- package.yaml
+- README.md
+- stack.yaml
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
--- /dev/null
+++ b/stack.yaml
@@ -0,0 +1,14 @@
+resolver: lts-8.19
+
+packages:
+  - location: .
+  - location: '../haskell-hedgehog'
+    extra-dep: true
+    subdirs:
+      - hedgehog
+
+extra-deps: []
+
+flags: {}
+
+extra-package-dbs: []
diff --git a/test-suite/Main.hs b/test-suite/Main.hs
new file mode 100644
--- /dev/null
+++ b/test-suite/Main.hs
@@ -0,0 +1,269 @@
+import           Hedgehog
+import qualified Hedgehog.Gen   as Gen
+import qualified Hedgehog.Range as Range
+
+-- import           Algebra
+-- import           EllipticCurve
+import           Lemmata        hiding (negate, one, zero, (*), (+), (-), (/))
+
+import Noether.Test.Algebra
+
+main :: IO ()
+main = tests
+
+-- genInt :: (Monad m, Num a) => Gen m a
+-- genInt = map fromIntegral $ Gen.integral (Range.linearFrom 0 (-100) 100)
+
+-- genIntNonzero :: (Monad m, Eq a, Num a) => Gen m a
+-- genIntNonzero = Gen.filter (/=0) genInt
+
+-- genRational :: (Monad m) => Gen m Rational
+-- genRational = (/) <$> genInt <*> genIntNonzero
+
+-- genNonzero :: (Monad m) => Gen m Rational
+-- genNonzero = (/) <$> genIntNonzero <*> genIntNonzero
+
+-- testNonzero :: (Monad m) => Test m Rational
+-- testNonzero = forAll genNonzero
+
+-- genP1 :: Monad m => Gen m (P1 Rational)
+-- genP1 = Gen.filter nonsingular $ P1 <$> genRational <*> genRational
+--   where
+--     nonsingular (P1 a b) = a /= 0 && b /= 0
+
+-- testP1 :: Monad m => Test m (P1 Rational)
+-- testP1 = forAll genP1
+
+-- scale :: Rg r => r -> P1 r -> P1 r
+-- scale lambda (P1 a b) = P1 (lambda * a) (lambda * b)
+
+-- genP2 :: Monad m => Gen m (P2 Rational)
+-- genP2 = Gen.filter nonsingular $ P2 <$> genRational <*> genRational <*> genRational
+--   where
+--     nonsingular (P2 a b c) = a /= 0 || b /= 0 || c /= 0
+
+-- testP2 :: Monad m => Test m (P2 Rational)
+-- testP2 = forAll genP2
+
+-- genEC :: Monad m => WM Rational -> Gen m (P2 Rational)
+-- genEC wm =
+--   Gen.filter (\p -> nonsingular p && onCurve wm p) $
+--   P2 <$> genRational <*> genRational <*> genRational
+--   where
+--     nonsingular (P2 a b c) = (a /= 0 && c /= 0) || (a == 0 && c == 0 && b /= 0)
+
+-- testEC :: Monad m => WM Rational -> Test m (P2 Rational)
+-- testEC wm = forAll (genEC wm)
+
+-- -- genCurvePt
+-- --   :: (Typeable s, Monad m)
+-- --   => Gen m (CurvePt Rational s)
+-- -- genCurvePt = pt <$> genNonzero <*> genNonzero <*> genNonzero
+
+-- -- testCurvePt
+-- --   :: (Typeable s, Monad m)
+-- --   => Test m (CurvePt Rational s)
+-- -- testCurvePt = forAll genCurvePt
+
+-- genCurve :: Monad m => Gen m (WM Rational)
+-- genCurve = Gen.filter ((/= 0) . discriminant) (WM <$> genNonzero <*> genNonzero)
+
+-- testCurve :: Monad m => Test m (WM Rational)
+-- testCurve = forAll genCurve
+
+-- prop_rp1_eq_refl :: Property
+-- prop_rp1_eq_refl =
+--   property $ do
+--     a <- testP1
+--     a === a
+
+-- prop_rp1_eq_1 :: Property
+-- prop_rp1_eq_1 =
+--   property $ do
+--     p <- testP1
+--     lambda <- testNonzero
+--     p === scale lambda p
+
+-- prop_rp1_eq_2 :: Property
+-- prop_rp1_eq_2 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     P1 a 0 === P1 b 0
+
+-- prop_rp1_eq_3 :: Property
+-- prop_rp1_eq_3 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     P1 0 a === P1 0 b
+
+-- prop_rp1_eq_4 :: Property
+-- prop_rp1_eq_4 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     c <- testNonzero
+--     assert $ P1 a c /= P1 b 0
+
+-- prop_rp2_eq_1 :: Property
+-- prop_rp2_eq_1 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     lambda <- testNonzero
+--     P2 a b 0 === P2 (lambda * a) (lambda * b) 0
+
+-- prop_rp2_eq_2 :: Property
+-- prop_rp2_eq_2 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     lambda <- testNonzero
+--     P2 0 a b === P2 0 (lambda * a) (lambda * b)
+
+-- prop_rp2_eq_3 :: Property
+-- prop_rp2_eq_3 =
+--   property $ do
+--     a <- testNonzero
+--     b <- testNonzero
+--     lambda <- testNonzero
+--     P2 a 0 b === P2 (lambda * a) 0 (lambda * b)
+
+-- ellipticCurveProperty :: Test IO () -> Property
+-- ellipticCurveProperty = withTests 20 . withDiscards 10000 . property
+
+-- prop_ec_plus_id_left :: Property
+-- prop_ec_plus_id_left =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     a' <- testEC k
+--     let a, z :: CurvePt Rational s
+--         a = liftEC a'
+--         z = liftEC inf
+--         lhs = computeOver k $ a + z
+--         rhs = computeOver k a
+--     lhs === rhs
+
+-- prop_ec_plus_id_right :: Property
+-- prop_ec_plus_id_right =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     a' <- testEC k
+--     let a, z :: CurvePt Rational s
+--         a = liftEC a'
+--         z = liftEC inf
+--         lhs = computeOver k $ z + a
+--         rhs = computeOver k a
+--     lhs === rhs
+
+-- prop_ec_plus_inverses :: Property
+-- prop_ec_plus_inverses =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     p <- testEC k
+--     let a, z :: CurvePt Rational s
+--         a = liftEC p
+--         z = liftEC inf
+--         lhs = computeOver k $ a + (negate a)
+--         rhs = computeOver k z
+--     lhs === rhs
+
+-- prop_ec_plus_sym :: Property
+-- prop_ec_plus_sym =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     a' <- testEC k
+--     b' <- testEC k
+--     let a, b :: CurvePt Rational s
+--         a = liftEC a'
+--         b = liftEC b'
+--         lhs = computeOver k $ a + b
+--         rhs = computeOver k $ b + a
+--     lhs === rhs
+
+-- prop_ec_plus_regression_1 :: Property
+-- prop_ec_plus_regression_1 =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     a' <- testEC k
+--     b' <- testEC k
+--     let a, b :: CurvePt Rational s
+--         a = liftEC a'
+--         b = liftEC b'
+--         lhs = computeOver k $ a + (b - a)
+--         rhs = computeOver k $ (a + b) - a
+--     lhs === rhs
+
+-- prop_ec_plus_assoc :: Property
+-- prop_ec_plus_assoc =
+--   ellipticCurveProperty $ do
+--     k <- testCurve
+--     a' <- testEC k
+--     b' <- testEC k
+--     c' <- testEC k
+--     let a, b, c :: CurvePt Rational s
+--         a = liftEC a'
+--         b = liftEC b'
+--         c = liftEC c'
+--         lhs = computeOver k $ a + (b + c)
+--         rhs = computeOver k $ (a + b) + c
+--     lhs === rhs
+
+-- tests :: IO ()
+-- tests = do
+--   putText "\n -> Projective spaces\n"
+
+--   checkParallel' $
+--     Group
+--       "Real projective space : order 2 : equality"
+--       [ ("[x : y] == [ x :  y]", prop_rp1_eq_refl)
+--       , ("[x : y] == [ax : ay]", prop_rp1_eq_1)
+--       , ("[a : 0] == [ b :  0]", prop_rp1_eq_2)
+--       , ("[0 : a] == [ 0 :  b]", prop_rp1_eq_3)
+--       , ("[a : b] /= [ c :  0]", prop_rp1_eq_4)
+--       ]
+--   checkParallel' $
+--     Group
+--       "Real projective space : order 3 : equality"
+--       [ ("[x : y : 0] == [ax : ay :  0]", prop_rp2_eq_1)
+--       , ("[0 : y : z] == [ 0 : ay : az]", prop_rp2_eq_2)
+--       , ("[x : 0 : z] == [ax :  0 : az]", prop_rp2_eq_3)
+--       ]
+
+--   putText "\n -> Elliptic curves\n"
+
+--   checkParallel' $
+--     Group
+--       "Elliptic curves : group law : axioms"
+--       [ ("P + 0 = P", prop_ec_plus_id_right)
+--       , ("0 + P = P", prop_ec_plus_id_left)
+--       , ("P + (-P)    =  0         ", prop_ec_plus_inverses)
+--       , ("P +  Q      =  Q + P     ", prop_ec_plus_sym)
+--       , ("P + (Q + R) = (P + Q) + R", prop_ec_plus_assoc)
+--       ]
+--   checkParallel' $
+--     Group
+--       "Elliptic curves : group law : regression tests"
+--       [("(P + Q) - P = P + (Q - P)", prop_ec_plus_regression_1)]
+
+--   where
+--     checkParallel' = void . checkParallel
+
+-- -- Tasty makes it easy to test your code. It is a test framework that can
+-- -- combine many different types of tests into one suite. See its website for
+-- -- help: <http://documentup.com/feuerbach/tasty>.
+-- import qualified Test.Tasty
+-- -- Hspec is one of the providers for Tasty. It provides a nice syntax for
+-- -- writing tests. Its website has more info: <https://hspec.github.io>.
+-- import Test.Tasty.Hspec
+
+-- main :: IO ()
+-- main = do
+--     test <- testSpec "noether" spec
+--     Test.Tasty.defaultMain test
+
+-- spec :: Spec
+-- spec = parallel $ do
+--     it "is trivially true" $ do
+--         True `shouldBe` True
diff --git a/test-suite/Noether/Test/Algebra.hs b/test-suite/Noether/Test/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/test-suite/Noether/Test/Algebra.hs
@@ -0,0 +1,184 @@
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+module Noether.Test.Algebra where
+
+import           Hedgehog                   hiding (Group)
+import qualified Hedgehog.Gen               as Gen
+import           Hedgehog.Internal.Property hiding (Group)
+import qualified Hedgehog.Internal.Property as Prop
+import           Hedgehog.Internal.Show
+import           Hedgehog.Internal.Source
+import qualified Hedgehog.Range             as Range
+
+import           GHC.Stack
+import qualified Prelude                    as P
+
+import           Noether.Algebra.Single
+import           Noether.Algebra.Tags
+import           Noether.Lemmata.Prelude
+import           Noether.Lemmata.TypeFu
+
+genDouble
+  :: Monad m
+  => Test m Double
+genDouble = forAll $ Gen.realFloat $ Range.linearFrac (-100) 100
+
+almostEqual
+  :: (Ord a, Fractional a)
+  => a -> a -> Bool
+almostEqual a b = abs (a P.- b) < 0.05
+
+(=~=)
+  :: (Monad m, HasCallStack, Ord a, Fractional a, Show a)
+  => a -> a -> Test m ()
+(=~=) x y =
+  if (x `almostEqual` y)
+    then success
+    else withFrozenCallStack <$>
+         maybe
+           (failWith
+              Nothing
+              (unlines ["━━━ Not Equal ━━━", showPretty x, showPretty y]))
+           (\diff ->
+              failWith
+                (Just (Diff "Failed (" "- lhs" "=/=" "+ rhs" ")" diff))
+                "")
+           (valueDiff <$> mkValue x <*> mkValue y)
+
+-- | Create a property for an 'Integral' type.
+mkProp_integral
+  :: forall a t.
+     (Integral a, Show a)
+  => t -> (a -> a -> a) -> (a -> a -> a) -> (t, Property)
+mkProp_integral name preludeOp noetherOp =
+  namedProperty
+    name
+    (do let r = forAll (Gen.integral (Range.linear (-100) 100))
+        a <- r
+        b <- r
+        (a `preludeOp` b) === (a `noetherOp` b))
+
+prop_prelude_add_int = mkProp_integral @Int "(+) : Int" (P.+) (+)
+prop_prelude_mul_int = mkProp_integral @Int "(*) : Int" (P.*) (*)
+prop_prelude_sub_int = mkProp_integral @Int "(-) : Int" (P.-) (-)
+
+prop_prelude_add_integer = mkProp_integral @Integer "(+) : Integer" (P.+) (+)
+prop_prelude_mul_integer = mkProp_integral @Integer "(*) : Integer" (P.*) (*)
+prop_prelude_sub_integer = mkProp_integral @Integer "(-) : Integer" (P.-) (-)
+
+-- | Create a property for a 'RealFloat' type.
+mkProp_realFloat
+  :: (RealFloat a, Ord a, Show a)
+  => t
+  -> (a -> a -> a)
+  -> (a -> a -> a)
+  -> (t, Property)
+mkProp_realFloat name preludeOp noetherOp =
+  namedProperty
+    name
+    (do let r = forAll (Gen.realFloat (Range.linearFrac (-100) 100))
+        a <- r
+        b <- r
+        (a `preludeOp` b) =~= (a `noetherOp` b))
+
+prop_prelude_add_float = mkProp_realFloat @Float "(+) : Float" (P.+) (+)
+prop_prelude_mul_float = mkProp_realFloat @Float "(*) : Float" (P.*) (*)
+prop_prelude_sub_float = mkProp_realFloat @Float "(-) : Float" (P.-) (-)
+prop_prelude_div_float = mkProp_realFloat @Float "(/) : Float" (P./) (/)
+
+prop_prelude_add_double = mkProp_realFloat @Double "(+) : Double" (P.+) (+)
+prop_prelude_mul_double = mkProp_realFloat @Double "(*) : Double" (P.*) (*)
+prop_prelude_sub_double = mkProp_realFloat @Double "(-) : Double" (P.-) (-)
+prop_prelude_div_double = mkProp_realFloat @Double "(/) : Double" (P./) (/)
+
+namedProperty name prop = (name, property prop)
+
+-- | Create a property for a 'Ratio' type.
+mkProp_rational
+  :: forall a t.
+  (Ord a, Show a, Integral a)
+  => t
+  -> (Ratio a -> Ratio a -> Ratio a)
+  -> (Ratio a -> Ratio a -> Ratio a)
+  -> (t, Property)
+mkProp_rational name preludeOp noetherOp =
+  namedProperty
+    name
+    (do let
+          num = Gen.filter (/=0) (Gen.integral (Range.linear (-10) 10))
+          den = Gen.filter (/=0) (Gen.integral (Range.linear (-10) 10))
+          r = forAll ((%) <$> num <*> den)
+        a <- r
+        b <- r
+        (a `preludeOp` b) =~= (a `noetherOp` b))
+
+prop_prelude_add_rational_integer = mkProp_rational @Integer "(+) : Ratio Integer" (P.+) (+)
+prop_prelude_mul_rational_integer = mkProp_rational @Integer "(*) : Ratio Integer" (P.*) (*)
+prop_prelude_sub_rational_integer = mkProp_rational @Integer "(-) : Ratio Integer" (P.-) (-)
+prop_prelude_div_rational_integer = mkProp_rational @Integer "(/) : Ratio Integer" (P./) (/)
+
+prop_prelude_add_rational_int8 = mkProp_rational @Int8 "(+) : Ratio Int8" (P.+) (+)
+prop_prelude_mul_rational_int8 = mkProp_rational @Int8 "(*) : Ratio Int8" (P.*) (*)
+prop_prelude_sub_rational_int8 = mkProp_rational @Int8 "(-) : Ratio Int8" (P.-) (-)
+prop_prelude_div_rational_int8 = mkProp_rational @Int8 "(/) : Ratio Int8" (P./) (/)
+
+prop_prelude_add_rational_int16 = mkProp_rational @Int16 "(+) : Ratio Int16" (P.+) (+)
+prop_prelude_mul_rational_int16 = mkProp_rational @Int16 "(*) : Ratio Int16" (P.*) (*)
+prop_prelude_sub_rational_int16 = mkProp_rational @Int16 "(-) : Ratio Int16" (P.-) (-)
+prop_prelude_div_rational_int16 = mkProp_rational @Int16 "(/) : Ratio Int16" (P./) (/)
+
+prop_prelude_add_rational_int32 = mkProp_rational @Int32 "(+) : Ratio Int32" (P.+) (+)
+prop_prelude_mul_rational_int32 = mkProp_rational @Int32 "(*) : Ratio Int32" (P.*) (*)
+prop_prelude_sub_rational_int32 = mkProp_rational @Int32 "(-) : Ratio Int32" (P.-) (-)
+prop_prelude_div_rational_int32 = mkProp_rational @Int32 "(/) : Ratio Int32" (P./) (/)
+
+prop_prelude_add_rational_int64 = mkProp_rational @Int64 "(+) : Ratio Int64" (P.+) (+)
+prop_prelude_mul_rational_int64 = mkProp_rational @Int64 "(*) : Ratio Int64" (P.*) (*)
+prop_prelude_sub_rational_int64 = mkProp_rational @Int64 "(-) : Ratio Int64" (P.-) (-)
+prop_prelude_div_rational_int64 = mkProp_rational @Int64 "(/) : Ratio Int64" (P./) (/)
+
+tests :: IO ()
+tests = do
+  checkParallel'
+    "Noether numerics agree with Prelude ops"
+    [ prop_prelude_add_int
+    , prop_prelude_sub_int
+    , prop_prelude_mul_int
+    , prop_prelude_add_integer
+    , prop_prelude_sub_integer
+    , prop_prelude_mul_integer
+    , prop_prelude_add_float
+    , prop_prelude_sub_float
+    , prop_prelude_mul_float
+    , prop_prelude_div_float
+    , prop_prelude_add_double
+    , prop_prelude_sub_double
+    , prop_prelude_mul_double
+    , prop_prelude_div_double
+    , prop_prelude_add_rational_integer
+    , prop_prelude_sub_rational_integer
+    , prop_prelude_mul_rational_integer
+    , prop_prelude_div_rational_integer
+    -- , prop_prelude_add_rational_int8
+    -- , prop_prelude_sub_rational_int8
+    -- , prop_prelude_mul_rational_int8
+    -- , prop_prelude_div_rational_int8
+    -- , prop_prelude_add_rational_int16
+    -- , prop_prelude_sub_rational_int16
+    -- , prop_prelude_mul_rational_int16
+    -- , prop_prelude_div_rational_int16
+    , prop_prelude_add_rational_int32
+    , prop_prelude_sub_rational_int32
+    , prop_prelude_mul_rational_int32
+    , prop_prelude_div_rational_int32
+    , prop_prelude_add_rational_int64
+    , prop_prelude_sub_rational_int64
+    , prop_prelude_mul_rational_int64
+    , prop_prelude_div_rational_int64
+    ]
+  putStrLn "asdf"
+  where
+    checkParallel' name tests = checkParallel (Prop.Group name tests)