diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2023, Oleg Grenrus
+
+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 Oleg Grenrus 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/debruijn.cabal b/debruijn.cabal
new file mode 100644
--- /dev/null
+++ b/debruijn.cabal
@@ -0,0 +1,86 @@
+cabal-version: 2.4
+name:          debruijn
+version:       0.1
+license:       BSD-3-Clause
+license-file:  LICENSE
+category:      Development
+synopsis:      de Bruijn indices and levels
+description:
+  de Bruijn indices and levels for well-scoped terms.
+  .
+  This is "unsafe" (as it uses 'unsafeCoerce') implementation, but it's fast.
+  The API is the same as in @debruin-safe@ package.
+
+author:        Oleg Grenrus <oleg.grenrus@iki.fi>
+maintainer:    Oleg Grenrus <oleg.grenrus@iki.fi>
+build-type:    Simple
+tested-with:   GHC ==9.2.8 || ==9.4.8 || ==9.6.4 || ==9.8.1
+
+source-repository head
+  type:     git
+  location: https://github.com/phadej/debruijn.git
+  subdir:   debruijn
+
+library
+  default-language:   Haskell2010
+  ghc-options:        -Wall -Wno-unticked-promoted-constructors
+  hs-source-dirs:     src src-common
+
+  -- GHC-boot libraries
+  build-depends:
+    , base          ^>=4.16.3.0 || ^>=4.17.0.0 || ^>=4.18.0.0 || ^>=4.19.0.0
+    , deepseq       ^>=1.4.6.1  || ^>=1.5.0.0
+    , transformers  ^>=0.5.6.2  || ^>=0.6.1.0
+
+  -- rest of the dependencies
+  build-depends:
+    , fin        ^>=0.3
+    , skew-list  ^>=0.1
+    , some       ^>=1.0.5
+
+  exposed-modules:
+    DeBruijn
+    DeBruijn.Add
+    DeBruijn.Ctx
+    DeBruijn.Env
+    DeBruijn.Idx
+    DeBruijn.Lte
+    DeBruijn.Lvl
+    DeBruijn.Ren
+    DeBruijn.Size
+    DeBruijn.Sub
+    DeBruijn.Wk
+
+  -- These modules are exported, but shouldn't be used directly.
+  exposed-modules:
+    DeBruijn.Internal.Add
+    DeBruijn.Internal.Env
+    DeBruijn.Internal.Idx
+    DeBruijn.Internal.Lvl
+    DeBruijn.Internal.Size
+
+  other-modules:
+    DeBruijn.RenExtras
+    TrustworthyCompat
+
+  default-extensions:
+    BangPatterns
+    DataKinds
+    DeriveGeneric
+    DeriveTraversable
+    DerivingStrategies
+    EmptyCase
+    FlexibleInstances
+    FunctionalDependencies
+    GADTs
+    OverloadedStrings
+    PatternSynonyms
+    QuantifiedConstraints
+    RankNTypes
+    RoleAnnotations
+    ScopedTypeVariables
+    StandaloneDeriving
+    StandaloneKindSignatures
+    TypeApplications
+    TypeOperators
+    ViewPatterns
diff --git a/src-common/DeBruijn.hs b/src-common/DeBruijn.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn.hs
@@ -0,0 +1,38 @@
+module DeBruijn (
+    -- * Basic building blocks
+    -- |
+    --
+    -- @
+    -- data 'Ctx'  :: Kind                   -- contexts
+    -- data 'Idx'  :: 'Ctx' -> Type            -- de Bruijn indices
+    -- data 'Env'  :: 'Ctx' -> Type -> Type    -- environments
+    -- data 'Lvl'  :: 'Ctx' -> Type            -- de Bruijn levels
+    -- data 'Size' :: 'Ctx' -> Type            -- context size
+    -- @
+    --
+    module DeBruijn.Ctx,
+    module DeBruijn.Idx,
+    module DeBruijn.Env,
+    module DeBruijn.Lvl,
+    module DeBruijn.Size,
+    -- * Weakenings, renamings and substitutions
+    module DeBruijn.Wk,
+    module DeBruijn.Ren,
+    module DeBruijn.Sub,
+    weakenUsingSize,
+    -- * Size addition and less-than-equal predicate
+    module DeBruijn.Add,
+    -- | Module "DeBruijn.Lte" is not exported,
+    -- as it's not that useful in general.
+) where
+
+import DeBruijn.Add
+import DeBruijn.Ctx
+import DeBruijn.Env
+import DeBruijn.Idx
+import DeBruijn.Lvl
+import DeBruijn.Ren
+import DeBruijn.RenExtras
+import DeBruijn.Size
+import DeBruijn.Sub
+import DeBruijn.Wk
diff --git a/src-common/DeBruijn/Ctx.hs b/src-common/DeBruijn/Ctx.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn/Ctx.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE Safe #-}
+module DeBruijn.Ctx (
+    Ctx,
+    EmptyCtx,
+    S,
+    Ctx1, Ctx2, Ctx3, Ctx4, Ctx5, Ctx6, Ctx7, Ctx8, Ctx9,
+) where
+
+import Data.Kind (Type)
+import Data.Nat  (Nat (..))
+
+-- | Context counts variables, in other words context is just a natural number.
+type Ctx :: Type
+type Ctx = Nat
+
+-- | Empty context is zero.
+type EmptyCtx :: Ctx
+type EmptyCtx = Z
+
+-- | And context extension is a successor.
+type S :: Ctx -> Ctx
+type S = 'S
+
+type Ctx1 = S EmptyCtx
+type Ctx2 = S Ctx1
+type Ctx3 = S Ctx2
+type Ctx4 = S Ctx3
+type Ctx5 = S Ctx4
+type Ctx6 = S Ctx5
+type Ctx7 = S Ctx6
+type Ctx8 = S Ctx7
+type Ctx9 = S Ctx8
diff --git a/src-common/DeBruijn/Lte.hs b/src-common/DeBruijn/Lte.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn/Lte.hs
@@ -0,0 +1,17 @@
+module DeBruijn.Lte (
+    Lte (..),
+) where
+
+import Data.Kind (Type)
+
+import DeBruijn.Ctx
+
+-- | @'Lte' ctx ctx'@ is evidence that @ctx'@ is smaller than of @'ctx'@, /less-than-or-equal/,
+-- and produced by simple skipping only, i.e. nothing is inserted into @ctx@, only appended
+-- to the end.
+--
+type Lte :: Ctx -> Ctx -> Type
+type role Lte nominal nominal
+data Lte ctx ctx' where
+    LZ :: Lte ctx ctx
+    LS :: !(Lte ctx ctx') -> Lte ctx (S ctx')
diff --git a/src-common/DeBruijn/Ren.hs b/src-common/DeBruijn/Ren.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn/Ren.hs
@@ -0,0 +1,200 @@
+{-# LANGUAGE Safe #-}
+module DeBruijn.Ren (
+    -- * Renamings
+    Ren (..),
+    renameIdx,
+    keepRen,
+    skipRen,
+    absurdRen,
+    wkToRen,
+    -- ** Category
+    idRen,
+    compRen,
+    -- * Applicative renamings
+    RenA (..),
+    renameIdxA,
+    keepRenA,
+    unusedIdx,
+    -- * Renamable things
+    IdxMapping (..),
+    keepAdd,
+    Renamable (..),
+    RenamableA (..),
+    defaultRename,
+    defaultWeaken,
+) where
+
+import Data.Functor.Identity (Identity (..))
+import Data.Kind             (Constraint, Type)
+import Data.Proxy            (Proxy (..))
+
+import DeBruijn.Add
+import DeBruijn.Ctx
+import DeBruijn.Env
+import DeBruijn.Idx
+import DeBruijn.Size
+import DeBruijn.Wk
+
+import TrustworthyCompat (coerce)
+
+-------------------------------------------------------------------------------
+-- Renamings
+-------------------------------------------------------------------------------
+
+-- | Renamings are mappings of de Bruijn indices.
+--
+-- One possible representation is just @Idx ctx -> Idx ctx'@,
+-- but using 'Env' makes this representation inspectable
+-- and (hopefully) makes 'renameIdx' perform better.
+--
+-- On the other hand, 'idRen' requires @'Size' ctx@.
+-- However this isn't an issue, as either there is 'Size' or using 'Wk' is an option.
+type Ren :: Ctx -> Ctx -> Type
+newtype Ren ctx ctx' = MkRen (Env ctx (Idx ctx'))
+
+-- | Rename de Bruijn index.
+renameIdx :: Ren ctx ctx' -> Idx ctx -> Idx ctx'
+renameIdx (MkRen js) i = lookupEnv i js
+
+-- | Identity renaming.
+idRen :: Size ctx -> Ren ctx ctx
+idRen s = MkRen $ tabulateEnv s id
+
+-- | Lift renaming (used when going under a binder).
+keepRen :: Ren ctx ctx' -> Ren (S ctx) (S ctx')
+keepRen (MkRen js) = MkRen (fmap IS js :> IZ)
+
+skipRen :: Ren ctx ctx' -> Ren ctx (S ctx')
+skipRen (MkRen js) = MkRen (fmap IS js)
+
+-- | Convert 'Wk' to 'Ren'.
+--
+-- Note post and precompositions won't need 'Size'.
+wkToRen :: Size ctx -> Wk ctx ctx' -> Ren ctx ctx'
+wkToRen s      IdWk       = idRen s
+wkToRen s      (SkipWk w) = skipRen (wkToRen s w)
+wkToRen (SS s) (KeepWk w) = keepRen (wkToRen s w)
+
+-- | Renaming composition.
+compRen :: Ren ctx ctx' -> Ren ctx' ctx'' -> Ren ctx ctx''
+compRen (MkRen r) r' = MkRen (fmap (rename r') r)
+
+-- | It's simple to have no indices in any context.
+absurdRen :: Ren EmptyCtx ctx
+absurdRen = MkRen EmptyEnv
+
+-------------------------------------------------------------------------------
+-- Applicative renamings
+-------------------------------------------------------------------------------
+
+type RenA :: (Type -> Type) -> Ctx -> Ctx -> Type
+newtype RenA f ctx ctx' = MkRenA (Env ctx (f (Idx ctx')))
+
+-- | Lift renaming (used when going under a binder).
+keepRenA :: Applicative f => RenA f ctx ctx' -> RenA f (S ctx) (S ctx')
+keepRenA (MkRenA js) = MkRenA (fmap (fmap IS) js :> pure IZ)
+
+unusedIdx :: Size ctx -> RenA Maybe (S ctx) ctx
+unusedIdx s = MkRenA $ tabulateEnv (SS s) $ unIdx Nothing Just
+
+-------------------------------------------------------------------------------
+-- Renamable & RenamableA
+-------------------------------------------------------------------------------
+
+-- | 'IdxMapping' generalizes over various index mappings, also effectful ones.
+type IdxMapping :: (Type -> Type) -> (Ctx -> Ctx -> Type) -> Constraint
+class Applicative f => IdxMapping f t | t -> f where
+    -- | 'IdxMapping' action.
+    mapIdx :: t ctx ctx' -> Idx ctx -> f (Idx ctx')
+
+    -- | 'keep' is often called @lift@, but we stick with 'Wk' terminology.
+    -- One benefit is that the name 'keep' is less likely to clash.
+    keep   :: t ctx ctx' -> t (S ctx) (S ctx')
+
+    -- | Compose weakening with an index mapping.
+    --
+    -- This is useful when you have explicit weakening in your terms.
+    -- (a similar idea as in @bound@'s @Scope@ possibly lifting whole term).
+    weakenIdxMapping :: Wk ctx ctx' -> t ctx' ctx'' -> t ctx ctx''
+
+-- | 'keep' 'IdxMapping' @arity@ times.
+keepAdd
+    :: IdxMapping f m
+    => Add arity ctxA ctxA'
+    -> m ctxA ctxB
+    -> (forall ctxB'. Add arity ctxB ctxB' -> m ctxA' ctxB' -> r)
+    -> r
+keepAdd AZ     w kont = kont AZ w
+keepAdd (AS a) w kont = keepAdd a w $ \a' w' -> kont (AS a') (keep w')
+
+instance IdxMapping Identity Wk where
+    keep = KeepWk
+    mapIdx w x = Identity (weakenIdx w x)
+    weakenIdxMapping = compWk
+
+instance IdxMapping Identity Ren where
+    keep = keepRen
+    mapIdx w x = Identity (renameIdx w x)
+    weakenIdxMapping w (MkRen is) = MkRen (weakenEnv w is)
+
+instance Applicative f => IdxMapping f (RenA f) where
+    keep = keepRenA
+    mapIdx = renameIdxA
+    weakenIdxMapping w (MkRenA is) = MkRenA (weakenEnv w is)
+
+renameIdxA :: RenA f ctx ctx' -> Idx ctx -> f (Idx ctx')
+renameIdxA (MkRenA js) i = lookupEnv i js
+
+-- | Renamable things.
+--
+-- For most terms it's enough to define a single traversal: an instance of 'RenamableA' type-class,
+-- and then define 'Renamable' as:
+--
+-- @
+-- instance 'Renamable' Term where 'rename' = 'defaultRename'; 'weaken' = 'defaultWeaken'
+-- @
+--
+class Renamable t where
+    rename :: Ren n m -> t n -> t m
+    weaken :: Wk n m -> t n -> t m
+
+-- | 'rename' implementation using 'grename'.
+defaultRename :: forall t n m. RenamableA t => Ren n m -> t n -> t m
+defaultRename = coerce (grename @t @Ren @Identity @n @m)
+
+-- | 'weaken' implementation using 'grename'.
+defaultWeaken :: forall t n m. RenamableA t => Wk n m -> t n -> t m
+defaultWeaken = coerce (grename @t @Wk @Identity @n @m)
+
+-- | Effectful renamings.
+--
+-- An common example is checking whether a binding is used:
+--
+-- @
+-- Just t' <- 'renameA' 'unusedIdx' t
+-- @
+--
+class Renamable t => RenamableA t where
+    renameA :: forall f ctx ctx'. Applicative f => RenA f ctx ctx' -> t ctx -> f (t ctx')
+    renameA = grename
+
+    -- | Generic renaming of a term @t@ using any 'IdxMapping'.
+    grename :: forall m f ctx ctx'. IdxMapping f m => m ctx ctx' -> t ctx -> f (t ctx')
+
+instance Renamable Proxy where
+    rename _ _ = Proxy
+    weaken _ _ = Proxy
+
+instance RenamableA Proxy where
+    grename _ _ = pure Proxy
+
+instance Renamable Idx where
+    rename = renameIdx
+    weaken = weakenIdx
+
+instance RenamableA Idx where
+    grename = mapIdx
+
+instance Renamable (Ren n) where
+    rename r r' = compRen r' r
+    weaken w (MkRen js) = MkRen (fmap (weaken w) js)
diff --git a/src-common/DeBruijn/Sub.hs b/src-common/DeBruijn/Sub.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn/Sub.hs
@@ -0,0 +1,95 @@
+module DeBruijn.Sub (
+    -- * Substitution
+    Sub (..),
+    unSub,
+    substIdx,
+    emptySub,
+    snocSub,
+    keepSub,
+    weakenSub,
+    nameMe,
+    -- ** Category
+    idSub,
+    compSub,
+    -- * Classes
+    Var (..),
+    Subst (..),
+) where
+
+import Data.Coerce (coerce)
+import Data.Kind   (Constraint, Type)
+import Data.Proxy  (Proxy (..))
+
+import DeBruijn.Ctx
+import DeBruijn.Env
+import DeBruijn.Idx
+import DeBruijn.Ren
+import DeBruijn.Size
+import DeBruijn.Wk
+
+-- | Substitutions.
+type Sub :: (Ctx -> Type) -> Ctx -> Ctx -> Type
+newtype Sub t ctx ctx' = MkSub (Env ctx (t ctx'))
+
+unSub :: Sub t ctx ctx' -> Env ctx (t ctx')
+unSub = coerce
+
+-- | Substitute index.
+substIdx :: Sub t ctx ctx' -> Idx ctx -> t ctx'
+substIdx (MkSub ts) i = lookupEnv i ts
+
+-- | Substitution from empty context.
+emptySub :: Sub t EmptyCtx ctx'
+emptySub = MkSub EmptyEnv
+
+snocSub :: Sub t ctx ctx' -> t ctx' -> Sub t (S ctx) ctx'
+snocSub (MkSub s) t = MkSub (s :> t)
+
+keepSub :: (Renamable t, Var t) => Sub t ctx ctx' -> Sub t (S ctx) (S ctx')
+keepSub (MkSub ts) = MkSub (fmap (weaken wk1) ts :> var IZ)
+
+-- | Precompose 'Sub' with weakening.
+weakenSub :: Wk ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
+weakenSub w (MkSub ts) = MkSub (weakenEnv w ts)
+
+-- TODO:
+nameMe :: Renamable t => Sub t ctx ctx' -> Wk ctx' ctx'' -> Sub t ctx ctx''
+nameMe (MkSub ts) w = MkSub (fmap (weaken w) ts)
+
+-------------------------------------------------------------------------------
+-- Classes
+-------------------------------------------------------------------------------
+
+-- | Terms which contain indices as variables.
+type Var :: (Ctx -> Type) -> Constraint
+class Var t where
+    var :: Idx ctx -> t ctx
+
+-- | Terms which we can subsitute into.
+type Subst :: (Ctx -> Type) -> Constraint
+class Var t => Subst t where
+    subst :: Sub t ctx ctx' -> t ctx -> t ctx'
+
+instance Var Proxy where
+    var _ = Proxy
+
+instance Subst Proxy where
+    subst _ _ = Proxy
+
+instance Var Idx where
+    var = id
+
+instance Subst Idx where
+    subst = substIdx
+
+-------------------------------------------------------------------------------
+-- Category
+-------------------------------------------------------------------------------
+
+-- | Identity substitution
+idSub :: Var t => Size ctx -> Sub t ctx ctx
+idSub s = MkSub $ tabulateEnv s var
+
+-- | Substitution composition.
+compSub :: Subst t => Sub t ctx ctx' -> Sub t ctx' ctx'' -> Sub t ctx ctx''
+compSub (MkSub s) s' = MkSub (fmap (subst s') s)
diff --git a/src-common/DeBruijn/Wk.hs b/src-common/DeBruijn/Wk.hs
new file mode 100644
--- /dev/null
+++ b/src-common/DeBruijn/Wk.hs
@@ -0,0 +1,201 @@
+{-# LANGUAGE Safe #-}
+module DeBruijn.Wk (
+    Wk(IdWk, SkipWk, KeepWk),
+    -- * Combinators
+    wk1,
+    compWk,
+    -- * Index weakening
+    weakenIdx,
+    -- * Size weakening
+    weakenSize,
+    contractSize,
+    -- * Environment contraction
+    weakenEnv,
+    setWeakenEnv,
+    overWeakenEnv,
+) where
+
+import Data.Kind (Type)
+
+import DeBruijn.Ctx
+import DeBruijn.Env
+import DeBruijn.Idx
+import DeBruijn.Size
+
+-- $setup
+-- >>> :set -XGADTs
+-- >>> import DeBruijn
+-- >>> import Data.Function ((&))
+-- >>> import Data.Char (toUpper)
+
+-- | Weakenings, order preserving embeddings.
+--
+-- @Wk n m@ could be represented as @m@ bit field with popCount of @n@.
+--
+-- Constructor names make sense when you look at the implementation of 'weakenEnv'.
+--
+-- Note: usually 'ViewWk is defined as
+--
+-- @
+-- data Wk ctx ctx' where
+--     WkNil  :: Wk EmptyCtx EmptyCtx
+--     KeepWk :: Wk ctx ctx' -> Wk (S ctx)  (S ctx')
+--     SkipWk :: Wk ctx ctx' -> Wk    ctx   (S ctx')
+-- @
+--
+-- However that representation doesn't allow to make @'wkId' :: 'ViewWk ctx ctx@ without knowing the size of context.
+-- Therefore we morally use a representation closer to
+--
+-- @
+-- data 'Wk' ctx ctx' where
+--     'IdWk'   :: Wk ctx ctx
+--     'KeepWk' :: Wk ctx ctx' -> Wk (S ctx)  (S ctx')
+--     'SkipWk' :: Wk ctx ctx' -> Wk    ctx   (S ctx')
+-- @
+--
+-- But we keep an invariant that identity weakenings are always represented by 'IdWk'.
+--
+-- >>> KeepWk IdWk
+-- IdWk
+--
+-- And 'KeepWk' pattern doesn't match on identity weakenings.
+--
+-- >>> case IdWk :: Wk Ctx2 Ctx2 of { KeepWk _ -> "keep"; SkipWk _ -> "skip"; IdWk -> "id" } :: String
+-- "id"
+--
+type Wk :: Ctx -> Ctx -> Type
+type role Wk nominal nominal
+data Wk ctx ctx' where
+    IdWk :: Wk ctx ctx
+    NeWk :: Wk1 ctx ctx' -> Wk ctx ctx'
+
+type Wk1 :: Ctx -> Ctx -> Type
+data Wk1 ctx ctx' where
+    Wk1     ::                 Wk1    ctx   (S ctx)
+    KeepWk1 :: Wk1 ctx ctx' -> Wk1 (S ctx)  (S ctx')
+    SkipWk1 :: Wk1 ctx ctx' -> Wk1    ctx   (S ctx')
+
+deriving instance Eq (Wk ctx ctx')
+deriving instance Eq (Wk1 ctx ctx')
+
+-- | Keep variable.
+keepWk :: Wk ctx ctx' -> Wk (S ctx) (S ctx')
+keepWk IdWk     = IdWk
+keepWk (NeWk w) = NeWk (KeepWk1 w)
+
+-- | Skip variable.
+skipWk :: Wk ctx ctx' -> Wk ctx (S ctx')
+skipWk IdWk     = wk1
+skipWk (NeWk w) = NeWk (SkipWk1 w)
+
+viewWk :: Wk ctx ctx' -> ViewWk ctx ctx'
+viewWk IdWk               = IdWk'
+viewWk (NeWk Wk1)         = SkipWk' IdWk
+viewWk (NeWk (SkipWk1 w)) = SkipWk' (NeWk w)
+viewWk (NeWk (KeepWk1 w)) = KeepWk' (NeWk w)
+
+type ViewWk :: Ctx -> Ctx -> Type
+data ViewWk ctx ctx' where
+    IdWk'   :: ViewWk ctx ctx
+    SkipWk' :: Wk ctx ctx' -> ViewWk    ctx  (S ctx')
+    KeepWk' :: Wk ctx ctx' -> ViewWk (S ctx) (S ctx')
+
+pattern KeepWk :: () => (a ~ S a', b ~ S b') => Wk a' b' -> Wk a b
+pattern KeepWk w <- (viewWk -> KeepWk' w)
+  where KeepWk w = keepWk w
+
+pattern SkipWk :: () => (b ~ S b') => Wk a b' -> Wk a b
+pattern SkipWk w <- (viewWk -> SkipWk' w)
+  where SkipWk w = skipWk w
+
+{-# COMPLETE IdWk, SkipWk, KeepWk #-}
+
+instance Show (Wk ctx ctx') where
+    showsPrec _ IdWk       = showString "IdWk"
+    showsPrec d (KeepWk w) = showParen (d > 10) $ showString "KeepWk " . showsPrec 11 w
+    showsPrec d (SkipWk w) = showParen (d > 10) $ showString "SkipWk " . showsPrec 11 w
+
+-- | Weaken by one. @'wk1' = 'SkipWk' 'IdWk'@.
+wk1 :: Wk ctx (S ctx)
+wk1 = NeWk Wk1
+
+-- | Weakening composition.
+compWk :: Wk a b -> Wk b c -> Wk a c
+compWk IdWk     w'        = w'
+compWk (NeWk w) IdWk      = NeWk w
+compWk (NeWk w) (NeWk w') = NeWk (compWk1 w w')
+
+compWk1 :: Wk1  a b -> Wk1 b c -> Wk1 a c
+compWk1 w           Wk1          = SkipWk1 w
+compWk1 w           (SkipWk1 w') = SkipWk1 (compWk1 w w')
+compWk1 Wk1         (KeepWk1 w') = SkipWk1 w'
+compWk1 (SkipWk1 w) (KeepWk1 w') = SkipWk1 (compWk1 w w')
+compWk1 (KeepWk1 w) (KeepWk1 w') = KeepWk1 (compWk1 w w')
+
+-- | Weaken 'Idx', i.e. map index from smaller to larger context.
+weakenIdx :: Wk ctx ctx' -> Idx ctx -> Idx ctx'
+weakenIdx IdWk     x = x
+weakenIdx (NeWk w) x = weaken1Idx w x
+
+weaken1Idx :: Wk1 ctx ctx' -> Idx ctx -> Idx ctx'
+weaken1Idx Wk1         x      = IS x
+weaken1Idx (SkipWk1 w) x      = IS (weaken1Idx w x)
+weaken1Idx (KeepWk1 _) IZ     = IZ
+weaken1Idx (KeepWk1 w) (IS x) = IS (weaken1Idx w x)
+
+-- | Weaken 'Size'.
+weakenSize :: Wk ctx ctx' -> Size ctx -> Size ctx'
+weakenSize IdWk     x = x
+weakenSize (NeWk w) x = weaken1Size w x
+
+weaken1Size :: Wk1 ctx ctx' -> Size ctx -> Size ctx'
+weaken1Size Wk1         x      = SS x
+weaken1Size (SkipWk1 w) x      = SS (weaken1Size w x)
+weaken1Size (KeepWk1 w) (SS x) = SS (weaken1Size w x)
+
+contractSize :: Wk ctx ctx' -> Size ctx' -> Size ctx
+contractSize IdWk     x = x
+contractSize (NeWk w) x = contract1Size w x
+
+contract1Size :: Wk1 ctx ctx' -> Size ctx' -> Size ctx
+contract1Size Wk1         (SS x) = x
+contract1Size (SkipWk1 w) (SS x) = contract1Size w x
+contract1Size (KeepWk1 w) (SS x) = SS (contract1Size w x)
+
+-- | Contract 'Env' i.e. drop elements from larger context.
+--
+-- This function explains the 'KeepWk' and 'SkipWk' constructor names:
+--
+-- >>> weakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b' :> 'c' :> 'd' :> 'e')
+-- EmptyEnv :> 'a' :> 'b' :> 'c' :> 'e'
+--
+weakenEnv :: Wk ctx ctx' -> Env ctx' a -> Env ctx a
+weakenEnv IdWk     xs = xs
+weakenEnv (NeWk w) xs = weaken1Env w xs
+
+weaken1Env :: Wk1 ctx ctx' -> Env ctx' a -> Env ctx a
+weaken1Env Wk1         (xs :> _) = xs
+weaken1Env (SkipWk1 w) (xs :> _) = weaken1Env w xs
+weaken1Env (KeepWk1 w) (xs :> x) = weaken1Env w xs :> x
+
+-- | 'setWeakenEnv' and 'weakenEnv' together form a lens.
+--
+-- >>> setWeakenEnv (IdWk & SkipWk & KeepWk) (EmptyEnv :> 'a' :> 'b') (EmptyEnv :> 'x' :> 'y' :> 'z')
+-- EmptyEnv :> 'a' :> 'y' :> 'b'
+--
+setWeakenEnv :: Wk ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
+setWeakenEnv IdWk     env _    = env
+setWeakenEnv (NeWk w) env env' = setWeaken1Env w env env'
+
+-- | Setter made from 'setWeakenEnv' and 'weakenEnv'.
+--
+-- >>> overWeakenEnv (IdWk & SkipWk & KeepWk) (fmap toUpper) (EmptyEnv :> 'a' :> 'x' :> 'y' :> 'z')
+-- EmptyEnv :> 'A' :> 'X' :> 'y' :> 'Z'
+--
+overWeakenEnv :: Wk ctx ctx' -> (Env ctx a -> Env ctx a) -> Env ctx' a -> Env ctx' a
+overWeakenEnv w f env = setWeakenEnv w (f (weakenEnv w env)) env
+
+setWeaken1Env :: Wk1 ctx ctx' -> Env ctx a -> Env ctx' a -> Env ctx' a
+setWeaken1Env Wk1         xs        (_ :> y)  = xs :> y
+setWeaken1Env (SkipWk1 w) xs        (ys :> y) = setWeaken1Env w xs ys :> y
+setWeaken1Env (KeepWk1 w) (xs :> x) (ys :> _) = setWeaken1Env w xs ys :> x
diff --git a/src-common/TrustworthyCompat.hs b/src-common/TrustworthyCompat.hs
new file mode 100644
--- /dev/null
+++ b/src-common/TrustworthyCompat.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE Trustworthy #-}
+module TrustworthyCompat (
+    coerce,
+) where
+
+import Data.Coerce (coerce)
diff --git a/src/DeBruijn/Add.hs b/src/DeBruijn/Add.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Add.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE Trustworthy #-}
+module DeBruijn.Add (
+    Add (AZ, AS),
+    addToInt,
+    addToSize,
+    adding,
+    -- * Lemmas
+    rzeroAdd,
+    unrzeroAdd,
+    lzeroAdd,
+    unlzeroAdd,
+    rsuccAdd,
+    unrsuccAdd,
+    lsuccAdd,
+    unlsuccAdd,
+    swapAdd,
+    unswapAdd,
+) where
+
+import DeBruijn.Internal.Add
diff --git a/src/DeBruijn/Env.hs b/src/DeBruijn/Env.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Env.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE Trustworthy #-}
+module DeBruijn.Env (
+    Env (EmptyEnv, (:>)),
+    lookupEnv,
+    sizeEnv,
+    tabulateEnv,
+) where
+
+import DeBruijn.Internal.Env
diff --git a/src/DeBruijn/Idx.hs b/src/DeBruijn/Idx.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Idx.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE Trustworthy #-}
+-- | de Bruijn indices for well-scoped terms.
+module DeBruijn.Idx (
+    -- * de Bruijn indices
+    Idx (IZ, IS),
+    absurdIdx,
+    unIdx,
+    idxToInt,
+    -- * Common indices
+    pattern I1,
+    pattern I2,
+    pattern I3,
+    pattern I4,
+    pattern I5,
+    pattern I6,
+    pattern I7,
+    pattern I8,
+    pattern I9,
+) where
+
+
+import DeBruijn.Internal.Idx
diff --git a/src/DeBruijn/Internal/Add.hs b/src/DeBruijn/Internal/Add.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Internal/Add.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE Unsafe #-}
+module DeBruijn.Internal.Add (
+    Add (AZ, AS, UnsafeAdd),
+    addToInt,
+    addToSize,
+    adding,
+    -- * Lemmas
+    rzeroAdd,
+    unrzeroAdd,
+    lzeroAdd,
+    unlzeroAdd,
+    rsuccAdd,
+    unrsuccAdd,
+    lsuccAdd,
+    unlsuccAdd,
+    swapAdd,
+    unswapAdd,
+) where
+
+
+import Data.Coerce        (coerce)
+import Data.GADT.Show     (GShow (..))
+import Data.Kind          (Type)
+import Data.Some          (Some (..))
+import Data.Type.Equality ((:~:) (Refl))
+import Unsafe.Coerce      (unsafeCoerce)
+
+import DeBruijn.Ctx
+import DeBruijn.Internal.Size
+
+-- $setup
+-- >>> import DeBruijn
+
+-- | @'Add' n m p@ is an evidence that @n + m = p@.
+--
+-- Useful when you have an arity @n@ thing and need to extend a context @ctx@ with: @'Add' n ctx ctx'@.
+--
+-- Using a type representing a graph of a type function is often more convenient than defining type-family to begin with.
+--
+type Add :: Ctx -> Ctx -> Ctx -> Type
+type role Add nominal nominal nominal
+
+newtype Add n m p = UnsafeAdd { _addToInt :: Int }
+
+addToInt :: Add n m p -> Int
+addToInt = _addToInt
+
+addToSize :: Add n m p -> Size n
+addToSize (UnsafeAdd n) = UnsafeSize n
+
+instance Show (Add n m p) where
+    showsPrec d a = showsPrec d (addToInt a)
+
+instance GShow (Add n m) where
+    gshowsPrec = showsPrec
+
+type ViewAdd :: Ctx -> Ctx -> Ctx -> Type
+type role ViewAdd nominal nominal nominal
+data ViewAdd n m p where
+    AZ' :: ViewAdd EmptyCtx ctx ctx
+    AS' :: !(Add n ctx ctx') -> ViewAdd (S n) ctx (S ctx')
+
+viewAdd :: Add n m p -> ViewAdd n m p
+viewAdd (UnsafeAdd n)
+    | n <= 0    = unsafeCoerce AZ'
+    | otherwise = unsafeCoerce (AS' (UnsafeAdd (n - 1)))
+
+pattern AZ :: () => (n ~ EmptyCtx, m ~ p) => Add n m p
+pattern AZ <- (viewAdd -> AZ')
+  where AZ = UnsafeAdd 0
+
+pattern AS :: () => (n ~ S n', p ~ S p') => Add n' m p' -> Add n m p
+pattern AS a <- (viewAdd -> AS' a)
+  where AS a = UnsafeAdd (_addToInt a + 1)
+
+{-# COMPLETE AZ, AS #-}
+
+-- | Add @n@ to some context @ctx@.
+--
+-- >>> adding (SS (SS SZ))
+-- Some 2
+--
+adding :: Size n -> Some (Add n ctx)
+adding (UnsafeSize n) = Some (UnsafeAdd n)
+
+-------------------------------------------------------------------------------
+-- Lemmas: zero
+-------------------------------------------------------------------------------
+
+-- | @n + 0 ≡ 0@
+rzeroAdd :: Size n -> Add n EmptyCtx n
+rzeroAdd (UnsafeSize n) = UnsafeAdd n
+
+-- | @n + 0 ≡ m → n ≡ m@
+unrzeroAdd :: Add n EmptyCtx m -> n :~: m
+unrzeroAdd (UnsafeAdd !_) = unsafeCoerce Refl
+
+-- | @0 + n ≡ 0@
+lzeroAdd :: Size n -> Add EmptyCtx n n
+lzeroAdd _ = AZ
+
+-- | @0 + n ≡ m → n ≡ m@
+unlzeroAdd :: Add EmptyCtx n m -> n :~: m
+unlzeroAdd AZ = Refl
+
+-------------------------------------------------------------------------------
+-- Lemmas: succ
+-------------------------------------------------------------------------------
+
+-- | @n + m ≡ p → n + S m ≡ S p@
+rsuccAdd :: Add n m p -> Add n (S m) (S p)
+rsuccAdd = coerce
+
+-- | @n + S m ≡ S p → n + m ≡ p@
+unrsuccAdd :: Add n (S m) (S p) -> Add n m p
+unrsuccAdd = coerce
+
+-- | @n + m ≡ p → S n + m ≡ S p@
+lsuccAdd :: Add n m p -> Add (S n) m (S p)
+lsuccAdd = AS
+
+-- | @S n + m ≡ S p → n + m ≡ p@
+unlsuccAdd :: Add (S n) m (S p) -> Add n m p
+unlsuccAdd (AS a)= a
+
+-------------------------------------------------------------------------------
+-- Lemmas: swap
+-------------------------------------------------------------------------------
+
+-- | @n + S m ≡ p → S n + m ≡ p@
+swapAdd :: Add n (S m) p -> Add (S n) m p
+swapAdd (UnsafeAdd n) = UnsafeAdd (n + 1)
+
+-- | @S n + m ≡ p → n + S m ≡ p@
+unswapAdd :: Add (S n) m p -> Add n (S m) p
+unswapAdd (UnsafeAdd n) = UnsafeAdd (n - 1)
diff --git a/src/DeBruijn/Internal/Env.hs b/src/DeBruijn/Internal/Env.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Internal/Env.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE Unsafe #-}
+module DeBruijn.Internal.Env (
+    Env (EmptyEnv, (:>), UnsafeEnv),
+    lookupEnv,
+    sizeEnv,
+    tabulateEnv,
+) where
+
+import Data.Coerce          (coerce)
+import Data.Functor.Reverse (Reverse (..))
+import Data.Kind            (Type)
+import Data.SkewList.Lazy   (SkewList)
+import Unsafe.Coerce        (unsafeCoerce)
+
+import qualified Data.SkewList.Lazy as SL
+
+import DeBruijn.Ctx
+import DeBruijn.Internal.Idx
+import DeBruijn.Internal.Size
+
+-- $setup
+-- >>> import DeBruijn
+-- >>> import Data.Foldable (toList)
+
+-------------------------------------------------------------------------------
+-- Environment
+-------------------------------------------------------------------------------
+
+-- | Environment
+--
+-- >>> EmptyEnv :> 'a' :> 'b'
+-- EmptyEnv :> 'a' :> 'b'
+--
+type Env :: Ctx -> Type -> Type
+type role Env nominal representational
+newtype Env ctx a = UnsafeEnv { unEnv :: SkewList a }
+
+-------------------------------------------------------------------------------
+-- Pattern synonyms
+-------------------------------------------------------------------------------
+
+-- We need a GADT to implement pattern synonyms.
+type ViewEnv :: Ctx -> Type -> Type
+type role ViewEnv nominal representational
+data ViewEnv ctx a where
+    EmptyViewEnv :: ViewEnv EmptyCtx a
+    (:>>)     :: Env ctx a -> a -> ViewEnv (S ctx) a
+
+viewEnv :: Env ctx a -> ViewEnv ctx a
+viewEnv (UnsafeEnv env) = case SL.uncons env of
+    Nothing      -> unsafeCoerce EmptyViewEnv
+    Just (x, xs) -> unsafeCoerce (UnsafeEnv xs :>> x)
+
+pattern EmptyEnv :: () => (ctx ~ EmptyCtx) => Env ctx a
+pattern EmptyEnv <- (viewEnv -> EmptyViewEnv)
+  where EmptyEnv = UnsafeEnv SL.Nil
+
+infixl 5 :>
+pattern (:>) :: () => (ctx ~ S ctx') => Env ctx' a -> a -> Env ctx a
+pattern xs :> x <- (viewEnv -> xs :>> x)
+  where xs :> x = UnsafeEnv (SL.cons x (unEnv xs))
+
+{-# COMPLETE EmptyEnv, (:>) #-}
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+deriving instance Functor (Env ctx)
+
+-- |
+--
+-- >>> toList (tabulateEnv S3 id)
+-- [2,1,0]
+--
+instance Foldable (Env ctx) where
+    foldMap f (UnsafeEnv xs) = foldMap f (Reverse xs)
+
+-- |
+--
+-- >>> traverse print (tabulateEnv S3 id)
+-- 2
+-- 1
+-- 0
+-- EmptyEnv :> () :> () :> ()
+--
+instance Traversable (Env ctx) where
+    traverse f (UnsafeEnv xs) = fmap (UnsafeEnv . getReverse) (traverse f (Reverse xs))
+
+instance Show a => Show (Env ctx a) where
+    showsPrec d0 (UnsafeEnv xs0) = go d0 xs0 where
+        go d ys = case SL.uncons ys of
+            Nothing      -> showString "EmptyEnv"
+            Just (x, xs) -> showParen (d > 5)
+                $ go 5 xs
+                . showString " :> "
+                . showsPrec 6 x
+
+-------------------------------------------------------------------------------
+-- Combinators
+-------------------------------------------------------------------------------
+
+-- | Lookup in the context.
+--
+-- >>> lookupEnv IZ (EmptyEnv :> 'a' :> 'b')
+-- 'b'
+--
+lookupEnv :: Idx ctx -> Env ctx a -> a
+lookupEnv (UnsafeIdx i) (UnsafeEnv xs) = xs SL.! i
+
+-- | Size of the environment.
+--
+-- >>> sizeEnv (EmptyEnv :> 'a' :> 'b')
+-- 2
+--
+sizeEnv :: Env n a -> Size n
+sizeEnv (UnsafeEnv xs) = UnsafeSize (length xs)
+
+-- | Create 'Env' by creating elements given an 'Idx'.
+--
+-- >>> tabulateEnv S4 id
+-- EmptyEnv :> 3 :> 2 :> 1 :> 0
+--
+tabulateEnv :: Size ctx -> (Idx ctx -> a) -> Env ctx a
+tabulateEnv (UnsafeSize s) f = UnsafeEnv $ SL.fromList $ map (coerce f) [0 .. s - 1]
diff --git a/src/DeBruijn/Internal/Idx.hs b/src/DeBruijn/Internal/Idx.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Internal/Idx.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE Unsafe #-}
+-- | de Bruijn indices for well-scoped terms.
+module DeBruijn.Internal.Idx (
+    -- * de Bruijn indices
+    Idx (IZ, IS, UnsafeIdx),
+    absurdIdx,
+    unIdx,
+    idxToInt,
+    -- * Common indices
+    pattern I1,
+    pattern I2,
+    pattern I3,
+    pattern I4,
+    pattern I5,
+    pattern I6,
+    pattern I7,
+    pattern I8,
+    pattern I9,
+) where
+
+import Data.Kind    (Type)
+import DeBruijn.Ctx
+
+import Unsafe.Coerce (unsafeCoerce)
+
+-------------------------------------------------------------------------------
+-- de Bruijn indices
+-------------------------------------------------------------------------------
+
+-- | de Bruijn indices.
+--
+-- >>> IS (IS (IS IZ))
+-- 3
+--
+type Idx :: Ctx -> Type
+type role Idx nominal
+
+newtype Idx j = UnsafeIdx { _idxToInt :: Int }
+
+-------------------------------------------------------------------------------
+-- Combinators
+-------------------------------------------------------------------------------
+
+-- | Convert index to 'Int'.
+idxToInt :: Idx ctx -> Int
+idxToInt = _idxToInt
+
+-- | Derive anything from index into empty scope.
+--
+-- Note: don't use @EmptyCase@ on 'Idx' as it doesn't work for unsafe representation.
+--
+absurdIdx :: Idx EmptyCtx -> a
+absurdIdx x = x `seq` error "absurd: Idx Z"
+
+-------------------------------------------------------------------------------
+-- Pattern synonyms
+-------------------------------------------------------------------------------
+
+-- We need a GADT to implement pattern synonyms.
+type ViewIdx :: Ctx -> Type
+type role ViewIdx nominal
+data ViewIdx n where
+    IZ' :: ViewIdx (S n)
+    IS' :: Idx n -> ViewIdx (S n)
+
+viewIdx :: Idx n -> ViewIdx n
+viewIdx (UnsafeIdx 0) = unsafeCoerce IZ'
+viewIdx (UnsafeIdx n) = unsafeCoerce (IS' (UnsafeIdx (n - 1)))
+
+pattern IZ :: () => (m ~ S n) => Idx m
+pattern IZ <- (viewIdx -> IZ')
+  where IZ = UnsafeIdx 0
+
+pattern IS :: () => (m ~ S n) => Idx n -> Idx m
+pattern IS n <- (viewIdx -> IS' n)
+  where IS n = UnsafeIdx (idxToInt n + 1)
+
+{-# COMPLETE IZ, IS #-}
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+deriving instance Eq (Idx n)
+deriving instance Ord (Idx n)
+
+instance Show (Idx j) where
+    showsPrec d = showsPrec d . idxToInt
+
+-------------------------------------------------------------------------------
+-- Common Combinators
+-------------------------------------------------------------------------------
+
+-- | Case on 'Idx'. (compare to 'maybe').
+unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a
+unIdx z _ IZ     = z
+unIdx _ s (IS x) = s x
+
+pattern I1 :: () => (m ~ S (S n)) => Idx m
+pattern I1 = IS IZ
+
+pattern I2 :: () => (m ~ S (S (S n))) => Idx m
+pattern I2 = IS I1
+
+pattern I3 :: () => (m ~ S (S (S (S n)))) => Idx m
+pattern I3 = IS I2
+
+pattern I4 :: () => (m ~ S (S (S (S (S n))))) => Idx m
+pattern I4 = IS I3
+
+pattern I5 :: () => (m ~ S (S (S (S (S (S n)))))) => Idx m
+pattern I5 = IS I4
+
+pattern I6 :: () => (m ~ S (S (S (S (S (S (S n))))))) => Idx m
+pattern I6 = IS I5
+
+pattern I7 :: () => (m ~ S (S (S (S (S (S (S (S n)))))))) => Idx m
+pattern I7 = IS I6
+
+pattern I8 :: () => (m ~ S (S (S (S (S (S (S (S (S n))))))))) => Idx m
+pattern I8 = IS I7
+
+pattern I9 :: () => (m ~ S (S (S (S (S (S (S (S (S (S n)))))))))) => Idx m
+pattern I9 = IS I8
diff --git a/src/DeBruijn/Internal/Lvl.hs b/src/DeBruijn/Internal/Lvl.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Internal/Lvl.hs
@@ -0,0 +1,123 @@
+{-# LANGUAGE Unsafe #-}
+-- | de Bruijn levels for well-scoped terms.
+module DeBruijn.Internal.Lvl (
+    -- * Levels
+    Lvl (UnsafeLvl),
+    lvlToIdx,
+    idxToLvl,
+    lvlZ,
+    sinkLvl,
+    Sinkable (..),
+    sink,
+    mapSink,
+    sinkSize,
+    mapSinkSize,
+    sinkAdd,
+    mapSinkAdd,
+) where
+
+import Data.Coerce   (coerce)
+import Data.Kind     (Constraint, Type)
+import Data.Proxy    (Proxy (..))
+import Unsafe.Coerce (unsafeCoerce)
+
+import DeBruijn.Add
+import DeBruijn.Ctx
+import DeBruijn.Internal.Idx
+import DeBruijn.Internal.Size
+import DeBruijn.Lte
+
+-- $setup
+-- >>> import DeBruijn
+-- >>> import DeBruijn.Lte
+
+-------------------------------------------------------------------------------
+-- de Bruijn levels
+-------------------------------------------------------------------------------
+
+-- | de Bruijn levels.
+type Lvl :: Ctx -> Type
+type role Lvl nominal
+newtype Lvl ctx = UnsafeLvl { _unLvl :: Int }
+  deriving (Eq, Ord)
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance Show (Lvl ctx) where
+    showsPrec d (UnsafeLvl i) = showsPrec d i
+
+-------------------------------------------------------------------------------
+-- Helpers
+-------------------------------------------------------------------------------
+
+-- | Convert level to index.
+--
+-- >>> lvlToIdx S2 (lvlZ S1)
+-- 0
+--
+lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
+lvlToIdx (UnsafeSize ctx) (UnsafeLvl lvl) = UnsafeIdx (ctx - lvl - 1)
+
+idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
+idxToLvl (UnsafeSize ctx) (UnsafeIdx idx) = UnsafeLvl (ctx - idx - 1)
+
+-- | Last level.
+--
+-- >>> lvlZ S1
+-- 1
+--
+-- >>> lvlZ S5
+-- 5
+--
+lvlZ :: Size ctx -> Lvl (S ctx)
+lvlZ (UnsafeSize s) = UnsafeLvl s
+
+-- | Sink 'Lvl' into a larger context.
+--
+-- >>> sinkLvl (lvlZ S3)
+-- 3
+--
+-- >>> sink (lvlZ S3)
+-- 3
+--
+-- >>> mapLvl (LS LZ) (lvlZ S3)
+-- 3
+--
+sinkLvl :: Lvl n -> Lvl (S n)
+sinkLvl = coerce
+
+-------------------------------------------------------------------------------
+-- Sinkable
+-------------------------------------------------------------------------------
+
+-- | Sinkable terms can be weakened (sunk) cheaply.
+type Sinkable :: (Ctx -> Type) -> Constraint
+class Sinkable t where
+    mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'
+
+instance Sinkable Lvl where mapLvl _ = coerce
+instance Sinkable Proxy where mapLvl _ = coerce
+
+-- | Sink term.
+sink :: Sinkable t => t ctx -> t (S ctx)
+sink = unsafeCoerce
+
+-- | Sink term from empty context to a context of given size.
+sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
+sinkSize _ = unsafeCoerce
+
+-- | Essentially @'fmap' 'sink'@
+mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
+mapSink = unsafeCoerce
+
+-- | Essentially @'fmap' . 'sinkSize'@
+mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
+mapSinkSize _ = unsafeCoerce
+
+sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
+sinkAdd _ = unsafeCoerce
+
+mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')
+mapSinkAdd _ = unsafeCoerce
diff --git a/src/DeBruijn/Internal/Size.hs b/src/DeBruijn/Internal/Size.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Internal/Size.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE Unsafe #-}
+module DeBruijn.Internal.Size (
+    Size (SZ, SS, UnsafeSize),
+    unSS,
+    sizeToInt,
+    pattern S1,
+    pattern S2,
+    pattern S3,
+    pattern S4,
+    pattern S5,
+    pattern S6,
+    pattern S7,
+    pattern S8,
+    pattern S9,
+) where
+
+import Data.EqP           (EqP (..))
+import Data.GADT.Compare  (GCompare (..), GEq (..), GOrdering (..))
+import Data.GADT.Show     (GShow (..))
+import Data.Kind          (Type)
+import Data.OrdP          (OrdP (..))
+import Data.Type.Equality (TestEquality (testEquality), (:~:) (Refl))
+import Unsafe.Coerce      (unsafeCoerce)
+
+import DeBruijn.Ctx
+
+-- | Term level witness of the size of a context.
+--
+-- >>> SZ
+-- 0
+--
+-- >>> SS (SS SZ)
+-- 2
+--
+type Size :: Ctx -> Type
+type role Size nominal
+
+newtype Size ctx = UnsafeSize { _sizeToInt :: Int }
+
+-------------------------------------------------------------------------------
+-- Helpers
+-------------------------------------------------------------------------------
+
+-- | Unapply 'SS'. Occasionally more useful than pattern matching.
+unSS :: Size (S ctx) -> Size ctx
+unSS (SS x) = x
+
+-- | Convert 'Size' to 'Int.
+sizeToInt :: Size ctx -> Int
+sizeToInt = _sizeToInt
+
+-------------------------------------------------------------------------------
+-- Instances
+-------------------------------------------------------------------------------
+
+instance Show (Size ctx) where
+    showsPrec d (UnsafeSize i) = showsPrec d i
+
+instance GShow Size where
+    gshowsPrec = showsPrec
+
+instance Eq (Size ctx) where
+    _ == _ = True
+
+instance Ord (Size ctx) where
+    compare _ _ = EQ
+
+instance EqP Size where
+    eqp (UnsafeSize n) (UnsafeSize m) = n == m
+
+instance OrdP Size where
+    comparep (UnsafeSize n) (UnsafeSize m) = compare n m
+
+instance GEq Size where
+    geq (UnsafeSize n) (UnsafeSize m) =
+        if n == m then Just (unsafeCoerce Refl) else Nothing
+
+instance GCompare Size where
+    gcompare (UnsafeSize n) (UnsafeSize m) = case compare n m of
+        LT -> GLT
+        EQ -> unsafeCoerce GEQ
+        GT -> GGT
+
+instance TestEquality Size where
+    testEquality = geq
+
+-------------------------------------------------------------------------------
+-- Pattern synonyms
+-------------------------------------------------------------------------------
+
+-- We need a GADT to implement pattern synonyms.
+type ViewSize :: Ctx -> Type
+type role ViewSize nominal
+data ViewSize ctx where
+    SZ' :: ViewSize EmptyCtx
+    SS' :: Size n -> ViewSize (S n)
+
+viewSize :: Size n -> ViewSize n
+viewSize (UnsafeSize 0) = unsafeCoerce SZ'
+viewSize (UnsafeSize n) = unsafeCoerce (SS' (UnsafeSize (n - 1)))
+
+pattern SZ :: () => (m ~ EmptyCtx) => Size m
+pattern SZ <- (viewSize -> SZ')
+  where SZ = UnsafeSize 0
+
+pattern SS :: () => (m ~ S n) => Size n -> Size m
+pattern SS n <- (viewSize -> SS' n)
+  where SS n = UnsafeSize (_sizeToInt n + 1)
+
+{-# COMPLETE SZ, SS #-}
+
+-------------------------------------------------------------------------------
+-- Sizes
+-------------------------------------------------------------------------------
+
+pattern S1 :: () => (m ~ Ctx1) => Size m
+pattern S1 = SS SZ
+
+pattern S2 :: () => (m ~ Ctx2) => Size m
+pattern S2 = SS S1
+
+pattern S3 :: () => (m ~ Ctx3) => Size m
+pattern S3 = SS S2
+
+pattern S4 :: () => (m ~ Ctx4) => Size m
+pattern S4 = SS S3
+
+pattern S5 :: () => (m ~ Ctx5) => Size m
+pattern S5 = SS S4
+
+pattern S6 :: () => (m ~ Ctx6) => Size m
+pattern S6 = SS S5
+
+pattern S7 :: () => (m ~ Ctx7) => Size m
+pattern S7 = SS S6
+
+pattern S8 :: () => (m ~ Ctx8) => Size m
+pattern S8 = SS S7
+
+pattern S9 :: () => (m ~ Ctx9) => Size m
+pattern S9 = SS S8
diff --git a/src/DeBruijn/Lvl.hs b/src/DeBruijn/Lvl.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Lvl.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE Trustworthy #-}
+module DeBruijn.Lvl (
+    Lvl,
+    lvlToIdx,
+    lvlZ,
+    idxToLvl,
+    -- * Sinking
+    Sinkable (..),
+    sink,
+    sinkSize,
+    sinkAdd,
+    mapSink,
+    mapSinkSize,
+    mapSinkAdd,
+) where
+
+import DeBruijn.Internal.Lvl
diff --git a/src/DeBruijn/RenExtras.hs b/src/DeBruijn/RenExtras.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/RenExtras.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE Trustworthy #-}
+module DeBruijn.RenExtras (
+    weakenUsingSize,
+) where
+
+import DeBruijn.Ctx
+import DeBruijn.Ren
+import DeBruijn.Size
+
+import Unsafe.Coerce (unsafeCoerce)
+
+-- | Weaken closed term to arbitrary context.
+--
+-- Note: this has different requirements than 'sinkSize'.
+weakenUsingSize :: Renamable t => Size ctx -> t EmptyCtx -> t ctx
+weakenUsingSize _ = unsafeCoerce
diff --git a/src/DeBruijn/Size.hs b/src/DeBruijn/Size.hs
new file mode 100644
--- /dev/null
+++ b/src/DeBruijn/Size.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE Trustworthy #-}
+module DeBruijn.Size (
+    Size (SZ, SS),
+    unSS,
+    sizeToInt,
+    -- * Common sizes
+    pattern S1,
+    pattern S2,
+    pattern S3,
+    pattern S4,
+    pattern S5,
+    pattern S6,
+    pattern S7,
+    pattern S8,
+    pattern S9,
+) where
+
+import DeBruijn.Internal.Size