diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,13 +1,34 @@
+# 0.8.0.0
+
+- Add modules
+    + `Fcf.Data.Symbol` (currently just reexports `Symbol`) (thanks to gspia)
+    + `Fcf.Data.Function`
+    + "Overloaded type families" ("type-level type classes")
+        * `Fcf.Class.Ord`
+        * `Fcf.Class.Monoid`
+        * `Fcf.Class.Monoid.Types` (which exports just an `Endo a` to wrap `a -> Exp a`)
+        * `Fcf.Class.Functor`
+        * `Fcf.Class.Bifunctor`
+        * `Fcf.Class.Foldable`
+
+- Add functions in `Fcf.Data.List`:
+  `Intersperse`, `Intercalate`, `Span`, `Break`, `Tails`, `IsPrefixOf`,
+  `IsSuffixOf`, `IsInfixOf`, `Partition`.
+- Generalize `Foldr`, `Concat` and `ConcatMap` to foldable types.
+
+- Remove deprecated `Guarded`, `Guard((:=))`, `Otherwise`.
+- Deprecate `Fcf.Classes`
+
 # 0.7.0.0
 
 - Add `Unfoldr`, `Concat`, `ConcatMap`, `Replicate`, `Take`, `Drop`,
-  `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (gspia)
+  `TakeWhile`, `DropWhile`, `Reverse` to `Data.List`. (thanks to gspia)
 - Change `Elem`, `Lookup`, `Zip` to be `data` instead of `type` synonyms.
 - Fix performance of `Filter` and `Find`.
 
 # 0.6.0.0
 
-- Add `Fcf.Utils.Case` and `(Fcf.Combinators.>>=)` (TheMatten)
+- Add `Fcf.Utils.Case` and `(Fcf.Combinators.>>=)` (thanks to TheMatten)
 - Deprecate `Fcf.Bool.Guarded`
 - GHC 8.8 compatibility
 
@@ -24,7 +45,7 @@
 
 # 0.4.0.0
 
-- New functions (blmage)
+- New functions (thanks to blmage)
 
     + `LiftM`, `LiftM2`, `LiftM3`
     + `(<=)`, `(>=)`, `(<)`, `(>)`
@@ -36,11 +57,11 @@
 
 # 0.3.0.0
 
-- More new functions, (isovector)
+- More new functions, (thanks to isovector)
 
 # 0.2.0.0
 
-- A whole bunch of basic functions (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/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,21 @@
 # First-class type families [![Hackage](https://img.shields.io/hackage/v/first-class-families.svg)](https://hackage.haskell.org/package/first-class-families) [![Build Status](https://travis-ci.org/Lysxia/first-class-families.svg)](https://travis-ci.org/Lysxia/first-class-families)
 
+First-class type families are type-level functions that can be
+composed using higher-order functions.
+
+The core of the idea is an extensible kind of "type-level expressions"
+and an open type family for evaluating such expressions.
+
+```haskell
+type Exp (k :: Type) :: Type
+type family Eval (e :: Exp k) :: k
+```
+
+This library provides that core foundation,
+and also exports basic first-class type families.
+
+## Example
+
 For example, consider this simple type family:
 
 ```haskell
@@ -38,9 +54,49 @@
     UndecidableInstances #-}
 ```
 
+## Overview
+
+- `Fcf.Core`: definition of `Exp` and `Eval`.
+- `Fcf.Combinators`: general combinators to compose first-class families.
+- `Fcf.Data.*`: first-class families on common data types.
+- `Fcf.Class.*`: overloaded first-class families.
+- `Fcf.Utils`: miscellaneous.
+
+The top-level module `Fcf` is a prelude to get acquainted with the library.
+For regular use, import what you need from the specialized modules
+above, preferably with explicit import lists.
+
+```haskell
+import Fcf                       -- Simple but fragile
+
+import Fcf.Class.Functor (FMap)  -- Explicit and robust
+```
+
+## Features
+
+### Overloaded type families
+
+Value-level functions can be overloaded using type classes.
+Type families---type-level functions---are open by design,
+so overloading is as easy as just declaring them with more general types.
+
+```haskell
+data Map :: (a -> Exp b) -> f a -> Exp (f b)
+
+-- Instances for f = []
+type instance Eval (Map f '[]) = '[]
+type instance Eval (Map f (x ': xs)) = Eval (f x) ': Eval (Map f xs)
+
+-- Instances for f = Maybe
+type instance Eval (Map f 'Nothing) = 'Nothing
+type instance Eval (Map f ('Just x)) = 'Just (Eval (f x))
+```
+
 ## See also
 
-[Haskell with only one type family](http://blog.poisson.chat/posts/2018-08-06-one-type-family.html) (blogpost)
+- [Haskell with only one type family](http://blog.poisson.chat/posts/2018-08-06-one-type-family.html)
+- [Overloaded type families](https://blog.poisson.chat/posts/2018-09-29-overloaded-families.html)
+- [The *singletons* library](https://hackage.haskell.org/package/singletons)
 
 ---
 
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.7.0.0
+version:             0.8.0.0
 synopsis:
   First class type families
 description:
@@ -28,9 +28,17 @@
     Fcf.Combinators
     Fcf.Data.Bool
     Fcf.Data.Common
+    Fcf.Data.Function
     Fcf.Data.List
     Fcf.Data.Nat
+    Fcf.Data.Symbol
     Fcf.Classes
+    Fcf.Class.Bifunctor
+    Fcf.Class.Foldable
+    Fcf.Class.Functor
+    Fcf.Class.Monoid
+    Fcf.Class.Monoid.Types
+    Fcf.Class.Ord
     Fcf.Utils
   build-depends:
     -- This upper bound is conservative.
diff --git a/src/Fcf.hs b/src/Fcf.hs
--- a/src/Fcf.hs
+++ b/src/Fcf.hs
@@ -104,12 +104,6 @@
   , type (&&)
   , Not
 
-    -- *** Multi-way if
-
-  , Guarded
-  , Guard((:=))
-  , Otherwise
-
     -- ** Case splitting
 
   , Case
@@ -152,5 +146,6 @@
 import Fcf.Data.Common
 import Fcf.Data.List
 import Fcf.Data.Nat
-import Fcf.Classes
+import Fcf.Class.Functor
+import Fcf.Class.Bifunctor
 import Fcf.Utils
diff --git a/src/Fcf/Class/Bifunctor.hs b/src/Fcf/Class/Bifunctor.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Bifunctor.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Bifunctors.
+--
+-- Bifunctors are "two-argument functors".
+--
+-- This module is the type-level equivalent of "Data.Bifunctor".
+module Fcf.Class.Bifunctor
+  ( Bimap
+  , First
+  , Second
+  ) where
+
+import Fcf.Core (Exp, Eval)
+import Fcf.Combinators (Pure)
+
+-- $setup
+-- >>> import Fcf.Combinators (Flip)
+-- >>> import Fcf.Data.Nat (Nat, type (+), type (-))
+-- >>> import Fcf.Data.Symbol (Symbol)
+
+-- | Type-level 'Data.Bifunctor.bimap'.
+--
+-- >>> :kind! Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4))
+-- Eval (Bimap ((+) 1) (Flip (-) 1) '(2, 4)) :: (Nat, Nat)
+-- = '(3, 3)
+data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
+
+-- (,)
+type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))
+
+-- Either
+type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))
+type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
+
+
+-- | Type-level 'Data.Bifunctor.first'.
+-- Apply a function along the first parameter of a bifunctor.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (First ((+) 1) '(3,"a"))
+-- Eval (First ((+) 1) '(3,"a")) :: (Nat, Symbol)
+-- = '(4, "a")
+data First :: (a -> Exp b) -> f a c -> Exp (f b c)
+type instance Eval (First f x) = Eval (Bimap f Pure x)
+
+-- | Type-level 'Data.Bifunctor.second'.
+-- Apply a function along the second parameter of a bifunctor.
+--
+-- This is generally equivalent to 'Data.Functor.Map'.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Second ((+) 1) '("a",3))
+-- Eval (Second ((+) 1) '("a",3)) :: (Symbol, Nat)
+-- = '("a", 4)
+data Second :: (c -> Exp d) -> f a c -> Exp (f a d)
+type instance Eval (Second g x) = Eval (Bimap Pure g x)
diff --git a/src/Fcf/Class/Foldable.hs b/src/Fcf/Class/Foldable.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Foldable.hs
@@ -0,0 +1,233 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Foldable types.
+--
+-- A minimal implementation of this interface is given by either 'FoldMap' or
+-- 'Foldr', but a default still needs to be given explicitly for the other.
+--
+-- @
+-- data MyType a = ... {- Some custom Foldable type -}
+--
+-- -- Method 1: Implement Foldr, default FoldMap.
+-- type instance 'Eval' ('Foldr' f y xs) = ... {- Explicit implementation -}
+-- type instance 'Eval' ('FoldMap' f xs) = 'FoldMapDefault_' f xs {- Default -}
+--
+-- -- Method 2: Implement FoldMap, default Foldr.
+-- type instance 'Eval' ('FoldMap' f xs) = ... {- Explicit implementation -}
+-- type instance 'Eval' ('Foldr' f y xs) = 'FoldrDefault_' f y xs {- Default -}
+-- @
+module Fcf.Class.Foldable
+  ( -- * Core interface
+    Foldr
+  , FoldMap
+
+    -- ** Default implementations
+  , FoldMapDefault_
+  , FoldrDefault_
+
+    -- * Derived operations
+
+    -- ** Predicates
+  , And
+  , Or
+  , All
+  , Any
+
+    -- ** Numbers
+  , Sum
+
+    -- ** Lists
+  , Concat
+  , ConcatMap
+  ) where
+
+import Fcf.Core (Exp, Eval)
+import Fcf.Combinators (Pure, Pure1, type (<=<))
+import Fcf.Data.Function (Bicomap)
+import Fcf.Class.Monoid
+import Fcf.Class.Monoid.Types (Endo(..), UnEndo)
+import Fcf.Data.Bool (type (&&), type (||))
+import Fcf.Data.Nat (Nat, type (+))
+
+-- $setup
+-- >>> import Fcf.Combinators (Flip)
+-- >>> import Fcf.Class.Ord (type (<))
+
+-- | Type-level 'Data.Foldable.foldMap'.
+data FoldMap :: (a -> Exp m) -> t a -> Exp m
+
+-- List
+type instance Eval (FoldMap f '[]) = MEmpty
+type instance Eval (FoldMap f (x ': xs)) = Eval (f x) <> Eval (FoldMap f xs)
+
+-- Maybe
+type instance Eval (FoldMap f 'Nothing) = MEmpty
+type instance Eval (FoldMap f ('Just x)) = Eval (f x)
+
+-- Either
+type instance Eval (FoldMap f ('Left _a)) = MEmpty
+type instance Eval (FoldMap f ('Right x)) = Eval (f x)
+
+-- | Default implementation of 'FoldMap'.
+--
+-- === __Usage__
+--
+-- To define an instance of 'FoldMap' for a custom @MyType@ for which you already have
+-- an instance of 'Foldr':
+--
+-- @
+-- type instance 'Eval' ('FoldMap' f (xs :: MyType a)) = 'FoldMapDefault_' f xs
+-- @
+--
+-- ==== __Example__
+--
+-- >>> :kind! FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ]
+-- FoldMapDefault_ Pure '[ 'EQ, 'LT, 'GT ] :: Ordering
+-- = 'LT
+type FoldMapDefault_ f xs = Eval (Foldr (Bicomap f Pure (.<>)) MEmpty xs)
+
+-- | Default implementation of 'Foldr'.
+--
+-- === __Usage__
+--
+-- To define an instance of 'Foldr' for a custom @MyType@ for which you already
+-- have an instance of 'FoldMap':
+--
+-- @
+-- type instance 'Eval' ('Foldr' f y (xs :: MyType a)) = 'FoldrDefault_' f y xs
+-- @
+--
+-- ==== __Example__
+--
+-- >>> :kind! FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ]
+-- FoldrDefault_ (.<>) 'EQ '[ 'EQ, 'LT, 'GT ] :: Ordering
+-- = 'LT
+type FoldrDefault_ f y xs = Eval (UnEndo (Eval (FoldMap (Pure1 'Endo <=< Pure1 f) xs)) y)
+
+-- | Right fold.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
+-- Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
+-- = 10
+data Foldr :: (a -> b -> Exp b) -> b -> t a -> Exp b
+
+-- List
+type instance Eval (Foldr f y '[]) = y
+type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))
+
+-- Maybe
+type instance Eval (Foldr f y 'Nothing) = y
+type instance Eval (Foldr f y ('Just x)) = Eval (f x y)
+
+-- Either
+type instance Eval (Foldr f y ('Left _a)) = y
+type instance Eval (Foldr f y ('Right x)) = Eval (f x y)
+
+-- * Derived operations
+
+-- | Give @True@ if all of the booleans in the list are @True@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (And '[ 'True, 'True])
+-- Eval (And '[ 'True, 'True]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (And '[ 'True, 'True, 'False])
+-- Eval (And '[ 'True, 'True, 'False]) :: Bool
+-- = 'False
+data And :: t Bool -> Exp Bool
+type instance Eval (And lst) = Eval (Foldr (&&) 'True lst)
+
+-- | Whether all elements of the list satisfy a predicate.
+--
+-- Note: this identifier conflicts with 'Data.Monoid.All' (from "Data.Monoid").
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (All (Flip (<) 6) '[0,1,2,3,4,5])
+-- Eval (All (Flip (<) 6) '[0,1,2,3,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (All (Flip (<) 5) '[0,1,2,3,4,5])
+-- Eval (All (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
+-- = 'False
+data All :: (a -> Exp Bool) -> t a -> Exp Bool
+type instance Eval (All p lst) = Eval (Foldr (Bicomap p Pure (&&)) 'True lst)
+
+
+-- | Give @True@ if any of the booleans in the list are @True@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Or '[ 'True, 'True])
+-- Eval (Or '[ 'True, 'True]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (Or '[ 'False, 'False])
+-- Eval (Or '[ 'False, 'False]) :: Bool
+-- = 'False
+data Or :: t Bool -> Exp Bool
+type instance Eval (Or lst) = Eval (Foldr (||) 'False lst)
+
+
+-- | Whether any element of the list satisfies a predicate.
+--
+-- Note: this identifier conflicts with 'Fcf.Utils.Any' (from "Fcf.Utils"),
+-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Any (Flip (<) 5) '[0,1,2,3,4,5])
+-- Eval (Any (Flip (<) 5) '[0,1,2,3,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (Any (Flip (<) 0) '[0,1,2,3,4,5])
+-- Eval (Any (Flip (<) 0) '[0,1,2,3,4,5]) :: Bool
+-- = 'False
+data Any :: (a -> Exp Bool) -> t a -> Exp Bool
+type instance Eval (Any p lst) = Eval (Foldr (Bicomap p Pure (||)) 'False lst)
+
+
+-- | Sum a @Nat@-list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Sum '[1,2,3])
+-- Eval (Sum '[1,2,3]) :: Nat
+-- = 6
+data Sum :: t Nat -> Exp Nat
+type instance Eval (Sum ns) = Eval (Foldr (+) 0 ns)
+
+
+-- | Concatenate a collection of elements from a monoid.
+--
+-- === __Example__
+--
+-- For example, fold a list of lists.
+--
+-- > Concat :: [[a]] -> Exp [a]
+--
+-- >>> :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
+-- Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
+-- = '[1, 2, 3, 4, 5, 6]
+-- >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
+-- Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
+-- = '[Int, Maybe Int, Maybe String, Either Double Int]
+--
+data Concat :: t m -> Exp m
+type instance Eval (Concat xs) = Eval (FoldMap Pure xs)
+
+-- | Map a function and concatenate the results.
+--
+-- This is 'FoldMap' specialized to the list monoid.
+data ConcatMap :: (a -> Exp [b]) -> t a -> Exp [b]
+type instance Eval (ConcatMap f xs) = Eval (FoldMap f xs)
diff --git a/src/Fcf/Class/Functor.hs b/src/Fcf/Class/Functor.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Functor.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+module Fcf.Class.Functor
+  ( Map
+  , FMap
+  ) where
+
+import Fcf.Core (Exp, Eval)
+
+-- | Type-level 'fmap' for type-level functors.
+--
+-- Note: this name clashes with 'Data.Map.Lazy.Map' from /containers/.
+-- 'FMap' is provided as a synonym to avoid this.
+--
+-- === __Example__
+--
+-- >>> import Fcf.Data.Nat
+-- >>> import qualified GHC.TypeLits as TL
+-- >>> data AddMul :: Nat -> Nat -> Exp Nat
+-- >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
+-- >>> :kind! Eval (Map (AddMul 2) '[0, 1, 2, 3, 4])
+-- Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]
+-- = '[4, 9, 16, 25, 36]
+data Map :: (a -> Exp b) -> f a -> Exp (f b)
+
+-- | Synonym of 'Map' to avoid name clashes.
+type FMap = Map
+
+-- []
+type instance Eval (Map f '[]) = '[]
+type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
+
+-- Maybe
+type instance Eval (Map f 'Nothing) = 'Nothing
+type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))
+
+-- Either
+type instance Eval (Map f ('Left x)) = 'Left x
+type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))
+
+-- Tuples
+type instance Eval (Map f '(x, a)) =
+  '(x, Eval (f a))
+type instance Eval (Map f '(x, y, a)) =
+  '(x, y, Eval (f a))
+type instance Eval (Map f '(x, y, z, a)) =
+  '(x, y, z, Eval (f a))
+type instance Eval (Map f '(x, y, z, w, a)) =
+  '(x, y, z, w, Eval (f a))
diff --git a/src/Fcf/Class/Monoid.hs b/src/Fcf/Class/Monoid.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Monoid.hs
@@ -0,0 +1,128 @@
+{-# LANGUAGE
+    CPP,
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Semigroups and monoids.
+module Fcf.Class.Monoid
+  ( -- * Pure type families
+    -- | Nicer to use when applied explicitly.
+    type (<>)
+  , MEmpty
+
+    -- * First-class families
+    -- | Can be composed and passed to higher-order functions.
+  , type (.<>)
+  , MEmpty_
+  ) where
+
+import Fcf.Core (Exp, Eval)
+import Data.Monoid (All(..), Any(..))
+import Data.Type.Bool (type (&&), type (||))
+
+#if __GLASGOW_HASKELL__ >= 802
+import GHC.TypeLits (AppendSymbol)
+#endif
+
+-- $setup
+-- >>> import GHC.TypeLits (Nat)
+
+-- | Type-level semigroup composition @('Data.Semigroup.<>')@.
+--
+-- This is the fcf-encoding of @('<>')@.
+-- To define a new semigroup, add type instances to @('<>')@.
+data (.<>) :: a -> a -> Exp a
+type instance Eval (x .<> y) = x <> y
+
+-- | Type-level semigroup composition @('Data.Semigroup.<>')@.
+type family (<>) (x :: a) (y :: a) :: a
+
+-- (,)
+type instance (<>) '(a1, a2) '(b1, b2) = '(a1 <> b1, a2 <> b2)
+
+-- (,,)
+type instance (<>) '(a1, a2, a3) '(b1, b2, b3) = '(a1 <> b1, a2 <> b2, a3 <> b3)
+
+-- List
+type instance (<>) '[] ys = ys
+type instance (<>) (x ': xs) ys = x ': (<>) xs ys
+
+-- Maybe
+type instance (<>) 'Nothing b = b
+type instance (<>) a 'Nothing = a
+type instance (<>) ('Just a) ('Just b) = 'Just (a <> b)
+
+-- Ordering
+type instance (<>) 'EQ b = b
+type instance (<>) a 'EQ = a
+type instance (<>) 'LT _b = 'LT
+type instance (<>) 'GT _b = 'GT
+
+-- ()
+type instance (<>) _a _b = '()
+
+-- All
+type instance (<>) ('All a) ('All b) = 'All (a && b)
+
+-- Any
+type instance (<>) ('Any a) ('Any b) = 'Any (a || b)
+
+#if __GLASGOW_HASKELL__ >= 802
+-- Symbol
+-- | With /base >= 4.10.0.0/.
+type instance (<>) x y = AppendSymbol x y
+#endif
+
+-- | Type-level monoid identity 'Data.Monoid.mempty'.
+--
+-- This is the fcf-encoding of 'MEmpty'.
+data MEmpty_ :: Exp a
+type instance Eval MEmpty_ = MEmpty
+
+-- | Type-level monoid identity 'Data.Monoid.mempty'.
+--
+-- === __Examples__
+--
+-- >>> :kind! 'LT <> MEmpty
+-- 'LT <> MEmpty :: Ordering
+-- = 'LT
+--
+-- >>> :kind! MEmpty <> '( 'EQ, '[1, 2])
+-- MEmpty <> '( 'EQ, '[1, 2]) :: (Ordering, [Nat])
+-- = '( 'EQ, '[1, 2])
+--
+-- >>> :kind! '( 'GT, 'Just '()) <> MEmpty
+-- '( 'GT, 'Just '()) <> MEmpty :: (Ordering, Maybe ())
+-- = '( 'GT, 'Just '())
+type family MEmpty :: a
+
+-- (,)
+type instance MEmpty = '(MEmpty, MEmpty)
+
+-- (,,)
+type instance MEmpty = '(MEmpty, MEmpty, MEmpty)
+
+-- List
+type instance MEmpty = '[]
+
+-- Maybe
+type instance MEmpty = 'Nothing
+
+-- Ordering
+type instance MEmpty = 'EQ
+
+-- ()
+type instance MEmpty = '()
+
+-- All
+type instance MEmpty = 'All 'True
+
+-- Any
+type instance MEmpty = 'Any 'False
+
+-- Symbol
+type instance MEmpty = ""
diff --git a/src/Fcf/Class/Monoid/Types.hs b/src/Fcf/Class/Monoid/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Monoid/Types.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Carriers of useful monoid instances.
+module Fcf.Class.Monoid.Types
+  ( -- * Endo
+    Endo(..)
+  , UnEndo
+  ) where
+
+import Fcf.Core (Exp)
+import Fcf.Combinators (Pure, type (<=<))
+import Fcf.Class.Monoid
+
+-- | Endofunctions.
+--
+-- === __Details__
+--
+-- This is is used in the default implementation of
+-- 'Fcf.Class.Foldable.Foldr' in terms of
+-- 'Fcf.Class.Foldable.FoldMap'.
+newtype Endo a = Endo (a -> Exp a)
+
+-- | Inverse of the 'Endo' constructor.
+type family UnEndo (e :: Endo a) :: a -> Exp a where
+  UnEndo ('Endo f) = f
+
+-- * Endo as a monoid
+--
+-- Note it is only a monoid up to 'Eval'.
+
+type instance 'Endo f <> 'Endo g = 'Endo (f <=< g)
+type instance MEmpty = 'Endo Pure
diff --git a/src/Fcf/Class/Ord.hs b/src/Fcf/Class/Ord.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Class/Ord.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Equality and ordering.
+--
+-- Note that equality doesn't really require a class,
+-- it can be defined uniformly as 'TyEq'.
+module Fcf.Class.Ord
+  ( -- * Order
+    Compare
+  , type (<=)
+  , type (>=)
+  , type (<)
+  , type (>)
+
+    -- * Equality
+  , TyEq
+  ) where
+
+import qualified GHC.TypeLits as TL
+
+import Fcf.Core
+import Fcf.Class.Monoid (type (<>))  -- Semigroup Ordering
+import Fcf.Data.Bool (Not)
+import Fcf.Utils (TyEq)
+
+-- | Type-level 'compare' for totally ordered data types.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Compare "a" "b")
+-- Eval (Compare "a" "b") :: Ordering
+-- = 'LT
+--
+-- >>> :kind! Eval (Compare '[1, 2, 3] '[1, 2, 3])
+-- Eval (Compare '[1, 2, 3] '[1, 2, 3]) :: Ordering
+-- = 'EQ
+--
+-- >>> :kind! Eval (Compare '[1, 3] '[1, 2])
+-- Eval (Compare '[1, 3] '[1, 2]) :: Ordering
+-- = 'GT
+data Compare :: a -> a -> Exp Ordering
+
+-- (,)
+type instance Eval (Compare '(a1, a2) '(b1, b2)) = Eval (Compare a1 b1) <> Eval (Compare a2 b2)
+
+-- (,,)
+type instance Eval (Compare '(a1, a2, a3) '(b1, b2, b3))
+  = Eval (Compare a1 b1) <> Eval (Compare a2 b2) <> Eval (Compare a3 b3)
+
+-- Either
+type instance Eval (Compare ('Left a) ('Left b)) = Eval (Compare a b)
+type instance Eval (Compare ('Right a) ('Right b)) = Eval (Compare a b)
+type instance Eval (Compare ('Left _a) ('Right _b)) = 'LT
+type instance Eval (Compare ('Right _a) ('Left _b)) = 'GT
+
+-- Maybe
+type instance Eval (Compare 'Nothing 'Nothing) = 'EQ
+type instance Eval (Compare ('Just a) ('Just b)) = Eval (Compare a b)
+type instance Eval (Compare 'Nothing ('Just _b)) = 'LT
+type instance Eval (Compare ('Just _a) 'Nothing) = 'GT
+
+-- List
+type instance Eval (Compare '[] '[]) = 'EQ
+type instance Eval (Compare (x ': xs) (y ': ys)) = Eval (Compare x y) <> Eval (Compare xs ys)
+type instance Eval (Compare '[] (_y ': _ys)) = 'LT
+type instance Eval (Compare (_x ': _xs) '[]) = 'GT
+
+-- Bool
+type instance Eval (Compare (a :: Bool) a) = 'EQ
+type instance Eval (Compare 'False 'True) = 'GT
+type instance Eval (Compare 'True 'False) = 'GT
+
+-- Ordering
+type instance Eval (Compare (a :: Ordering) a) = 'EQ
+type instance Eval (Compare 'LT 'EQ) = 'LT
+type instance Eval (Compare 'LT 'GT) = 'LT
+type instance Eval (Compare 'EQ 'GT) = 'LT
+type instance Eval (Compare 'EQ 'LT) = 'GT
+type instance Eval (Compare 'GT 'LT) = 'GT
+type instance Eval (Compare 'GT 'EQ) = 'GT
+
+-- Symbol
+type instance Eval (Compare a b) = TL.CmpSymbol a b
+
+-- Nat
+type instance Eval (Compare a b) = TL.CmpNat a b
+
+-- ()
+type instance Eval (Compare (a :: ()) b) = 'EQ
+
+-- * Derived operations
+
+-- Asymmetric comparison operators @Exp a -> a -> Bool@.
+type a ~== b = Eval (TyEq (Eval a) b)
+type a ~/= b = Eval (Not (a ~== b))
+
+-- | "Smaller than or equal to". Type-level version of @('<=')@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ("b" <= "a")
+-- Eval ("b" <= "a") :: Bool
+-- = 'False
+data (<=) :: a -> a -> Exp Bool
+type instance Eval ((<=) a b) = Compare a b ~/= 'GT
+
+-- | "Greater than or equal to". Type-level version of @('>=')@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ("b" >= "a")
+-- Eval ("b" >= "a") :: Bool
+-- = 'True
+data (>=) :: a -> a -> Exp Bool
+type instance Eval ((>=) a b) = Compare a b ~/= 'LT
+
+-- | "Smaller than". Type-level version of @('<')@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ("a" < "b")
+-- Eval ("a" < "b") :: Bool
+-- = 'True
+data (<) :: a -> a -> Exp Bool
+type instance Eval ((<) a b) = Compare a b ~== 'LT
+
+-- | "Greater than". Type-level version of @('>')@.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ("b" > "a")
+-- Eval ("b" > "a") :: Bool
+-- = 'True
+data (>) :: a -> a -> Exp Bool
+type instance Eval ((>) a b) = Compare a b ~== 'GT
diff --git a/src/Fcf/Classes.hs b/src/Fcf/Classes.hs
--- a/src/Fcf/Classes.hs
+++ b/src/Fcf/Classes.hs
@@ -1,65 +1,12 @@
 {-# LANGUAGE
-    DataKinds,
-    PolyKinds,
-    TypeFamilies,
-    TypeInType,
     TypeOperators #-}
 
 -- | Overloaded functions.
 module Fcf.Classes
+  {-# DEPRECATED "Use Fcf.Class.Functor or Fcf.Class.Bifunctor instead." #-}
   ( Map
   , Bimap
   ) where
 
-
-import Fcf.Core
-
-
--- $
--- >>> import Fcf.Core
-
-
--- | Type-level 'fmap' for type-level functors.
---
--- === __Example__
---
--- >>> import Fcf.Data.Nat
--- >>> import qualified GHC.TypeLits as TL
--- >>> data AddMul :: Nat -> Nat -> Exp Nat
--- >>> type instance Eval (AddMul x y) = (x TL.+ y) TL.* (x TL.+ y)
--- >>> :kind! Eval (Map (AddMul 2) '[0, 1, 2, 3, 4])
--- Eval (Map (AddMul 2) '[0, 1, 2, 3, 4]) :: [Nat]
--- = '[4, 9, 16, 25, 36]
-data Map :: (a -> Exp b) -> f a -> Exp (f b)
-
--- []
-type instance Eval (Map f '[]) = '[]
-type instance Eval (Map f (a ': as)) = Eval (f a) ': Eval (Map f as)
-
--- Maybe
-type instance Eval (Map f 'Nothing) = 'Nothing
-type instance Eval (Map f ('Just a)) = 'Just (Eval (f a))
-
--- Either
-type instance Eval (Map f ('Left x)) = 'Left x
-type instance Eval (Map f ('Right a)) = 'Right (Eval (f a))
-
--- Tuples
-type instance Eval (Map f '(x, a)) =
-  '(x, Eval (f a))
-type instance Eval (Map f '(x, y, a)) =
-  '(x, y, Eval (f a))
-type instance Eval (Map f '(x, y, z, a)) =
-  '(x, y, z, Eval (f a))
-type instance Eval (Map f '(x, y, z, w, a)) =
-  '(x, y, z, w, Eval (f a))
-
--- | Type-level 'Data.Bifunctor.bimap'.
-data Bimap :: (a -> Exp a') -> (b -> Exp b') -> f a b -> Exp (f a' b')
-
--- (,)
-type instance Eval (Bimap f g '(x, y)) = '(Eval (f x), Eval (g y))
-
--- Either
-type instance Eval (Bimap f g ('Left  x)) = 'Left  (Eval (f x))
-type instance Eval (Bimap f g ('Right y)) = 'Right (Eval (g y))
+import Fcf.Class.Functor
+import Fcf.Class.Bifunctor
diff --git a/src/Fcf/Combinators.hs b/src/Fcf/Combinators.hs
--- a/src/Fcf/Combinators.hs
+++ b/src/Fcf/Combinators.hs
@@ -7,6 +7,8 @@
     UndecidableInstances #-}
 
 -- | General fcf combinators.
+--
+-- See also "Fcf.Data.Function" for more.
 module Fcf.Combinators
   ( Pure
   , Pure1
diff --git a/src/Fcf/Data/Bool.hs b/src/Fcf/Data/Bool.hs
--- a/src/Fcf/Data/Bool.hs
+++ b/src/Fcf/Data/Bool.hs
@@ -15,17 +15,9 @@
   , type (||)
   , type (&&)
   , Not
-
-    -- *** Multi-way if
-
-  , Guarded
-  , Guard((:=))
-  , Otherwise
   ) where
 
 import Fcf.Core
-import Fcf.Combinators (ConstFn)
-import Fcf.Utils
 
 -- | N.B.: The order of the two branches is the opposite of "if":
 -- @UnBool ifFalse ifTrue bool@.
@@ -58,32 +50,3 @@
 data Not :: Bool -> Exp Bool
 type instance Eval (Not 'True)  = 'False
 type instance Eval (Not 'False) = 'True
-
--- | A conditional choosing the first branch whose guard @a -> 'Exp' 'Bool'@
--- accepts a given value @a@.
---
--- === Example
---
--- @
--- type UnitPrefix n = 'Eval' ('Guarded' n
---   '[ 'TyEq' 0 \'':=' 'Pure' \"\"
---    , 'TyEq' 1 \'':=' 'Pure' \"deci\"
---    , 'TyEq' 2 \'':=' 'Pure' \"hecto\"
---    , 'TyEq' 3 \'':=' 'Pure' \"kilo\"
---    , 'TyEq' 6 \'':=' 'Pure' \"mega\"
---    , 'TyEq' 9 \'':=' 'Pure' \"giga\"
---    , 'Otherwise' \'':=' 'Error' "Something else"
---    ])
--- @
-data Guarded :: a -> [Guard (a -> Exp Bool) (Exp b)] -> Exp b
-type instance Eval (Guarded x ((p ':= y) ': ys)) =
-    Eval (If (Eval (p x)) y (Guarded x ys))
-{-# DEPRECATED Guarded "Use 'Case' instead" #-}
-
--- | A fancy-looking pair type to use with 'Guarded'.
-data Guard a b = a := b
-infixr 0 :=
-
--- | A catch-all guard for 'Guarded'.
-type Otherwise = ConstFn 'True
-
diff --git a/src/Fcf/Data/Common.hs b/src/Fcf/Data/Common.hs
--- a/src/Fcf/Data/Common.hs
+++ b/src/Fcf/Data/Common.hs
@@ -8,20 +8,17 @@
 -- | Common data types: tuples, 'Either', 'Maybe'.
 module Fcf.Data.Common
   ( -- ** Pairs
-
     Uncurry
   , Fst
   , Snd
   , type (***)
 
     -- ** Either
-
   , UnEither
   , IsLeft
   , IsRight
 
     -- ** Maybe
-
   , UnMaybe
   , FromMaybe
   , IsNothing
@@ -41,12 +38,14 @@
 data Snd :: (a, b) -> Exp b
 type instance Eval (Snd '(_a, b)) = b
 
+
 infixr 3 ***
 
--- | Equivalent to 'Bimap' for pairs.
+-- | Specialization of 'Fcf.Class.Bifunctor.Bimap' for pairs.
 data (***) :: (b -> Exp c) -> (b' -> Exp c') -> (b, b') -> Exp (c, c')
 type instance Eval ((***) f f' '(b, b')) = '(Eval (f b), Eval (f' b'))
 
+
 -- ** Either
 
 data UnEither :: (a -> Exp c) -> (b -> Exp c) -> Either a b -> Exp c
@@ -60,6 +59,7 @@
 data IsRight :: Either a b -> Exp Bool
 type instance Eval (IsRight ('Left _a)) = 'False
 type instance Eval (IsRight ('Right _a)) = 'True
+
 
 -- ** Maybe
 
diff --git a/src/Fcf/Data/Function.hs b/src/Fcf/Data/Function.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Function.hs
@@ -0,0 +1,53 @@
+{-# LANGUAGE
+    DataKinds,
+    PolyKinds,
+    TypeFamilies,
+    TypeInType,
+    TypeOperators,
+    UndecidableInstances #-}
+
+-- | Simple combinators for functions.
+module Fcf.Data.Function
+  ( type (&)
+  , On
+  , Bicomap
+  ) where
+
+import Fcf.Core
+
+infixl 1 &
+
+-- $setup
+-- >>> import Fcf.Combinators (Pure)
+-- >>> import Fcf.Data.Common (Fst)
+-- >>> import Fcf.Data.Bool (type (&&), type (||))
+
+-- | Reverse function application, argument first.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval ('( 'True, 'Nothing) & Fst)
+-- Eval ('( 'True, 'Nothing) & Fst) :: Bool
+-- = 'True
+data (&) :: a -> (a -> Exp b) -> Exp b
+type instance Eval (x & f) = Eval (f x)
+
+-- | Lift a binary function to the domain of a projection.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '()))
+-- Eval (((&&) `On` Fst) '( 'True, 'Nothing) '( 'False, 'Just '())) :: Bool
+-- = 'False
+data On :: (b -> b -> Exp c) -> (a -> Exp b) -> a -> a -> Exp c
+type instance Eval (On r f x y) = Eval (r (Eval (f x)) (Eval (f y)))
+
+-- | Pre-compose a binary function with a function for each argument.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True)
+-- Eval (Bicomap Fst Pure (||) '( 'False, 'Nothing) 'True) :: Bool
+-- = 'True
+data Bicomap :: (a -> Exp c) -> (b -> Exp d) -> (c -> d -> Exp e) -> a -> b -> Exp e
+type instance Eval (Bicomap f g r x y) = Eval (r (Eval (f x)) (Eval (g y)))
diff --git a/src/Fcf/Data/List.hs b/src/Fcf/Data/List.hs
--- a/src/Fcf/Data/List.hs
+++ b/src/Fcf/Data/List.hs
@@ -7,57 +7,130 @@
     UndecidableInstances #-}
 
 -- | Lists.
+--
+-- See also "Fcf.Class.Foldable" for additional functions.
 module Fcf.Data.List
-  ( Foldr
-  , Unfoldr
-  , UnList
-  , Cons
-  , type (++)
-  , Concat
-  , ConcatMap
-  , Filter
+  ( -- * Basic functions
+    type (++)
   , Head
   , Last
   , Tail
+  , Cons
+  , Snoc
+  , Cons2
   , Init
   , Null
   , Length
+
+  -- * List transformations
+  , Reverse
+  , Intersperse
+  , Intercalate
+
+  -- * Reducing lists
+  -- | See also "Fcf.Class.Foldable".
+  , Foldr
+  , UnList
+  , Concat
+  , ConcatMap
+
+  -- * Unfolding and building
+  , Unfoldr
   , Replicate
-  , Find
-  , FindIndex
+
+  -- * Sublists
+  , Take
+  , Drop
+  , TakeWhile
+  , DropWhile
+  , Span
+  , Break
+  , Tails
+
+  -- ** Predicates
+  , IsPrefixOf
+  , IsSuffixOf
+  , IsInfixOf
+
+  -- * Searching
   , Elem
   , Lookup
+  , Find
+  , Filter
+  , Partition
+
+  -- * Indexing lists
+  , FindIndex
   , SetIndex
+
+  -- * Zipping and unzipping
   , ZipWith
   , Zip
   , Unzip
-  , Cons2
-  , Take
-  , Drop
-  , TakeWhile
-  , DropWhile
-  , Reverse
   ) where
 
 import qualified GHC.TypeLits as TL
 
 import Fcf.Core
 import Fcf.Combinators
-import Fcf.Classes
+import Fcf.Class.Functor (Map)
+import Fcf.Class.Monoid (type (<>))
+import Fcf.Class.Foldable
+import Fcf.Data.Bool
 import Fcf.Data.Common
 import Fcf.Data.Nat
-import Fcf.Utils
+import Fcf.Utils (If, TyEq)
 
--- $
+-- $setup
 -- >>> import Fcf.Core
 -- >>> import Fcf.Combinators
 -- >>> import qualified GHC.TypeLits as TL
 
 
--- | Append an element for type-level lists.
+-- | List catenation.
 --
 -- === __Example__
 --
+-- >>> :kind! Eval ('[1, 2] ++ '[3, 4])
+-- Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
+-- = '[1, 2, 3, 4]
+--
+data (++) :: [a] -> [a] -> Exp [a]
+type instance Eval ((++) xs ys) = xs <> ys
+
+
+data Head :: [a] -> Exp (Maybe a)
+type instance Eval (Head '[]) = 'Nothing
+type instance Eval (Head (a ': _as)) = 'Just a
+
+data Last :: [a] -> Exp (Maybe a)
+type instance Eval (Last '[]) = 'Nothing
+type instance Eval (Last (a ': '[])) = 'Just a
+type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))
+
+data Init :: [a] -> Exp (Maybe [a])
+type instance Eval (Init '[]) = 'Nothing
+type instance Eval (Init (a ': '[])) = 'Just '[]
+type instance Eval (Init (a ': b ': as)) =
+  Eval (Map (Cons a) =<< (Init (b ': as)))
+
+data Tail :: [a] -> Exp (Maybe [a])
+type instance Eval (Tail '[]) = 'Nothing
+type instance Eval (Tail (_a ': as)) = 'Just as
+
+data Null :: [a] -> Exp Bool
+type instance Eval (Null '[]) = 'True
+type instance Eval (Null (a ': as)) = 'False
+
+data Length :: [a] -> Exp Nat
+type instance Eval (Length '[]) = 0
+type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
+
+
+-- | Append an element to a list.
+--
+-- === __Example__
+--
 -- >>> :kind! Eval (Cons 1 '[2, 3])
 -- Eval (Cons 1 '[2, 3]) :: [Nat]
 -- = '[1, 2, 3]
@@ -68,28 +141,76 @@
 data Cons :: a -> [a] -> Exp [a]
 type instance Eval (Cons a as) = a ': as
 
--- | Foldr for type-level lists.
+-- | Append elements to two lists. Used in the definition of 'Unzip'.
+data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
+type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
+
+-- | Append an element to the end of a list.
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Foldr (+) 0 '[1, 2, 3, 4])
--- Eval (Foldr (+) 0 '[1, 2, 3, 4]) :: Nat
--- = 10
-data Foldr :: (a -> b -> Exp b) -> b -> [a] -> Exp b
-type instance Eval (Foldr f y '[]) = y
-type instance Eval (Foldr f y (x ': xs)) = Eval (f x (Eval (Foldr f y xs)))
+-- >>> :kind! Eval (Snoc '[1,2,3] 4)
+-- Eval (Snoc '[1,2,3] 4) :: [Nat]
+-- = '[1, 2, 3, 4]
+data Snoc :: [a] -> a -> Exp [a]
+type instance Eval (Snoc lst a) = Eval (lst ++ '[a])
 
--- | N.B.: This is equivalent to a 'Foldr' flipped.
+
+-- Helper for Reverse. This corresponds to rev in the data list lib.
+data Rev :: [a] -> [a] -> Exp [a]
+type instance Eval (Rev '[]       ys) = ys
+type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))
+
+
+-- | Reverse a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Reverse '[1,2,3,4,5])
+-- Eval (Reverse '[1,2,3,4,5]) :: [Nat]
+-- = '[5, 4, 3, 2, 1]
+data Reverse :: [a] -> Exp [a]
+type instance Eval (Reverse l) = Eval (Rev l '[])
+
+-- | Intersperse a separator between elements of a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Intersperse 0 '[1,2,3,4])
+-- Eval (Intersperse 0 '[1,2,3,4]) :: [Nat]
+-- = '[1, 0, 2, 0, 3, 0, 4]
+data Intersperse :: a -> [a] -> Exp [a]
+type instance Eval (Intersperse _   '[]      ) = '[]
+type instance Eval (Intersperse sep (x ': xs)) = x ': Eval (PrependToAll sep xs)
+
+-- | Helper for Intersperse
+data PrependToAll :: a -> [a] -> Exp [a]
+type instance Eval (PrependToAll _   '[]      ) = '[]
+type instance Eval (PrependToAll sep (x ': xs)) = sep ': x ': Eval (PrependToAll sep xs)
+
+-- | Join a list of words separated by some word.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ])
+-- Eval (Intercalate '[", "] '[ '["Lorem"], '["ipsum"], '["dolor"] ]) :: [TL.Symbol]
+-- = '["Lorem", ", ", "ipsum", ", ", "dolor"]
+data Intercalate :: [a] -> [[a]] -> Exp [a]
+type instance Eval (Intercalate xs xss) = Eval (Concat =<< Intersperse xs xss)
+
+
+-- | This is 'Foldr' with its argument flipped.
 data UnList :: b -> (a -> b -> Exp b) -> [a] -> Exp b
 type instance Eval (UnList y f xs) = Eval (Foldr f y xs)
 
+
 -- Helper for the Unfoldr.
 data UnfoldrCase :: (b -> Exp (Maybe (a, b))) -> Maybe (a, b) -> Exp [a]
 type instance Eval (UnfoldrCase f ('Just ab)) =
   Eval (Fst ab) ': Eval (Unfoldr f (Eval (Snd ab)))
 type instance Eval (UnfoldrCase _ 'Nothing) = '[]
 
--- | Type-level Unfoldr.
+-- | Unfold a generator into a list.
 --
 -- === __Example__
 --
@@ -109,70 +230,7 @@
 data Unfoldr :: (b -> Exp (Maybe (a, b))) -> b -> Exp [a]
 type instance Eval (Unfoldr f c) = Eval (UnfoldrCase f (f @@ c))
 
--- | Type-level list catenation.
---
--- === __Example__
---
--- >>> :kind! Eval ('[1, 2] ++ '[3, 4])
--- Eval ('[1, 2] ++ '[3, 4]) :: [Nat]
--- = '[1, 2, 3, 4]
---
-data (++) :: [a] -> [a] -> Exp [a]
-type instance Eval ((++) '[] ys) = ys
-type instance Eval ((++) (x ': xs) ys) = x ': Eval ((++) xs ys)
 
--- | Concat for lists.
---
--- === __Example__
---
--- >>> :kind! Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]]))
--- Eval (Concat ( '[ '[1,2], '[3,4], '[5,6]])) :: [Nat]
--- = '[1, 2, 3, 4, 5, 6]
--- >>> :kind! Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]]))
--- Eval (Concat ( '[ '[Int, Maybe Int], '[Maybe String, Either Double Int]])) :: [*]
--- = '[Int, Maybe Int, Maybe String, Either Double Int]
---
-data Concat :: [[a]] -> Exp [a]
-type instance Eval (Concat lsts) = Eval (Foldr (++) '[] lsts)
-
--- | ConcatMap for lists.
-data ConcatMap :: (a -> Exp [b]) -> [a] -> Exp [b]
-type instance Eval (ConcatMap f lst) = Eval (Concat (Eval (Map f lst)))
-
-data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (Filter _p '[]) = '[]
-type instance Eval (Filter p (a ': as)) =
-  Eval (If (Eval (p a))
-    ('(:) a <$> Filter p as)
-    (Filter p as))
-
-data Head :: [a] -> Exp (Maybe a)
-type instance Eval (Head '[]) = 'Nothing
-type instance Eval (Head (a ': _as)) = 'Just a
-
-data Last :: [a] -> Exp (Maybe a)
-type instance Eval (Last '[]) = 'Nothing
-type instance Eval (Last (a ': '[])) = 'Just a
-type instance Eval (Last (a ': b ': as)) = Eval (Last (b ': as))
-
-data Init :: [a] -> Exp (Maybe [a])
-type instance Eval (Init '[]) = 'Nothing
-type instance Eval (Init (a ': '[])) = 'Just '[]
-type instance Eval (Init (a ': b ': as)) =
-  Eval (Map (Cons a) =<< (Init (b ': as)))
-
-data Tail :: [a] -> Exp (Maybe [a])
-type instance Eval (Tail '[]) = 'Nothing
-type instance Eval (Tail (_a ': as)) = 'Just as
-
-data Null :: [a] -> Exp Bool
-type instance Eval (Null '[]) = 'True
-type instance Eval (Null (a ': as)) = 'False
-
-data Length :: [a] -> Exp Nat
-type instance Eval (Length '[]) = 0
-type instance Eval (Length (a ': as)) = 1 TL.+ Eval (Length as)
-
 -- Helper for the Replicate.
 data NumIter :: a -> Nat -> Exp (Maybe (a, Nat))
 type instance Eval (NumIter a s) =
@@ -180,8 +238,7 @@
     ('Just '(a, s TL.- 1))
     'Nothing
 
-
--- | Type-level `Replicate` for lists.
+-- | Repeat the same element in a list.
 --
 -- === __Example__
 --
@@ -191,68 +248,8 @@
 data Replicate :: Nat -> a -> Exp [a]
 type instance Eval (Replicate n a) = Eval (Unfoldr (NumIter a) n)
 
-data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
-type instance Eval (Find _p '[]) = 'Nothing
-type instance Eval (Find p (a ': as)) =
-  Eval (If (Eval (p a))
-    (Pure ('Just a))
-    (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))
-
--- | Type-level `Elem` for lists.
---
--- === __Example__
---
--- >>> :kind! Eval (Elem 1 '[1,2,3])
--- Eval (Elem 1 '[1,2,3]) :: Bool
--- = 'True
--- >>> :kind! Eval (Elem 1 '[2,3])
--- Eval (Elem 1 '[2,3]) :: Bool
--- = 'False
---
-data Elem :: a -> [a] -> Exp Bool
-type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)
-
--- | Find an element associated with a key.
-data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
-type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
-  Eval (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 '[]) = '[]
-type instance Eval (ZipWith f (a ': as) (b ': bs)) =
-  Eval (f a b) ': Eval (ZipWith f as bs)
-
-data Zip :: [a] -> [b] -> Exp [(a, b)]
-type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs)
-
-data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
-type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
-
-data Cons2 :: (a, b) -> ([a], [b]) -> Exp ([a], [b])
-type instance Eval (Cons2 '(a, b) '(as, bs)) = '(a ': as, b ': bs)
-
-
--- | Type-level list take.
+-- | Take a prefix of fixed length.
 --
 -- === __Example__
 --
@@ -267,7 +264,7 @@
   Take_ _ '[]       = '[]
   Take_ n (x ': xs) = x ': Take_ (n TL.- 1) xs
 
--- | Type-level list drop.
+-- | Drop a prefix of fixed length, evaluate to the remaining suffix.
 --
 -- === __Example__
 --
@@ -282,7 +279,7 @@
   Drop_ _ '[]       = '[]
   Drop_ n (x ': xs) = Drop_ (n TL.- 1) xs
 
--- | Type-level list takeWhile.
+-- | Take the longest prefix of elements satisfying a predicate.
 --
 -- === __Example__
 --
@@ -296,7 +293,8 @@
       ('(:) x <$> TakeWhile p xs)
       (Pure '[]))
 
--- | Type-level list dropWhile.
+-- | Drop the longest prefix of elements satisfying a predicate,
+-- evaluate to the remaining suffix.
 --
 -- === __Example__
 --
@@ -311,19 +309,259 @@
       (Pure (x ': xs)))
 
 
--- Helper for Reverse. This corresponds to rev in the data list lib.
-data Rev :: [a] -> [a] -> Exp [a]
-type instance Eval (Rev '[]       ys) = ys
-type instance Eval (Rev (x ': xs) ys) = Eval (Rev xs (x ': ys))
+-- | 'Span', applied to a predicate @p@ and a list @xs@, returns a tuple:
+-- the first component is the longest prefix (possibly empty) of @xs@ whose elements
+-- satisfy @p@;
+-- the second component is the remainder of the list.
+--
+-- See also 'TakeWhile', 'DropWhile', and 'Break'.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4])
+-- Eval (Span (Flip (<) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
+-- = '( '[1, 2], '[3, 4, 1, 2, 3, 4])
+--
+-- >>> :kind! Eval (Span (Flip (<) 9) '[1,2,3])
+-- Eval (Span (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
+-- = '( '[1, 2, 3], '[])
+--
+-- >>> :kind! Eval (Span (Flip (<) 0) '[1,2,3])
+-- Eval (Span (Flip (<) 0) '[1,2,3]) :: ([Nat], [Nat])
+-- = '( '[], '[1, 2, 3])
+data Span :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
+type instance Eval (Span p lst) = '( Eval (TakeWhile p lst), Eval (DropWhile p lst))
 
 
--- | Type-level list reverse.
+-- | 'Break', applied to a predicate @p@ and a list @xs@, returns a tuple:
+-- the first component is the longest prefix (possibly empty) of @xs@ whose elements
+-- /do not satisfy/ @p@; the second component is the remainder of the list.
 --
 -- === __Example__
 --
--- >>> :kind! Eval (Reverse '[1,2,3,4,5])
--- Eval (Reverse '[1,2,3,4,5]) :: [Nat]
--- = '[5, 4, 3, 2, 1]
-data Reverse :: [a] -> Exp [a]
-type instance Eval (Reverse l) = Eval (Rev l '[])
+-- >>> :kind! Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4])
+-- Eval (Break (Flip (>) 3) '[1,2,3,4,1,2,3,4]) :: ([Nat], [Nat])
+-- = '( '[1, 2, 3], '[4, 1, 2, 3, 4])
+--
+-- >>> :kind! Eval (Break (Flip (<) 9) '[1,2,3])
+-- Eval (Break (Flip (<) 9) '[1,2,3]) :: ([Nat], [Nat])
+-- = '( '[], '[1, 2, 3])
+--
+-- >>> :kind! Eval (Break (Flip (>) 9) '[1,2,3])
+-- Eval (Break (Flip (>) 9) '[1,2,3]) :: ([Nat], [Nat])
+-- = '( '[1, 2, 3], '[])
+data Break :: (a -> Exp Bool) -> [a] -> Exp ([a],[a])
+type instance Eval (Break p lst) = Eval (Span (Not <=< p) lst)
 
+
+-- | List of suffixes of a list.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Tails '[0,1,2,3])
+-- Eval (Tails '[0,1,2,3]) :: [[Nat]]
+-- = '[ '[0, 1, 2, 3], '[1, 2, 3], '[2, 3], '[3]]
+data Tails :: [a] -> Exp [[a]]
+type instance Eval (Tails '[]) = '[]
+type instance Eval (Tails (a ': as)) = (a ': as) ': Eval (Tails as)
+
+
+-- | Return @True@ when the first list is a prefix of the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5])
+-- Eval (IsPrefixOf '[0,1,2] '[0,1,2,3,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5])
+-- Eval (IsPrefixOf '[0,1,2] '[0,1,3,2,4,5]) :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsPrefixOf '[] '[0,1,3,2,4,5])
+-- Eval (IsPrefixOf '[] '[0,1,3,2,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsPrefixOf '[0,1,3,2,4,5] '[])
+-- Eval (IsPrefixOf '[0,1,3,2,4,5] '[]) :: Bool
+-- = 'False
+data IsPrefixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsPrefixOf xs ys) = IsPrefixOf_ xs ys
+
+-- helper for IsPrefixOf
+type family IsPrefixOf_ (xs :: [a]) (ys :: [a]) :: Bool where
+  IsPrefixOf_ '[] _ = 'True
+  IsPrefixOf_ _ '[] = 'False
+  IsPrefixOf_ (x ': xs) (y ': ys) =
+     Eval ((Eval (TyEq x y)) && IsPrefixOf_ xs ys)
+
+
+-- | Return @True@ when the first list is a suffix of the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5])
+-- Eval (IsSuffixOf '[3,4,5] '[0,1,2,3,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5])
+-- Eval (IsSuffixOf '[3,4,5] '[0,1,3,2,4,5]) :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsSuffixOf '[] '[0,1,3,2,4,5])
+-- Eval (IsSuffixOf '[] '[0,1,3,2,4,5]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsSuffixOf '[0,1,3,2,4,5] '[])
+-- Eval (IsSuffixOf '[0,1,3,2,4,5] '[]) :: Bool
+-- = 'False
+data IsSuffixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsSuffixOf xs ys) =
+  Eval (IsPrefixOf (Reverse @@ xs) (Reverse @@ ys))
+
+
+-- | Return @True@ when the first list is contained within the second.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6])
+-- Eval (IsInfixOf '[2,3,4] '[0,1,2,3,4,5,6]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6])
+-- Eval (IsInfixOf '[2,4,4] '[0,1,2,3,4,5,6]) :: Bool
+-- = 'False
+data IsInfixOf :: [a] -> [a] -> Exp Bool
+type instance Eval (IsInfixOf xs ys) = Eval (Any (IsPrefixOf xs) =<< Tails ys)
+
+
+-- | Return @True@ if an element is in a list.
+--
+-- See also 'FindIndex'.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Elem 1 '[1,2,3])
+-- Eval (Elem 1 '[1,2,3]) :: Bool
+-- = 'True
+-- >>> :kind! Eval (Elem 1 '[2,3])
+-- Eval (Elem 1 '[2,3]) :: Bool
+-- = 'False
+--
+data Elem :: a -> [a] -> Exp Bool
+type instance Eval (Elem a as) = Eval (IsJust =<< FindIndex (TyEq a) as)
+
+-- | Find an element associated with a key in an association list.
+data Lookup :: k -> [(k, b)] -> Exp (Maybe b)
+type instance Eval (Lookup (a :: k) (as :: [(k, b)])) =
+  Eval (Map Snd (Eval (Find (TyEq a <=< Fst) as)) :: Exp (Maybe b))
+
+
+-- | Find @Just@ the first element satisfying a predicate, or evaluate to
+-- @Nothing@ if no element satisfies the predicate.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3])
+-- Eval (Find (TyEq 0) '[1,2,3]) :: Maybe Nat
+-- = 'Nothing
+--
+-- >>> :kind! Eval (Find (TyEq 0) '[1,2,3,0])
+-- Eval (Find (TyEq 0) '[1,2,3,0]) :: Maybe Nat
+-- = 'Just 0
+data Find :: (a -> Exp Bool) -> [a] -> Exp (Maybe a)
+type instance Eval (Find _p '[]) = 'Nothing
+type instance Eval (Find p (a ': as)) =
+  Eval (If (Eval (p a))
+    (Pure ('Just a))
+    (Find p as))
+
+
+-- | Keep all elements that satisfy a predicate, remove all that don't.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Filter ((>) 3) '[1,2,3,0])
+-- Eval (Filter ((>) 3) '[1,2,3,0]) :: [Nat]
+-- = '[1, 2, 0]
+data Filter :: (a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (Filter _p '[]) = '[]
+type instance Eval (Filter p (a ': as)) =
+  Eval (If (Eval (p a))
+    ('(:) a <$> Filter p as)
+    (Filter p as))
+
+
+-- | Split a list into one where all elements satisfy a predicate,
+-- and a second where no elements satisfy it.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Partition ((>=) 35) '[ 20, 30, 40, 50])
+-- Eval (Partition ((>=) 35) '[ 20, 30, 40, 50]) :: ([Nat], [Nat])
+-- = '( '[20, 30], '[40, 50])
+data Partition :: (a -> Exp Bool) -> [a] -> Exp ([a], [a])
+type instance Eval (Partition p lst) = Eval (Foldr (PartHelp p) '( '[], '[]) lst)
+
+-- | Helper for 'Partition'.
+data PartHelp :: (a -> Exp Bool) -> a -> ([a],[a]) -> Exp ([a],[a])
+type instance Eval (PartHelp p a '(xs,ys)) =
+  If (Eval (p a))
+    '(a ': xs, ys)
+    '(xs, a ': ys)
+
+
+-- | Find the index of an element satisfying the predicate.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3])
+-- Eval (FindIndex ((<=) 3) '[1,2,3,1,2,3]) :: Maybe Nat
+-- = 'Just 2
+--
+-- >>> :kind! Eval (FindIndex ((>) 0) '[1,2,3,1,2,3])
+-- Eval (FindIndex ((>) 0) '[1,2,3,1,2,3]) :: Maybe Nat
+-- = 'Nothing
+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))
+
+
+-- | Modify an element at a given index.
+--
+-- The list is unchanged if the index is out of bounds.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (SetIndex 2 7 '[1,2,3])
+-- Eval (SetIndex 2 7 '[1,2,3]) :: [Nat]
+-- = '[1, 2, 7]
+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
+
+-- | Combine elements of two lists pairwise.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (ZipWith (+) '[1,2,3] '[1,1,1])
+-- Eval (ZipWith (+) '[1,2,3] '[1,1,1]) :: [Nat]
+-- = '[2, 3, 4]
+data ZipWith :: (a -> b -> Exp c) -> [a] -> [b] -> Exp [c]
+type instance Eval (ZipWith _f '[] _bs) = '[]
+type instance Eval (ZipWith _f _as '[]) = '[]
+type instance Eval (ZipWith f (a ': as) (b ': bs)) =
+  Eval (f a b) ': Eval (ZipWith f as bs)
+
+data Zip :: [a] -> [b] -> Exp [(a, b)]
+type instance Eval (Zip as bs) = Eval (ZipWith (Pure2 '(,)) as bs)
+
+data Unzip :: Exp [(a, b)] -> Exp ([a], [b])
+type instance Eval (Unzip as) = Eval (Foldr Cons2 '( '[], '[]) (Eval as))
diff --git a/src/Fcf/Data/Nat.hs b/src/Fcf/Data/Nat.hs
--- a/src/Fcf/Data/Nat.hs
+++ b/src/Fcf/Data/Nat.hs
@@ -27,6 +27,9 @@
   , type (-)
   , type (Fcf.Data.Nat.*)
   , type (^)
+
+    -- * Comparisons
+    -- | Note that these conflict with "Fcf.Class.Ord".
   , type (<=)
   , type (>=)
   , type (<)
diff --git a/src/Fcf/Data/Symbol.hs b/src/Fcf/Data/Symbol.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Symbol.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{-|
+Module      : Fcf.Data.Symbol
+Description : Type-level strings
+
+= Symbols
+
+Type-level strings.
+
+Note that the operators from this module conflict with "GHC.TypeLits".
+
+'Symbol' also has instances of @('Fcf.Class.Monoid.<>')@ and 'Fcf.Class.Monoid.MEmpty'.
+
+-}
+module Fcf.Data.Symbol
+    ( -- * Type of symbols
+      -- | From "GHC.TypeLits".
+
+      Symbol
+    )
+  where
+
+import           GHC.TypeLits (Symbol)
diff --git a/src/Fcf/Utils.hs b/src/Fcf/Utils.hs
--- a/src/Fcf/Utils.hs
+++ b/src/Fcf/Utils.hs
@@ -33,6 +33,7 @@
 import GHC.TypeLits (Symbol, TypeError, ErrorMessage(..))
 
 import Fcf.Core
+import Fcf.Combinators (Pure)
 
 -- | Type-level 'error'.
 data Error :: Symbol -> Exp a
@@ -48,10 +49,19 @@
 type instance Eval (Constraints (a ': as)) = (a, Eval (Constraints as))
 
 -- | Type equality.
+--
+-- === __Details__
+--
+-- The base library also defines a similar @('Type.Equality.==')@;
+-- it differs from 'TyEq' in the following ways:
+--
+-- * 'TyEq' is heterogeneous: its arguments may have different kinds;
+-- * 'TyEq' is reflexive: @TyEq a a@ always reduces to 'True' even if @a@ is
+--   a variable.
 data TyEq :: a -> b -> Exp Bool
 type instance Eval (TyEq a b) = TyEqImpl a b
 
-type family TyEqImpl (a :: k) (b :: k) :: Bool where
+type family TyEqImpl (a :: k) (b :: l) :: Bool where
   TyEqImpl a a = 'True
   TyEqImpl a b = 'False
 
@@ -81,28 +91,27 @@
 -- to subcomputation ('Else'). Examples:
 --
 -- @
--- type BoolToNat = Case
---   [ 'True  --> 0
---   , 'False --> 1
+-- type BoolToNat = 'Case'
+--   [ 'True  '-->' 0
+--   , 'False '-->' 1
 --   ]
 --
--- type NatToBool = Case
---   [ 0 --> 'False
---   , Any   'True
+-- type NatToBool = 'Case'
+--   [ 0 '-->' 'False
+--   , 'Any'   'True
 --   ]
 --
--- type ZeroOneOrSucc = Case
---   [ 0  --> 0
---   , 1  --> 1
---   , Else   ((+) 1)
+-- type ZeroOneOrSucc = 'Case'
+--   [ 0  '-->' 0
+--   , 1  '-->' 1
+--   , 'Else'   (('+') 1)
 --   ]
 -- @
 data Case :: [Match j k] -> j -> Exp k
 type instance Eval (Case ms a) = Case_ ms a
 
 type family Case_ (ms :: [Match j k]) (a :: j) :: k where
-  Case_ ('Match_ a b : _ ) a = b
-  Case_ ('Match_ _ _ : ms) a = Case_ ms a
+  Case_ ('Match_ a' b : ms) a = Eval (If (TyEqImpl a' a) (Pure b) (Case ms a))
   Case_ ('Is_ p b    : ms) a = Case_ [ 'True  --> b
                                      , 'False --> Case_ ms a
                                      ] (p @@ a)
@@ -116,6 +125,11 @@
 type Is = ('Is_ :: (j -> Exp Bool) -> k -> Match j k)
 
 -- | Match any type in 'Case'. Should be used as a final branch.
+--
+-- Note: this identifier conflicts with 'Fcf.Class.Foldable.Any' (from "Fcf.Class.Foldable")
+-- 'Data.Monoid.Any' (from "Data.Monoid"), and 'GHC.Exts.Any' (from "GHC.Exts").
+--
+-- We recommend importing this one qualified.
 type Any = ('Any_ :: k -> Match j k)
 
 -- | Pass type being matched in 'Case' to subcomputation. Should be used as a
diff --git a/test/test.hs b/test/test.hs
--- a/test/test.hs
+++ b/test/test.hs
@@ -1,39 +1,98 @@
 {-# LANGUAGE
+    CPP,
     DataKinds,
     KindSignatures,
     TypeOperators #-}
 
 import Data.Type.Equality ((:~:)(Refl))
-import GHC.TypeLits (Nat)
-import Fcf
+import qualified Data.Monoid as Monoid
 
-type UnitPrefix (n :: Nat) = Eval (Guarded n
-  [ TyEq 0 ':= Pure ""
-  , TyEq 1 ':= Pure "deci"
-  , TyEq 2 ':= Pure "hecto"
-  , TyEq 3 ':= Pure "kilo"
-  , TyEq 6 ':= Pure "mega"
-  , TyEq 9 ':= Pure "giga"
-  , Otherwise ':= Error "Something else"
-  ])
+import Fcf.Core (Eval, type (@@))
+import Fcf.Combinators
+import Fcf.Utils (Case, type (-->), Error)
+import qualified Fcf.Utils as Case
 
-type UnitPrefix' = Case
+import Fcf.Class.Bifunctor
+import Fcf.Class.Foldable
+import Fcf.Class.Monoid
+import Fcf.Class.Ord
+
+import Fcf.Data.Function
+import Fcf.Data.List
+import Fcf.Data.Nat (type (+))
+
+type UnitPrefix = Case
   [ 0 --> ""
   , 1 --> "deci"
   , 2 --> "hecto"
   , 3 --> "kilo"
   , 6 --> "mega"
   , 9 --> "giga"
-  , Any   (Error @@ "Something Else")
+  , Case.Any   (Error @@ "Something Else")
   ]
 
 -- Compile-time tests
 
-_ = Refl :: UnitPrefix 0 :~: ""
-_ = Refl :: UnitPrefix 9 :~: "giga"
+_ = Refl :: Eval (UnitPrefix 0) :~: ""
+_ = Refl :: Eval (UnitPrefix 3) :~: "kilo"
 
-_ = Refl :: Eval (UnitPrefix' 0) :~: ""
-_ = Refl :: Eval (UnitPrefix' 3) :~: "kilo"
+-- * Class
+
+-- ** Ord
+
+_ = Refl :: Eval (Compare '( '(), 0 ) '( '(), 1 )) :~: 'LT
+_ = Refl :: Eval (Compare '( 1, 3 ) '( 1, 2 )) :~: 'GT
+_ = Refl :: Eval (Compare ('Left '()) ('Right 'LT)) :~: 'LT
+_ = Refl :: Eval (Compare ('Right 'EQ) ('Right 'EQ)) :~: 'EQ
+_ = Refl :: Eval (Compare '[ 'LT, 'EQ, 'GT ] '[ 'LT, 'EQ, 'GT ]) :~: 'EQ
+_ = Refl :: Eval (Compare 'True 'True) :~: 'EQ
+_ = Refl :: Eval (Compare "A" "B") :~: 'LT
+
+_ = Refl :: Eval (1 <= 1) :~: 'True
+_ = Refl :: Eval (2 <= 1) :~: 'False
+_ = Refl :: Eval (1 < 1) :~: 'False
+_ = Refl :: Eval (1 < 2) :~: 'True
+_ = Refl :: Eval (1 >= 1) :~: 'True
+_ = Refl :: Eval (1 >= 2) :~: 'False
+_ = Refl :: Eval (1 > 1) :~: 'False
+_ = Refl :: Eval (2 > 1) :~: 'True
+
+-- ** Monoid
+
+_ = Refl :: Eval ('( '(), '[ 'LT, 'EQ ]) .<> '( '(), '[ 'GT ])) :~: '( '(), '[ 'LT, 'EQ, 'GT ])
+_ = Refl :: Eval ('Nothing .<> 'Just '[]) :~: 'Just '[]
+_ = Refl :: Eval ('LT .<> 'GT) :~: 'LT
+_ = Refl :: Eval ('EQ .<> 'GT) :~: 'GT
+_ = Refl :: Eval ('Monoid.All 'True .<> 'Monoid.All 'False) :~: 'Monoid.All 'False
+_ = Refl :: Eval ('Monoid.Any 'True .<> 'Monoid.Any 'False) :~: 'Monoid.Any 'True
+#if __GLASGOW_HASKELL__ >= 802
+_ = Refl :: Eval ("a" .<> MEmpty) :~: "a"
+#endif
+
+-- ** Foldable
+
+_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) '[ 'True, 'False ]) :~: 'Monoid.All 'False
+_ = Refl :: Eval (FoldMap (Pure1 'Monoid.All) 'Nothing) :~: 'Monoid.All 'True
+_ = Refl :: Eval (Foldr (.<>) 'LT '[ 'EQ, 'EQ ]) :~: 'LT
+_ = Refl :: Eval (And '[ 'False, 'False ]) :~: 'False
+_ = Refl :: Eval (Or '[ 'False, 'False ]) :~: 'False
+_ = Refl :: Eval (Concat ('Right 'LT)) :~: 'LT
+
+_ = Refl :: FoldMapDefault_ (Pure1 'Monoid.All) 'Nothing :~: 'Monoid.All 'True
+_ = Refl :: FoldrDefault_ (.<>) 'LT '[ 'EQ, 'EQ ] :~: 'LT
+
+-- ** Functor
+
+_ = Refl :: Eval (Bimap ((+) 1) (Pure2 '(:) '()) '(8, '[])) :~: '(9, '[ '()])
+_ = Refl :: Eval (First ((+) 1) ('Left 8)) :~: 'Left 9
+_ = Refl :: Eval (First ((+) 1) ('Right 0)) :~: 'Right 0
+_ = Refl :: Eval (Second ((+) 1) ('Left 0)) :~: 'Left 0
+_ = Refl :: Eval (Second ((+) 1) ('Right 8)) :~: 'Right 9
+
+-- ** Function
+
+_ = Refl :: Eval (3 & Pure) :~: 3
+_ = Refl :: Eval (((+) `On` Length) '[1,2,3] '[1,2]) :~: 5
 
 -- Dummy