diff --git a/.gitignore b/.gitignore
index 8075013..4aa2854 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /dist-newstyle
+cabal.project.local
diff --git a/Plutarch/CPS/Optics/Iso.hs b/Plutarch/CPS/Optics/Iso.hs
new file mode 100644
index 0000000..c1d268d
--- /dev/null
+++ b/Plutarch/CPS/Optics/Iso.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Optics.Iso where
+
+import Plutarch.CPS.Optics.Optic
+import Plutarch.CPS.Profunctor
+
+type CIso r s t a b = forall p. (IsCIso r p) => COptic r p s t a b
+
+type CIso' r s a = CIso r s s a a
+
+class (CProfunctor r p) => IsCIso r p
+
+instance IsCIso r (->)
+instance (Functor f) => IsCIso r (CStar r f)
diff --git a/Plutarch/CPS/Optics/Lens.hs b/Plutarch/CPS/Optics/Lens.hs
new file mode 100644
index 0000000..96ab270
--- /dev/null
+++ b/Plutarch/CPS/Optics/Lens.hs
@@ -0,0 +1,47 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Optics.Lens where
+
+import Control.Monad
+import Control.Monad.Trans.Cont
+import Plutarch.CPS.Optics.Iso
+import Plutarch.CPS.Optics.Optic
+import Plutarch.CPS.Profunctor
+
+type CLens r s t a b = forall p. (IsCLens r p) => COptic r p s t a b
+
+type CLens' r s a = CLens r s s a a
+
+class (IsCIso r p, CStrong r p) => IsCLens r p
+
+instance (Functor f) => IsCLens r (CStar r f)
+
+clens :: (s -> Cont r a) -> (s -> b -> Cont r t) -> CLens r s t a b
+clens get set = cdimap (\s -> (s,) <$> get s) (uncurry set) . csecond'
+
+withCLens :: CLens r s t a b -> ((s -> Cont r a) -> (s -> b -> Cont r t) -> r') -> r'
+withCLens o f = f (clensGet l) (clensSet l)
+  where
+    l = o $ ConcreteLens {clensGet = return, clensSet = const return}
+
+data ConcreteLens r a b s t = ConcreteLens
+  { clensGet :: s -> Cont r a
+  , clensSet :: s -> b -> t
+  }
+
+instance CProfunctor r (ConcreteLens r a b) where
+  cdimap ab cd l =
+    ConcreteLens
+      { clensGet = ab >=> clensGet l
+      , clensSet = \a b -> ab a >>= \b' -> clensSet l b' b >>= cd
+      }
+
+instance CStrong r (ConcreteLens r a b) where
+  cfirst' l =
+    ConcreteLens
+      { clensGet = clensGet l . fst
+      , clensSet = \(a, c) b -> (,c) <$> clensSet l a b
+      }
+
+instance IsCIso r (ConcreteLens r a b)
+instance IsCLens r (ConcreteLens r a b)
diff --git a/Plutarch/CPS/Optics/Optic.hs b/Plutarch/CPS/Optics/Optic.hs
new file mode 100644
index 0000000..bab5219
--- /dev/null
+++ b/Plutarch/CPS/Optics/Optic.hs
@@ -0,0 +1,7 @@
+module Plutarch.CPS.Optics.Optic where
+
+import Control.Monad.Trans.Cont
+
+type COptic r p s t a b = p a (Cont r b) -> p s (Cont r t)
+
+type COptic' r p s a = COptic r p s s a a
diff --git a/Plutarch/CPS/Optics/Optional.hs b/Plutarch/CPS/Optics/Optional.hs
new file mode 100644
index 0000000..7edab44
--- /dev/null
+++ b/Plutarch/CPS/Optics/Optional.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Optics.Optional where
+
+import Plutarch.CPS.Optics.Lens
+import Plutarch.CPS.Optics.Optic
+import Plutarch.CPS.Optics.Prism
+
+import Control.Arrow
+import Control.Monad
+
+import Control.Monad.Trans.Cont
+import Plutarch.CPS.Optics.Iso
+import Plutarch.CPS.Profunctor
+
+type COptional r s t a b = forall p. (IsCOptional r p) => COptic r p s t a b
+
+type COptional' r s a = COptional r s s a a
+
+class (IsCLens r p, IsCPrism r p) => IsCOptional r p
+
+instance (Applicative f) => IsCOptional r (CStar r f)
+
+withCOptional :: COptional r s t a b -> ((s -> Cont r (Either t a)) -> (s -> b -> Cont r t) -> r') -> r'
+withCOptional o f = f (coptionalGet l >=> either (fmap Left) (return . Right)) (coptionalSet l)
+  where
+    l = o $ ConcreteOptional {coptionalGet = return . Right, coptionalSet = const return}
+
+data ConcreteOptional r a b s t = ConcreteOptional
+  { coptionalGet :: s -> Cont r (Either t a)
+  , coptionalSet :: s -> b -> t
+  }
+
+instance CProfunctor r (ConcreteOptional r a b) where
+  cdimap ab cd o =
+    ConcreteOptional
+      { coptionalGet =
+          ab >=> coptionalGet o >=> return . left (>>= cd)
+      , coptionalSet = \a b -> ab a >>= \b' -> coptionalSet o b' b >>= cd
+      }
+
+instance CStrong r (ConcreteOptional r a b) where
+  cfirst' o =
+    ConcreteOptional
+      { coptionalGet = \(a, c) -> left (fmap (,c)) <$> coptionalGet o a
+      , coptionalSet = \(a, c) b -> (,c) <$> coptionalSet o a b
+      }
+
+  csecond' o =
+    ConcreteOptional
+      { coptionalGet = \(c, a) -> left (fmap (c,)) <$> coptionalGet o a
+      , coptionalSet = \(c, a) b -> (c,) <$> coptionalSet o a b
+      }
+
+instance CChoice r (ConcreteOptional r a b) where
+  cleft' o =
+    ConcreteOptional
+      { coptionalGet =
+          either
+            ( coptionalGet o
+                >=> return . left (fmap Left)
+            )
+            (return . Left . return . Right)
+      , coptionalSet =
+          \e b -> either (\a -> Left <$> coptionalSet o a b) (return . Right) e
+      }
+
+  cright' o =
+    ConcreteOptional
+      { coptionalGet =
+          either
+            (return . Left . return . Left)
+            ( coptionalGet o
+                >=> return . left (fmap Right)
+            )
+      , coptionalSet =
+          \e b -> either (return . Left) (\a -> Right <$> coptionalSet o a b) e
+      }
+
+instance IsCIso r (ConcreteOptional r a b)
+instance IsCLens r (ConcreteOptional r a b)
+instance IsCPrism r (ConcreteOptional r a b)
+instance IsCOptional r (ConcreteOptional r a b)
diff --git a/Plutarch/CPS/Optics/Prism.hs b/Plutarch/CPS/Optics/Prism.hs
new file mode 100644
index 0000000..4f8dfaf
--- /dev/null
+++ b/Plutarch/CPS/Optics/Prism.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Optics.Prism where
+
+import Control.Monad
+import Control.Monad.Trans.Cont
+import Plutarch.CPS.Optics.Iso
+import Plutarch.CPS.Optics.Optic
+import Plutarch.CPS.Profunctor
+
+type CPrism r s t a b = forall p. IsCPrism r p => COptic r p s t a b
+
+type CPrism' r a b = CPrism r a a b b
+
+class (IsCIso r p, CChoice r p) => IsCPrism r p
+
+instance (Applicative f) => IsCPrism r (CStar r f)
+
+cprism :: (b -> Cont r t) -> (s -> Cont r (Either t a)) -> CPrism r s t a b
+cprism inj prj = cdimap prj (either return inj) . cright'
+
+cprism' :: (b -> Cont r s) -> (s -> Cont r (Maybe a)) -> CPrism r s s a b
+cprism' inj prj = cprism inj (\s -> prj s >>= maybe (return $ Left s) (return . Right))
+
+withCPrism ::
+  CPrism r s t a b ->
+  ((b -> Cont r t) -> (s -> Cont r (Either t a)) -> r') ->
+  r'
+withCPrism o f =
+  f (cprismSet l) (cprismGet l >=> either (fmap Left) (return . Right))
+  where
+    l = o $ ConcretePrism {cprismSet = return, cprismGet = return . Right}
+
+data ConcretePrism r a b s t = ConcretePrism
+  { cprismGet :: s -> Cont r (Either t a)
+  , cprismSet :: b -> t
+  }
+
+instance CProfunctor r (ConcretePrism r a b) where
+  cdimap ab cd p =
+    ConcretePrism
+      { cprismGet =
+          ab
+            >=> cprismGet p
+            >=> either
+              (\c -> Left . return <$> (c >>= cd))
+              (return . Right)
+      , cprismSet = cprismSet p >=> cd
+      }
+
+instance CChoice r (ConcretePrism r a b) where
+  cleft' p =
+    ConcretePrism
+      { cprismGet =
+          either
+            (cprismGet p >=> either (fmap (Left . return . Left)) (return . Right))
+            (return . Left . return . Right)
+      , cprismSet = fmap Left . cprismSet p
+      }
+
+instance IsCIso r (ConcretePrism r a b)
+instance IsCPrism r (ConcretePrism r a b)
diff --git a/Plutarch/CPS/Optics/Traversal.hs b/Plutarch/CPS/Optics/Traversal.hs
new file mode 100644
index 0000000..ea1ce85
--- /dev/null
+++ b/Plutarch/CPS/Optics/Traversal.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Optics.Traversal(
+  CTraversal,
+  CTraversal',
+  ctraverse,
+  ctraverseOf,
+  ctraversal,
+  ) where
+
+import Control.Monad.Trans.Cont
+import Plutarch.CPS.Optics.Optic
+import Plutarch.CPS.Optics.Optional
+import Plutarch.CPS.Profunctor
+
+type CTraversal r s t a b = forall p. (IsCTraversal r p) => COptic r p s t a b
+
+type CTraversal' r s a = CTraversal r s s a a
+
+class (IsCOptional r p, CMonoidal r p) => IsCTraversal r p
+
+instance (Applicative f) => IsCTraversal r (CStar r f)
+
+ctraverse :: (CChoice r p, CMonoidal r p) => p a (Cont r b) -> p (FunList a c t) (Cont r (FunList b c t))
+ctraverse k = cdimap (return . unFunList) (return . FunList) . cright' $ cpar k (ctraverse k)
+
+ctraverseOf ::
+  (Applicative f) =>
+  CTraversal r s t a b ->
+  (a -> Cont r (f b)) ->
+  s ->
+  Cont r (f (Cont r t))
+ctraverseOf p = runCStar . p . CStar . (fmap . fmap . fmap) return
+
+newtype FunList a b t = FunList {unFunList :: Either t (a, FunList a b (b -> t))}
+
+single :: a -> FunList a b b
+single a = FunList $ Right (a, FunList $ Left id)
+
+instance Functor (FunList a b) where
+  fmap f (FunList (Left t)) = FunList (Left (f t))
+  fmap f (FunList (Right (a, as))) = FunList (Right (a, fmap (f .) as))
+
+instance Applicative (FunList a b) where
+  pure = FunList . Left
+  FunList (Left f) <*> l' = fmap f l'
+  FunList (Right (a, l)) <*> l' = FunList (Right (a, fmap flip l <*> l'))
+
+fuse :: FunList b b t -> Cont r t
+fuse = either return (\(a, c) -> ($ a) <$> fuse c) . unFunList
+
+ctraversal ::
+  (forall f. Applicative f => (a -> f b) -> (s -> Cont r (f t))) ->
+  CTraversal r s t a b
+ctraversal h = cdimap (h single) fuse . ctraverse
diff --git a/Plutarch/CPS/Profunctor.hs b/Plutarch/CPS/Profunctor.hs
new file mode 100644
index 0000000..bd773f9
--- /dev/null
+++ b/Plutarch/CPS/Profunctor.hs
@@ -0,0 +1,77 @@
+{-# LANGUAGE FlexibleInstances #-}
+
+module Plutarch.CPS.Profunctor where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Trans.Cont
+import Data.Tuple
+
+newtype CStar r f a b = CStar {runCStar :: a -> Cont r (f b)}
+
+class CProfunctor r p where
+  cdimap :: (a -> Cont r b) -> (c -> Cont r d) -> p b (Cont r c) -> p a (Cont r d)
+
+clmap :: (CProfunctor r p) => (a -> Cont r b) -> p b (Cont r c) -> p a (Cont r c)
+clmap f = cdimap f return
+
+crmap :: (CProfunctor r p) => (b -> Cont r c) -> p a (Cont r b) -> p a (Cont r c)
+crmap = cdimap return
+
+instance CProfunctor r (->) where
+  cdimap ab cd bc = ab >=> bc >=> cd
+
+instance (Functor f) => CProfunctor r (CStar r f) where
+  cdimap ab cd (CStar bc) = CStar $ ab >=> bc >=> return . fmap (>>= cd)
+
+class (CProfunctor r p) => CStrong r p where
+  cfirst' :: p a (Cont r b) -> p (a, c) (Cont r (b, c))
+  cfirst' = cdimap (return . swap) (return . swap) . csecond'
+
+  csecond' :: p a (Cont r b) -> p (c, a) (Cont r (c, b))
+  csecond' = cdimap (return . swap) (return . swap) . cfirst'
+
+instance CStrong r (->) where
+  cfirst' ab (a, c) = (,c) <$> ab a
+  csecond' ab (c, a) = (c,) <$> ab a
+
+instance (Functor f) => CStrong r (CStar r f) where
+  cfirst' (CStar afb) = CStar \(a, c) -> (fmap . fmap . fmap) (,c) (afb a)
+  csecond' (CStar afb) = CStar \(c, a) -> (fmap . fmap . fmap) (c,) (afb a)
+
+class (CProfunctor r p) => CChoice r p where
+  cleft' :: p a (Cont r b) -> p (Either a c) (Cont r (Either b c))
+  cleft' = cdimap (return . either Right Left) (return . either Right Left) . cright'
+
+  cright' :: p a (Cont r b) -> p (Either c a) (Cont r (Either c b))
+  cright' = cdimap (return . either Right Left) (return . either Right Left) . cleft'
+
+instance CChoice r (->) where
+  cleft' ab = either (fmap Left . ab) (return . Right)
+  cright' ab = either (return . Left) (fmap Right . ab)
+
+instance (Applicative f) => CChoice r (CStar r f) where
+  cleft' (CStar afb) =
+    CStar $
+      either
+        ((fmap . fmap . fmap) Left . afb)
+        (return . pure . return . Right)
+
+  cright' (CStar afb) =
+    CStar $
+      either
+        (return . pure . return . Left)
+        ((fmap . fmap . fmap) Right . afb)
+
+class (CProfunctor r p) => CMonoidal r p where
+  cunit :: p () (Cont r ())
+  cpar :: p a (Cont r b) -> p c (Cont r d) -> p (a, c) (Cont r (b, d))
+
+instance CMonoidal r (->) where
+  cunit () = return ()
+  cpar ab cd (a, c) = (,) <$> ab a <*> cd c
+
+instance (Applicative f) => CMonoidal r (CStar r f) where
+  cunit = CStar $ \() -> return . pure . return $ ()
+  cpar (CStar afb) (CStar cfd) =
+    CStar (\(a, c) -> (liftA2 . liftA2) (,) <$> afb a <*> cfd c)
diff --git a/Plutarch/Cont.hs b/Plutarch/Cont.hs
new file mode 100644
index 0000000..5751fc2
--- /dev/null
+++ b/Plutarch/Cont.hs
@@ -0,0 +1,17 @@
+module Plutarch.Cont(PCont, pmatchCont) where
+
+import Control.Monad.Trans.Cont
+
+import Plutarch.Core
+
+type PCont edsl r = Cont (Term edsl r)
+
+pmatchCont ::
+  (
+    PConstructable edsl a,
+    IsPType edsl r
+  ) =>
+  (PConcrete edsl a -> PCont edsl r b) ->
+  Term edsl a ->
+  PCont edsl r b
+pmatchCont cnt t = cont \c -> pmatch t \con -> runCont (cnt con) c
\ No newline at end of file
diff --git a/Plutarch/Core.hs b/Plutarch/Core.hs
index cd0553a..9bd9359 100644
--- a/Plutarch/Core.hs
+++ b/Plutarch/Core.hs
@@ -33,6 +33,9 @@ module Plutarch.Core (
   PDelay (PDelay),
   PPair (PPair),
   PEither (PLeft, PRight),
+  peither,
+  pleft,
+  pright,
   PForall (PForall),
   PSome (PSome),
   PFix (PFix),
@@ -41,6 +44,7 @@ module Plutarch.Core (
   PSOP,
   PIsSOP,
   PUnit (PUnit),
+  punit,
   PDSL,
   PLC,
   unTerm,
@@ -57,9 +61,11 @@ module Plutarch.Core (
   papl,
   PIsProduct,
   PIsSum,
+  PCode,
   IsPCodeOf,
   sopFrom,
   sopTo,
+  (:-->),
 ) where
 
 import Data.Functor.Compose (Compose)
@@ -268,12 +274,31 @@ instance PHasRepr (PSome ef) where type PReprSort _ = PReprPrimitive
 newtype PFix f ef = PFix (ef /$ f (PFix f))
 instance PHasRepr (PFix f) where type PReprSort _ = PReprPrimitive
 
+punit :: (PConstructable edsl PUnit) => Term edsl PUnit
+punit = pcon PUnit
+
 data PUnit (ef :: PTypeF) = PUnit deriving stock (Generic)
 instance PHasRepr PUnit where type PReprSort _ = PReprPrimitive
 
 data PPair a b ef = PPair (ef /$ a) (ef /$ b) deriving stock (Generic)
 instance PHasRepr (PPair a b) where type PReprSort _ = PReprPrimitive
 
+pleft :: (PSOP edsl, IsPType edsl a, IsPType edsl b) => Term edsl a -> Term edsl (PEither a b)
+pleft = pcon . PLeft
+
+pright :: (PSOP edsl, IsPType edsl a, IsPType edsl b) => Term edsl b -> Term edsl (PEither a b)
+pright = pcon . PRight
+
+peither ::
+  (PSOP edsl, IsPType edsl a, IsPType edsl b, IsPType edsl c) =>
+  (Term edsl a -> Term edsl c) ->
+  (Term edsl b -> Term edsl c) ->
+  Term edsl (PEither a b) ->
+  Term edsl c
+peither f g te = pmatch te \case
+  PLeft x -> f x
+  PRight x -> g x
+
 data PEither a b ef = PLeft (ef /$ a) | PRight (ef /$ b) deriving stock (Generic)
 instance PHasRepr (PEither a b) where type PReprSort _ = PReprPrimitive
 
@@ -341,6 +366,10 @@ type PSOP edsl =
   , IsPType edsl PPType
   )
 
+
+type family PCode edsl a where
+  PCode edsl a = SOPG.GCode (PConcrete edsl a)
+
 class
   ( SOP.AllZip2 (SOP.LiftedCoercible SOP.I (Term edsl)) tss pss
   , SOP.AllZip2 (SOP.LiftedCoercible (Term edsl) SOP.I) pss tss
@@ -377,3 +406,6 @@ type Compile variant output =
   (HasCallStack, Monad m, forall edsl. variant edsl => IsPType edsl a) =>
   (forall edsl. (variant edsl, PEmbeds m edsl) => Term edsl a) ->
   m output
+
+-- | Useful combinator for unembedded functions.
+type (:-->) a b edsl = Term edsl a -> Term edsl b
diff --git a/Plutarch/Optics/Fix.hs b/Plutarch/Optics/Fix.hs
new file mode 100644
index 0000000..871b5c4
--- /dev/null
+++ b/Plutarch/Optics/Fix.hs
@@ -0,0 +1,167 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Plutarch.Optics.Fix(
+  pfix,
+  PFixable,
+  pconstrained,
+  ptraverse,
+  PTraversible,
+  ) where
+
+import Data.Function
+import Data.Profunctor
+
+import Generics.SOP
+
+import Plutarch.Core
+import Plutarch.Cont
+import Plutarch.CPS.Optics.Traversal
+import Generics.SOP.GGP
+import Data.Kind
+
+class
+  ( PConstructable edsl (PFix a)
+  , PConstructable edsl (a (PFix a))
+  ) => PFixable edsl a
+instance
+  ( PConstructable edsl (PFix a)
+  , PConstructable edsl (a (PFix a))
+  ) => PFixable edsl a
+
+-- | Not a 'Plutarch.CPS.Optics.Traversal.CTraversal', but can be used to construct one.
+pfix ::
+  (
+    PFixable edsl a,
+    PFixable edsl b,
+    PConstructable edsl r,
+    Applicative f
+  ) =>
+  (
+    forall ra rb.
+    (
+      PConstructable edsl (a ra),
+      PConstructable edsl (b rb)
+    ) =>
+    (Term edsl    ra    -> PCont edsl r (f (Term edsl    rb  ))) ->
+     Term edsl (a ra  ) -> PCont edsl r (f (Term edsl (b rb  )))
+  ) ->
+     Term edsl (PFix a) -> PCont edsl r (f (Term edsl (PFix b)))
+pfix f =
+  pmatchCont \(PFix a) ->
+    fmap (pcon . PFix)
+      <$> fix
+        (f .
+          dimap
+            (\fa -> pmatch fa \(PFix a') -> a')
+            (fmap (fmap (pcon . PFix)))
+        )
+        a
+
+class (forall r. PGeneric (a r)) => PGeneric1 a
+instance (forall r. PGeneric (a r)) => PGeneric1 a
+
+class
+  ( AllZip2 (Fixer c (Term edsl ra) (Term edsl rb)) (GCode (PConcrete edsl (a ra))) (GCode (PConcrete edsl (b rb)))
+  , SListI2 (GCode (PConcrete edsl (b rb)))
+  ) => PConstrained' edsl c a b ra rb
+instance
+  ( AllZip2 (Fixer c (Term edsl ra) (Term edsl rb)) (GCode (PConcrete edsl (a ra))) (GCode (PConcrete edsl (b rb)))
+  , SListI2 (GCode (PConcrete edsl (b rb)))
+  ) => PConstrained' edsl c a b ra rb
+
+class
+  ( PFixable edsl a
+  , PFixable edsl b
+  , (forall ra rb. PConstrained' edsl c a b ra rb)
+  , PGeneric1 a
+  , PGeneric1 b
+  ) => PConstrainedFixable edsl c a b
+instance
+  ( PFixable edsl a
+  , PFixable edsl b
+  , PGeneric1 a
+  , PGeneric1 b
+  , (forall ra rb. PConstrained' edsl c a b ra rb)
+  ) => PConstrainedFixable edsl c a b
+
+
+
+pconstrained ::
+  forall edsl f a b r (c :: Type -> Type -> Constraint).
+  ( PConstrainedFixable edsl c a b
+  , PConstructable edsl r
+  , Applicative f
+  ) =>
+  Proxy c ->
+  (forall a' b'. c a' b' => a' -> PCont edsl r (f b')) ->
+  Term edsl (PFix a) ->
+  PCont edsl r (f (Term edsl (PFix b)))
+pconstrained _ f =
+  pfix fixer
+  where
+    fixer ::
+      forall ra rb.
+      ( PConstructable edsl (a ra)
+      , PConstructable edsl (b rb)
+      , AllZip2 (Fixer c (Term edsl ra) (Term edsl rb)) (GCode (PConcrete edsl (a ra))) (GCode (PConcrete edsl (b rb)))
+      , SListI2 (GCode (PConcrete edsl (b rb)))
+      ) =>
+      (Term edsl ra -> PCont edsl r (f (Term edsl rb))) ->
+      Term edsl (a ra) ->
+      PCont edsl r (f (Term edsl (b rb)))
+    fixer r =
+      pmatchCont $
+        fmap (fmap (pcon . gto) . hsequence')
+        . hsequence'
+        . htrans
+          (Proxy @(Fixer c (Term edsl ra) (Term edsl rb)))
+          (Comp . fmap (Comp . fmap I) . fixerTrans @c r f . unI)
+        . gfrom
+
+class Fixer c a b a' b' where
+  fixerTrans ::
+    (a -> PCont edsl r (f b)) ->
+    (c a' b' => a' -> PCont edsl r (f b')) ->
+    a' ->
+    PCont edsl r (f b')
+
+instance Fixer c a b a b where
+  fixerTrans f _ = f
+
+instance (c a' b') => Fixer c a b a' b' where
+  fixerTrans _ f = f
+
+class (forall a b. PConstrainedFixable edsl (PTraverse (Term edsl a) (Term edsl b)) (t a) (t b)) => PTraversible edsl t 
+instance (forall a b. PConstrainedFixable edsl (PTraverse (Term edsl a) (Term edsl b)) (t a) (t b)) => PTraversible edsl t 
+
+ptraverse ::
+    forall edsl a b t r.
+  ( PTraversible edsl t
+  , PConstructable edsl r
+  ) =>
+  CTraversal
+    (Term edsl r)
+    (Term edsl (PFix (t a)))
+    (Term edsl (PFix (t b)))
+    (Term edsl a)
+    (Term edsl b)
+ptraverse =
+  ctraversal
+    \f -> pconstrained (Proxy @(PTraverse (Term edsl a) (Term edsl b))) (return . ptraverse' f)
+
+class PTraverse a b a' b' where
+  ptraverse' ::
+    Applicative f =>
+    (a -> f b) ->
+    a' ->
+    f b'
+
+instance PTraverse a b a b where
+  ptraverse' = ($)
+
+instance PTraverse a b a' a' where
+  ptraverse' _ = pure
\ No newline at end of file
diff --git a/Plutarch/Optics/Optic.hs b/Plutarch/Optics/Optic.hs
new file mode 100644
index 0000000..a58ba4b
--- /dev/null
+++ b/Plutarch/Optics/Optic.hs
@@ -0,0 +1,8 @@
+module Plutarch.Optics.Optic (
+  POptic,
+  POptic',
+) where
+
+type POptic p s t a b = p a b -> p s t
+
+type POptic' p s a = POptic p s s a a
diff --git a/Plutarch/Optics/PEither.hs b/Plutarch/Optics/PEither.hs
new file mode 100644
index 0000000..4c7efba
--- /dev/null
+++ b/Plutarch/Optics/PEither.hs
@@ -0,0 +1,38 @@
+module Plutarch.Optics.PEither where
+
+import Plutarch.CPS.Optics.Prism
+
+import Plutarch.Core
+import Plutarch.Cont
+
+_PLeft ::
+  (PSOP edsl, IsPType edsl a, IsPType edsl a', IsPType edsl b, IsPType edsl r) =>
+  CPrism
+    (Term edsl r)
+    (Term edsl (PEither a b))
+    (Term edsl (PEither a' b))
+    (Term edsl a)
+    (Term edsl a')
+_PLeft =
+  cprism
+    (return . pleft)
+    (pmatchCont \case
+      PLeft a -> return $ Right a
+      PRight b -> return $ Left (pright b)
+    )
+
+_PRight ::
+  (PSOP edsl, IsPType edsl a, IsPType edsl b, IsPType edsl b', IsPType edsl r) =>
+  CPrism
+    (Term edsl r)
+    (Term edsl (PEither a b))
+    (Term edsl (PEither a b'))
+    (Term edsl b)
+    (Term edsl b')
+_PRight =
+  cprism
+    (return . pright)
+    (pmatchCont \case
+        PLeft a -> return $ Left (pleft a)
+        PRight b -> return $ Right b
+    )
diff --git a/Plutarch/Optics/PList.hs b/Plutarch/Optics/PList.hs
new file mode 100644
index 0000000..ba13e1c
--- /dev/null
+++ b/Plutarch/Optics/PList.hs
@@ -0,0 +1,36 @@
+module Plutarch.Optics.PList where
+
+import Plutarch.CPS.Optics.Traversal
+import Plutarch.Core
+import Plutarch.PList
+import Plutarch.Optics.Fix
+import Plutarch.CPS.Profunctor
+import Plutarch.Cont
+
+plist
+  ::
+  ( PTraversible edsl PListF
+  , PConstructable edsl (PList a)
+  , PConstructable edsl (PList b)
+  , PConstructable edsl r) =>
+  CTraversal
+    (Term edsl r)
+    (Term edsl (PList a))
+    (Term edsl (PList b))
+    (Term edsl a)
+    (Term edsl b)
+plist =
+  cdimap (pmatchCont (\(PList as) -> return as)) (return . pcon . PList)
+    . plist'
+
+plist'
+  ::
+  ( PTraversible edsl PListF
+  , PConstructable edsl r) =>
+  CTraversal
+    (Term edsl r)
+    (Term edsl (PFix (PListF a)))
+    (Term edsl (PFix (PListF b)))
+    (Term edsl a)
+    (Term edsl b)
+plist' = ptraverse
\ No newline at end of file
diff --git a/Plutarch/Optics/PPair.hs b/Plutarch/Optics/PPair.hs
new file mode 100644
index 0000000..4645730
--- /dev/null
+++ b/Plutarch/Optics/PPair.hs
@@ -0,0 +1,31 @@
+module Plutarch.Optics.PPair where
+
+import Plutarch.Core
+
+import Plutarch.CPS.Optics.Lens
+
+pfst ::
+  (PSOP edsl, IsPType edsl a, IsPType edsl a', IsPType edsl b) =>
+  CLens
+    r
+    (Term edsl (PPair a b))
+    (Term edsl (PPair a' b))
+    (Term edsl a)
+    (Term edsl a')
+pfst =
+  clens
+    (\tp -> return $ pmatch tp \(PPair a _) -> a)
+    (\ts a' -> return $ pmatch ts \(PPair _ b) -> pcon $ PPair a' b)
+
+psnd ::
+  (PSOP edsl, IsPType edsl a, IsPType edsl b, IsPType edsl b') =>
+  CLens
+    r
+    (Term edsl (PPair a b))
+    (Term edsl (PPair a b'))
+    (Term edsl b)
+    (Term edsl b')
+psnd =
+  clens
+    (\tp -> return $ pmatch tp \(PPair _ b) -> b)
+    (\ts b' -> return $ pmatch ts \(PPair a _) -> pcon $ PPair a b')
diff --git a/Plutarch/PList.hs b/Plutarch/PList.hs
new file mode 100644
index 0000000..1b465b9
--- /dev/null
+++ b/Plutarch/PList.hs
@@ -0,0 +1,40 @@
+module Plutarch.PList where
+
+import GHC.Generics
+import Plutarch.Core
+import Plutarch.PType
+
+data PListF a self ef
+  = PNil
+  | PCons (ef /$ a) (ef /$ self)
+  deriving stock (Generic)
+  deriving anyclass PHasRepr
+
+newtype PList a ef = PList {unPList :: ef /$ PFix (PListF a)}
+  deriving stock (Generic)
+  deriving anyclass PHasRepr
+
+mkPList ::
+  ( PSOP edsl
+  , PConstructable edsl (PFix (PListF a))
+  ) =>
+  PConcrete edsl (PListF a (PFix (PListF a))) ->
+  Term edsl (PList a)
+mkPList = pcon . PList . pcon . PFix . pcon
+
+pnil ::
+  ( PSOP edsl
+  , PConstructable edsl (PFix (PListF a))
+  ) =>
+  Term edsl (PList a)
+pnil = mkPList PNil
+
+pcons ::
+  ( PSOP edsl
+  , IsPType edsl (PFix (PListF a))
+  , PConstructable edsl (PFix (PListF a))
+  ) =>
+  Term edsl a ->
+  Term edsl (PList a) ->
+  Term edsl (PList a)
+pcons a las = mkPList $ PCons a (pmatch las unPList)
diff --git a/Plutarch/STLC.hs b/Plutarch/STLC.hs
index 6e9d7dd..9e2bd1e 100644
--- a/Plutarch/STLC.hs
+++ b/Plutarch/STLC.hs
@@ -10,7 +10,7 @@ import GHC.Stack (callStack)
 import qualified Generics.SOP as SOP
 import qualified Generics.SOP.GGP as SOPG
 import Plutarch.Core
-import Plutarch.EType
+import Plutarch.PType
 
 newtype Lvl = Lvl Int
 
@@ -37,12 +37,12 @@ data SimpleTerm
   | MkSumRight SimpleType SimpleTerm
   | Match SimpleTerm SimpleTerm SimpleTerm
 
-type ESTLC edsl = (ELC edsl, ESOP edsl)
+type ESTLC edsl = (ELC edsl, PSOP edsl)
 
 newtype Impl (m :: Type -> Type) (a :: ETypeRepr) = Impl {runImpl :: Lvl -> m SimpleTerm}
 
 instance EDSL (Impl m) where
-  type IsEType' (Impl m) = TypeInfo' m
+  type IsPType' (Impl m) = TypeInfo' m
 
 class TypeInfo' (m :: Type -> Type) (a :: ETypeRepr) where
   typeInfo' :: Proxy m -> Proxy a -> SimpleType
@@ -56,34 +56,34 @@ typeInfo p _ = typeInfo' p (Proxy @(ERepr a))
 instance TypeInfo' m (MkETypeRepr EUnit) where
   typeInfo' _ _ = UnitType
 
-instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m (MkETypeRepr (EPair a b)) where
+instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m (MkETypeRepr (PPair a b)) where
   typeInfo' m _ = ProductType (typeInfo m $ Proxy @a) (typeInfo m $ Proxy @b)
 
-instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m (MkETypeRepr (EEither a b)) where
+instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m (MkETypeRepr (PEither a b)) where
   typeInfo' m _ = SumType (typeInfo m $ Proxy @a) (typeInfo m $ Proxy @b)
 
 instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m (MkETypeRepr (a #-> b)) where
   typeInfo' m _ = FunctionType (typeInfo m $ Proxy @a) (typeInfo m $ Proxy @b)
 
-instance Applicative m => EConstructable' (Impl m) (MkETypeRepr EUnit) where
+instance Applicative m => PConstructable' (Impl m) (MkETypeRepr EUnit) where
   econImpl EUnit = Impl $ \_ -> pure MkUnit
   ematchImpl _ f = f EUnit
 
-instance (Applicative m, TypeInfo m a, TypeInfo m b) => EConstructable' (Impl m) (MkETypeRepr (EPair a b)) where
-  econImpl (EPair (Term x) (Term y)) = Impl \lvl -> MkProduct <$> (runImpl x lvl) <*> (runImpl y lvl)
+instance (Applicative m, TypeInfo m a, TypeInfo m b) => PConstructable' (Impl m) (MkETypeRepr (PPair a b)) where
+  econImpl (PPair (Term x) (Term y)) = Impl \lvl -> MkProduct <$> (runImpl x lvl) <*> (runImpl y lvl)
   ematchImpl t f = Term $ Impl \lvl ->
-    Let <$> runImpl t lvl <*> (flip runImpl (succLvl lvl) $ unTerm $ f $ EPair (Term $ Impl \_ -> pure $ Fst (Var lvl)) (Term $ Impl \_ -> pure $ Snd (Var lvl)))
+    Let <$> runImpl t lvl <*> (flip runImpl (succLvl lvl) $ unTerm $ f $ PPair (Term $ Impl \_ -> pure $ Fst (Var lvl)) (Term $ Impl \_ -> pure $ Snd (Var lvl)))
 
-instance (Applicative m, TypeInfo m a, TypeInfo m b) => EConstructable' (Impl m) (MkETypeRepr (EEither a b)) where
-  econImpl (ELeft (Term x)) = Impl \lvl -> MkSumLeft <$> runImpl x lvl <*> pure (typeInfo (Proxy @m) $ Proxy @b)
-  econImpl (ERight (Term y)) = Impl \lvl -> MkSumRight (typeInfo (Proxy @m) $ Proxy @a) <$> (runImpl y lvl)
+instance (Applicative m, TypeInfo m a, TypeInfo m b) => PConstructable' (Impl m) (MkETypeRepr (PEither a b)) where
+  econImpl (PLeft (Term x)) = Impl \lvl -> MkSumLeft <$> runImpl x lvl <*> pure (typeInfo (Proxy @m) $ Proxy @b)
+  econImpl (PRight (Term y)) = Impl \lvl -> MkSumRight (typeInfo (Proxy @m) $ Proxy @a) <$> (runImpl y lvl)
   ematchImpl t f = Term $ Impl \lvl ->
     Match
       <$> (runImpl t lvl)
-      <*> (runImpl ((unTerm $ elam \left -> f (ELeft left))) lvl)
-      <*> (runImpl ((unTerm $ elam \right -> f (ERight right))) lvl)
+      <*> (runImpl ((unTerm $ elam \left -> f (PLeft left))) lvl)
+      <*> (runImpl ((unTerm $ elam \right -> f (PRight right))) lvl)
 
-instance (Applicative m, TypeInfo m a, TypeInfo m b) => EConstructable' (Impl m) (MkETypeRepr (a #-> b)) where
+instance (Applicative m, TypeInfo m a, TypeInfo m b) => PConstructable' (Impl m) (MkETypeRepr (a #-> b)) where
   econImpl (ELam f) = Impl \lvl -> Lam (typeInfo (Proxy @m) $ Proxy @a) <$> runImpl (unTerm . f . Term $ Impl \_ -> pure $ Var lvl) (succLvl lvl)
   ematchImpl f g = g $ ELam \(Term x) -> Term $ Impl \lvl -> App <$> runImpl f lvl <*> runImpl x lvl
 
@@ -96,34 +96,34 @@ instance Monad m => EEmbeds m (Impl m) where
     t' <- t
     runImpl (unTerm $ t') lvl
 
-gpInfo :: forall (a :: [EType]) m. SOP.All (TypeInfo m) a => Proxy m -> Proxy a -> SimpleType
+gpInfo :: forall (a :: [PType]) m. SOP.All (TypeInfo m) a => Proxy m -> Proxy a -> SimpleType
 gpInfo _ _ = getConst $ (SOP.cpara_SList (Proxy @(TypeInfo m)) (Const UnitType) go :: Const SimpleType a)
   where
     go :: forall y ys. TypeInfo m y => Const SimpleType ys -> Const SimpleType (y : ys)
     go (Const UnitType) = Const $ typeInfo (Proxy @m) (Proxy @y)
     go (Const x) = Const $ ProductType (typeInfo (Proxy @m) (Proxy @y)) x
 
-gsInfo :: forall (a :: [[EType]]) m. SOP.All2 (TypeInfo m) a => Proxy m -> Proxy a -> SimpleType
+gsInfo :: forall (a :: [[PType]]) m. SOP.All2 (TypeInfo m) a => Proxy m -> Proxy a -> SimpleType
 gsInfo _ _ = getConst $ (SOP.cpara_SList (Proxy @(SOP.All (TypeInfo m))) (Const VoidType) go :: Const SimpleType a)
   where
     go :: forall y ys. (SOP.All (TypeInfo m) y) => Const SimpleType ys -> Const SimpleType (y : ys)
     go (Const VoidType) = Const $ gpInfo (Proxy @m) (Proxy @y)
     go (Const x) = Const $ SumType (gpInfo (Proxy @m) (Proxy @y)) x
 
-gpCon :: forall (a :: [EType]) m. (Applicative m, SOP.All (TypeInfo m) a) => SOP.NP (Term (Impl m)) a -> Lvl -> m (SimpleTerm)
+gpCon :: forall (a :: [PType]) m. (Applicative m, SOP.All (TypeInfo m) a) => SOP.NP (Term (Impl m)) a -> Lvl -> m (SimpleTerm)
 gpCon SOP.Nil _ = pure MkUnit
 gpCon (x SOP.:* SOP.Nil) lvl = runImpl (unTerm x) lvl
 gpCon (x SOP.:* xs) lvl = MkProduct <$> runImpl (unTerm x) lvl <*> gpCon xs lvl
 
 -- FIXME: Ormolu doesn't support `@` in patterns
 {- ORMOLU_DISABLE -}
-gsCon :: forall (a :: [[EType]]) m. (Applicative m, SOP.All2 (TypeInfo m) a) => SOP.SOP (Term (Impl m)) a -> Lvl -> m (SimpleTerm)
-gsCon (SOP.SOP (SOP.Z @_ @_ @_ @(at :: [[EType]]) t)) = case SOP.sList :: SOP.SList at of
+gsCon :: forall (a :: [[PType]]) m. (Applicative m, SOP.All2 (TypeInfo m) a) => SOP.SOP (Term (Impl m)) a -> Lvl -> m (SimpleTerm)
+gsCon (SOP.SOP (SOP.Z @_ @_ @_ @(at :: [[PType]]) t)) = case SOP.sList :: SOP.SList at of
   SOP.SNil -> gpCon t
   SOP.SCons -> \lvl -> MkSumLeft <$> (gpCon t lvl) <*> (pure $ gsInfo (Proxy @m) (Proxy @at))
-gsCon (SOP.SOP (SOP.S @_ @_ @_ @(ah :: [EType]) sum)) = \lvl -> MkSumRight (gpInfo (Proxy @m) (Proxy @ah)) <$> (gsCon (SOP.SOP sum) lvl)
+gsCon (SOP.SOP (SOP.S @_ @_ @_ @(ah :: [PType]) sum)) = \lvl -> MkSumRight (gpInfo (Proxy @m) (Proxy @ah)) <$> (gsCon (SOP.SOP sum) lvl)
 
-gpMatch :: forall (a :: [EType]) m a' b. (Applicative m, SOP.All (TypeInfo m) a) => Impl m a' -> (SOP.NP (Term (Impl m)) a -> Term (Impl m) b) -> Term (Impl m) b
+gpMatch :: forall (a :: [PType]) m a' b. (Applicative m, SOP.All (TypeInfo m) a) => Impl m a' -> (SOP.NP (Term (Impl m)) a -> Term (Impl m) b) -> Term (Impl m) b
 gpMatch = case SOP.sList :: SOP.SList a of
   SOP.SNil -> \_ f -> f SOP.Nil
   SOP.SCons @_ @at -> case SOP.sList :: SOP.SList at of
@@ -134,7 +134,7 @@ gpMatch = case SOP.sList :: SOP.SList a of
           (f $ (Term $ Impl \_ -> pure $ Fst (Var lvl)) SOP.:* sop)
       )
 
-gsMatch :: forall (a :: [[EType]]) m a' b. (Applicative m, SOP.All2 (TypeInfo m) a) => Impl m a' -> (SOP.SOP (Term (Impl m)) a -> Term (Impl m) b) -> Term (Impl m) b
+gsMatch :: forall (a :: [[PType]]) m a' b. (Applicative m, SOP.All2 (TypeInfo m) a) => Impl m a' -> (SOP.SOP (Term (Impl m)) a -> Term (Impl m) b) -> Term (Impl m) b
 gsMatch = case SOP.sList :: SOP.SList a of
   SOP.SNil -> \(Impl t) _ -> Term $ Impl t
   SOP.SCons @_ @at @ah -> case SOP.sList :: SOP.SList at of
@@ -155,8 +155,8 @@ mapAll2 _ c d f = case (SOP.sList :: SOP.SList a) of
   SOP.SCons @_ @at @ah -> mapAll2 (Proxy @at) c d $ mapAll (Proxy @ah) c d f
 {- ORMOLU_ENABLE -}
 
-helper2 :: forall a b m. SOP.All2 (IsEType (Impl m)) a => Proxy m -> Proxy a -> (SOP.All2 (TypeInfo m) a => b) -> b
-helper2 _ _ = mapAll2 (Proxy @a) (Proxy @(IsEType (Impl m))) (Proxy @(TypeInfo m))
+helper2 :: forall a b m. SOP.All2 (IsPType (Impl m)) a => Proxy m -> Proxy a -> (SOP.All2 (TypeInfo m) a => b) -> b
+helper2 _ _ = mapAll2 (Proxy @a) (Proxy @(IsPType (Impl m))) (Proxy @(TypeInfo m))
 
 instance (EIsSOP (Impl m) a) => TypeInfo' m (MkENewtype a) where
   typeInfo' m _ =
@@ -165,10 +165,10 @@ instance (EIsSOP (Impl m) a) => TypeInfo' m (MkENewtype a) where
 
 instance
   ( EIsSOP (Impl m) a
-  , IsEType (Impl m) a
+  , IsPType (Impl m) a
   , Applicative m
   ) =>
-  EConstructable' (Impl m) (MkENewtype a)
+  PConstructable' (Impl m) (MkENewtype a)
   where
   econImpl (ENewtype x) =
     case esop (Proxy @(Impl m)) (Proxy @a) of
@@ -177,7 +177,7 @@ instance
     case esop (Proxy @(Impl m)) (Proxy @a) of
       EIsSumR {inner, to} -> helper2 (Proxy @m) inner $ gsMatch x \sop -> f $ ENewtype $ SOPG.gto (to sop)
 
-compile' :: forall a m. (Applicative m, IsEType (Impl m) a) => Term (Impl m) a -> m (SimpleTerm, SimpleType)
+compile' :: forall a m. (Applicative m, IsPType (Impl m) a) => Term (Impl m) a -> m (SimpleTerm, SimpleType)
 compile' (Term t) = (,) <$> runImpl t (Lvl 0) <*> pure (typeInfo (Proxy @m) $ Proxy @a)
 
 compile :: Compile ESTLC (SimpleTerm, SimpleType)
diff --git a/Plutarch/SystemF.hs b/Plutarch/SystemF.hs
index 75bfc83..5bf2ca6 100644
--- a/Plutarch/SystemF.hs
+++ b/Plutarch/SystemF.hs
@@ -11,7 +11,7 @@ import GHC.Stack (callStack)
 import Plutarch.Internal.WithDictHack (unsafeWithDict)
 import Plutarch.Experimental (EEq)
 import Plutarch.Core
-import Plutarch.EType
+import Plutarch.PType
 import qualified Generics.SOP as SOP
 import qualified Generics.SOP.GGP as SOPG
 import Data.Functor.Const (Const (Const), getConst)
@@ -74,13 +74,13 @@ type SFType = Fix SFTypeF
 
 type SFTerm = Fix (SFTermF () SFType)
 
-type ESystemF edsl = (ELC edsl, EPolymorphic edsl, ESOP edsl)
+type ESystemF edsl = (ELC edsl, EPolymorphic edsl, PSOP edsl)
 
-newtype Impl' (m :: Type -> Type) (a :: EType) = Impl {runImpl :: forall n. SNat n -> m SFTerm}
+newtype Impl' (m :: Type -> Type) (a :: PType) = Impl {runImpl :: forall n. SNat n -> m SFTerm}
 type Impl m = 'EDSLKind (Impl' m)
 
 instance EDSL (Impl m) where
-  type IsEType' (Impl m) = TypeInfo' m
+  type IsPType' (Impl m) = TypeInfo' m
 
 class TypeInfo' (m :: Type -> Type) (a :: k) where
   typeInfo' :: Proxy m -> Proxy a -> SNat n -> SFType
@@ -105,10 +105,10 @@ withEvilHack _ _ _ f = unsafeWithDict (Proxy @(TypeInfo m (EvilHack k n))) (g $
 instance TypeInfo' m EUnit where
   typeInfo' _ _ _ = Fix SFTyUnit
 
-instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((EPair a b)) where
+instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((PPair a b)) where
   typeInfo' m _ lvl = Fix $ SFTyPair (typeInfo m (Proxy @a) lvl) (typeInfo m (Proxy @b) lvl)
 
-instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((EEither a b)) where
+instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((PEither a b)) where
   typeInfo' m _ lvl = Fix $ SFTyEither (typeInfo m (Proxy @a) lvl) (typeInfo m (Proxy @b) lvl)
 
 instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((a #-> b)) where
@@ -117,34 +117,34 @@ instance (TypeInfo m a, TypeInfo m b) => TypeInfo' m ((a #-> b)) where
 instance TypeInfo' m 'EUnit where
   typeInfo' _ _ _ = Fix $ SFTyTerm $ Fix $ SFUnit
 
-instance (TypeInfo m x, TypeInfo m y) => TypeInfo' m ('EPair x y) where
+instance (TypeInfo m x, TypeInfo m y) => TypeInfo' m ('PPair x y) where
   typeInfo' m _ lvl = Fix $ SFTyTerm $ Fix $ SFPair
     (Fix $ SFTermTy $ typeInfo m (Proxy @x) lvl)
     (Fix $ SFTermTy $ typeInfo m (Proxy @y) lvl)
 
-instance forall (ef :: ETypeF) (a :: EType) (b :: EType) (m :: Type -> Type) (x :: ef /$ a).
-  (TypeInfo m x, TypeInfo m b) => TypeInfo' m ('ELeft x :: EEither a b ef) where
+instance forall (ef :: ETypeF) (a :: PType) (b :: PType) (m :: Type -> Type) (x :: ef /$ a).
+  (TypeInfo m x, TypeInfo m b) => TypeInfo' m ('PLeft x :: PEither a b ef) where
   typeInfo' m _ lvl = Fix $ SFTyTerm $ Fix $ SFLeft
     (Fix $ SFTermTy $ typeInfo m (Proxy @x) lvl)
     (typeInfo m (Proxy @b) lvl)
 
-instance forall (ef :: ETypeF) (a :: EType) (b :: EType) (m :: Type -> Type) (y :: ef /$ b).
-  (TypeInfo m a, TypeInfo m y) => TypeInfo' m ('ERight y :: EEither a b ef) where
+instance forall (ef :: ETypeF) (a :: PType) (b :: PType) (m :: Type -> Type) (y :: ef /$ b).
+  (TypeInfo m a, TypeInfo m y) => TypeInfo' m ('PRight y :: PEither a b ef) where
   typeInfo' m _ lvl = Fix $ SFTyTerm $ Fix $ SFRight
     (typeInfo m (Proxy @a) lvl)
     (Fix $ SFTermTy $ typeInfo m (Proxy @y) lvl)
 
-gpInfo :: forall (a :: [EType]) m lvl. SOP.All (TypeInfo m) a => Proxy m -> Proxy a -> SNat lvl -> SFType
+gpInfo :: forall (a :: [PType]) m lvl. SOP.All (TypeInfo m) a => Proxy m -> Proxy a -> SNat lvl -> SFType
 gpInfo _ _ lvl = getConst $ (SOP.cpara_SList (Proxy @(TypeInfo m)) (Const (Fix SFTyUnit)) go :: Const SFType a)
   where
-    go :: forall (y :: EType) ys. TypeInfo m y => Const SFType ys -> Const SFType (y : ys)
+    go :: forall (y :: PType) ys. TypeInfo m y => Const SFType ys -> Const SFType (y : ys)
     go (Const (Fix SFTyUnit)) = Const $ typeInfo (Proxy @m) (Proxy @y) lvl
     go (Const x) = Const $ Fix $ SFTyPair (typeInfo (Proxy @m) (Proxy @y) lvl) x
 
-gsInfo :: forall (a :: [[EType]]) m lvl. SOP.All2 (TypeInfo m) a => Proxy m -> Proxy a -> SNat lvl -> SFType
+gsInfo :: forall (a :: [[PType]]) m lvl. SOP.All2 (TypeInfo m) a => Proxy m -> Proxy a -> SNat lvl -> SFType
 gsInfo _ _ lvl = getConst $ (SOP.cpara_SList (Proxy @(SOP.All (TypeInfo m))) (Const (Fix SFTyVoid)) go :: Const SFType a)
   where
-    go :: forall (y :: [EType]) ys. (SOP.All (TypeInfo m) y) => Const SFType ys -> Const SFType (y : ys)
+    go :: forall (y :: [PType]) ys. (SOP.All (TypeInfo m) y) => Const SFType ys -> Const SFType (y : ys)
     go (Const (Fix SFTyVoid)) = Const $ gpInfo (Proxy @m) (Proxy @y) lvl
     go (Const x) = Const $ Fix $ SFTyEither (gpInfo (Proxy @m) (Proxy @y) lvl) x
 
@@ -158,8 +158,8 @@ mapAll2 _ c d f = case (SOP.sList :: SOP.SList a) of
   SOP.SNil -> f
   SOP.SCons @_ @at @ah -> mapAll2 (Proxy @at) c d $ mapAll (Proxy @ah) c d f
 
-helper2 :: forall a b m. SOP.All2 (IsEType (Impl m)) a => Proxy m -> Proxy a -> (SOP.All2 (TypeInfo m) a => b) -> b
-helper2 _ _ = mapAll2 (Proxy @a) (Proxy @(IsEType (Impl m))) (Proxy @(TypeInfo m))
+helper2 :: forall a b m. SOP.All2 (IsPType (Impl m)) a => Proxy m -> Proxy a -> (SOP.All2 (TypeInfo m) a => b) -> b
+helper2 _ _ = mapAll2 (Proxy @a) (Proxy @(IsPType (Impl m))) (Proxy @(TypeInfo m))
 
 instance (EIsSOP (Impl m) a) => TypeInfo' m (ESOPed a) where
   typeInfo' m _ lvl =
@@ -174,7 +174,7 @@ instance (TypeInfo m k, forall (a :: k). TypeInfo m a => TypeInfo m (f a)) => Ty
     snatIn lvl $ withEvilHack (Proxy @m) (Proxy @k) (Proxy @lvl) $
       typeInfo m (Proxy @(f (EvilHack k lvl))) (SS lvl)
 
-instance TypeInfo m f => TypeInfo' m (EForall (f :: k -> EType)) where
+instance TypeInfo m f => TypeInfo' m (EForall (f :: k -> PType)) where
   typeInfo' m _ (lvl :: SNat lvl) = Fix $ SFTyForall (Fix SFTyType) $ typeInfo m (Proxy @f) (SS lvl)
 
 instance Applicative m => EAp m (Impl m) where
@@ -186,38 +186,38 @@ instance Monad m => EEmbeds m (Impl m) where
     t' <- t
     runImpl (unTerm $ t') lvl
 
-instance (Applicative m, TypeInfo m a, TypeInfo m b) => EConstructable' (Impl m) (a #-> b) where
+instance (Applicative m, TypeInfo m a, TypeInfo m b) => PConstructable' (Impl m) (a #-> b) where
   econImpl (ELam f) = Impl \lvl -> fmap Fix $ SFLam (typeInfo (Proxy @m) (Proxy @a) lvl) <$> runImpl (unTerm . f . Term $ Impl \_ -> pure $ Fix $ SFVar (lvlFromSNat lvl)) (SS lvl)
   --ematchImpl f g = g $ ELam \(Term x) -> Term $ Impl \lvl -> runImpl f lvl `SFApp` runImpl x lvl
 {-
 
-instance EConstructable Impl EUnit where
-  econ EUnit = Term $ Impl \_ -> SFUnit'
-  ematch _ f = f EUnit
+instance PConstructable Impl EUnit where
+  pcon EUnit = Term $ Impl \_ -> SFUnit'
+  pmatch _ f = f EUnit
 
-instance (TypeInfo a, TypeInfo b) => EConstructable Impl (EPair a b) where
-  econ (EPair (Term x) (Term y)) = Term $ Impl \lvl -> SFPair' (runImpl x lvl) (runImpl y lvl)
-  ematch (Term t) f = f $ EPair (Term $ Impl \lvl -> SFFst' $ runImpl t lvl) (Term $ Impl \lvl -> SFSnd' $ runImpl t lvl)
+instance (TypeInfo a, TypeInfo b) => PConstructable Impl (PPair a b) where
+  pcon (PPair (Term x) (Term y)) = Term $ Impl \lvl -> SFPair' (runImpl x lvl) (runImpl y lvl)
+  pmatch (Term t) f = f $ PPair (Term $ Impl \lvl -> SFFst' $ runImpl t lvl) (Term $ Impl \lvl -> SFSnd' $ runImpl t lvl)
 
-instance (TypeInfo a, TypeInfo b) => EConstructable Impl (EEither a b) where
-  econ (ELeft (Term x)) = Term $ Impl \lvl -> SFLeft' (runImpl x lvl) (typeInfo (Proxy @b) lvl)
-  econ (ERight (Term y)) = Term $ Impl \lvl -> SFRight' (typeInfo (Proxy @a) lvl) (runImpl y lvl)
-  ematch (Term t) f = Term $ Impl \lvl ->
+instance (TypeInfo a, TypeInfo b) => PConstructable Impl (PEither a b) where
+  pcon (PLeft (Term x)) = Term $ Impl \lvl -> SFLeft' (runImpl x lvl) (typeInfo (Proxy @b) lvl)
+  pcon (PRight (Term y)) = Term $ Impl \lvl -> SFRight' (typeInfo (Proxy @a) lvl) (runImpl y lvl)
+  pmatch (Term t) f = Term $ Impl \lvl ->
     SFMatch' (runImpl t lvl)
-      (runImpl (unTerm $ elam \left -> f (ELeft left)) lvl)
-      (runImpl (unTerm $ elam \right -> f (ERight right)) lvl)
+      (runImpl (unTerm $ elam \left -> f (PLeft left)) lvl)
+      (runImpl (unTerm $ elam \right -> f (PRight right)) lvl)
 
-instance (forall a. TypeInfo a => TypeInfo (f a)) => EConstructable Impl (EForall (IsEType Impl) f) where
-  econ t' = Term $ Impl \(lvl :: SNat lvl) -> snatIn lvl $ case t' of
+instance (forall a. TypeInfo a => TypeInfo (f a)) => PConstructable Impl (EForall (IsPType Impl) f) where
+  pcon t' = Term $ Impl \(lvl :: SNat lvl) -> snatIn lvl $ case t' of
     (EForall (Term (t :: Impl (f (TyVar lvl))))) -> SFForall' SFKindType $ runImpl t (SS lvl)
-  ematch (Term t) f =
+  pmatch (Term t) f =
     let
       applied :: forall a. TypeInfo a => Impl (f a)
       applied = Impl \lvl -> runImpl t lvl `SFInst'` (typeInfo (Proxy @a) lvl)
     in
     f $ EForall $ Term applied
 
-compile' :: forall a m. (Applicative m, IsEType (Impl m) a) => Term (Impl m) a -> m (SFTerm, SFType)
+compile' :: forall a m. (Applicative m, IsPType (Impl m) a) => Term (Impl m) a -> m (SFTerm, SFType)
 compile' (Term t) = (,) <$> runImpl t SN <*> pure (typeInfo (Proxy @m) (Proxy @a) SN)
 
 compile :: Compile EDSL (SFTerm, SFType)
diff --git a/Plutarch/ULC.hs b/Plutarch/ULC.hs
index 464cd94..1a85cbe 100644
--- a/Plutarch/ULC.hs
+++ b/Plutarch/ULC.hs
@@ -1,7 +1,7 @@
 module Plutarch.ULC (ULC (..), compile) where
 
 import Plutarch.Core
-import Plutarch.EType
+import Plutarch.PType
 
 newtype Lvl = Lvl Int
 
@@ -11,17 +11,17 @@ data ULC
   | Var Lvl
   | Error
 
-newtype ULCImpl (a :: EType) = ULCImpl {runImpl :: Lvl -> ULC}
+newtype ULCImpl (a :: PType) = ULCImpl {runImpl :: Lvl -> ULC}
 
-class Top (a :: EType)
+class Top (a :: PType)
 instance Top a
 
-data Arrow (a :: EType) (b :: EType) (f :: ETypeF)
+data Arrow (a :: PType) (b :: PType) (f :: ETypeF)
 
-class (forall a b. EConstructable edsl (EPair a b), EUntyped edsl, ELC edsl, EPartial edsl) => EULC edsl
+class (forall a b. PConstructable edsl (PPair a b), EUntyped edsl, ELC edsl, EPartial edsl) => EULC edsl
 
 instance EDSL ULCImpl where
-  type IsEType ULCImpl = Top
+  type IsPType ULCImpl = Top
 
 instance ELC ULCImpl where
   type EArrow ULCImpl = Arrow
@@ -34,8 +34,8 @@ instance EUntyped ULCImpl where
 instance EPartial ULCImpl where
   eerror = ULCImpl . pure $ Error
 
-instance EConstructable ULCImpl (EPair a b) where
-  pcon (EPair x y) = ULCImpl \lvl -> Lam $ Var lvl `App` runImpl x lvl `App` runImpl y lvl
+instance PConstructable ULCImpl (PPair a b) where
+  pcon (PPair x y) = ULCImpl \lvl -> Lam $ Var lvl `App` runImpl x lvl `App` runImpl y lvl
 
 instance EULC ULCImpl
 
diff --git a/README.md b/README.md
index 2769648..264bb31 100644
--- a/README.md
+++ b/README.md
@@ -21,7 +21,7 @@ AFAICT the techniques employed in Plutarch 2 are novel, but I might be wrong.
 Notably, we don't use TH magic. It's all pure Haskell, with many quantified constraints.
 
 The core design of Plutarch 2 has been settled.
-That is, `Plutarch.Core` and `Plutarch.EType` are unlikely to change.
+That is, `Plutarch.Core` and `Plutarch.PType` are unlikely to change.
 One missing feature is supporting arbitrary data kinds at the type-level,
 however, it is not yet clear if this is possible without type-level generic `to` and `from`.
 
diff --git a/plutarch-core.cabal b/plutarch-core.cabal
index bfcfeb5..a15587c 100644
--- a/plutarch-core.cabal
+++ b/plutarch-core.cabal
@@ -60,11 +60,24 @@ library
     -fprint-equality-relations -fprint-explicit-foralls
 
   exposed-modules:
+    Plutarch.Cont
     Plutarch.Core
+    Plutarch.CPS.Optics.Iso
+    Plutarch.CPS.Optics.Lens
+    Plutarch.CPS.Optics.Optic
+    Plutarch.CPS.Optics.Optional
+    Plutarch.CPS.Optics.Prism
+    Plutarch.CPS.Optics.Traversal
+    Plutarch.CPS.Profunctor
     Plutarch.Experimental
     Plutarch.Internal.WithDictHack
     Plutarch.Internal.Witness
     Plutarch.Lam
+    Plutarch.Optics.Fix
+    Plutarch.Optics.Optic
+    Plutarch.Optics.PEither
+    Plutarch.Optics.PPair
+    Plutarch.PList
     Plutarch.Prelude
     Plutarch.PType
     Plutarch.Reduce
@@ -72,3 +85,5 @@ library
   build-depends:
     , base
     , generics-sop
+    , profunctors
+    , transformers