diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,15 @@
 
+# 0.3.0
+
+20200209
+
+ - a separate Sort module
+ - add possibility to sort a list of lists
+ - a Text module
+ - several list functions (And, Or, All, Any, ..)
+ - IsProperSubsetOf, IsSubsetOf in Set
+ - add new example that uses MapC and Text
+
 # 0.2.0
 
  - remove the methods that can be found from fcf 0.7.0
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# fcf-containers
+# fcf-containers [![Hackage](https://img.shields.io/hackage/v/fcf-containers.svg)](https://hackage.haskell.org/package/fcf-containers) [![Build Status](https://travis-ci.org/gspia/fcf-containers.svg)](https://travis-ci.org/gspia/fcf-containers)
 
 Fcf-containers mimicks the containers package but for type-level computations. 
 That is, we provide e.g. trees and maps. In addition to that, this package 
diff --git a/examples/Haiku.hs b/examples/Haiku.hs
new file mode 100644
--- /dev/null
+++ b/examples/Haiku.hs
@@ -0,0 +1,134 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{-|
+
+Example on how to do compile-time (ie type-level) computations and how
+to get the results into use on term-level (ie runtime).
+
+This exemplifies the use of @MapC@ and @Text@.
+
+Exercises:
+ - Write a method for structurally wrong Haiku's and output something other in those cases
+ - Vocabulary with syllables is somewhat parameterized (except WSmap) but 
+   not the other half.
+   Change CheckHaiku to accepts the vocabulary to use and the haiku the check.
+
+-}
+
+--------------------------------------------------------------------------------
+
+import qualified GHC.TypeLits as TL
+
+import           Data.Proxy
+
+import           Fcf ( Eval, Exp, Map, type (=<<), type (@@), If, IsNothing, Pure
+                     , FromMaybe, Flip)
+import           Fcf.Data.Nat
+import           Fcf.Data.List as L
+
+import           Fcf.Data.MapC as M
+import           Fcf.Data.Text as T
+
+import           Fcf.Alg.List (Equal)
+
+--------------------------------------------------------------------------------
+
+-- | Type-level variable containing vocabulary split in syllables.
+data HaikuWords :: Exp [[Text]]
+type instance Eval HaikuWords =
+    '[ '[ 'Text '["a","a"], 'Text '["m","u"]]
+     , '[ 'Text '["a","a"], 'Text '["m","u","l"], 'Text '["l","a"]]
+     , '[ 'Text '["a"], 'Text '["j","a"], 'Text '["t","u","s"]]
+     , '[ 'Text '["j","o"], 'Text '["k","i","n"]]
+     , '[ 'Text '["k","i","e"], 'Text '["l","i"]]
+     , '[ 'Text '["l","o","i"], 'Text '["k","o","i"], 'Text '["l","e"], 'Text '["v","a"]]
+     , '[ 'Text '["m","u","u"]]
+     , '[ 'Text '["v","a","n"], 'Text '["h","e"], 'Text '["n","e","e"]]
+     , '[ 'Text '["u","u"], 'Text '["s","i"]]
+     ]
+
+-- | Turn syllables into words
+data MkWords :: [[Text]] -> Exp [Text]
+type instance Eval (MkWords words) = Eval (Fcf.Map T.Concat words)
+
+-- | We want ghc to count the the syllables per word for us
+data SyllableCount :: [[Text]] -> Exp [Nat]
+type instance Eval (SyllableCount words) = Eval (Fcf.Map L.Length words)
+
+-- | Construct a mapping that maps a word to the number of syllables in it
+data WordSyllables :: [[Text]] -> Exp (MapC Text Nat)
+type instance Eval (WordSyllables words) =
+    Eval (M.FromList =<< Zip (MkWords @@ words) (SyllableCount @@ words))
+
+-- | Hmm, type-level global variable...
+data WSmap :: Exp (MapC Text Nat)
+type instance Eval WSmap = Eval (WordSyllables =<< HaikuWords)
+
+--------------------------------------------------------------------------------
+
+-- | The count of syllables per lines and number of lines that is required for 
+-- correct Haiku. This is used for Haiku structural check.
+data ReqSyllablesPerLine :: Exp [Nat]
+type instance Eval ReqSyllablesPerLine = '[5,7,5]
+
+--------------------------------------------------------------------------------
+
+-- | Our executable associated Haiku we want to check.
+data Haiku :: Exp Text
+type instance Eval Haiku =
+    'Text '[ "k","i","e","l","i"," ","v","a","n","h","e","n","e","e","\n"
+           , "l","o","i","k","o","i","l","e","v","a"," ","a","j","a","t","u","s","\n"
+           , "a","a","m","u","l","l","a"," ","u","u","s","i"
+           -- , "j","o", "k","i","n" -- test with clearly wrong input (won't compile)
+           ]
+
+-- | Split the Haiku into more easily processable form
+data HaikuAsLineWords :: Exp [[Text]]
+type instance Eval HaikuAsLineWords = Eval (Fcf.Map Words =<< Lines =<< Haiku)
+
+-- | After applying the lookups, we have lot's of Maybe's.
+data SumJusts :: [Maybe Nat] -> Nat -> Exp Nat
+type instance Eval (SumJusts '[] acc) = acc
+type instance Eval (SumJusts (n ': ns) acc) = Eval
+    (If (IsNothing @@ n)
+        (Pure 0)
+        (SumJusts ns (Eval (acc + (Eval (FromMaybe 0 n) ))))
+    )
+
+-- | The main method, we list of lines, and on each line a list of words,
+-- for which we try to find out the syllable count from our map, 
+-- and as a last thing we count the syllable sums for each line.
+data HaikuSyllCountsPerLine :: Exp [Nat]
+type instance Eval HaikuSyllCountsPerLine =
+    Eval (Fcf.Map (Flip SumJusts 0)
+      =<< Fcf.Map (Fcf.Map (Flip M.Lookup (Eval WSmap)))
+      =<< HaikuAsLineWords)
+
+-- | To check the Haiku, compare the correct number of syllables (and at the
+-- same time, number of lines) to the figures we got from the input Haiku.
+data CheckHaiku :: Exp Bool
+type instance Eval CheckHaiku =
+    Eval (Equal (Eval ReqSyllablesPerLine) (Eval HaikuSyllCountsPerLine))
+
+--------------------------------------------------------------------------------
+
+-- | We left something here as well. We don't want this executable to compile
+-- if the Haiku is not ok.
+showHaiku
+    :: forall symbol. (symbol ~ Eval (ToSymbol =<< Haiku), 'True ~ Eval CheckHaiku)
+    => String
+showHaiku = TL.symbolVal @symbol Proxy
+
+main :: IO ()
+main = putStrLn $ "The Haiku is:\n" ++ showHaiku
+
+
diff --git a/examples/Orbits.hs b/examples/Orbits.hs
--- a/examples/Orbits.hs
+++ b/examples/Orbits.hs
@@ -118,3 +118,4 @@
 
 main :: IO ()
 main = putStrLn $ "Number of orbits is " ++ showResult
+
diff --git a/fcf-containers.cabal b/fcf-containers.cabal
--- a/fcf-containers.cabal
+++ b/fcf-containers.cabal
@@ -6,7 +6,7 @@
     contents of containers-package and show how these can be used. Everything is
     based on the ideas given in the first-class-families -package.
 Homepage:            https://github.com/gspia/fcf-containers
-Version:             0.2.0
+Version:             0.3.0
 Build-type:          Simple
 Author:              gspia
 Maintainer:          iahogsp@gmail.com
@@ -24,7 +24,9 @@
                    , Fcf.Data.Tree
                    , Fcf.Data.Set
                    , Fcf.Data.Symbol
+                   , Fcf.Data.Text
                    , Fcf.Alg.List
+                   , Fcf.Alg.Sort
                    , Fcf.Alg.Tree
                    , Fcf.Alg.Morphism
   build-depends:     base >= 4.9 && < 4.14
@@ -48,6 +50,20 @@
   -- ghc-options:
      --  -ddump-simpl
      --  -O2
+
+Executable haiku
+  hs-source-dirs:   examples,src
+  main-is:          Haiku.hs
+  default-language: Haskell2010
+  other-modules:    Fcf.Alg.Morphism
+                  , Fcf.Alg.List
+                  , Fcf.Data.Tree
+                  , Fcf.Data.MapC
+                  , Fcf.Data.Set
+                  , Fcf.Data.Symbol
+                  , Fcf.Data.Text
+  build-depends:    base
+                  , first-class-families
 
 test-suite fcf-test
   type:                exitcode-stdio-1.0
diff --git a/src/Fcf/Alg/List.hs b/src/Fcf/Alg/List.hs
--- a/src/Fcf/Alg/List.hs
+++ b/src/Fcf/Alg/List.hs
@@ -29,11 +29,13 @@
 
 import qualified GHC.TypeLits as TL
 
-import           Fcf.Core (Eval, Exp)
+import           Fcf.Core (Eval, Exp, type (@@))
 import           Fcf.Classes (Map)
-import           Fcf.Data.List (Foldr)
-import           Fcf.Utils (If)
-import           Fcf.Data.Bool (type (&&), type  (||))
+import           Fcf.Combinators (type (=<<), type (<=<))
+import           Fcf.Data.List (Foldr, Concat, TakeWhile, DropWhile, Reverse
+                               , type (++), ZipWith)
+import           Fcf.Utils (If, TyEq)
+import           Fcf.Data.Bool (type (&&), type  (||), Not)
 import           Fcf.Data.Nat
 
 import           Fcf.Alg.Morphism
@@ -125,6 +127,160 @@
         '(a ': xs, ys)
         '(xs, a ': ys)
 
+-- | Intersperse for type-level lists.
+--
+-- === __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)
+
+-- | Intercalate for type-level lists.
+-- 
+-- === __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)
+
+
+-- | 'Span', applied to a predicate @p@ and a type-level list @xs@, returns a 
+-- type-level tuple where
+-- first element is longest prefix (possibly empty) of @xs@ of elements that
+-- satisfy @p@ and second element is the remainder of the list:
+--
+-- === __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))
+
+
+-- | 'Break', applied to a predicate @p@ and a type-level list @xs@, returns a 
+-- type-level tuple where
+-- first element is longest prefix (possibly empty) of @xs@ of elements that
+-- /do not satisfy/ @p@ and second element is the remainder of the list:
+--
+-- === __Example__
+-- 
+-- >>> :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)
+
+
+-- | IsPrefixOf takes two type-level lists and returns true
+-- iff 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)
+
+
+-- | IsSuffixOf take two type-level lists and returns true
+-- iff 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))
+
+
+-- | IsInfixOf take two type-level lists and returns true
+-- iff the first list is a infix of 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)
+
+
+-- | Tails
+-- 
+-- === __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)
+
 --------------------------------------------------------------------------------
 
 
@@ -132,31 +288,96 @@
 --
 -- === __Example__
 -- 
--- >>> :kind! Eval (All '[ 'True, 'True])
--- Eval (All '[ 'True, 'True]) :: Bool
+-- >>> :kind! Eval (And '[ 'True, 'True])
+-- Eval (And '[ 'True, 'True]) :: Bool
 -- = 'True
 --
--- >>> :kind! Eval (All '[ 'True, 'True, 'False])
--- Eval (All '[ 'True, 'True, 'False]) :: Bool
+-- >>> :kind! Eval (And '[ 'True, 'True, 'False])
+-- Eval (And '[ 'True, 'True, 'False]) :: Bool
 -- = 'False
-data All :: [Bool] -> Exp Bool
-type instance Eval (All lst) = Eval (Foldr (&&) 'True lst)
+data And :: [Bool] -> Exp Bool
+type instance Eval (And lst) = Eval (Foldr (&&) 'True lst)
 
 
+-- | Type-level All.
+--
+-- === __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) -> [a] -> Exp Bool
+type instance Eval (All p lst) = Eval (And =<< Map p lst)
+
+
 -- | Give true if any of the booleans in the list is true.
 --
 -- === __Example__
 -- 
--- >>> :kind! Eval (Any '[ 'True, 'True])
--- Eval (Any '[ 'True, 'True]) :: Bool
+-- >>> :kind! Eval (Or '[ 'True, 'True])
+-- Eval (Or '[ 'True, 'True]) :: Bool
 -- = 'True
 -- 
--- >>> :kind! Eval (Any '[ 'False, 'False])
--- Eval (Any '[ 'False, 'False]) :: Bool
+-- >>> :kind! Eval (Or '[ 'False, 'False])
+-- Eval (Or '[ 'False, 'False]) :: Bool
 -- = 'False
-data Any :: [Bool] -> Exp Bool
-type instance Eval (Any lst) = Eval (Foldr (||) 'False lst)
+data Or :: [Bool] -> Exp Bool
+type instance Eval (Or lst) = Eval (Foldr (||) 'False lst)
 
 
+-- | Type-level Any.
+--
+-- === __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) -> [a] -> Exp Bool
+type instance Eval (Any p lst) = Eval (Or =<< Map p lst)
+
+--------------------------------------------------------------------------------
+
+-- | Snoc for type-level lists.
+--
+-- === __Example__
+-- 
+-- >>> :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])
+
+-- | ToList for type-level lists.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (ToList 1)
+-- Eval (ToList 1) :: [Nat]
+-- = '[1]
+data ToList :: a -> Exp [a]
+type instance Eval (ToList a) = '[a]
+
+
+-- | Equal tests for list equality. We may change the name to (==).
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Equal '[1,2,3] '[1,2,3])
+-- Eval (Equal '[1,2,3] '[1,2,3]) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (Equal '[1,2,3] '[1,3,2])
+-- Eval (Equal '[1,2,3] '[1,3,2]) :: Bool
+-- = 'False
+data Equal :: [a] -> [a] -> Exp Bool
+type instance Eval (Equal as bs) = Eval (And =<< ZipWith TyEq as bs)
 
 
diff --git a/src/Fcf/Alg/Sort.hs b/src/Fcf/Alg/Sort.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Alg/Sort.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{-|
+Module      : Fcf.Alg.Sort
+Description : Type-level sorting algorithms and utilities
+Copyright   : (c) gspia 2020-
+License     : BSD
+Maintainer  : gspia
+
+= Fcf.Alg.Sort
+
+-}
+
+--------------------------------------------------------------------------------
+
+module Fcf.Alg.Sort where
+
+import qualified GHC.TypeLits as TL
+
+import           Fcf ( If, Eval, Exp, type (<=<), type (=<<)
+                     , Flip, Not, TyEq, Pure )
+import           Fcf.Data.List ( ZipWith, Filter, type (++) )
+import           Fcf.Data.Nat (Nat)
+
+--------------------------------------------------------------------------------
+
+import           Fcf.Alg.Tree (BTreeF(..))
+import           Fcf.Alg.Morphism
+import           Fcf.Data.Symbol (Symbol, SymbolOrd)
+
+--------------------------------------------------------------------------------
+
+-- For the doctests:
+
+-- $setup
+-- >>> import qualified Fcf.Data.Nat as N ( type (<) )
+-- >>> import qualified Fcf.Data.Symbol as S ( type (<) )
+
+--------------------------------------------------------------------------------
+
+-- helper for the ListCmp
+data ListCmpFnd :: [Ordering] -> Exp Ordering
+type instance Eval (ListCmpFnd '[]) = 'EQ
+type instance Eval (ListCmpFnd (a ': as)) = Eval
+    (If (Eval (TyEq a 'EQ))
+        (ListCmpFnd as)
+        (Pure a)
+    )
+
+-- | Compare lists with the given comparison for the elements.
+data ListCmp :: (a -> a -> Exp Ordering) -> [a] -> [a] -> Exp Ordering
+type instance Eval (ListCmp f as bs) = Eval (ListCmpFnd =<< ZipWith f as bs)
+
+-- | Give true if the first list is before the second, given the comparison
+-- function for the elements.
+data ListOrd :: (a -> a -> Exp Ordering) -> [a] -> [a] -> Exp Bool
+type instance Eval (ListOrd f as bs) = Eval
+    (If (Eval (TyEq 'LT (Eval (ListCmp f as bs))))
+        (Pure 'True)
+        (Pure 'False)
+    )
+
+-- | Comparison for the Nats.
+-- 
+-- TODO: Would this fit to Fcf.Data.Nat on first-class-families?
+data NatOrd :: Nat -> Nat -> Exp Ordering
+type instance Eval (NatOrd a b) = TL.CmpNat a b
+
+-- | Comparison for Symbol lists.
+--
+-- Useful when sorting with Qsort.
+data SymbolListOrd :: [Symbol] -> [Symbol] -> Exp Bool
+type instance Eval (SymbolListOrd as bs) = Eval (ListOrd SymbolOrd as bs)
+
+-- | Comparison for Nat lists.
+--
+-- Useful when sorting with Qsort.
+data NatListOrd :: [Nat] -> [Nat] -> Exp Bool
+type instance Eval (NatListOrd as bs) = Eval (ListOrd NatOrd as bs)
+
+--------------------------------------------------------------------------------
+
+
+-- helper
+data PartHlp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]
+type instance Eval (PartHlp _ '[]) = 'BEmptyF
+type instance Eval (PartHlp smaller (h ': t)) =
+    'BNodeF h
+        (Eval (Filter (smaller h) t))
+        (Eval (Filter (Not <=< smaller h) t))
+
+-- helper
+data Inord :: Algebra (BTreeF a) [a]
+type instance Eval (Inord 'BEmptyF) = '[]
+type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ (Eval ('[v] ++ r)))
+
+
+-- | Qsort - give the comparison function @a -> a -> Exp Bool@ comparing your 
+-- list elements and then Qsort will order the list.
+-- 
+-- __Example__
+--
+-- >>> :kind! Eval (Qsort (N.<) '[5,3,1,9,4,6,3])
+-- Eval (Qsort (N.<) '[5,3,1,9,4,6,3]) :: [Nat]
+-- = '[1, 3, 3, 4, 5, 6, 9]
+--
+-- >>> :kind! Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ])
+-- Eval (Qsort (S.<) '[ "bb", "e", "a", "e", "d" ]) :: [Symbol]
+-- = '["a", "bb", "d", "e", "e"]
+data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]
+type instance Eval (Qsort cmp lst) = Eval (Hylo Inord (PartCmp cmp) lst)
+
+-- Helper
+--
+-- We use the Flip version so that using <-comparison will give an inreasing 
+-- Nat-list. Sorting would work without PartCmp.
+data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a] 
+type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)
+
+
diff --git a/src/Fcf/Alg/Tree.hs b/src/Fcf/Alg/Tree.hs
--- a/src/Fcf/Alg/Tree.hs
+++ b/src/Fcf/Alg/Tree.hs
@@ -133,49 +133,3 @@
 type instance Eval (Map f 'BEmptyF) = 'BEmptyF
 type instance Eval (Map f ('BNodeF a b1 b2)) = 'BNodeF a (Eval (f b1)) (Eval (f b2))
 
-
--- helper
-data PartHlp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a]
-type instance Eval (PartHlp _ '[]) = 'BEmptyF
-type instance Eval (PartHlp smaller (h ': t)) =
-    'BNodeF h
-        (Eval (Filter (smaller h) t))
-        (Eval (Filter (Not <=< smaller h) t))
-
--- | Use this if you want to sort symbols into increasing order.
-data SymbolCompareInc :: TL.Symbol -> TL.Symbol -> Exp Bool
-type instance Eval (SymbolCompareInc n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'LT)
-
--- | Use this if you want to sort symbols into decreasing order.
-data SymbolCompareDec :: TL.Symbol -> TL.Symbol -> Exp Bool
-type instance Eval (SymbolCompareDec n1 n2) = Eval (TyEq (TL.CmpSymbol n1 n2) 'GT)
-    
--- helper
-data Inord :: Algebra (BTreeF a) [a]
-type instance Eval (Inord 'BEmptyF) = '[]
-type instance Eval (Inord ('BNodeF v l r)) = Eval (l ++ (Eval ('[v] ++ r)))
-
-
--- | Qsort - give the comparison function @a -> a -> Exp Bool@ comparing your 
--- list elements and then Qsort will order the list.
--- 
--- __Example__
---
--- >>> :kind! Eval (Qsort (<) '[5,3,1,9,4,6,3])
--- Eval (Qsort (<) '[5,3,1,9,4,6,3]) :: [Nat]
--- = '[1, 3, 3, 4, 5, 6, 9]
---
--- >>> :kind! Eval (Qsort SymbolCompareInc '[ "bb", "e", "a", "e", "d" ])
--- Eval (Qsort SymbolCompareInc '[ "bb", "e", "a", "e", "d" ]) :: [TL.Symbol]
--- = '["a", "bb", "d", "e", "e"]
-data Qsort :: (a -> a -> Exp Bool) -> [a] -> Exp [a]
-type instance Eval (Qsort cmp lst) = Eval (Hylo Inord (PartCmp cmp) lst)
-
--- Helper
---
--- We use the Flip version so that using <-comparison will give an inreasing 
--- Nat-list. Sorting would work without PartCmp.
-data PartCmp :: (a -> a -> Exp Bool) -> CoAlgebra (BTreeF a) [a] 
-type instance Eval (PartCmp cmp coalg) = Eval (PartHlp (Flip cmp) coalg)
-
-
diff --git a/src/Fcf/Data/Set.hs b/src/Fcf/Data/Set.hs
--- a/src/Fcf/Data/Set.hs
+++ b/src/Fcf/Data/Set.hs
@@ -17,7 +17,7 @@
 = Fcf.Data.Set
 
 Set provides an interface which is similar to the that given by the
-container-package. If a method is missing here that you need, please do open
+containers-package. If a method is missing here that you need, please do open
 up an issue or better, make a PR.
 
 Many of the examples are from containers-package. The internal representation
@@ -36,6 +36,8 @@
     , NotMember
     , Null
     , Size
+    , IsSubsetOf
+    , IsProperSubsetOf
       
     -- * Construction
     , Empty
@@ -55,16 +57,20 @@
     )
   where
 
+--------------------------------------------------------------------------------
+
 import qualified GHC.TypeLits as TL
 
-import           Fcf ( Eval, Exp, type (=<<), type (<=<)
-                     , Not, If, Map, TyEq )
+import           Fcf ( Eval, Exp, type (=<<), type (<=<), type (&&)
+                     , Not, If, Map, Flip, TyEq )
 import qualified Fcf as Fcf (Foldr, Filter)
 import           Fcf.Data.List ( Elem, Cons, Concat, Reverse, Length, type (++)
                                , ZipWith, Replicate)
+import           Fcf.Alg.List ( All, Any )
 
+--------------------------------------------------------------------------------
 
-import           Fcf.Alg.List
+import           Fcf.Alg.List ( ListF(..), ListToFix)
 import           Fcf.Alg.Morphism
 
 --------------------------------------------------------------------------------
@@ -75,6 +81,7 @@
 -- >>> import qualified GHC.TypeLits as TL
 -- >>> import           Fcf.Data.Nat
 -- >>> import           Fcf.Data.Symbol
+-- >>> import           Fcf.Alg.Sort
 
 --------------------------------------------------------------------------------
 
@@ -82,6 +89,7 @@
 data Set a = Set [a]
 
 
+--------------------------------------------------------------------------------
 
 -- | Empty
 -- 
@@ -192,6 +200,48 @@
 type instance Eval (Size ('Set lst)) = Eval (Length lst)
 
 
+-- | IsSubsetOf 
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
+-- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'False
+data IsSubsetOf :: Set a -> Set a -> Exp Bool
+type instance Eval (IsSubsetOf ('Set s1) ('Set s2)) =
+    Eval (All (Flip Elem s2) s1)
+
+
+-- | IsProperSubsetOf 
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
+-- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
+-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool
+-- = 'True
+data IsProperSubsetOf :: Set a -> Set a -> Exp Bool
+type instance Eval (IsProperSubsetOf ('Set s1) ('Set s2)) = Eval
+    (Eval (All (Flip Elem s2) s1) &&
+    Eval (Any (Not <=< Flip Elem s1) s2))
+
+
+
 -- | Type-level set union.
 --
 -- === __Example__
@@ -281,7 +331,7 @@
     Eval (Concat =<< ZipWith SelWithBool elms bls)
 
 -- | Calculate the power sets of a given type-level list. The algorithm is based 
--- Gray codes.
+-- on Gray codes.
 --
 -- === __Example__
 --
@@ -325,6 +375,10 @@
 -- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set Nat]
 -- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
 --      'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
+--
+-- >>> :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
+-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[Nat]]
+-- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
 data ToList :: Set v -> Exp [v]
 type instance Eval (ToList ('Set lst)) = lst
 
diff --git a/src/Fcf/Data/Symbol.hs b/src/Fcf/Data/Symbol.hs
--- a/src/Fcf/Data/Symbol.hs
+++ b/src/Fcf/Data/Symbol.hs
@@ -21,6 +21,8 @@
 Note that the operators from this module conflict with "GHC.TypeLits".
 
 
+TODO: Would this whole module have a place first-class-families?
+
 -}
 
 --------------------------------------------------------------------------------
@@ -35,9 +37,15 @@
 
     , Append
     , Intercalate
+    , IsSpace
+    , IsNewLine
+    , IsTab
+    , IsSpaceDelim
+    , IsDigit
 
      -- * Comparison functions
 
+    , SymbolOrd
     , type (<=)
     , type (>=)
     , type (<)
@@ -52,7 +60,7 @@
 import qualified GHC.TypeLits as TL
 
 import           Fcf.Core (Eval, Exp)
-import           Fcf.Data.List (Foldr)
+import           Fcf.Data.List (Foldr, Elem)
 import           Fcf.Data.Bool (type (||))
 import           Fcf.Utils (TyEq)
 
@@ -95,8 +103,98 @@
 data InterCalHelp :: Symbol -> Symbol -> Symbol -> Exp Symbol
 type instance Eval (InterCalHelp s s1 s2) = Eval (Append (Eval (Append s s1)) s2)
 
+
+-- | IsSpace
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsSpace "a")
+-- Eval (IsSpace "a") :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsSpace " ")
+-- Eval (IsSpace " ") :: Bool
+-- = 'True
+data IsSpace :: Symbol -> Exp Bool
+type instance Eval (IsSpace s) = Eval (s == " ")
+
+
+-- | IsNewline
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsNewLine "a")
+-- Eval (IsNewLine "a") :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsNewLine "\n")
+-- Eval (IsNewLine "\n") :: Bool
+-- = 'True
+data IsNewLine :: Symbol -> Exp Bool
+type instance Eval (IsNewLine s) = Eval (s == "\n")
+
+
+-- | IsTab
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsTab "a")
+-- Eval (IsTab "a") :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsTab "\t")
+-- Eval (IsTab "\t") :: Bool
+-- = 'True
+data IsTab :: Symbol -> Exp Bool
+type instance Eval (IsTab s) = Eval (s == "\t")
+
+
+-- | IsSpaceDelim
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsSpaceDelim "a")
+-- Eval (IsSpaceDelim "a") :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (IsSpaceDelim "\n")
+-- Eval (IsSpaceDelim "\n") :: Bool
+-- = 'True
+data IsSpaceDelim :: Symbol -> Exp Bool
+type instance Eval (IsSpaceDelim s) =
+    Eval (Eval (IsSpace s) || (Eval (Eval (IsNewLine s) || Eval (IsTab s))))
+
+
+-- | IsDigit
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsDigit "3")
+-- Eval (IsDigit "3") :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (IsDigit "a")
+-- Eval (IsDigit "a") :: Bool
+-- = 'False
+data IsDigit :: Symbol -> Exp Bool
+type instance Eval (IsDigit s)
+    = Eval (Elem s '["0","1","2","3","4","5","6","7","8","9"])
+
+
+
 --------------------------------------------------------------------------------
 
+
+-- | SymbolOrd - compare two symbols and give type-level Ordering 
+-- ( $ 'LT $, $ 'EQ $ or $ 'GT $ ).
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (SymbolOrd "a" "b")
+-- Eval (SymbolOrd "a" "b") :: Ordering
+-- = 'LT
+data SymbolOrd :: Symbol -> Symbol -> Exp Ordering
+type instance Eval (SymbolOrd a b) = TL.CmpSymbol a b
 
 -- | Less-than-or-equal comparison for symbols.
 -- 
diff --git a/src/Fcf/Data/Text.hs b/src/Fcf/Data/Text.hs
new file mode 100644
--- /dev/null
+++ b/src/Fcf/Data/Text.hs
@@ -0,0 +1,716 @@
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeInType             #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+{-# OPTIONS_GHC -Wall                       #-}
+{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
+
+{-|
+Module      : Fcf.Data.Text
+Description : Type-level Text data structure with methods
+Copyright   : (c) gspia 2020-
+License     : BSD
+Maintainer  : gspia
+
+= Fcf.Data.Text
+
+We mimick Data.Text but on type level. The internal representation is based on
+type level lists.
+
+-}
+
+--------------------------------------------------------------------------------
+
+module Fcf.Data.Text
+    ( Text (..)
+
+    -- * Creation
+    , Empty
+    , Singleton
+    , FromList
+    , ToList
+    , ToSymbol
+
+    -- * Basic Interface
+    , Null
+    , Length
+    , Append
+    , Cons
+    , Snoc
+    , Uncons
+    , Unsnoc
+    , Head
+    , Tail
+    , Init
+    , CompareLength
+
+    -- * Transformation
+    , Map
+    , Intercalate
+    , Intersperse
+    , Reverse
+    , Replace
+
+    -- * Special Folds
+    , Concat
+    , ConcatMap
+    , Any
+    , All
+
+    -- * Substrings
+    , Take
+    , TakeEnd
+    , Drop
+    , DropEnd
+    , TakeWhile
+    , TakeWhileEnd
+    , DropWhile
+    , DropWhileEnd
+    , DropAround
+    , Strip
+
+    -- * Breaking etc
+    , SplitOn
+    , Split
+    , Lines
+    , Words
+    , Unlines
+    , Unwords
+
+    -- * Predicates
+    , IsPrefixOf
+    , IsSuffixOf
+    , IsInfixOf
+    )
+  where
+
+import qualified GHC.TypeLits as TL
+
+import           Fcf ( If, Eval, Exp, type (=<<), type (@@)
+                     , Flip, Pure )
+import           Fcf.Data.List ( type (++) )
+import qualified Fcf.Data.List as F
+    ( Length, Head, Tail, Init, Reverse, Take, Drop, TakeWhile, DropWhile
+    , Foldr)
+
+import qualified Fcf.Classes as F ( Map )
+
+import qualified Fcf.Alg.List as F
+    ( Any, All, IsPrefixOf, IsSuffixOf, IsInfixOf, Snoc, Intercalate
+    , Intersperse)
+
+
+import           Fcf.Data.Nat (Nat)
+import           Fcf.Alg.Morphism (First,Second)
+import           Fcf.Data.Symbol (Symbol)
+import qualified Fcf.Data.Symbol as S
+
+--------------------------------------------------------------------------------
+
+
+-- For the doctests:
+
+-- $setup
+-- >>> import           Fcf (type (<=<), Not)
+
+--------------------------------------------------------------------------------
+
+-- | 'Text' is a data structure, that is, a list to hold type-level symbols of
+-- length one.
+data Text = Text [Symbol]
+
+--------------------------------------------------------------------------------
+
+-- | Empty
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! (Eval Empty :: Text)
+-- (Eval Empty :: Text) :: Text
+-- = 'Text '[]
+--
+-- See also the other examples in this module.
+data Empty :: Exp Text
+type instance Eval Empty = 'Text '[]
+
+-- | Singleton
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Singleton "a")
+-- Eval (Singleton "a") :: Text
+-- = 'Text '["a"]
+data Singleton :: Symbol -> Exp Text
+type instance Eval (Singleton s) = 'Text '[s]
+
+
+
+-- | Use FromList to construct a Text from type-level list.
+--
+-- === __Example__
+-- 
+-- :kind! Eval (FromList '["h", "e", "l", "l", "u", "r", "e", "i"])
+-- Eval (FromList '["h", "e", "l", "l", "u", "r", "e", "i"]) :: Text
+-- = 'Text '["h", "e", "l", "l", "u", "r", "e", "i"]
+data FromList :: [Symbol] -> Exp Text
+type instance Eval (FromList lst) = 'Text lst
+
+-- | Get the type-level list out of the 'Text'.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (ToList =<< FromList '["a", "b"])
+-- Eval (ToList =<< FromList '["a", "b"]) :: [Symbol]
+-- = '["a", "b"]
+data ToList :: Text -> Exp [Symbol]
+type instance Eval (ToList ('Text lst)) = lst
+
+
+-- | ToSymbol
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (ToSymbol =<< FromList '["w", "o", "r", "d"])
+-- Eval (ToSymbol =<< FromList '["w", "o", "r", "d"]) :: Symbol
+-- = "word"
+data ToSymbol :: Text -> Exp Symbol
+type instance Eval (ToSymbol ('Text lst)) = Eval (F.Foldr S.Append "" lst)
+
+
+
+-- | Null
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Null =<< FromList '["a", "b"])
+-- Eval (Null =<< FromList '["a", "b"]) :: Bool
+-- = 'False
+-- >>> :kind! Eval (Null =<< Empty)
+-- Eval (Null =<< Empty) :: Bool
+-- = 'True
+data Null :: Text -> Exp Bool
+type instance Eval (Null ('Text '[])) = 'True
+type instance Eval (Null ('Text (_ ': _))) = 'False
+
+
+-- | Length
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Length =<< FromList '["a", "b"])
+-- Eval (Length =<< FromList '["a", "b"]) :: Nat
+-- = 2
+data Length :: Text -> Exp Nat
+type instance Eval (Length ('Text lst)) = Eval (F.Length lst)
+
+
+-- | Add a symbol to the beginning of a type-level text.
+--
+-- === __Example__
+-- 
+-- > :kind! Eval (Cons "h" ('Text '["a", "a", "m", "u"]))
+-- Eval (Cons "h" ('Text '["a", "a", "m", "u"])) :: Text
+-- = 'Text '["h", "a", "a", "m", "u"]
+data Cons :: Symbol -> Text -> Exp Text
+type instance Eval (Cons s ('Text lst)) = 'Text (s ': lst)
+
+-- | Add a symbol to the end of a type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Snoc ('Text '["a", "a", "m"]) "u")
+-- Eval (Snoc ('Text '["a", "a", "m"]) "u") :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data Snoc :: Text -> Symbol -> Exp Text
+type instance Eval (Snoc ('Text lst) s) = 'Text (Eval (lst ++ '[s]))
+
+-- | Append two type-level texts.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Append ('Text '["a", "a"]) ('Text '["m", "u"]))
+-- Eval (Append ('Text '["a", "a"]) ('Text '["m", "u"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data Append :: Text -> Text -> Exp Text
+type instance Eval (Append ('Text l1) ('Text l2)) = 'Text (Eval (l1 ++ l2))
+
+
+-- | Get the first symbol from type-level text.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Uncons ('Text '["h", "a", "a", "m", "u"]))
+-- Eval (Uncons ('Text '["h", "a", "a", "m", "u"])) :: Maybe
+--                                                       (Symbol, Text)
+-- = 'Just '("h", 'Text '["a", "a", "m", "u"])
+--
+-- >>> :kind! Eval (Uncons ('Text '[]))
+-- Eval (Uncons ('Text '[])) :: Maybe (Symbol, Text)
+-- = 'Nothing
+data Uncons :: Text -> Exp (Maybe (Symbol, Text))
+type instance Eval (Uncons ('Text '[])) = 'Nothing
+type instance Eval (Uncons ('Text (t ': txt))) = 'Just '(t, 'Text txt)
+
+
+-- | Get the last symbol from type-level text.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Unsnoc ('Text '["a", "a", "m", "u", "n"]))
+-- Eval (Unsnoc ('Text '["a", "a", "m", "u", "n"])) :: Maybe
+--                                                       (Symbol, Text)
+-- = 'Just '("n", 'Text '["a", "a", "m", "u"])
+--
+-- >>> :kind! Eval (Unsnoc ('Text '[]))
+-- Eval (Unsnoc ('Text '[])) :: Maybe (Symbol, Text)
+-- = 'Nothing
+data Unsnoc :: Text -> Exp (Maybe (Symbol, Text))
+type instance Eval (Unsnoc txt) =
+    Eval (F.Map (Second Reverse) =<< Uncons =<< Reverse txt)
+
+
+-- | Get the first symbol of type-level text.
+--
+-- === __Example__
+--
+-- >>> :kind! Eval (Head ('Text '["a", "a", "m", "u"]))
+-- Eval (Head ('Text '["a", "a", "m", "u"])) :: Maybe Symbol
+-- = 'Just "a"
+-- 
+-- >>> :kind! Eval (Head ('Text '[]))
+-- Eval (Head ('Text '[])) :: Maybe Symbol
+-- = 'Nothing
+data Head :: Text -> Exp (Maybe Symbol)
+type instance Eval (Head ('Text lst)) = Eval (F.Head lst)
+
+-- | Get the tail of a type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Tail ('Text '["h", "a", "a", "m", "u"]))
+-- Eval (Tail ('Text '["h", "a", "a", "m", "u"])) :: Maybe Text
+-- = 'Just ('Text '["a", "a", "m", "u"])
+--
+-- >>> :kind! Eval (Tail ('Text '[]))
+-- Eval (Tail ('Text '[])) :: Maybe Text
+-- = 'Nothing
+data Tail :: Text -> Exp (Maybe Text)
+type instance Eval (Tail ('Text lst)) = Eval (F.Map FromList =<< F.Tail lst)
+
+-- | Take all except the last symbol from type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Init ('Text '["a", "a", "m", "u", "n"]))
+-- Eval (Init ('Text '["a", "a", "m", "u", "n"])) :: Maybe Text
+-- = 'Just ('Text '["a", "a", "m", "u"])
+--
+-- >>> :kind! Eval (Init ('Text '[]))
+-- Eval (Init ('Text '[])) :: Maybe Text
+-- = 'Nothing
+data Init :: Text -> Exp (Maybe Text)
+type instance Eval (Init ('Text lst)) = Eval (F.Map FromList =<< F.Init lst)
+
+
+-- | Compare the length of type-level text to given Nat and give
+-- the Ordering.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (CompareLength ('Text '["a", "a", "m", "u"]) 3)
+-- Eval (CompareLength ('Text '["a", "a", "m", "u"]) 3) :: Ordering
+-- = 'GT
+data CompareLength :: Text -> Nat -> Exp Ordering
+type instance Eval (CompareLength txt n) = TL.CmpNat (Length @@ txt) n
+
+
+
+-- | Map for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :{
+-- data IsIsymb :: Symbol -> Exp Bool
+-- type instance Eval (IsIsymb s) = Eval ("i" S.== s)
+-- data Isymb2e :: Symbol -> Exp Symbol
+-- type instance Eval (Isymb2e s) = Eval
+--     (If (IsIsymb @@ s)
+--         (Pure "e")
+--         (Pure s)
+--     )
+-- :}
+-- 
+-- >>> :kind! Eval (Map Isymb2e ('Text '["i","m","u"]))
+-- Eval (Map Isymb2e ('Text '["i","m","u"])) :: Text
+-- = 'Text '["e", "m", "u"]
+data Map :: (Symbol -> Exp Symbol) -> Text -> Exp Text
+type instance Eval (Map f ('Text lst)) = 'Text (Eval (F.Map f lst))
+
+
+-- | Intercalate for type-level text.
+-- 
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Intercalate ('Text '[" ", "&", " "]) ('[ 'Text '["a", "a", "m", "u"], 'Text '["v", "a", "l", "o"]]))
+-- Eval (Intercalate ('Text '[" ", "&", " "]) ('[ 'Text '["a", "a", "m", "u"], 'Text '["v", "a", "l", "o"]])) :: Text
+-- = 'Text '["a", "a", "m", "u", " ", "&", " ", "v", "a", "l", "o"]
+data Intercalate :: Text -> [Text] -> Exp Text
+type instance Eval (Intercalate ('Text txt) txts) =
+    Eval (FromList =<< F.Intercalate txt =<< F.Map ToList txts)
+
+
+-- | Intersperse for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Intersperse "." ('Text '["a", "a", "m", "u"]))
+-- Eval (Intersperse "." ('Text '["a", "a", "m", "u"])) :: Text
+-- = 'Text '["a", ".", "a", ".", "m", ".", "u"]
+data Intersperse :: Symbol -> Text -> Exp Text
+type instance Eval (Intersperse s ('Text txt)) = Eval (FromList =<< F.Intersperse s txt)
+
+-- | Reverse for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Reverse ('Text '["a", "a", "m", "u"]))
+-- Eval (Reverse ('Text '["a", "a", "m", "u"])) :: Text
+-- = 'Text '["u", "m", "a", "a"]
+--
+-- >>> :kind! Eval (Reverse =<< Reverse ('Text '["a", "a", "m", "u"]))
+-- Eval (Reverse =<< Reverse ('Text '["a", "a", "m", "u"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data Reverse :: Text -> Exp Text
+type instance Eval (Reverse ('Text lst)) = 'Text (Eval (F.Reverse lst))
+
+-- | Replace for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Replace ('Text '["t","u"]) ('Text '["l","a"]) ('Text '["t","u","u","t","u","t","t","a","a"]))
+-- Eval (Replace ('Text '["t","u"]) ('Text '["l","a"]) ('Text '["t","u","u","t","u","t","t","a","a"])) :: Text
+-- = 'Text '["l", "a", "u", "l", "a", "t", "t", "a", "a"]
+data Replace :: Text -> Text -> Text -> Exp Text
+type instance Eval (Replace orig new txt) =
+    Eval (Intercalate new =<< SplitOn orig txt)
+
+
+-- | Concat for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Concat '[ 'Text '["l","a"], 'Text '["k","a","n","a"]])
+-- Eval (Concat '[ 'Text '["l","a"], 'Text '["k","a","n","a"]]) :: Text
+-- = 'Text '["l", "a", "k", "a", "n", "a"]
+data Concat :: [Text] -> Exp Text
+type instance Eval (Concat lst) = Eval (F.Foldr Append (Eval Empty :: Text) lst)
+
+
+
+-- | ConcatMap for type-level text.
+--
+-- === __Example__
+--
+-- >>> :{
+-- data IsIsymb :: Symbol -> Exp Bool
+-- type instance Eval (IsIsymb s) = Eval ("i" S.== s)
+-- data Isymb2aa :: Symbol -> Exp Text
+-- type instance Eval (Isymb2aa s) = Eval
+--     (If (IsIsymb @@ s)
+--         (Pure ('Text '["a","a"]))
+--         (Pure ('Text '[s]))
+--     )
+-- :}
+--
+-- >>> :kind! Eval (ConcatMap Isymb2aa ('Text '["i","m","u"," ","i","h"]))
+-- Eval (ConcatMap Isymb2aa ('Text '["i","m","u"," ","i","h"])) :: Text
+-- = 'Text '["a", "a", "m", "u", " ", "a", "a", "h"]
+data ConcatMap :: (Symbol -> Exp Text) -> Text -> Exp Text
+type instance Eval (ConcatMap f ('Text lst)) = Eval (Concat =<< F.Map f lst)
+
+-- | Any for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Any S.IsDigit ('Text '["a","a","m","u","1"]))
+-- Eval (Any S.IsDigit ('Text '["a","a","m","u","1"])) :: Bool
+-- = 'True
+--
+-- >>> :kind! Eval (Any S.IsDigit ('Text '["a","a","m","u"]))
+-- Eval (Any S.IsDigit ('Text '["a","a","m","u"])) :: Bool
+-- = 'False
+data Any :: (Symbol -> Exp Bool) -> Text -> Exp Bool
+type instance Eval (Any f ('Text lst)) = Eval (F.Any f lst)
+
+
+-- | All for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (All S.IsDigit ('Text '["a","a","m","u","1"]))
+-- Eval (All S.IsDigit ('Text '["a","a","m","u","1"])) :: Bool
+-- = 'False
+--
+-- >>> :kind! Eval (All S.IsDigit ('Text '["3","2","1"]))
+-- Eval (All S.IsDigit ('Text '["3","2","1"])) :: Bool
+-- = 'True
+data All :: (Symbol -> Exp Bool) -> Text -> Exp Bool
+type instance Eval (All f ('Text lst)) = Eval (F.All f lst)
+
+
+
+
+
+-- | Take for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Take 4 ('Text '["a", "a", "m", "u", "n"]))
+-- Eval (Take 4 ('Text '["a", "a", "m", "u", "n"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data Take :: Nat -> Text -> Exp Text
+type instance Eval (Take n ('Text lst)) = 'Text (Eval (F.Take n lst))
+
+
+-- | TakeEnd for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (TakeEnd 4 ('Text '["h", "a", "a", "m", "u"]))
+-- Eval (TakeEnd 4 ('Text '["h", "a", "a", "m", "u"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data TakeEnd :: Nat -> Text -> Exp Text
+type instance Eval (TakeEnd n ('Text lst)) =
+    'Text (Eval (F.Reverse =<< F.Take n =<< F.Reverse lst))
+
+
+-- | Drop for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Drop 2 ('Text '["a", "a", "m", "u", "n", "a"]))
+-- Eval (Drop 2 ('Text '["a", "a", "m", "u", "n", "a"])) :: Text
+-- = 'Text '["m", "u", "n", "a"]
+data Drop :: Nat -> Text -> Exp Text
+type instance Eval (Drop n ('Text lst)) = 'Text (Eval (F.Drop n lst))
+
+-- | DropEnd for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (DropEnd 2 ('Text '["a", "a", "m", "u", "n", "a"]))
+-- Eval (DropEnd 2 ('Text '["a", "a", "m", "u", "n", "a"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data DropEnd :: Nat -> Text -> Exp Text
+type instance Eval (DropEnd n ('Text lst)) =
+    'Text (Eval (F.Reverse =<< F.Drop n =<< F.Reverse lst))
+
+
+-- | TakeWhile for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (TakeWhile (Not <=< S.IsDigit) ('Text '["a","a","m","u","1","2"]))
+-- Eval (TakeWhile (Not <=< S.IsDigit) ('Text '["a","a","m","u","1","2"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data TakeWhile :: (Symbol -> Exp Bool) -> Text -> Exp Text
+type instance Eval (TakeWhile f ('Text lst)) = 'Text (Eval (F.TakeWhile f lst))
+
+
+-- | TakeWhileEnd for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (TakeWhileEnd (Not <=< S.IsDigit) ('Text '["1","2","a","a","m","u"]))
+-- Eval (TakeWhileEnd (Not <=< S.IsDigit) ('Text '["1","2","a","a","m","u"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data TakeWhileEnd :: (Symbol -> Exp Bool) -> Text -> Exp Text
+type instance Eval (TakeWhileEnd f ('Text lst)) =
+    'Text (Eval (F.Reverse =<< F.TakeWhile f =<< F.Reverse lst))
+
+
+-- | DropWhile for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (DropWhile S.IsDigit ('Text '["1","2","a","a","m","u"]))
+-- Eval (DropWhile S.IsDigit ('Text '["1","2","a","a","m","u"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data DropWhile :: (Symbol -> Exp Bool) -> Text -> Exp Text
+type instance Eval (DropWhile f ('Text lst)) = 'Text (Eval (F.DropWhile f lst))
+
+
+-- | DropWhileEnd for type-level text.
+-- === __Example__
+-- 
+-- >>> :kind! Eval (DropWhileEnd S.IsDigit ('Text '["a","a","m","u","1","2"]))
+-- Eval (DropWhileEnd S.IsDigit ('Text '["a","a","m","u","1","2"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data DropWhileEnd :: (Symbol -> Exp Bool) -> Text -> Exp Text
+type instance Eval (DropWhileEnd f ('Text lst)) =
+    'Text (Eval (F.Reverse =<< F.DropWhile f =<< F.Reverse lst))
+
+
+-- | DropAround for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (DropAround S.IsDigit ('Text '["3","4","a","a","m","u","1","2"]))
+-- Eval (DropAround S.IsDigit ('Text '["3","4","a","a","m","u","1","2"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data DropAround :: (Symbol -> Exp Bool) -> Text -> Exp Text
+type instance Eval (DropAround f txt) = Eval (DropWhile f =<< DropWhileEnd f txt)
+
+
+
+-- | Strip the space, newline and tab -symbols from the beginning and and
+-- of type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Strip ('Text '[" ", " ", "a", "a", "m", "u", " ", "\n"]))
+-- Eval (Strip ('Text '[" ", " ", "a", "a", "m", "u", " ", "\n"])) :: Text
+-- = 'Text '["a", "a", "m", "u"]
+data Strip :: Text -> Exp Text
+type instance Eval (Strip txt) = Eval (DropAround S.IsSpaceDelim txt)
+
+
+-- | SplitOn for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (SplitOn (Eval (FromList '["a", "b"])) (Eval (FromList '[ "c", "d", "a", "b", "f", "g", "a", "b", "h"])))
+-- Eval (SplitOn (Eval (FromList '["a", "b"])) (Eval (FromList '[ "c", "d", "a", "b", "f", "g", "a", "b", "h"]))) :: [Text]
+-- = '[ 'Text '["c", "d"], 'Text '["f", "g"], 'Text '["h"]]
+data SplitOn :: Text -> Text -> Exp [Text]
+type instance Eval (SplitOn ('Text sep) ('Text txt)) =
+    Eval (F.Map FromList =<< SOLoop sep '( '[], txt))
+
+
+-- | Helper for SplitOn
+--
+-- >>> :kind! Eval (SOTake '["a", "b"] '[ "c", "d", "a", "b", "f", "g"] '[])
+-- Eval (SOTake '["a", "b"] '[ "c", "d", "a", "b", "f", "g"] '[]) :: ([Symbol],
+--                                                                    [Symbol])
+-- = '( '["c", "d"], '["f", "g"])
+data SOTake :: [Symbol] -> [Symbol] -> [Symbol] -> Exp ([Symbol], [Symbol])
+type instance Eval (SOTake sep '[] accum) = '(accum, '[])
+type instance Eval (SOTake sep (t ': txt) accum) = Eval
+    (If (Eval (F.IsPrefixOf sep (t ': txt)))
+        (Pure '(accum, Eval (F.Drop (Eval (F.Length sep)) (t ': txt))))
+        (SOTake sep txt (Eval (accum ++ '[t])))
+    )
+
+-- | Helper for SplitOn
+data SOLoop :: [Symbol] -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]]
+type instance Eval (SOLoop sep '(acc, '[])) = acc
+type instance Eval (SOLoop sep '(acc, (t ': txt))) =
+    Eval (SOLoop sep =<< First (F.Snoc acc) =<< SOTake sep (t ': txt) '[])
+
+
+-- | Split for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Split S.IsSpace (Eval (FromList '[ "c", "d", " ", "b", "f", " ", "a", "b", "h"])))
+-- Eval (Split S.IsSpace (Eval (FromList '[ "c", "d", " ", "b", "f", " ", "a", "b", "h"]))) :: [Text]
+-- = '[ 'Text '["c", "d"], 'Text '["b", "f"], 'Text '["a", "b", "h"]]
+data Split :: (Symbol -> Exp Bool) -> Text -> Exp [Text]
+type instance Eval (Split p ('Text txt)) =
+    Eval (F.Map FromList =<< SplitLoop p '( '[], txt))
+
+-- | Helper for Split
+data SplitTake :: (Symbol -> Exp Bool) -> [Symbol] -> [Symbol] -> Exp ([Symbol], [Symbol])
+type instance Eval (SplitTake p '[] accum) = '(accum, '[])
+type instance Eval (SplitTake p (t ': txt) accum) = Eval
+    (If (Eval (p t))
+        (Pure '(accum, txt))
+        (SplitTake p txt (Eval (accum ++ '[t])))
+    )
+
+-- | Helper for Split
+data SplitLoop :: (Symbol -> Exp Bool) -> ([[Symbol]],[Symbol]) -> Exp [[Symbol]]
+type instance Eval (SplitLoop p '(acc, '[])) = acc
+type instance Eval (SplitLoop p '(acc, (t ': txt))) =
+    Eval (SplitLoop p =<< First (F.Snoc acc) =<< SplitTake p (t ': txt) '[])
+
+
+
+-- | Lines for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Lines =<< FromList '[ "o", "k", "\n", "h", "m", "m ", "\n", "a", "b"])
+-- Eval (Lines =<< FromList '[ "o", "k", "\n", "h", "m", "m ", "\n", "a", "b"]) :: [Text]
+-- = '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]
+data Lines :: Text -> Exp [Text]
+type instance Eval (Lines txt) = Eval (Split S.IsNewLine txt)
+
+-- | Words for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Words =<< FromList '[ "o", "k", " ", "h", "m", "m ", "\n", "a", "b"])
+-- Eval (Words =<< FromList '[ "o", "k", " ", "h", "m", "m ", "\n", "a", "b"]) :: [Text]
+-- = '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]
+data Words :: Text -> Exp [Text]
+type instance Eval (Words txt) = Eval (Split S.IsSpaceDelim txt)
+
+-- | Unlines for type-level text. This adds a newline to each Text and then
+-- concats them.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Unlines '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]])
+-- Eval (Unlines '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]) :: Text
+-- = 'Text '["o", "k", "\n", "h", "m", "m ", "\n", "a", "b", "\n"]
+data Unlines :: [Text] -> Exp Text
+type instance Eval (Unlines txts) =
+    Eval (Concat =<< F.Map (Flip Append (Singleton @@ "\n")) txts)
+
+-- | Unwords for type-level text. This uses 'Intercalate' to add space-symbol
+-- between the given texts.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (Unwords '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]])
+-- Eval (Unwords '[ 'Text '["o", "k"], 'Text '["h", "m", "m "], 'Text '["a", "b"]]) :: Text
+-- = 'Text '["o", "k", " ", "h", "m", "m ", " ", "a", "b"]
+data Unwords :: [Text] -> Exp Text
+type instance Eval (Unwords txts) = Eval (Intercalate ('Text '[" "]) txts)
+
+
+-- | IsPrefixOf for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsPrefixOf ('Text '["a", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))
+-- Eval (IsPrefixOf ('Text '["a", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool
+-- = 'True
+data IsPrefixOf :: Text -> Text -> Exp Bool
+type instance Eval (IsPrefixOf ('Text l1) ('Text l2) ) = Eval (F.IsPrefixOf l1 l2)
+
+
+-- | IsSuffixOf for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsSuffixOf ('Text '["n", "e", "n"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))
+-- Eval (IsSuffixOf ('Text '["n", "e", "n"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool
+-- = 'True
+data IsSuffixOf :: Text -> Text -> Exp Bool
+type instance Eval (IsSuffixOf ('Text l1) ('Text l2) ) = Eval (F.IsSuffixOf l1 l2)
+
+
+-- | IsInfixOf for type-level text.
+--
+-- === __Example__
+-- 
+-- >>> :kind! Eval (IsInfixOf ('Text '["m", "i", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"]))
+-- Eval (IsInfixOf ('Text '["m", "i", "a"]) ('Text '["a", "a", "m", "i", "a", "i", "n", "e", "n"])) :: Bool
+-- = 'True
+data IsInfixOf :: Text -> Text -> Exp Bool
+type instance Eval (IsInfixOf ('Text l1) ('Text l2) ) = Eval (F.IsInfixOf l1 l2) 
+