diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,10 @@
+# 0.3.0.0
+
+- More new functions, thanks to isovector
+
 # 0.2.0.0
 
-- A whole bunch of basic functions, thanks to @isovector
+- A whole bunch of basic functions, thanks to isovector
 - Remove `Traverse` (now `Map`), `BimapPair`, `BimapEither` (now `Bimap`)
 
 # 0.1.0.0
diff --git a/first-class-families.cabal b/first-class-families.cabal
--- a/first-class-families.cabal
+++ b/first-class-families.cabal
@@ -1,5 +1,5 @@
 name:                first-class-families
-version:             0.2.0.0
+version:             0.3.0.0
 synopsis:
   First class type families
 description:
diff --git a/src/Fcf.hs b/src/Fcf.hs
--- a/src/Fcf.hs
+++ b/src/Fcf.hs
@@ -28,11 +28,22 @@
 --
 -- - Fcfs can be higher-order.
 -- - The kind constructor 'Exp' is a monad: there's @('=<<')@ and 'Pure'.
+--
+-- Essential language extensions for "Fcf":
+--
+-- > {-# LANGUAGE
+-- >     DataKinds,
+-- >     PolyKinds,
+-- >     TypeFamilies,
+-- >     TypeInType,
+-- >     TypeOperators,
+-- >     UndecidableInstances #-}
 
 module Fcf where
 
 import Data.Kind (Type, Constraint)
-import GHC.TypeLits (Symbol, Nat, type (+), TypeError, ErrorMessage(..))
+import GHC.TypeLits (Symbol, Nat, TypeError, ErrorMessage(..))
+import qualified GHC.TypeLits as TL
 
 -- * First-class type families
 
@@ -86,10 +97,6 @@
 type instance Eval (UnEither f g ('Left  x)) = Eval (f x)
 type instance Eval (UnEither f g ('Right y)) = Eval (g y)
 
-data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
-type instance Eval (UnMaybe y f 'Nothing) = Eval y
-type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)
-
 data ConstFn :: a -> b -> Exp a
 type instance Eval (ConstFn a _b) = a
 
@@ -142,7 +149,7 @@
 
 data Length :: [a] -> Exp Nat
 type instance Eval (Length '[]) = 0
-type instance Eval (Length (a ': as)) = 1 + Eval (Length as)
+type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
 
 data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
 type instance Eval (Find _p '[]) = 'Nothing
@@ -151,13 +158,32 @@
     ('Just a)
     (Eval (Find p as))
 
--- |
+-- | Find the index of an element satisfying the predicate.
+data FindIndex :: (a -> Exp Bool) -> [a] -> Exp (Maybe Nat)
+type instance Eval (FindIndex _p '[]) = 'Nothing
+type instance Eval (FindIndex p (a ': as)) =
+  Eval (If (Eval (p a))
+    (Pure ('Just 0))
+    (Map ((+) 1) =<< FindIndex p as))
+
+-- | Find an element associated with a key.
 -- @
 -- 'Lookup' :: k -> [(k, b)] -> 'Exp' ('Maybe' b)
 -- @
 type Lookup (a :: k) (as :: [(k, b)]) =
   (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
 
+-- | Modify an element at a given index.
+--
+-- The list is unchanged if the index is out of bounds.
+data SetIndex :: Nat -> a -> [a] -> Exp [a]
+type instance Eval (SetIndex n a' as) = SetIndexImpl n a' as
+
+type family SetIndexImpl (n :: Nat) (a' :: k) (as :: [k]) where
+  SetIndexImpl _n _a' '[] = '[]
+  SetIndexImpl 0 a' (_a ': as) = a' ': as
+  SetIndexImpl n a' (a ': as) = a ': SetIndexImpl (n TL.- 1) a' as
+
 data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
 type instance Eval (ZipWith _f '[] _bs) = '[]
 type instance Eval (ZipWith _f _as '[]) = '[]
@@ -176,6 +202,34 @@
 data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
 type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
 
+-- ** Maybe
+
+data UnMaybe :: Exp b -> (a -> Exp b) -> Maybe a -> Exp b
+type instance Eval (UnMaybe y f 'Nothing) = Eval y
+type instance Eval (UnMaybe y f ('Just x)) = Eval (f x)
+
+data FromMaybe :: k -> Maybe k -> Exp k
+type instance Eval (FromMaybe a 'Nothing)   = a
+type instance Eval (FromMaybe _a ('Just b)) = b
+
+data IsJust :: Maybe a -> Exp Bool
+type instance Eval (IsJust ('Just _a)) = 'True
+type instance Eval (IsJust 'Nothing) = 'False
+
+data IsNothing :: Maybe a -> Exp Bool
+type instance Eval (IsNothing ('Just _a)) = 'False
+type instance Eval (IsNothing 'Nothing) = 'True
+
+-- ** Either
+
+data IsLeft :: Either a b -> Exp Bool
+type instance Eval (IsLeft ('Left _a)) = 'True
+type instance Eval (IsLeft ('Right _a)) = 'False
+
+data IsRight :: Either a b -> Exp Bool
+type instance Eval (IsRight ('Left _a)) = 'False
+type instance Eval (IsRight ('Right _a)) = 'True
+
 -- ** Overloaded functions
 
 -- | Type-level 'fmap' for type-level functors.
@@ -206,6 +260,8 @@
 type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))
 type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
 
+-- ** Bool
+
 -- | N.B.: The order of the two branches is the opposite of "if":
 -- @UnBool ifFalse ifTrue bool@.
 --
@@ -219,8 +275,6 @@
 type instance Eval (UnBool fal tru 'False) = Eval fal
 type instance Eval (UnBool fal tru 'True ) = Eval tru
 
--- ** Primitives
-
 infixr 2 ||
 infixr 3 &&
 
@@ -236,6 +290,24 @@
 type instance Eval ('True && b) = b
 type instance Eval (a && 'True) = a
 
+data Not :: Bool -> Exp Bool
+type instance Eval (Not 'True)  = 'False
+type instance Eval (Not 'False) = 'True
+
+-- ** Nat
+
+data (+) :: Nat -> Nat -> Exp Nat
+type instance Eval ((+) a b) = a TL.+ b
+
+data (-) :: Nat -> Nat -> Exp Nat
+type instance Eval ((-) a b) = a TL.- b
+
+data (*) :: Nat -> Nat -> Exp Nat
+type instance Eval ((*) a b) = a TL.* b
+
+data (^) :: Nat -> Nat -> Exp Nat
+type instance Eval ((^) a b) = a TL.^ b
+
 -- ** Other
 
 data Error :: Symbol -> Exp a
@@ -253,8 +325,14 @@
   TyEqImpl a b = 'False
 
 infixr 0 $
+
+-- | Note that this denotes the identity function, so @($) f@ can usually be
+-- replaced with @f@.
 data ($) :: (a -> Exp b) -> a -> Exp b
 type instance Eval (($) f a) = Eval (f a)
+
+-- | A stuck type that can be used like a type-level 'undefined'.
+type family Stuck :: a
 
 -- * Helpful shorthands