diff --git a/bowtie.cabal b/bowtie.cabal
--- a/bowtie.cabal
+++ b/bowtie.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           bowtie
-version:        0.3.1
+version:        0.4.0
 synopsis:       Tying knots in polynomial functors
 description:    Please see the README on GitHub at <https://github.com/ejconlon/bowtie#readme>
 homepage:       https://github.com/ejconlon/bowtie#readme
@@ -16,7 +16,7 @@
 license:        BSD3
 build-type:     Simple
 tested-with:
-    GHC == 9.6.3
+    GHC == 9.6.4
 extra-source-files:
     README.md
 
@@ -27,7 +27,15 @@
 library
   exposed-modules:
       Bowtie
+      Bowtie.Anno
+      Bowtie.Attr
+      Bowtie.Fix
+      Bowtie.Foldable
+      Bowtie.Jot
+      Bowtie.Knot
+      Bowtie.Memo
       Bowtie.Rewrite
+      Bowtie.SMap
   other-modules:
       Paths_bowtie
   hs-source-dirs:
@@ -63,9 +71,12 @@
       base >=4.12 && <5
     , bifunctors ==5.6.*
     , comonad ==5.0.*
+    , dependent-map ==0.4.*
     , mtl ==2.3.*
     , nonempty-containers ==0.3.*
+    , optics ==0.4.*
     , prettyprinter ==1.7.*
     , recursion-schemes ==5.2.*
     , semigroupoids ==6.0.*
+    , some ==1.0.*
   default-language: GHC2021
diff --git a/src/Bowtie.hs b/src/Bowtie.hs
--- a/src/Bowtie.hs
+++ b/src/Bowtie.hs
@@ -1,473 +1,23 @@
-{-# LANGUAGE PatternSynonyms #-}
-{-# LANGUAGE UndecidableInstances #-}
-
 -- | Some useful fixpoints of Functors and Bifunctors.
 module Bowtie
-  ( Base1
-  , Recursive1 (..)
-  , Corecursive1 (..)
-  , cata1
-  , cata1M
-  , fmapViaBi
-  , foldrViaBi
-  , traverseViaBi
-  , Fix (..)
-  , mkFix
-  , unMkFix
-  , transFix
-  , Knot (..)
-  , mkKnot
-  , unMkKnot
-  , transKnot
-  , Anno (..)
-  , annoUnit
-  , annoUnitM
-  , annoCounit
-  , annoCounitM
-  , annoLeft
-  , annoLeftM
-  , annoRight
-  , annoRightM
-  , MemoF (..)
-  , pattern MemoFP
-  , memoFKey
-  , memoFVal
-  , Memo (..)
-  , pattern MemoP
-  , mkMemo
-  , unMkMemo
-  , transMemo
-  , memoKey
-  , memoVal
-  , memoCata
-  , memoCataM
-  , memoRight
-  , memoRightM
-  , memoExtend
-  , JotF (..)
-  , pattern JotFP
-  , jotFKey
-  , jotFVal
-  , Jot (..)
-  , pattern JotP
-  , mkJot
-  , unMkJot
-  , annoJot
-  , transJot
-  , jotKey
-  , jotVal
-  , jotCata
-  , jotCataM
-  , jotRight
-  , jotRightM
-  , jotExtend
+  ( module Bowtie.Anno
+  , module Bowtie.Attr
+  , module Bowtie.Fix
+  , module Bowtie.Foldable
+  , module Bowtie.Jot
+  , module Bowtie.Knot
+  , module Bowtie.Memo
+  , module Bowtie.Rewrite
+  , module Bowtie.SMap
   )
 where
 
-import Control.Comonad (Comonad (..))
-import Control.Exception (Exception)
-import Control.Monad ((>=>))
-import Control.Monad.Reader (Reader, ReaderT (..), runReader)
-import Data.Bifoldable (Bifoldable (..))
-import Data.Bifunctor (Bifunctor (..))
-import Data.Bitraversable (Bitraversable (..))
-import Data.Functor.Apply (Apply (..))
-import Data.Functor.Foldable (Base, Corecursive (..), Recursive (..))
-import Data.Functor.Identity (Identity (..))
-import Data.Kind (Type)
-import Data.String (IsString (..))
-import Data.Typeable (Typeable)
-import Prettyprinter (Pretty (..))
-
--- | 'Base' for Bifunctors
-type family Base1 (f :: Type -> Type) :: Type -> Type -> Type
-
--- | 'Recursive' for Bifunctors
-class (Bifunctor (Base1 f), Functor f) => Recursive1 f where
-  project1 :: f a -> Base1 f a (f a)
-
--- | 'Corecursive' for Bifunctors
-class (Bifunctor (Base1 f), Functor f) => Corecursive1 f where
-  embed1 :: Base1 f a (f a) -> f a
-
--- | 'cata' for Bifunctors
-cata1 :: (Recursive1 f, Base1 f ~ g) => (g a b -> b) -> f a -> b
-cata1 f = go where go = f . second go . project1
-
--- | 'cataM' for Bifunctors
-cata1M :: (Monad m, Recursive1 f, Base1 f ~ g, Bitraversable g) => (g a b -> m b) -> f a -> m b
-cata1M f = go where go = bitraverse pure go . project1 >=> f
-
--- | A useful default 'fmap'
-fmapViaBi :: (Recursive1 f, Corecursive1 f, Base1 f ~ g) => (a -> b) -> f a -> f b
-fmapViaBi f = go where go = embed1 . bimap f go . project1
-
--- | A useful default 'foldr'
-foldrViaBi :: (Recursive1 f, Base1 f ~ g, Bifoldable g) => (a -> b -> b) -> b -> f a -> b
-foldrViaBi f = flip go where go fa b = bifoldr f go b (project1 fa)
-
--- | A useful default 'traverse'
-traverseViaBi
-  :: (Recursive1 f, Corecursive1 f, Base1 f ~ g, Bitraversable g, Applicative m) => (a -> m b) -> f a -> m (f b)
-traverseViaBi f = go where go = fmap embed1 . bitraverse f go . project1
-
--- | A basic Functor fixpoint like you'd see anywhere.
-type Fix :: (Type -> Type) -> Type
-newtype Fix f = Fix {unFix :: f (Fix f)}
-
-deriving newtype instance (Eq (f (Fix f))) => Eq (Fix f)
-
-deriving newtype instance (Ord (f (Fix f))) => Ord (Fix f)
-
-deriving stock instance (Show (f (Fix f))) => Show (Fix f)
-
-deriving newtype instance (Pretty (f (Fix f))) => Pretty (Fix f)
-
-deriving newtype instance (IsString (f (Fix f))) => IsString (Fix f)
-
-type instance Base (Fix f) = f
-
-instance (Functor f) => Recursive (Fix f) where project = unFix
-
-instance (Functor f) => Corecursive (Fix f) where embed = Fix
-
--- | Pull a recursive structure apart and retie as a 'Fix'.
-mkFix :: (Recursive t, Base t ~ f) => t -> Fix f
-mkFix = cata Fix
-
--- | Go the other way.
-unMkFix :: (Corecursive t, Base t ~ f) => Fix f -> t
-unMkFix = cata embed
-
--- | Transform the base Functor.
-transFix :: (Functor f) => (forall x. f x -> g x) -> Fix f -> Fix g
-transFix nat = go
- where
-  go = Fix . nat . fmap go . unFix
-
--- | A fixpoint for a Bifunctor where the second type variable contains
--- the recursive structure.
-type Knot :: (Type -> Type -> Type) -> Type -> Type
-newtype Knot g a = Knot {unKnot :: g a (Knot g a)}
-
-deriving newtype instance (Eq (g a (Knot g a))) => Eq (Knot g a)
-
-deriving newtype instance (Ord (g a (Knot g a))) => Ord (Knot g a)
-
-deriving stock instance (Show (g a (Knot g a))) => Show (Knot g a)
-
-deriving newtype instance (Pretty (g a (Knot g a))) => Pretty (Knot g a)
-
-deriving newtype instance (IsString (g a (Knot g a))) => IsString (Knot g a)
-
-type instance Base1 (Knot g) = g
-
-instance (Bifunctor g) => Recursive1 (Knot g) where project1 = unKnot
-
-instance (Bifunctor g) => Corecursive1 (Knot g) where embed1 = Knot
-
-instance (Bifunctor g) => Functor (Knot g) where fmap = fmapViaBi
-
-instance (Bifunctor g, Bifoldable g) => Foldable (Knot g) where foldr = foldrViaBi
-
-instance (Bitraversable g) => Traversable (Knot g) where traverse = traverseViaBi
-
--- | Pull a recursive structure apart and retie as a 'Knot'.
-mkKnot :: (Recursive1 f, Base1 f ~ g) => f a -> Knot g a
-mkKnot = cata1 Knot
-
--- | Go the other way.
-unMkKnot :: (Corecursive1 f, Base1 f ~ g) => Knot g a -> f a
-unMkKnot = cata1 embed1
-
--- | Transform the base Bifunctor.
-transKnot :: (Bifunctor g) => (forall x y. g x y -> h x y) -> Knot g a -> Knot h a
-transKnot nat = go
- where
-  go = Knot . nat . second go . unKnot
-
--- | An "annotation" with associated value.
-type Anno :: Type -> Type -> Type
-data Anno k v = Anno {annoKey :: !k, annoVal :: !v}
-  deriving stock (Eq, Ord, Show, Functor, Foldable, Traversable)
-
-instance Bifunctor Anno where
-  bimap f g (Anno k v) = Anno (f k) (g v)
-
-instance Bifoldable Anno where
-  bifoldr f g z (Anno k v) = f k (g v z)
-
-instance Bitraversable Anno where
-  bitraverse f g (Anno k v) = liftA2 Anno (f k) (g v)
-
-instance (Semigroup k) => Apply (Anno k) where
-  liftF2 f (Anno k1 v1) (Anno k2 v2) = Anno (k1 <> k2) (f v1 v2)
-
-instance (Monoid k) => Applicative (Anno k) where
-  pure = Anno mempty
-  liftA2 = liftF2
-
-instance Comonad (Anno k) where
-  extract (Anno _ v) = v
-  duplicate an@(Anno k _) = Anno k an
-  extend f an@(Anno k _) = Anno k (f an)
-
-instance (Pretty v) => Pretty (Anno k v) where
-  pretty = pretty . annoVal
-
-instance (Monoid k, IsString v) => IsString (Anno k v) where
-  fromString = Anno mempty . fromString
-
-instance (Show k, Typeable k, Exception v) => Exception (Anno k v)
-
--- | 'unit' from 'Adjunction'
-annoUnit :: v -> Reader k (Anno k v)
-annoUnit v = ReaderT (Identity . (`Anno` v))
-
-annoUnitM :: (Applicative m) => v -> ReaderT k m (Anno k v)
-annoUnitM v = ReaderT (pure . (`Anno` v))
-
--- | 'counit' from 'Adjunction'
-annoCounit :: Anno k (Reader k v) -> v
-annoCounit (Anno k m) = runReader m k
-
-annoCounitM :: Anno k (ReaderT k m v) -> m v
-annoCounitM (Anno k m) = runReaderT m k
-
--- | 'leftAdjunct' from 'Adjunction'
-annoLeft :: (Anno k v -> x) -> v -> Reader k x
-annoLeft f v = ReaderT (Identity . f . (`Anno` v))
-
-annoLeftM :: (Anno k v -> m x) -> v -> ReaderT k m x
-annoLeftM f v = ReaderT (f . (`Anno` v))
-
--- | 'rightAdjunct' from 'Adjunction'
-annoRight :: (v -> Reader k x) -> Anno k v -> x
-annoRight f (Anno k v) = runReader (f v) k
-
-annoRightM :: (v -> ReaderT k m x) -> Anno k v -> m x
-annoRightM f (Anno k v) = runReaderT (f v) k
-
--- | The base functor for a 'Memo'
-newtype MemoF f k r = MemoF {unMemoF :: Anno k (f r)}
-  deriving stock (Show, Functor)
-  deriving newtype (Eq, Ord)
-
-pattern MemoFP :: k -> f r -> MemoF f k r
-pattern MemoFP k v = MemoF (Anno k v)
-
-{-# COMPLETE MemoFP #-}
-
-deriving newtype instance (Monoid k, IsString (f r)) => IsString (MemoF f k r)
-
-deriving newtype instance (Pretty (f r)) => Pretty (MemoF f k r)
-
-instance (Apply f, Semigroup k) => Apply (MemoF f k) where
-  liftF2 f (MemoF (Anno k1 v1)) (MemoF (Anno k2 v2)) = MemoF (Anno (k1 <> k2) (liftF2 f v1 v2))
-
-instance (Applicative f, Monoid k) => Applicative (MemoF f k) where
-  pure = MemoF . Anno mempty . pure
-  liftA2 f (MemoF (Anno k1 v1)) (MemoF (Anno k2 v2)) = MemoF (Anno (k1 <> k2) (liftA2 f v1 v2))
-
-memoFKey :: MemoF f k r -> k
-memoFKey (MemoFP k _) = k
-
-memoFVal :: MemoF f k r -> f r
-memoFVal (MemoFP _ v) = v
-
--- | An annotated 'Fix'
-type Memo :: (Type -> Type) -> Type -> Type
-newtype Memo f k = Memo {unMemo :: MemoF f k (Memo f k)}
-
-pattern MemoP :: k -> f (Memo f k) -> Memo f k
-pattern MemoP k v = Memo (MemoF (Anno k v))
-
-{-# COMPLETE MemoP #-}
-
-deriving newtype instance (Eq k, Eq (f (Memo f k))) => Eq (Memo f k)
-
-deriving newtype instance (Ord k, Ord (f (Memo f k))) => Ord (Memo f k)
-
-deriving stock instance (Show k, Show (f (Memo f k))) => Show (Memo f k)
-
-deriving newtype instance (Monoid k, IsString (f (Memo f k))) => IsString (Memo f k)
-
-deriving newtype instance (Pretty (f (Memo f k))) => Pretty (Memo f k)
-
-instance (Functor f) => Functor (Memo f) where
-  fmap f = go where go (MemoP k v) = MemoP (f k) (fmap go v)
-
-instance (Foldable f) => Foldable (Memo f) where
-  foldr f = flip go where go (MemoP k v) z = foldr go (f k z) v
-
-instance (Traversable f) => Traversable (Memo f) where
-  traverse f = go where go (MemoP k v) = liftA2 MemoP (f k) (traverse go v)
-
-type instance Base (Memo f k) = MemoF f k
-
-instance (Functor f) => Recursive (Memo f k) where project = unMemo
-
-instance (Functor f) => Corecursive (Memo f k) where embed = Memo
-
--- | Pull a recursive structure apart and retie as a 'Memo', using the given
--- function to calculate a key for every level.
-mkMemo :: (Recursive t, Base t ~ f) => (f k -> k) -> t -> Memo f k
-mkMemo f = cata (\v -> MemoP (f (fmap memoKey v)) v)
-
--- | Forget keys at every level and convert back to a plain structure.
-unMkMemo :: (Corecursive t, Base t ~ f) => Memo f k -> t
-unMkMemo (MemoP _ v) = embed (fmap unMkMemo v)
-
--- | Transform the base functor.
-transMemo :: (Functor f) => (forall x. f x -> g x) -> Memo f k -> Memo g k
-transMemo nat = go
- where
-  go (MemoP k v) = MemoP k (nat (fmap go v))
-
-memoKey :: Memo f k -> k
-memoKey (MemoP k _) = k
-
-memoVal :: Memo f k -> f (Memo f k)
-memoVal (MemoP _ v) = v
-
--- | 'cata' but nicer
-memoCata :: (Functor f) => (f x -> Reader k x) -> Memo f k -> x
-memoCata f = go
- where
-  go (MemoP k v) = runReader (f (fmap go v)) k
-
--- | 'cataM' but nicer
-memoCataM :: (Monad m, Traversable f) => (f x -> ReaderT k m x) -> Memo f k -> m x
-memoCataM f = go
- where
-  go (MemoP k v) = traverse go v >>= \x -> runReaderT (f x) k
-
--- | Peek at the top value like 'annoRight'
-memoRight :: (f (Memo f k) -> Reader k x) -> Memo f k -> x
-memoRight f = annoRight f . unMemoF . unMemo
-
--- | Peek at the top value like 'annoRightM'
-memoRightM :: (f (Memo f k) -> ReaderT k m x) -> Memo f k -> m x
-memoRightM f = annoRightM f . unMemoF . unMemo
-
--- | Re-annotate top-down
-memoExtend :: (Functor f) => (Memo f k -> x) -> Memo f k -> Memo f x
-memoExtend w = go where go m@(MemoP _ v) = MemoP (w m) (fmap go v)
-
--- | The base functor for a 'Jot'
-newtype JotF g k a r = JotF {unJotF :: Anno k (g a r)}
-  deriving stock (Show, Functor)
-  deriving newtype (Eq, Ord)
-
-pattern JotFP :: k -> g a r -> JotF g k a r
-pattern JotFP k v = JotF (Anno k v)
-
-{-# COMPLETE JotFP #-}
-
-deriving newtype instance (Monoid k, IsString (g a r)) => IsString (JotF g k a r)
-
-deriving newtype instance (Pretty (g a r)) => Pretty (JotF g k a r)
-
-instance (Bifunctor g) => Bifunctor (JotF g k) where
-  bimap f g = go where go = JotF . fmap (bimap f g) . unJotF
-
-instance (Bifoldable g) => Bifoldable (JotF g k) where
-  bifoldr f g = go where go z = bifoldr f g z . annoVal . unJotF
-
-instance (Bitraversable g) => Bitraversable (JotF g k) where
-  bitraverse f g = go where go = fmap JotF . traverse (bitraverse f g) . unJotF
-
-jotFKey :: JotF g k a r -> k
-jotFKey (JotFP k _) = k
-
-jotFVal :: JotF g k a r -> g a r
-jotFVal (JotFP _ v) = v
-
--- | An annotated 'Knot'
-type Jot :: (Type -> Type -> Type) -> Type -> Type -> Type
-newtype Jot g k a = Jot {unJot :: JotF g k a (Jot g k a)}
-
-pattern JotP :: k -> g a (Jot g k a) -> Jot g k a
-pattern JotP k v = Jot (JotF (Anno k v))
-
-{-# COMPLETE JotP #-}
-
-deriving newtype instance (Eq k, Eq (g a (Jot g k a))) => Eq (Jot g k a)
-
-deriving newtype instance (Ord k, Ord (g a (Jot g k a))) => Ord (Jot g k a)
-
-deriving stock instance (Show k, Show (g a (Jot g k a))) => Show (Jot g k a)
-
-deriving newtype instance (Monoid k, IsString (g a (Jot g k a))) => IsString (Jot g k a)
-
-deriving newtype instance (Pretty (g a (Jot g k a))) => Pretty (Jot g k a)
-
-type instance Base1 (Jot g k) = JotF g k
-
-instance (Bifunctor g) => Recursive1 (Jot g k) where project1 = unJot
-
-instance (Bifunctor g) => Corecursive1 (Jot g k) where embed1 = Jot
-
-instance (Bifunctor g) => Functor (Jot g k) where fmap = fmapViaBi
-
-instance (Bifunctor g, Bifoldable g) => Foldable (Jot g k) where foldr = foldrViaBi
-
-instance (Bitraversable g) => Traversable (Jot g k) where traverse = traverseViaBi
-
-instance (Bifunctor g) => Bifunctor (Jot g) where
-  bimap f g = go where go (JotP k v) = JotP (f k) (bimap g go v)
-
-instance (Bifoldable g) => Bifoldable (Jot g) where
-  bifoldr f g = flip go where go (JotP k v) z = f k (bifoldr g go z v)
-
-instance (Bitraversable g) => Bitraversable (Jot g) where
-  bitraverse f g = go where go (JotP k v) = liftA2 JotP (f k) (bitraverse g go v)
-
--- | Pull a recursive structure apart and retie as a 'Jot', using the given
--- function to calculate a key for every level.
-mkJot :: (Recursive1 t, Base1 t ~ g) => (g a k -> k) -> t a -> Jot g k a
-mkJot f = cata1 (\v -> JotP (f (fmap jotKey v)) v)
-
--- | Forget keys at every level and convert back to a plain structure.
-unMkJot :: (Corecursive1 t, Base1 t ~ g) => Jot g k a -> t a
-unMkJot (JotP _ v) = embed1 (fmap unMkJot v)
-
--- | Quick conversion from annotated functor.
-annoJot :: Anno b (g a (Jot g b a)) -> Jot g b a
-annoJot = Jot . JotF
-
--- | Transform the base functor.
-transJot :: (Bifunctor g) => (forall x. g a x -> h a x) -> Jot g k a -> Jot h k a
-transJot nat = go
- where
-  go (JotP k v) = JotP k (nat (second go v))
-
-jotKey :: Jot g k a -> k
-jotKey (JotP k _) = k
-
-jotVal :: Jot g k a -> g a (Jot g k a)
-jotVal (JotP _ v) = v
-
--- | 'cata' but nicer
-jotCata :: (Bifunctor g) => (g a x -> Reader k x) -> Jot g k a -> x
-jotCata f = go
- where
-  go (JotP k v) = runReader (f (fmap go v)) k
-
--- | 'cataM' but nicer
-jotCataM :: (Bifunctor g) => (g a (m x) -> ReaderT k m x) -> Jot g k a -> m x
-jotCataM f = go
- where
-  go (JotP k v) = runReaderT (f (fmap go v)) k
-
--- | Peek at the top value like 'annoRight'
-jotRight :: (g a (Jot g k a) -> Reader k x) -> Jot g k a -> x
-jotRight f = annoRight f . unJotF . unJot
-
--- | Peek at the top value like 'annoRightM'
-jotRightM :: (g a (Jot g k a) -> ReaderT k m x) -> Jot g k a -> m x
-jotRightM f = annoRightM f . unJotF . unJot
-
--- | Re-annotate top-down
-jotExtend :: (Bifunctor g) => (Jot g k a -> x) -> Jot g k a -> Jot g x a
-jotExtend w = go where go j@(JotP _ v) = JotP (w j) (fmap go v)
+import Bowtie.Anno
+import Bowtie.Attr
+import Bowtie.Fix
+import Bowtie.Foldable
+import Bowtie.Jot
+import Bowtie.Knot
+import Bowtie.Memo
+import Bowtie.Rewrite
+import Bowtie.SMap
diff --git a/src/Bowtie/Anno.hs b/src/Bowtie/Anno.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Anno.hs
@@ -0,0 +1,87 @@
+module Bowtie.Anno
+  ( Anno (..)
+  , annoUnit
+  , annoUnitM
+  , annoCounit
+  , annoCounitM
+  , annoLeft
+  , annoLeftM
+  , annoRight
+  , annoRightM
+  )
+where
+
+import Control.Comonad (Comonad (..))
+import Control.Exception (Exception)
+import Control.Monad.Reader (Reader, ReaderT (..), runReader)
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Functor.Apply (Apply (..))
+import Data.Functor.Identity (Identity (..))
+import Data.Kind (Type)
+import Data.String (IsString (..))
+import Data.Typeable (Typeable)
+import Prettyprinter (Pretty (..))
+
+-- | An "annotation" with associated value.
+type Anno :: Type -> Type -> Type
+data Anno k v = Anno {annoKey :: !k, annoVal :: !v}
+  deriving stock (Eq, Ord, Show, Functor, Foldable, Traversable)
+
+instance Bifunctor Anno where
+  bimap f g (Anno k v) = Anno (f k) (g v)
+
+instance Bifoldable Anno where
+  bifoldr f g z (Anno k v) = f k (g v z)
+
+instance Bitraversable Anno where
+  bitraverse f g (Anno k v) = liftA2 Anno (f k) (g v)
+
+instance (Semigroup k) => Apply (Anno k) where
+  liftF2 f (Anno k1 v1) (Anno k2 v2) = Anno (k1 <> k2) (f v1 v2)
+
+instance (Monoid k) => Applicative (Anno k) where
+  pure = Anno mempty
+  liftA2 = liftF2
+
+instance Comonad (Anno k) where
+  extract (Anno _ v) = v
+  duplicate an@(Anno k _) = Anno k an
+  extend f an@(Anno k _) = Anno k (f an)
+
+instance (Pretty v) => Pretty (Anno k v) where
+  pretty = pretty . annoVal
+
+instance (Monoid k, IsString v) => IsString (Anno k v) where
+  fromString = Anno mempty . fromString
+
+instance (Show k, Typeable k, Exception v) => Exception (Anno k v)
+
+-- | 'unit' from 'Adjunction'
+annoUnit :: v -> Reader k (Anno k v)
+annoUnit v = ReaderT (Identity . (`Anno` v))
+
+annoUnitM :: (Applicative m) => v -> ReaderT k m (Anno k v)
+annoUnitM v = ReaderT (pure . (`Anno` v))
+
+-- | 'counit' from 'Adjunction'
+annoCounit :: Anno k (Reader k v) -> v
+annoCounit (Anno k m) = runReader m k
+
+annoCounitM :: Anno k (ReaderT k m v) -> m v
+annoCounitM (Anno k m) = runReaderT m k
+
+-- | 'leftAdjunct' from 'Adjunction'
+annoLeft :: (Anno k v -> x) -> v -> Reader k x
+annoLeft f v = ReaderT (Identity . f . (`Anno` v))
+
+annoLeftM :: (Anno k v -> m x) -> v -> ReaderT k m x
+annoLeftM f v = ReaderT (f . (`Anno` v))
+
+-- | 'rightAdjunct' from 'Adjunction'
+annoRight :: (v -> Reader k x) -> Anno k v -> x
+annoRight f (Anno k v) = runReader (f v) k
+
+annoRightM :: (v -> ReaderT k m x) -> Anno k v -> m x
+annoRightM f (Anno k v) = runReaderT (f v) k
diff --git a/src/Bowtie/Attr.hs b/src/Bowtie/Attr.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Attr.hs
@@ -0,0 +1,78 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Bowtie.Attr
+  ( HasAttr (..)
+  , attrLens
+  , WithAttr (..)
+  , attrSetter
+  , memoWithAttr
+  , memoWithAttrM
+  , memoWithoutAttr
+  )
+where
+
+import Bowtie.Anno (Anno (..))
+import Bowtie.Memo (Memo (..), MemoF, memoFKey, reMkMemo, reMkMemoM, pattern MemoFP, pattern MemoP)
+import Bowtie.SMap (Deleted, Inserted, Member, SMap, Val, deleteSMap, indexSMap, insertSMap, updateSMap)
+import Data.Kind (Type)
+import Data.Proxy (Proxy)
+import GHC.TypeLits (KnownSymbol, Symbol)
+import Optics (Lens', Setter, lens, sets)
+
+class HasAttr (d :: Type) (s :: Symbol) (k :: Type) where
+  viewAttr :: Proxy d -> Proxy s -> k -> Val d s
+  setAttr :: Proxy d -> Proxy s -> Val d s -> k -> k
+
+instance (KnownSymbol s, Member s xs) => HasAttr d s (SMap d xs) where
+  viewAttr _ = indexSMap
+  setAttr _ = updateSMap
+
+instance (HasAttr d s k) => HasAttr d s (Anno k x) where
+  viewAttr pd ps (Anno k _) = viewAttr pd ps k
+  setAttr pd ps v (Anno k x) = Anno (setAttr pd ps v k) x
+
+instance (HasAttr d s k) => HasAttr d s (MemoF f k x) where
+  viewAttr pd ps (MemoFP k _) = viewAttr pd ps k
+  setAttr pd ps v (MemoFP k x) = MemoFP (setAttr pd ps v k) x
+
+instance (HasAttr d s k) => HasAttr d s (Memo f k) where
+  viewAttr pd ps (MemoP k _) = viewAttr pd ps k
+  setAttr pd ps v (MemoP k x) = MemoP (setAttr pd ps v k) x
+
+attrLens :: (HasAttr d s k) => Proxy d -> Proxy s -> Lens' k (Val d s)
+attrLens pd ps = lens (viewAttr pd ps) (flip (setAttr pd ps))
+
+class (HasAttr d s k) => WithAttr (d :: Type) (s :: Symbol) (k :: Type) (j :: Type) | d s k -> j, d s j -> k where
+  withAttr :: Proxy d -> Proxy s -> Val d s -> j -> k
+  withoutAttr :: Proxy d -> Proxy s -> k -> j
+
+instance (KnownSymbol s, Inserted s xs zs, Deleted s zs xs) => WithAttr d s (SMap d zs) (SMap d xs) where
+  withAttr _ = insertSMap
+  withoutAttr _ = deleteSMap
+
+instance (WithAttr d s k j) => WithAttr d s (Anno k x) (Anno j x) where
+  withAttr pd ps v (Anno j x) = Anno (withAttr pd ps v j) x
+  withoutAttr pd ps (Anno j x) = Anno (withoutAttr pd ps j) x
+
+instance (WithAttr d s k j) => WithAttr d s (MemoF f k x) (MemoF f j x) where
+  withAttr pd ps v (MemoFP j x) = MemoFP (withAttr pd ps v j) x
+  withoutAttr pd ps (MemoFP j x) = MemoFP (withoutAttr pd ps j) x
+
+attrSetter :: (WithAttr d s k j) => Proxy d -> Proxy s -> Setter j k () (Val d s)
+attrSetter pd ps = sets (\f -> withAttr pd ps (f ()))
+
+memoWithAttr
+  :: (WithAttr d s k j, Functor f) => Proxy d -> Proxy s -> (MemoF f j (Memo f k) -> Val d s) -> Memo f j -> Memo f k
+memoWithAttr pd ps f = reMkMemo (\mfmk -> let v = f mfmk in withAttr pd ps v (memoFKey mfmk))
+
+memoWithAttrM
+  :: (WithAttr d s k j, Traversable f, Monad m)
+  => Proxy d
+  -> Proxy s
+  -> (MemoF f j (Memo f k) -> m (Val d s))
+  -> Memo f j
+  -> m (Memo f k)
+memoWithAttrM pd ps f = reMkMemoM (\mfmk -> fmap (\v -> withAttr pd ps v (memoFKey mfmk)) (f mfmk))
+
+memoWithoutAttr :: (WithAttr d s k j, Functor f) => Proxy d -> Proxy s -> Memo f k -> Memo f j
+memoWithoutAttr pd ps = fmap (withoutAttr pd ps)
diff --git a/src/Bowtie/Fix.hs b/src/Bowtie/Fix.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Fix.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Bowtie.Fix
+  ( Fix (..)
+  , mkFix
+  , unMkFix
+  , transFix
+  )
+where
+
+import Data.Functor.Foldable (Base, Corecursive (..), Recursive (..))
+import Data.Kind (Type)
+import Data.String (IsString (..))
+import Prettyprinter (Pretty (..))
+
+-- | A basic Functor fixpoint like you'd see anywhere.
+type Fix :: (Type -> Type) -> Type
+newtype Fix f = Fix {unFix :: f (Fix f)}
+
+deriving newtype instance (Eq (f (Fix f))) => Eq (Fix f)
+
+deriving newtype instance (Ord (f (Fix f))) => Ord (Fix f)
+
+deriving stock instance (Show (f (Fix f))) => Show (Fix f)
+
+deriving newtype instance (Pretty (f (Fix f))) => Pretty (Fix f)
+
+deriving newtype instance (IsString (f (Fix f))) => IsString (Fix f)
+
+type instance Base (Fix f) = f
+
+instance (Functor f) => Recursive (Fix f) where project = unFix
+
+instance (Functor f) => Corecursive (Fix f) where embed = Fix
+
+-- | Pull a recursive structure apart and retie as a 'Fix'.
+mkFix :: (Recursive t, Base t ~ f) => t -> Fix f
+mkFix = cata Fix
+
+-- | Go the other way.
+unMkFix :: (Corecursive t, Base t ~ f) => Fix f -> t
+unMkFix = cata embed
+
+-- | Transform the base Functor.
+transFix :: (Functor f) => (forall x. f x -> g x) -> Fix f -> Fix g
+transFix nat = go
+ where
+  go = Fix . nat . fmap go . unFix
diff --git a/src/Bowtie/Foldable.hs b/src/Bowtie/Foldable.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Foldable.hs
@@ -0,0 +1,49 @@
+module Bowtie.Foldable
+  ( Base1
+  , Recursive1 (..)
+  , Corecursive1 (..)
+  , cata1
+  , cata1M
+  , fmapViaBi
+  , foldrViaBi
+  , traverseViaBi
+  )
+where
+
+import Control.Monad ((>=>))
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Kind (Type)
+
+-- | 'Base' for Bifunctors
+type family Base1 (f :: Type -> Type) :: Type -> Type -> Type
+
+-- | 'Recursive' for Bifunctors
+class (Bifunctor (Base1 f), Functor f) => Recursive1 f where
+  project1 :: f a -> Base1 f a (f a)
+
+-- | 'Corecursive' for Bifunctors
+class (Bifunctor (Base1 f), Functor f) => Corecursive1 f where
+  embed1 :: Base1 f a (f a) -> f a
+
+-- | 'cata' for Bifunctors
+cata1 :: (Recursive1 f, Base1 f ~ g) => (g a b -> b) -> f a -> b
+cata1 f = go where go = f . second go . project1
+
+-- | 'cataM' for Bifunctors
+cata1M :: (Monad m, Recursive1 f, Base1 f ~ g, Bitraversable g) => (g a b -> m b) -> f a -> m b
+cata1M f = go where go = bitraverse pure go . project1 >=> f
+
+-- | A useful default 'fmap'
+fmapViaBi :: (Recursive1 f, Corecursive1 f, Base1 f ~ g) => (a -> b) -> f a -> f b
+fmapViaBi f = go where go = embed1 . bimap f go . project1
+
+-- | A useful default 'foldr'
+foldrViaBi :: (Recursive1 f, Base1 f ~ g, Bifoldable g) => (a -> b -> b) -> b -> f a -> b
+foldrViaBi f = flip go where go fa b = bifoldr f go b (project1 fa)
+
+-- | A useful default 'traverse'
+traverseViaBi
+  :: (Recursive1 f, Corecursive1 f, Base1 f ~ g, Bitraversable g, Applicative m) => (a -> m b) -> f a -> m (f b)
+traverseViaBi f = go where go = fmap embed1 . bitraverse f go . project1
diff --git a/src/Bowtie/Jot.hs b/src/Bowtie/Jot.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Jot.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Bowtie.Jot
+  ( JotF (..)
+  , pattern JotFP
+  , jotFKey
+  , jotFVal
+  , Jot (..)
+  , pattern JotP
+  , mkJot
+  , unMkJot
+  , annoJot
+  , transJot
+  , jotKey
+  , jotVal
+  , jotCata
+  , jotCataM
+  , jotRight
+  , jotRightM
+  , jotExtend
+  )
+where
+
+import Bowtie.Anno (Anno (..), annoRight, annoRightM)
+import Bowtie.Foldable (Base1, Corecursive1 (..), Recursive1 (..), cata1, fmapViaBi, foldrViaBi, traverseViaBi)
+import Control.Monad.Reader (Reader, ReaderT (..), runReader)
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Kind (Type)
+import Data.String (IsString (..))
+import Prettyprinter (Pretty (..))
+
+-- | The base functor for a 'Jot'
+newtype JotF g k a r = JotF {unJotF :: Anno k (g a r)}
+  deriving stock (Show, Functor)
+  deriving newtype (Eq, Ord)
+
+pattern JotFP :: k -> g a r -> JotF g k a r
+pattern JotFP k v = JotF (Anno k v)
+
+{-# COMPLETE JotFP #-}
+
+deriving newtype instance (Monoid k, IsString (g a r)) => IsString (JotF g k a r)
+
+deriving newtype instance (Pretty (g a r)) => Pretty (JotF g k a r)
+
+instance (Bifunctor g) => Bifunctor (JotF g k) where
+  bimap f g = go where go = JotF . fmap (bimap f g) . unJotF
+
+instance (Bifoldable g) => Bifoldable (JotF g k) where
+  bifoldr f g = go where go z = bifoldr f g z . annoVal . unJotF
+
+instance (Bitraversable g) => Bitraversable (JotF g k) where
+  bitraverse f g = go where go = fmap JotF . traverse (bitraverse f g) . unJotF
+
+jotFKey :: JotF g k a r -> k
+jotFKey (JotFP k _) = k
+
+jotFVal :: JotF g k a r -> g a r
+jotFVal (JotFP _ v) = v
+
+-- | An annotated 'Knot'
+type Jot :: (Type -> Type -> Type) -> Type -> Type -> Type
+newtype Jot g k a = Jot {unJot :: JotF g k a (Jot g k a)}
+
+pattern JotP :: k -> g a (Jot g k a) -> Jot g k a
+pattern JotP k v = Jot (JotF (Anno k v))
+
+{-# COMPLETE JotP #-}
+
+deriving newtype instance (Eq k, Eq (g a (Jot g k a))) => Eq (Jot g k a)
+
+deriving newtype instance (Ord k, Ord (g a (Jot g k a))) => Ord (Jot g k a)
+
+deriving stock instance (Show k, Show (g a (Jot g k a))) => Show (Jot g k a)
+
+deriving newtype instance (Monoid k, IsString (g a (Jot g k a))) => IsString (Jot g k a)
+
+deriving newtype instance (Pretty (g a (Jot g k a))) => Pretty (Jot g k a)
+
+type instance Base1 (Jot g k) = JotF g k
+
+instance (Bifunctor g) => Recursive1 (Jot g k) where project1 = unJot
+
+instance (Bifunctor g) => Corecursive1 (Jot g k) where embed1 = Jot
+
+instance (Bifunctor g) => Functor (Jot g k) where fmap = fmapViaBi
+
+instance (Bifunctor g, Bifoldable g) => Foldable (Jot g k) where foldr = foldrViaBi
+
+instance (Bitraversable g) => Traversable (Jot g k) where traverse = traverseViaBi
+
+instance (Bifunctor g) => Bifunctor (Jot g) where
+  bimap f g = go where go (JotP k v) = JotP (f k) (bimap g go v)
+
+instance (Bifoldable g) => Bifoldable (Jot g) where
+  bifoldr f g = flip go where go (JotP k v) z = f k (bifoldr g go z v)
+
+instance (Bitraversable g) => Bitraversable (Jot g) where
+  bitraverse f g = go where go (JotP k v) = liftA2 JotP (f k) (bitraverse g go v)
+
+-- | Pull a recursive structure apart and retie as a 'Jot', using the given
+-- function to calculate a key for every level.
+mkJot :: (Recursive1 t, Base1 t ~ g) => (g a k -> k) -> t a -> Jot g k a
+mkJot f = cata1 (\v -> JotP (f (fmap jotKey v)) v)
+
+-- | Forget keys at every level and convert back to a plain structure.
+unMkJot :: (Corecursive1 t, Base1 t ~ g) => Jot g k a -> t a
+unMkJot (JotP _ v) = embed1 (fmap unMkJot v)
+
+-- | Quick conversion from annotated functor.
+annoJot :: Anno b (g a (Jot g b a)) -> Jot g b a
+annoJot = Jot . JotF
+
+-- | Transform the base functor.
+transJot :: (Bifunctor g) => (forall x. g a x -> h a x) -> Jot g k a -> Jot h k a
+transJot nat = go
+ where
+  go (JotP k v) = JotP k (nat (second go v))
+
+jotKey :: Jot g k a -> k
+jotKey (JotP k _) = k
+
+jotVal :: Jot g k a -> g a (Jot g k a)
+jotVal (JotP _ v) = v
+
+-- | 'cata' but nicer
+jotCata :: (Bifunctor g) => (g a x -> Reader k x) -> Jot g k a -> x
+jotCata f = go
+ where
+  go (JotP k v) = runReader (f (fmap go v)) k
+
+-- | 'cataM' but nicer
+jotCataM :: (Bifunctor g) => (g a (m x) -> ReaderT k m x) -> Jot g k a -> m x
+jotCataM f = go
+ where
+  go (JotP k v) = runReaderT (f (fmap go v)) k
+
+-- | Peek at the top value like 'annoRight'
+jotRight :: (g a (Jot g k a) -> Reader k x) -> Jot g k a -> x
+jotRight f = annoRight f . unJotF . unJot
+
+-- | Peek at the top value like 'annoRightM'
+jotRightM :: (g a (Jot g k a) -> ReaderT k m x) -> Jot g k a -> m x
+jotRightM f = annoRightM f . unJotF . unJot
+
+-- | Re-annotate top-down
+jotExtend :: (Bifunctor g) => (Jot g k a -> x) -> Jot g k a -> Jot g x a
+jotExtend w = go where go j@(JotP _ v) = JotP (w j) (fmap go v)
diff --git a/src/Bowtie/Knot.hs b/src/Bowtie/Knot.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Knot.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Bowtie.Knot
+  ( Knot (..)
+  , mkKnot
+  , unMkKnot
+  , transKnot
+  )
+where
+
+import Bowtie.Foldable (Base1, Corecursive1 (..), Recursive1 (..), cata1, fmapViaBi, foldrViaBi, traverseViaBi)
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bitraversable (Bitraversable (..))
+import Data.Kind (Type)
+import Data.String (IsString (..))
+import Prettyprinter (Pretty (..))
+
+-- | A fixpoint for a Bifunctor where the second type variable contains
+-- the recursive structure.
+type Knot :: (Type -> Type -> Type) -> Type -> Type
+newtype Knot g a = Knot {unKnot :: g a (Knot g a)}
+
+deriving newtype instance (Eq (g a (Knot g a))) => Eq (Knot g a)
+
+deriving newtype instance (Ord (g a (Knot g a))) => Ord (Knot g a)
+
+deriving stock instance (Show (g a (Knot g a))) => Show (Knot g a)
+
+deriving newtype instance (Pretty (g a (Knot g a))) => Pretty (Knot g a)
+
+deriving newtype instance (IsString (g a (Knot g a))) => IsString (Knot g a)
+
+type instance Base1 (Knot g) = g
+
+instance (Bifunctor g) => Recursive1 (Knot g) where project1 = unKnot
+
+instance (Bifunctor g) => Corecursive1 (Knot g) where embed1 = Knot
+
+instance (Bifunctor g) => Functor (Knot g) where fmap = fmapViaBi
+
+instance (Bifunctor g, Bifoldable g) => Foldable (Knot g) where foldr = foldrViaBi
+
+instance (Bitraversable g) => Traversable (Knot g) where traverse = traverseViaBi
+
+-- | Pull a recursive structure apart and retie as a 'Knot'.
+mkKnot :: (Recursive1 f, Base1 f ~ g) => f a -> Knot g a
+mkKnot = cata1 Knot
+
+-- | Go the other way.
+unMkKnot :: (Corecursive1 f, Base1 f ~ g) => Knot g a -> f a
+unMkKnot = cata1 embed1
+
+-- | Transform the base Bifunctor.
+transKnot :: (Bifunctor g) => (forall x y. g x y -> h x y) -> Knot g a -> Knot h a
+transKnot nat = go
+ where
+  go = Knot . nat . second go . unKnot
diff --git a/src/Bowtie/Memo.hs b/src/Bowtie/Memo.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/Memo.hs
@@ -0,0 +1,155 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Bowtie.Memo
+  ( MemoF (..)
+  , pattern MemoFP
+  , memoFKey
+  , memoFVal
+  , Memo (..)
+  , pattern MemoP
+  , mkMemo
+  , reMkMemo
+  , reMkMemoM
+  , unMkMemo
+  , transMemo
+  , memoKey
+  , memoVal
+  , memoCata
+  , memoCataM
+  , memoRight
+  , memoRightM
+  , memoExtend
+  )
+where
+
+import Bowtie.Anno (Anno (..), annoRight, annoRightM)
+import Control.Monad.Reader (Reader, ReaderT (..), runReader)
+import Data.Functor.Apply (Apply (..))
+import Data.Functor.Foldable (Base, Corecursive (..), Recursive (..))
+import Data.Kind (Type)
+import Data.String (IsString (..))
+import Prettyprinter (Pretty (..))
+
+-- | The base functor for a 'Memo'
+newtype MemoF f k r = MemoF {unMemoF :: Anno k (f r)}
+  deriving stock (Show, Functor)
+  deriving newtype (Eq, Ord)
+
+pattern MemoFP :: k -> f r -> MemoF f k r
+pattern MemoFP k v = MemoF (Anno k v)
+
+{-# COMPLETE MemoFP #-}
+
+deriving newtype instance (Monoid k, IsString (f r)) => IsString (MemoF f k r)
+
+deriving newtype instance (Pretty (f r)) => Pretty (MemoF f k r)
+
+instance (Apply f, Semigroup k) => Apply (MemoF f k) where
+  liftF2 f (MemoF (Anno k1 v1)) (MemoF (Anno k2 v2)) = MemoF (Anno (k1 <> k2) (liftF2 f v1 v2))
+
+instance (Applicative f, Monoid k) => Applicative (MemoF f k) where
+  pure = MemoF . Anno mempty . pure
+  liftA2 f (MemoF (Anno k1 v1)) (MemoF (Anno k2 v2)) = MemoF (Anno (k1 <> k2) (liftA2 f v1 v2))
+
+memoFKey :: MemoF f k r -> k
+memoFKey (MemoFP k _) = k
+
+memoFVal :: MemoF f k r -> f r
+memoFVal (MemoFP _ v) = v
+
+-- | An annotated 'Fix'
+type Memo :: (Type -> Type) -> Type -> Type
+newtype Memo f k = Memo {unMemo :: MemoF f k (Memo f k)}
+
+pattern MemoP :: k -> f (Memo f k) -> Memo f k
+pattern MemoP k v = Memo (MemoF (Anno k v))
+
+{-# COMPLETE MemoP #-}
+
+deriving newtype instance (Eq k, Eq (f (Memo f k))) => Eq (Memo f k)
+
+deriving newtype instance (Ord k, Ord (f (Memo f k))) => Ord (Memo f k)
+
+deriving stock instance (Show k, Show (f (Memo f k))) => Show (Memo f k)
+
+deriving newtype instance (Monoid k, IsString (f (Memo f k))) => IsString (Memo f k)
+
+deriving newtype instance (Pretty (f (Memo f k))) => Pretty (Memo f k)
+
+instance (Functor f) => Functor (Memo f) where
+  fmap f = go where go (MemoP k v) = MemoP (f k) (fmap go v)
+
+instance (Foldable f) => Foldable (Memo f) where
+  foldr f = flip go where go (MemoP k v) z = foldr go (f k z) v
+
+instance (Traversable f) => Traversable (Memo f) where
+  traverse f = go where go (MemoP k v) = liftA2 MemoP (f k) (traverse go v)
+
+type instance Base (Memo f k) = MemoF f k
+
+instance (Functor f) => Recursive (Memo f k) where project = unMemo
+
+instance (Functor f) => Corecursive (Memo f k) where embed = Memo
+
+-- | Pull a recursive structure apart and retie as a 'Memo', using the given
+-- function to calculate a key for every level.
+mkMemo :: (Recursive t, Base t ~ f) => (f k -> k) -> t -> Memo f k
+mkMemo f = cata (\v -> MemoP (f (fmap memoKey v)) v)
+
+-- | Rebuild a memo with a new annotation.
+reMkMemo :: (Functor f) => (MemoF f j (Memo f k) -> k) -> Memo f j -> Memo f k
+reMkMemo f = go
+ where
+  go (MemoP j fmj) =
+    let fmk = fmap go fmj
+        k = f (MemoFP j fmk)
+    in  MemoP k fmk
+
+-- | Rebuild a memo with a new annotation, effectfully.
+reMkMemoM :: (Traversable f, Monad m) => (MemoF f j (Memo f k) -> m k) -> Memo f j -> m (Memo f k)
+reMkMemoM f = go
+ where
+  go (MemoP j fmj) = do
+    fmk <- traverse go fmj
+    k <- f (MemoFP j fmk)
+    pure (MemoP k fmk)
+
+-- | Forget keys at every level and convert back to a plain structure.
+unMkMemo :: (Corecursive t, Base t ~ f) => Memo f k -> t
+unMkMemo (MemoP _ v) = embed (fmap unMkMemo v)
+
+-- | Transform the base functor.
+transMemo :: (Functor f) => (forall x. f x -> g x) -> Memo f k -> Memo g k
+transMemo nat = go
+ where
+  go (MemoP k v) = MemoP k (nat (fmap go v))
+
+memoKey :: Memo f k -> k
+memoKey (MemoP k _) = k
+
+memoVal :: Memo f k -> f (Memo f k)
+memoVal (MemoP _ v) = v
+
+-- | 'cata' but nicer
+memoCata :: (Functor f) => (f x -> Reader k x) -> Memo f k -> x
+memoCata f = go
+ where
+  go (MemoP k v) = runReader (f (fmap go v)) k
+
+-- | 'cataM' but nicer
+memoCataM :: (Monad m, Traversable f) => (f x -> ReaderT k m x) -> Memo f k -> m x
+memoCataM f = go
+ where
+  go (MemoP k v) = traverse go v >>= \x -> runReaderT (f x) k
+
+-- | Peek at the top value like 'annoRight'
+memoRight :: (f (Memo f k) -> Reader k x) -> Memo f k -> x
+memoRight f = annoRight f . unMemoF . unMemo
+
+-- | Peek at the top value like 'annoRightM'
+memoRightM :: (f (Memo f k) -> ReaderT k m x) -> Memo f k -> m x
+memoRightM f = annoRightM f . unMemoF . unMemo
+
+-- | Re-annotate top-down
+memoExtend :: (Functor f) => (Memo f k -> x) -> Memo f k -> Memo f x
+memoExtend w = go where go m@(MemoP _ v) = MemoP (w m) (fmap go v)
diff --git a/src/Bowtie/Rewrite.hs b/src/Bowtie/Rewrite.hs
--- a/src/Bowtie/Rewrite.hs
+++ b/src/Bowtie/Rewrite.hs
@@ -2,7 +2,7 @@
 
 module Bowtie.Rewrite where
 
-import Bowtie (Jot, pattern JotP)
+import Bowtie.Jot (Jot, pattern JotP)
 import Control.Exception (Exception)
 import Control.Monad ((>=>))
 import Control.Monad.Except (ExceptT (..), MonadError (..), runExceptT)
diff --git a/src/Bowtie/SMap.hs b/src/Bowtie/SMap.hs
new file mode 100644
--- /dev/null
+++ b/src/Bowtie/SMap.hs
@@ -0,0 +1,162 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
+-- | 'SMap' is a "symbol map": Given a domain 'd' and symbol 's', an 'SMap d'
+-- maps 's' to a value 'Val d s'.
+--
+-- Why is this useful? Consider the following scenario: you have some DAG of
+-- transformations that read and write annotations on some datatype, for example,
+-- in a compiler. Then you can type these transformations according to the
+-- what they read and write. These transormations can be grouped into a
+-- domain 'd', and each annotation can be identified by a key symbol 's' and
+-- a value type 'Val d s'.
+module Bowtie.SMap
+  ( Val
+  , Member
+  , NonMember
+  , Inserted
+  , Deleted
+  , Reordered
+  , SMap
+  , emptySMap
+  , singletonSMap
+  , indexSMap
+  , updateSMap
+  , insertSMap
+  , deleteSMap
+  , reorderSMap
+  )
+where
+
+import Data.Coerce (coerce)
+import Data.Dependent.Map (DMap)
+import Data.Dependent.Map qualified as DMap
+import Data.Functor.Identity (Identity (..))
+import Data.GADT.Compare (GCompare (..), GEq (..), GOrdering (..), defaultCompare, defaultEq)
+import Data.Kind (Type)
+import Data.Proxy (Proxy (..))
+import Data.Type.Bool (type (||))
+import Data.Type.Equality ((:~:) (..), type (==))
+import GHC.TypeLits (KnownSymbol, OrderingI (..), Symbol, cmpSymbol, sameSymbol)
+
+type family Val (d :: Type) (s :: Symbol) :: Type
+
+data Key (d :: Type) (v :: Type) where
+  Key
+    :: (KnownSymbol s, v ~ Val d s)
+    => Proxy s
+    -> Proxy v
+    -> Key d v
+
+instance GEq (Key d) where
+  geq (Key ps1 _) (Key ps2 _) =
+    fmap (\Refl -> Refl) (sameSymbol ps1 ps2)
+
+instance Eq (Key d v) where
+  (==) = defaultEq
+
+instance GCompare (Key d) where
+  gcompare (Key ps1 _) (Key ps2 _) =
+    case cmpSymbol ps1 ps2 of
+      LTI -> GLT
+      EQI -> GEQ
+      GTI -> GGT
+
+instance Ord (Key d v) where
+  compare = defaultCompare
+
+key :: (KnownSymbol s, v ~ Val d s) => Proxy s -> Key d v
+key = flip Key Proxy
+
+type DM (d :: Type) = DMap (Key d) Identity
+
+emptyDM :: DM d
+emptyDM = DMap.empty
+
+singletonDM :: (KnownSymbol s) => Proxy s -> Val d s -> DM d
+singletonDM ps v = DMap.singleton (key ps) (Identity v)
+
+lookupDM :: (KnownSymbol s) => Proxy s -> DM d -> Maybe (Val d s)
+lookupDM ps m = fmap runIdentity (DMap.lookup (key ps) m)
+
+indexDM :: (KnownSymbol s) => Proxy s -> DM d -> Val d s
+indexDM ps m = runIdentity (m DMap.! key ps)
+
+insertDM :: (KnownSymbol s) => Proxy s -> Val d s -> DM d -> DM d
+insertDM ps v = DMap.insert (key ps) (Identity v)
+
+deleteDM :: (KnownSymbol s) => Proxy s -> DM d -> DM d
+deleteDM ps = DMap.delete (key ps)
+
+-- type family BoolEqF (x :: Symbol) (y :: Symbol) :: Bool where
+--   BoolEqF x x = True
+--   BoolEqF x y = False
+--
+-- castBoolEq :: (BoolEqF x y == True) => x :~: y
+-- castBoolEq = undefined
+
+type family MemberF (x :: Symbol) (xs :: [Symbol]) :: Bool where
+  MemberF x '[] = False
+  MemberF x (x : zs) = True
+  MemberF x (y : zs) = MemberF x zs
+
+class Member (x :: Symbol) (xs :: [Symbol])
+
+instance (MemberF x (y : zs) ~ True, (x == y || MemberF x zs) ~ True) => Member x (y : zs)
+
+class NonMember (x :: Symbol) (xs :: [Symbol])
+
+instance NonMember x '[]
+
+instance (MemberF x (y : zs) ~ False, (x == y || MemberF x zs) ~ False) => NonMember x (y : zs)
+
+type family InsertedF (x :: Symbol) (xs :: [Symbol]) :: [Symbol] where
+  InsertedF x '[] = '[x]
+  InsertedF x (x : zs) = x : zs
+  InsertedF x (y : zs) = y : InsertedF x zs
+
+class (Member x zs) => Inserted (x :: Symbol) (xs :: [Symbol]) (zs :: [Symbol]) | x xs -> zs
+
+instance (zs ~ InsertedF x '[], Member x zs) => Inserted x '[] zs
+
+instance (zs ~ InsertedF x (y : ys), Member x zs) => Inserted x (y : ys) zs
+
+type family DeletedF (x :: Symbol) (xs :: [Symbol]) :: [Symbol] where
+  DeletedF x '[] = '[]
+  DeletedF x (x : zs) = zs
+  DeletedF x (y : zs) = y : DeletedF x zs
+
+class (NonMember x zs) => Deleted (x :: Symbol) (xs :: [Symbol]) (zs :: [Symbol]) | x xs -> zs
+
+instance (zs ~ DeletedF x '[]) => Deleted x '[] zs
+
+instance (zs ~ DeletedF x (y : ys), NonMember x zs) => Deleted x (y : ys) zs
+
+class Reordered (xs :: [Symbol]) (zs :: [Symbol])
+
+instance Reordered '[] '[]
+
+instance (Reordered xs (DeletedF x zs)) => Reordered (x : xs) zs
+
+newtype SMap (d :: Type) (xs :: [Symbol]) = SMap (DM d)
+
+emptySMap :: SMap d '[]
+emptySMap = SMap emptyDM
+
+singletonSMap :: (KnownSymbol s) => Proxy s -> Val d s -> SMap d '[s]
+singletonSMap ps v = SMap (singletonDM ps v)
+
+indexSMap :: (KnownSymbol s, Member s xs) => Proxy s -> SMap d xs -> Val d s
+indexSMap ps (SMap m) = indexDM ps m
+
+updateSMap :: (KnownSymbol s, Member s xs) => Proxy s -> Val d s -> SMap d xs -> SMap d xs
+updateSMap ps v (SMap m) = SMap (insertDM ps v m)
+
+insertSMap :: (KnownSymbol s, Inserted s xs zs) => Proxy s -> Val d s -> SMap d xs -> SMap d zs
+insertSMap ps v (SMap m) = SMap (insertDM ps v m)
+
+deleteSMap :: (KnownSymbol s, Deleted s xs zs) => Proxy s -> SMap d xs -> SMap d zs
+deleteSMap ps (SMap m) = SMap (deleteDM ps m)
+
+reorderSMap :: (Reordered xs zs) => SMap d xs -> SMap d zs
+reorderSMap = coerce