diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,9 @@
 # Change Log
 
+## 0.2
+
+* Add `embed` and `restrict` to convert between expression languages
+
 ## 0.1.9
 
 * Bump dependencies
diff --git a/expressions.cabal b/expressions.cabal
--- a/expressions.cabal
+++ b/expressions.cabal
@@ -1,5 +1,5 @@
 name:                expressions
-version:             0.1.9
+version:             0.2
 synopsis:            Expressions and Formulae a la carte
 description:
   This package is aimed at providing means of fixing a first-order language and
diff --git a/src/Data/Expression/Utils/Indexed/Sum.hs b/src/Data/Expression/Utils/Indexed/Sum.hs
--- a/src/Data/Expression/Utils/Indexed/Sum.hs
+++ b/src/Data/Expression/Utils/Indexed/Sum.hs
@@ -13,8 +13,10 @@
 -- Stability  :  experimental
 --------------------------------------------------------------------------------
 
-module Data.Expression.Utils.Indexed.Sum ((:+:)(..), (:<:)(..), inject, match) where
+module Data.Expression.Utils.Indexed.Sum ((:+:)(..), (:<:)(..), (:<<:), inject, match, embed, restrict) where
 
+import Control.Monad
+
 import Data.Expression.Utils.Indexed.Eq
 import Data.Expression.Utils.Indexed.Foldable
 import Data.Expression.Utils.Indexed.Functor
@@ -50,6 +52,24 @@
     prj (InL _) = Nothing
     prj (InR a) = prj a
 
+class (IFunctor f, IFunctor g) => f :<<: g where
+    emb :: f a i -> g a i
+    res :: g a i -> Maybe (f a i)
+
+instance IFunctor f => f :<<: f where
+    emb = id
+    res = Just
+
+instance (IFunctor f, IFunctor g) => f :<<: (g :+: f) where
+    emb = InR
+    res (InL _) = Nothing
+    res (InR a) = Just a
+
+instance {-# OVERLAPPABLE #-} (IFunctor f, IFunctor g, IFunctor h, f :<<: g) => f :<<: (h :+: g) where
+    emb = InR . emb
+    res (InL _) = Nothing
+    res (InR a) = res a
+
 -- | Inject a component into a sum.
 inject :: g :<: f => forall i. g (IFix f) i -> IFix f i
 inject = IFix . inj
@@ -57,6 +77,14 @@
 -- | Try to unpack a sum into a component.
 match :: g :<: f => forall i. IFix f i -> Maybe (g (IFix f) i)
 match = prj . unIFix
+
+-- | Embed a subset in a superset.
+embed :: (IFunctor f, f :<<: g) => IFix f i -> IFix g i
+embed = icata (IFix . emb)
+
+-- | Try to restrict a superset to a subset.
+restrict :: (ITraversable g, f :<<: g) => IFix g i -> Maybe (IFix f i)
+restrict = fmap IFix . res <=< (itraverse restrict) . unIFix
 
 instance (IEq1 f, IEq1 g) => IEq1 (f :+: g) where
     InL a `ieq1` InL b = a `ieq1` b
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -38,7 +38,10 @@
             , e4 == parseJust "(select (a : array int (array int bool)) (+ (b : int) 3))"
             , e5 == parseJust "(forall ((x : int)) (exists ((y : int)) (and true (= (b : bool) (< x y)))))"
             , e6 == parseJust "(and (forall ((x : int) (y : int)) (< x (+ y (z : int)))) (= z 3))"
-            , e7 == e8 ]
+            , e7 == e8
+            , e9 == e10
+            , isJust (restrict e9 :: Maybe (QFALia ('ArraySort 'IntegralSort 'BooleanSort)))
+            , isNothing (restrict e5 :: Maybe (QFLia 'BooleanSort)) ]
 
     e1, e2, e3 :: ALia 'IntegralSort
     e1 = a
@@ -55,3 +58,7 @@
     e7, e8 :: Lia 'IntegralSort
     e7 = a .*. (a .+. c3) `substitute` (c3 `for` (a .+. c3))
     e8 = inject (Mul [a, c3])
+
+    e9, e10 :: ALia ('ArraySort 'IntegralSort 'BooleanSort)
+    e9  = select a (b .+. c3)
+    e10 = embed e4