diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Eric Conlon (c) 2019
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Eric Conlon nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,5 @@
+# blanks
+
+[![CircleCI](https://circleci.com/gh/ejconlon/blanks/tree/master.svg?style=svg)](https://circleci.com/gh/ejconlon/blanks/tree/master)
+
+Fill-in-the-blanks - A library factoring out substitution from ASTs. (Not production ready!)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,5 @@
+module Main where
+
+-- TODO(ejconlon) Create demo app
+main :: IO ()
+main = pure ()
diff --git a/blanks.cabal b/blanks.cabal
new file mode 100644
--- /dev/null
+++ b/blanks.cabal
@@ -0,0 +1,92 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 6dd5dac29a7eb8991e9d2728daa61f8651bf8e283305aa1063f1daf4dce65fd8
+
+name:           blanks
+version:        0.3.0
+synopsis:       Fill-in-the-blanks - A library factoring out substitution from ASTs
+description:    Please see the README on GitHub at <https://github.com/ejconlon/blanks#readme>
+category:       Language
+homepage:       https://github.com/ejconlon/blanks#readme
+bug-reports:    https://github.com/ejconlon/blanks/issues
+author:         Eric Conlon
+maintainer:     ejconlon@gmail.com
+copyright:      (c) 2019 Eric Conlon
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+
+source-repository head
+  type: git
+  location: https://github.com/ejconlon/blanks
+
+library
+  exposed-modules:
+      Blanks
+      Blanks.Class
+      Blanks.LocScope
+      Blanks.Name
+      Blanks.PureScope
+      Blanks.RightAdjunct
+      Blanks.ScopeT
+      Blanks.Sub
+      Blanks.UnderScope
+  other-modules:
+      Paths_blanks
+  hs-source-dirs:
+      src
+  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds
+  build-depends:
+      adjunctions >=4.4
+    , base >=4.12 && <5
+    , containers >=0.6
+    , distributive >=0.6
+    , mtl >=2.2
+  default-language: Haskell2010
+
+executable blanks-exe
+  main-is: Main.hs
+  other-modules:
+      Paths_blanks
+  hs-source-dirs:
+      app
+  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      adjunctions >=4.4
+    , base >=4.12 && <5
+    , blanks
+    , containers >=0.6
+    , distributive >=0.6
+    , mtl >=2.2
+  default-language: Haskell2010
+
+test-suite blanks-test
+  type: exitcode-stdio-1.0
+  main-is: Tasty.hs
+  other-modules:
+      Test.Blanks.Assertions
+      Test.Blanks.BlanksTest
+      Paths_blanks
+  hs-source-dirs:
+      test
+  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      adjunctions >=4.4
+    , base >=4.12 && <5
+    , blanks
+    , containers >=0.6
+    , distributive >=0.6
+    , mtl >=2.2
+    , tasty
+    , tasty-discover
+    , tasty-hunit
+  default-language: Haskell2010
diff --git a/src/Blanks.hs b/src/Blanks.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks.hs
@@ -0,0 +1,12 @@
+module Blanks
+  ( module Blanks
+  ) where
+
+import Blanks.Class as Blanks
+import Blanks.LocScope as Blanks
+import Blanks.Name as Blanks
+import Blanks.PureScope as Blanks
+import Blanks.RightAdjunct as Blanks
+import Blanks.ScopeT as Blanks
+import Blanks.Sub as Blanks
+import Blanks.UnderScope as Blanks
diff --git a/src/Blanks/Class.hs b/src/Blanks/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Class.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module Blanks.Class
+  ( BlankAbstract (..)
+  , BlankCodomain
+  , BlankEmbed (..)
+  , BlankFunctor
+  , BlankInfo
+  ) where
+
+import Blanks.Sub (SubError)
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+
+type family BlankInfo (m :: * -> *) :: *
+type family BlankFunctor (m :: * -> *) :: * -> *
+type family BlankCodomain (m :: * -> *) :: * -> *
+
+class BlankEmbed (m :: * -> *) where
+  -- | "embed functor"
+  blankEmbed :: BlankFunctor m (m a) -> BlankCodomain m (m a)
+
+class BlankAbstract (m :: * -> *) where
+  -- | "free name"
+  blankFree :: a -> BlankCodomain m (m a)
+
+  -- | "abstract info names body"
+  blankAbstract :: Eq a => BlankInfo m -> Seq a -> m a -> BlankCodomain m (m a)
+
+  -- | 'blankAbstract' for a single argument
+  blankAbstract1 :: Eq a => BlankInfo m -> a -> m a -> BlankCodomain m (m a)
+  blankAbstract1 n k = blankAbstract n (Seq.singleton k)
+
+  -- | "unAbstract names body"
+  blankUnAbstract :: Seq a -> m a -> m a
+
+  -- 'blankUnAbstract' for a single argument
+  blankUnAbstract1 :: a -> m a -> m a
+  blankUnAbstract1 = blankUnAbstract . Seq.singleton
+
+  -- | "instantiate args body"
+  blankInstantiate :: Seq (BlankCodomain m (m a)) -> m a -> m a
+
+  -- | 'blankInstantiate' for a single argument
+  blankInstantiate1 :: BlankCodomain m (m a) -> m a -> m a
+  blankInstantiate1 = blankInstantiate . Seq.singleton
+
+  -- | "apply args abstraction"
+  blankApply :: Seq (BlankCodomain m (m a)) -> m a -> Either SubError (m a)
+
+  -- | 'blankApply' for a single argument
+  blankApply1 :: BlankCodomain m (m a) -> m a -> Either SubError (m a)
+  blankApply1 = blankApply . Seq.singleton
diff --git a/src/Blanks/LocScope.hs b/src/Blanks/LocScope.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/LocScope.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.LocScope
+  ( Colocated (..)
+  , Located (..)
+  , LocScope (..)
+  , LocScopeRawFold
+  , LocScopeFold
+  , askColocated
+  , colocated
+  , locScopeBind
+  , locScopeEmbed
+  , locScopeRawFold
+  , locScopeFold
+  , locScopeFree
+  , runColocated
+  ) where
+
+import Blanks.Class
+import Blanks.RightAdjunct (RightAdjunct)
+import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFold, scopeTFree, scopeTRawFold)
+import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)
+import Control.Monad (ap)
+import Control.Monad.Identity (Identity (..))
+import Control.Monad.Reader (MonadReader, Reader, ReaderT (..), ask, runReader)
+import Data.Distributive (Distributive (..))
+import Data.Functor.Adjunction (Adjunction (..))
+import Data.Functor.Rep (Representable)
+
+data Located l a = Located
+  { _locatedLoc :: !l
+  , _locatedVal :: !a
+  } deriving (Eq, Show, Functor, Foldable, Traversable)
+
+newtype Colocated l a = Colocated
+  { unColocated :: Reader l a
+  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)
+
+type instance RightAdjunct (Located l) = Colocated l
+
+colocated :: (l -> a) -> Colocated l a
+colocated f = Colocated (ReaderT (Identity . f))
+
+askColocated :: Colocated l l
+askColocated = Colocated ask
+
+runColocated :: Colocated l a -> l -> a
+runColocated = runReader . unColocated
+
+instance Distributive (Colocated l) where
+  distribute = Colocated . distribute . fmap unColocated
+
+instance Adjunction (Located l) (Colocated l) where
+  leftAdjunct v a = colocated (v . flip Located a)
+  rightAdjunct h (Located l a) = runColocated (h a) l
+
+instance Monoid l => Applicative (Located l) where
+  pure = Located mempty
+  (<*>) = ap
+
+instance Monoid l => Monad (Located l) where
+  return = pure
+  Located l a >>= f = let Located p b = f a in Located (l <> p) b
+
+newtype LocScope l n f a = LocScope
+  { unLocScope :: ScopeT (Located l) n f a
+  } deriving (Functor, Foldable, Traversable, BlankAbstract)
+
+type instance BlankInfo (LocScope l n f) = n
+type instance BlankFunctor (LocScope l n f) = f
+type instance BlankCodomain (LocScope l n f) = Colocated l
+
+instance Functor f => BlankEmbed (LocScope l n f) where
+  blankEmbed = locScopeEmbed
+
+instance (Eq (f (ScopeT (Located l) n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where
+  LocScope su == LocScope sv = su == sv
+
+instance (Show (f (ScopeT (Located l) n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where
+  showsPrec d (LocScope (ScopeT tu)) = showString "LocScope " . showsPrec (d+1) tu
+
+locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a)
+locScopeEmbed fe = colocated (\l -> LocScope (ScopeT (Located l (UnderEmbedScope (EmbedScope (fmap unLocScope fe))))))
+
+locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b
+locScopeBind f = LocScope . scopeTBind (fmap unLocScope . f) . unLocScope
+
+locScopeFree :: a -> Colocated l (LocScope l n f a)
+locScopeFree = fmap LocScope . scopeTFree
+
+type LocScopeRawFold l n f a r = UnderScopeFold n f (LocScope l n f a) a r
+type LocScopeFold l n f a r = LocScopeRawFold l n f a (Colocated l r)
+
+locScopeRawFold :: Functor f => LocScopeRawFold l n f a r -> LocScope l n f a -> Located l r
+locScopeRawFold usf = scopeTRawFold (underScopeFoldContraMap LocScope usf) . unLocScope
+
+locScopeFold :: Functor f => LocScopeFold l n f a r -> LocScope l n f a -> r
+locScopeFold usf = scopeTFold (underScopeFoldContraMap LocScope usf) . unLocScope
diff --git a/src/Blanks/Name.hs b/src/Blanks/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Name.hs
@@ -0,0 +1,16 @@
+module Blanks.Name
+  ( Name (..)
+  , NameOnly
+  ) where
+
+data Name n a =
+  Name
+    { nameKey :: n
+    , nameValue :: a
+    }
+  deriving (Show, Functor, Foldable, Traversable)
+
+instance Eq a => Eq (Name n a) where
+  Name _ x == Name _ y = x == y
+
+type NameOnly n = Name n ()
diff --git a/src/Blanks/PureScope.hs b/src/Blanks/PureScope.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/PureScope.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.PureScope
+  ( PureScope (..)
+  , PureScopeFold
+  , pureScopeBind
+  , pureScopeEmbed
+  , pureScopeFold
+  , pureScopeFree
+  ) where
+
+import Blanks.Class
+import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFree, scopeTRawFold)
+import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)
+import Control.Monad (ap)
+import Control.Monad.Identity (Identity (..))
+
+newtype PureScope n f a = PureScope
+  { unPureScope :: ScopeT Identity n f a
+  } deriving (Functor, Foldable, Traversable, BlankAbstract)
+
+type instance BlankInfo (PureScope n f) = n
+type instance BlankFunctor (PureScope n f) = f
+type instance BlankCodomain (PureScope n f) = Identity
+
+instance Functor f => Applicative (PureScope n f) where
+  pure = pureScopeFree
+  (<*>) = ap
+
+instance Functor f => Monad (PureScope n f) where
+  return = pureScopeFree
+  s >>= f = pureScopeBind f s
+
+instance Functor f => BlankEmbed (PureScope n f) where
+  blankEmbed = Identity . pureScopeEmbed
+
+instance (Eq (f (ScopeT Identity n f a)), Eq n, Eq a) => Eq (PureScope n f a) where
+  PureScope su == PureScope sv = su == sv
+
+instance (Show (f (ScopeT Identity n f a)), Show n, Show a) => Show (PureScope n f a) where
+  showsPrec d (PureScope (ScopeT tu)) = showString "PureScope " . showsPrec (d+1) tu
+
+pureScopeFree :: a -> PureScope n f a
+pureScopeFree = PureScope . runIdentity . scopeTFree
+
+pureScopeBind :: Functor f => (a -> PureScope n f b) -> PureScope n f a -> PureScope n f b
+pureScopeBind f = PureScope . scopeTBind (Identity . unPureScope . f) . unPureScope
+
+pureScopeEmbed :: Functor f => f (PureScope n f a) -> PureScope n f a
+pureScopeEmbed fe = PureScope (ScopeT (Identity (UnderEmbedScope (EmbedScope (fmap unPureScope fe)))))
+
+type PureScopeFold n f a r = UnderScopeFold n f (PureScope n f a) a r
+
+pureScopeFold :: Traversable f => PureScopeFold n f a r -> PureScope n f a -> r
+pureScopeFold usf = runIdentity . scopeTRawFold (underScopeFoldContraMap PureScope usf) . unPureScope
diff --git a/src/Blanks/RightAdjunct.hs b/src/Blanks/RightAdjunct.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/RightAdjunct.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.RightAdjunct
+  ( RightAdjunct
+  , RightAdjunction
+  , RightAdjunctionApplicative
+  ) where
+
+import Control.Monad.Identity (Identity)
+import Data.Functor.Adjunction (Adjunction (..))
+
+type family RightAdjunct (t :: * -> *) :: * -> *
+
+type instance RightAdjunct Identity = Identity
+
+type RightAdjunction (t :: * -> *) = Adjunction t (RightAdjunct t)
+
+type RightAdjunctionApplicative t = (RightAdjunction t, Applicative (RightAdjunct t))
diff --git a/src/Blanks/ScopeT.hs b/src/Blanks/ScopeT.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/ScopeT.hs
@@ -0,0 +1,171 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.ScopeT
+  ( ScopeT (..)
+  , ScopeTFold
+  , ScopeTRawFold
+  , scopeTBind
+  , scopeTEmbed
+  , scopeTFold
+  , scopeTFree
+  , scopeTHoistAnno
+  , scopeTLiftAnno
+  , scopeTRawFold
+  ) where
+
+import Blanks.Class
+import Blanks.RightAdjunct
+import Blanks.Sub (SubError (..))
+import Blanks.UnderScope (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..), UnderScope (..),
+                          UnderScopeFold (..), underScopeFold, underScopePure, underScopeShift)
+import Data.Bifoldable (bifoldr)
+import Data.Bifunctor (bimap, first)
+import Data.Bitraversable (bitraverse)
+import Data.Functor.Adjunction (Adjunction (..))
+import Data.Maybe (fromMaybe)
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+
+newtype ScopeT t n f a = ScopeT
+  { unScopeT :: t (UnderScope n f (ScopeT t n f a) a)
+  }
+
+instance Eq (t (UnderScope n f (ScopeT t n f a) a)) => Eq (ScopeT t n f a) where
+  ScopeT tu == ScopeT tv = tu == tv
+
+instance Show (t (UnderScope n f (ScopeT t n f a) a)) => Show (ScopeT t n f a) where
+  showsPrec d (ScopeT tu) = showString "ScopeT " . showsPrec (d+1) tu
+
+instance (Functor t, Functor f) => Functor (ScopeT t n f) where
+  fmap f (ScopeT tu) = ScopeT (fmap (bimap (fmap f) f) tu)
+
+instance (Foldable t, Foldable f) => Foldable (ScopeT t n f) where
+  foldr f z (ScopeT tu) = foldr (flip (bifoldr (flip (foldr f)) f)) z tu
+
+instance (Traversable t, Traversable f) => Traversable (ScopeT t n f) where
+  traverse f (ScopeT tu) = fmap ScopeT (traverse (bitraverse (traverse f) f) tu)
+
+type instance BlankFunctor (ScopeT t n f) = f
+type instance BlankInfo (ScopeT t n f) = n
+type instance BlankCodomain (ScopeT t n f) = RightAdjunct t
+
+instance RightAdjunction t => BlankEmbed (ScopeT t n f) where
+  blankEmbed = scopeTEmbed
+
+instance (RightAdjunctionApplicative t, Functor f) => BlankAbstract (ScopeT t n f) where
+  blankFree = scopeTFree
+  blankAbstract = scopeTAbstract
+  blankUnAbstract = scopeTUnAbstract
+  blankInstantiate = scopeTInstantiate
+  blankApply = scopeTApply
+
+scopeTWrap :: RightAdjunction t => UnderScope n f (ScopeT t n f a) a -> RightAdjunct t (ScopeT t n f a)
+scopeTWrap = fmap ScopeT . unit
+
+scopeTBound :: RightAdjunction t => Int -> RightAdjunct t (ScopeT t n f a)
+scopeTBound = scopeTWrap . UnderBoundScope . BoundScope
+
+scopeTFree :: RightAdjunction t => a -> RightAdjunct t (ScopeT t n f a)
+scopeTFree = scopeTWrap . UnderFreeScope . FreeScope
+
+scopeTBinder :: RightAdjunction t => Int -> n -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
+scopeTBinder r n e = scopeTWrap (UnderBinderScope (BinderScope r n e))
+
+scopeTEmbed :: RightAdjunction t => f (ScopeT t n f a) -> RightAdjunct t (ScopeT t n f a)
+scopeTEmbed fe = fmap ScopeT (unit (UnderEmbedScope (EmbedScope fe)))
+
+scopeTShiftN :: (Functor t, Functor f) => Int -> Int -> ScopeT t n f a -> ScopeT t n f a
+scopeTShiftN c d (ScopeT tu) = ScopeT (fmap (underScopeShift scopeTShiftN c d) tu)
+
+scopeTShift :: (Functor t, Functor f) => Int -> ScopeT t n f a -> ScopeT t n f a
+scopeTShift = scopeTShiftN 0
+
+scopeTBindOptN :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> Int -> ScopeT t n f a -> ScopeT t n f a
+scopeTBindOptN f = scopeTModOpt . go where
+  go i us =
+    case us of
+      UnderBoundScope _ -> Nothing
+      UnderFreeScope (FreeScope a) -> fmap (fmap (scopeTShift i)) (f a)
+      UnderBinderScope (BinderScope r x e) -> Just (scopeTBinder r x (scopeTBindOptN f (i + r) e))
+      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTBindOptN f i) fe))
+
+scopeTBindOpt :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a
+scopeTBindOpt f = scopeTBindOptN f 0
+
+scopeTBindN :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> Int -> ScopeT t n f a -> ScopeT t n f b
+scopeTBindN f = scopeTMod . go where
+  go i us =
+    case us of
+      UnderBoundScope (BoundScope b) -> scopeTBound b
+      UnderFreeScope (FreeScope a) -> fmap (scopeTShift i) (f a)
+      UnderBinderScope (BinderScope r x e) -> scopeTBinder r x (scopeTBindN f (i + r) e)
+      UnderEmbedScope (EmbedScope fe) -> scopeTEmbed (fmap (scopeTBindN f i) fe)
+
+scopeTBind :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> ScopeT t n f a -> ScopeT t n f b
+scopeTBind f = scopeTBindN f 0
+
+subScopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => Int -> n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
+subScopeTAbstract r n ks e =
+  let f = fmap scopeTBound . flip Seq.elemIndexL ks
+      e' = scopeTBindOpt f e
+  in scopeTBinder r n e'
+
+scopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
+scopeTAbstract n ks =
+  let r = Seq.length ks
+  in subScopeTAbstract r n ks . scopeTShift r
+
+scopeTUnAbstract :: (RightAdjunctionApplicative t, Functor f) => Seq a -> ScopeT t n f a -> ScopeT t n f a
+scopeTUnAbstract ks = scopeTInstantiate (fmap scopeTFree ks)
+
+scopeTModOpt :: RightAdjunctionApplicative t => (UnderScope n f (ScopeT t n f a) a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a
+scopeTModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeT s)
+
+scopeTModM :: (RightAdjunctionApplicative t, Traversable m) => (UnderScope n f (ScopeT t n f a) a -> m (RightAdjunct t x)) -> ScopeT t n f a -> m x
+scopeTModM f = rightAdjunct (sequenceA . f) . unScopeT
+
+scopeTMod :: RightAdjunction t => (UnderScope n f (ScopeT t n f a) a -> RightAdjunct t x) -> ScopeT t n f a -> x
+scopeTMod f = rightAdjunct f . unScopeT
+
+scopeTInstantiateN :: (RightAdjunctionApplicative t, Functor f) => Int -> Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a
+scopeTInstantiateN h vs = scopeTModOpt (go h vs) where
+  go i ws us =
+    case us of
+      UnderBoundScope (BoundScope b) -> vs Seq.!? (b - i)
+      UnderFreeScope _ -> Nothing
+      UnderBinderScope (BinderScope r n e) ->
+        let ws' = fmap (fmap (scopeTShift r)) ws
+            e' = scopeTInstantiateN (r + i) ws' e
+        in Just (scopeTBinder r n e')
+      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTInstantiateN i ws) fe))
+
+scopeTInstantiate :: (RightAdjunctionApplicative t,  Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a
+scopeTInstantiate = scopeTInstantiateN 0
+
+scopeTApply :: (RightAdjunctionApplicative t, Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> Either SubError (ScopeT t n f a)
+scopeTApply vs = scopeTModM go where
+  go us =
+    case us of
+      UnderBinderScope (BinderScope r _ e) ->
+        let len = Seq.length vs
+        in if len == r
+              then Right (pure (scopeTShift (-1) (scopeTInstantiate vs e)))
+              else Left (ApplyError len r)
+      _ -> Left NonBinderError
+
+type ScopeTRawFold t n f a r = UnderScopeFold n f (ScopeT t n f a) a r
+type ScopeTFold t n f a r = ScopeTRawFold t n f a (RightAdjunct t r)
+
+scopeTRawFold :: Functor t => ScopeTRawFold t n f a r -> ScopeT t n f a -> t r
+scopeTRawFold usf = fmap (underScopeFold usf) . unScopeT
+
+scopeTFold :: RightAdjunction t => ScopeTFold t n f a r -> ScopeT t n f a -> r
+scopeTFold usf = counit . scopeTRawFold usf
+
+scopeTLiftAnno :: Functor t => t a -> ScopeT t n f a
+scopeTLiftAnno ta = ScopeT (fmap underScopePure ta)
+
+scopeTHoistAnno :: (Functor t, Functor f) => (forall x. t x -> w x) -> ScopeT t n f a -> ScopeT w n f a
+scopeTHoistAnno nat (ScopeT tu) = ScopeT (nat (fmap (first (scopeTHoistAnno nat)) tu))
diff --git a/src/Blanks/Sub.hs b/src/Blanks/Sub.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Sub.hs
@@ -0,0 +1,37 @@
+module Blanks.Sub
+  ( Sub (..)
+  , SubError (..)
+  , ThrowSub (..)
+  , rethrowSub
+  , runSub
+  ) where
+
+import Control.Exception (Exception)
+import Control.Monad.Except (Except, MonadError (..), runExcept)
+import Data.Typeable (Typeable)
+
+data SubError
+  = ApplyError !Int !Int
+  | UnboundError !Int
+  | NonBinderError
+  deriving (Eq, Show, Typeable)
+
+instance Exception SubError
+
+class ThrowSub m where
+  throwSub :: SubError -> m a
+
+rethrowSub :: (Applicative m, ThrowSub m) => Either SubError a -> m a
+rethrowSub = either throwSub pure
+
+newtype Sub a =
+  Sub
+    { unSub :: Except SubError a
+    }
+  deriving (Functor, Applicative, Monad, Foldable, Traversable)
+
+instance ThrowSub Sub where
+  throwSub = Sub . throwError
+
+runSub :: Sub a -> Either SubError a
+runSub = runExcept . unSub
diff --git a/src/Blanks/UnderScope.hs b/src/Blanks/UnderScope.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/UnderScope.hs
@@ -0,0 +1,104 @@
+module Blanks.UnderScope
+  ( BinderScope (..)
+  , BoundScope (..)
+  , EmbedScope (..)
+  , FreeScope (..)
+  , UnderScope (..)
+  , UnderScopeFold (..)
+  , underScopeFold
+  , underScopeFoldContraMap
+  , underScopePure
+  , underScopeShift
+  ) where
+
+import Data.Bifoldable (Bifoldable (..))
+import Data.Bifunctor (Bifunctor (..))
+import Data.Bitraversable (Bitraversable (..))
+
+newtype BoundScope =
+  BoundScope
+    { unBoundScope :: Int
+    }
+  deriving (Eq, Show)
+
+newtype FreeScope a =
+  FreeScope
+    { unFreeScope :: a
+    }
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+data BinderScope n e =
+  BinderScope
+    { binderScopeArity :: !Int
+    , binderScopeInfo :: !n
+    , binderScopeBody :: !e
+    }
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+newtype EmbedScope f e =
+  EmbedScope
+    { unEmbedScope :: f e
+    }
+  deriving (Eq, Show, Functor)
+
+data UnderScope n f e a
+  = UnderBoundScope !BoundScope
+  | UnderFreeScope !(FreeScope a)
+  | UnderBinderScope !(BinderScope n e)
+  | UnderEmbedScope !(EmbedScope f e)
+  deriving (Eq, Show, Functor)
+
+instance Functor f => Bifunctor (UnderScope n f) where
+  bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b)
+  bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a))
+  bimap f _ (UnderBinderScope (BinderScope i x e)) = UnderBinderScope (BinderScope i x (f e))
+  bimap f _ (UnderEmbedScope (EmbedScope fe)) = UnderEmbedScope (EmbedScope (fmap f fe))
+
+instance Foldable f => Bifoldable (UnderScope n f) where
+  bifoldr _ _ z (UnderBoundScope _) = z
+  bifoldr _ g z (UnderFreeScope (FreeScope a)) = g a z
+  bifoldr f _ z (UnderBinderScope (BinderScope _ _ e)) = f e z
+  bifoldr f _ z (UnderEmbedScope (EmbedScope fe)) = foldr f z fe
+
+instance Traversable f => Bitraversable (UnderScope n f) where
+  bitraverse _ _ (UnderBoundScope (BoundScope b)) = pure (UnderBoundScope (BoundScope b))
+  bitraverse _ g (UnderFreeScope (FreeScope a)) = fmap (UnderFreeScope . FreeScope) (g a)
+  bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e)
+  bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe)
+
+underScopePure :: a -> UnderScope n f e a
+underScopePure = UnderFreeScope . FreeScope
+
+underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a
+underScopeShift recShift c d us =
+  case us of
+    UnderBoundScope (BoundScope b) ->
+      if b < c
+        then us
+        else UnderBoundScope (BoundScope (b + d))
+    UnderFreeScope _ -> us
+    UnderBinderScope (BinderScope i x e) -> UnderBinderScope (BinderScope i x (recShift (c + i) d e))
+    UnderEmbedScope (EmbedScope fe) -> UnderEmbedScope (EmbedScope (fmap (recShift c d) fe))
+
+data UnderScopeFold n f e a r =
+  UnderScopeFold
+    { usfBound :: BoundScope -> r
+    , usfFree :: FreeScope a -> r
+    , usfBinder :: BinderScope n e -> r
+    , usfEmbed :: EmbedScope f e -> r
+    }
+  deriving (Functor)
+
+underScopeFold :: UnderScopeFold n f e a r -> UnderScope n f e a -> r
+underScopeFold (UnderScopeFold bound free binder embed) us =
+  case us of
+    UnderBoundScope x -> bound x
+    UnderFreeScope x -> free x
+    UnderBinderScope x -> binder x
+    UnderEmbedScope x -> embed x
+
+underScopeFoldContraMap :: Functor f => (x -> e) -> UnderScopeFold n f e a r -> UnderScopeFold n f x a r
+underScopeFoldContraMap f (UnderScopeFold bound free binder embed) = UnderScopeFold bound free binder' embed' where
+  binder' (BinderScope r n x) = binder (BinderScope r n (f x))
+  embed' (EmbedScope fx) = embed (EmbedScope (fmap f fx))
+
diff --git a/test/Tasty.hs b/test/Tasty.hs
new file mode 100644
--- /dev/null
+++ b/test/Tasty.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover #-}
diff --git a/test/Test/Blanks/Assertions.hs b/test/Test/Blanks/Assertions.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Blanks/Assertions.hs
@@ -0,0 +1,25 @@
+module Test.Blanks.Assertions where
+
+import Control.Monad (unless)
+import Test.Tasty.HUnit (Assertion, HasCallStack, assertFailure)
+
+assertPredicate :: (Show a, HasCallStack) => (a -> a -> Bool) -> String -> a -> a -> Assertion
+assertPredicate predicate preface left right = unless (predicate left right) (assertFailure msg)
+  where
+    msg =
+      (if null preface
+         then ""
+         else preface ++ "\n") ++
+      "left: " ++ show left ++ "\n right: " ++ show right
+
+assertNotEqual :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion
+assertNotEqual = assertPredicate (/=) "Expected not equal"
+
+assertTrue :: HasCallStack => Bool -> Assertion
+assertTrue a = assertPredicate (==) "Expected True" a True
+
+assertFalse :: HasCallStack => Bool -> Assertion
+assertFalse a = assertPredicate (==) "Expected False" a False
+
+(@/=) :: (Eq a, Show a, HasCallStack) => a -> a -> Assertion
+(@/=) = assertNotEqual
diff --git a/test/Test/Blanks/BlanksTest.hs b/test/Test/Blanks/BlanksTest.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Blanks/BlanksTest.hs
@@ -0,0 +1,87 @@
+module Test.Blanks.BlanksTest where
+
+import Blanks
+import Control.Monad.Identity (Identity (..))
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Test.Blanks.Assertions ((@/=))
+import Test.Tasty
+import Test.Tasty.HUnit
+
+type BareScope = PureScope (NameOnly Char) Identity Char
+
+abst :: Char -> BareScope -> BareScope
+abst a = runIdentity . blankAbstract1 (Name a ()) a
+
+bound :: Int -> BareScope
+bound = PureScope . ScopeT . pure . UnderBoundScope . BoundScope
+
+var :: Char -> BareScope
+var = pure
+
+freeVars :: BareScope -> Set Char
+freeVars = foldMap Set.singleton
+
+test_sub :: TestTree
+test_sub =
+  let svar = var 'x'
+      sbound = bound 0
+      sfree = abst 'y' (var 'x')
+      sfree2 = abst 'z' (abst 'y' (var 'x'))
+      sid = abst 'x' (var 'x')
+      swonky = abst 'x' (bound 0)
+      sconst = abst 'x' (abst 'y' (var 'x'))
+      sflip = abst 'x' (abst 'y' (var 'y'))
+      svar2 = var 'e'
+      swonky2 = abst 'x' svar2
+
+      testEq =
+        testCase "eq" $ do
+          svar @?= svar
+          svar @/= svar2
+          sid @?= abst 'x' (var 'x')
+          sid @?= abst 'y' (var 'y')
+          sid @/= abst 'x' (var 'y')
+          sid @/= abst 'y' (var 'x')
+          sid @/= svar
+
+      testFreeVars =
+        testCase "free vars" $ do
+          freeVars svar @?= Set.singleton 'x'
+          freeVars sbound @?= Set.empty
+          freeVars sfree @?= Set.singleton 'x'
+          freeVars sfree2 @?= Set.singleton 'x'
+          freeVars sid @?= Set.empty
+          freeVars swonky @?= Set.empty
+          freeVars sconst @?= Set.empty
+          freeVars sflip @?= Set.empty
+          freeVars svar2 @=? Set.singleton 'e'
+          freeVars swonky2 @?= Set.singleton 'e'
+
+      testInstantiate =
+        testCase "instantiate" $ do
+          blankInstantiate1 (pure svar2) svar @?= svar
+          blankInstantiate1 (pure svar2) sbound @?= svar2
+          blankInstantiate1 (pure svar2) sid @?= sid
+          blankInstantiate1 (pure svar2) swonky @?= swonky2
+
+      testApply =
+        testCase "apply" $ do
+          blankApply1 (pure svar2) sid @?= Right svar2
+          blankApply1 (pure svar2) swonky @?= Right sbound
+          blankApply1 (pure svar2) sconst @?= Right swonky2
+          blankApply1 (pure svar2) sflip @?= Right sid
+
+      testVarSub =
+        testCase "var sub" $ do
+          (svar >>= const svar2) @?= svar2
+          (sfree >>= const svar2) @?= abst 'y' svar2
+          (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)
+
+      testIdSub =
+        testCase "id sub" $ do
+          (svar >>= const sid) @?= sid
+          (sfree >>= const sid) @?= abst 'y' sid
+          (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)
+
+   in testGroup "sub" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]