diff --git a/Cslib.lean b/Cslib.lean
index a4da6b124..6bdedc89b 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -77,6 +77,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.PFunctor.Basic
 public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Set.Saturation
diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean
new file mode 100644
index 000000000..9843b07c6
--- /dev/null
+++ b/Cslib/Foundations/Data/PFunctor/Basic.lean
@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Quang Dao
+-/
+module
+
+public import Cslib.Init
+public import Mathlib.Data.PFunctor.Univariate.Basic
+
+/-!
+# Polynomial Functors
+
+This file defines additional constructions on `PFunctor` that don't belong in core mathlib.
+The main definitions is `monomial A B` for the `PFunctor` with constant family `B` over `A`,
+as well as special cases of this such as a canonical choice of `0` and `1`.
+
+We also define the sum `P + Q` whose shapes are a sum of the shapes of `P` and `Q`,
+with a type family defined by sum elimination into the individual child types of `P` and `Q`.
+-/
+
+@[expose] public section
+
+universe uA uB uA₁ uA₂
+
+namespace PFunctor
+
+section monomial
+
+/-- The monomial `PFunctor` with head type `A` and constant `B` for any `a : A`. -/
+abbrev monomial (A : Type uA) (B : Type uB) : PFunctor := ⟨A, fun _ => B⟩
+
+lemma monomial_A (A : Type uA) (B : Type uB) : (monomial A B).A = A := rfl
+
+lemma monomial_B (A : Type uA) (B : Type uB) (a : (monomial A B).A) :
+    (monomial A B).B a = B := rfl
+
+end monomial
+
+section zero
+
+/-- The zero polynomial functor, defined as `A = PEmpty` and `B _ = PEmpty`, is the identity with
+  respect to sum (up to equivalence) -/
+instance instZeroPFunctor : Zero PFunctor where zero := monomial PEmpty PEmpty
+
+@[simp] lemma zero_A : (0 : PFunctor).A = PEmpty := rfl
+
+@[simp] lemma zero_B (a : (0 : PFunctor).A) : (0 : PFunctor).B a = PEmpty := rfl
+
+end zero
+
+section one
+
+/-- The unit polynomial functor, defined as `A = PUnit` and `B _ = PEmpty`, is the identity with
+  respect to product (up to equivalence) -/
+instance instOnePFunctor : One PFunctor where one := monomial PUnit PEmpty
+
+@[simp] lemma one_A : (1 : PFunctor).A = PUnit := rfl
+
+@[simp] lemma one_B (a : (1 : PFunctor).A) : (1 : PFunctor).B a = PEmpty := rfl
+
+end one
+
+/-- The constant polynomial functor `P(X) = A X^ PEmpty = A` -/
+abbrev const (A : Type uA) : PFunctor := monomial A PEmpty
+
+/-- The linear polynomial functor `P(X) = A X` -/
+abbrev linear (A : Type uA) : PFunctor := monomial A PUnit
+
+/-- The self monomial polynomial functor `P(X) = S X^ S` -/
+abbrev selfMonomial (S : Type uA) : PFunctor.{uA, uA} := monomial S S
+
+/-- The pure power polynomial functor `P(X) = X^ B` -/
+abbrev purePower (B : Type uB) : PFunctor := monomial PUnit B
+
+section add
+
+/-- The sum of two polynomial functors `P` and `Q`, written as `P + Q`,
+defined as the sum of the head types and the sum case analysis for the child types. -/
+def add (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
+    PFunctor.{max uA₁ uA₂, uB} := ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩
+
+instance instHAddPFunctor :
+  HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where
+  hAdd := add
+
+@[simp] lemma add_A (P Q : PFunctor) : (add P Q).A = (P.A ⊕ Q.A) := rfl
+
+@[simp] lemma add_B_inl (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) :
+    (add P Q).B (.inl a) = P.B a := rfl
+
+@[simp] lemma add_B_inr (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A) :
+    (add P Q).B (.inr a) = Q.B a := rfl
+
+end add
+
+end PFunctor
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index a29e97470..d0f7c9c6d 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -6,7 +6,7 @@ Authors: Quang Dao
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Data.PFunctor.Basic
 public import Mathlib.Data.PFunctor.Univariate.Basic
 
 /-!
@@ -14,8 +14,9 @@ public import Mathlib.Data.PFunctor.Univariate.Basic
 
 We define the free monad on a **polynomial functor** (`PFunctor`), and prove some basic properties.
 
-The free monad `PFunctor.FreeM P` extends the W-type construction with an extra `pure`
-constructor, yielding a monad that is free over the polynomial functor `P`.
+The free monad `PFunctor.FreeM P` extends the W-type construction with
+an extra `pure` constructor (represented by adding a `PFunctor.const` term over the return type),
+yielding a monad that is free over the polynomial functor `P`.
 
 ## Comparison with `Cslib.FreeM`
 
@@ -61,6 +62,22 @@ This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io)
 - `PFunctor.FreeM.lift`: Lift a shape of the base polynomial functor into the free monad.
 - `PFunctor.FreeM.liftObj`: Lift an object of the base polynomial functor into the free monad.
 - `PFunctor.FreeM.liftM`: Interpret `FreeM P` into any other monad.
+
+## Implementation Notes
+
+`FreeM P α` is a one-field structure wrapping the W-type of the polynomial functor
+`P.add (const α)`, whose `const α`-shaped nodes are leaves carrying pure values.
+The wrapper (rather than a `def` or `abbrev` type synonym) keeps `FreeM` a distinct type:
+no instances or definitional equalities leak between `FreeM` and the W-type, and the
+interface does not depend on the definition body being exposed across module boundaries.
+The conversions `FreeM.ofW` and `FreeM.toW` are definitional inverses (by eta for
+structures), so transport between the two representations is free; see `FreeM.equivW`.
+
+The raw W-type representation is confined to the constructors `FreeM.pure` and
+`FreeM.liftBind`, the recursor `FreeM.elim`, and a few (dis)equality lemmas; every other
+definition and proof factors through this interface. (The name `FreeM.rec` is taken by the
+structure's own recursor.) Definitions made with `FreeM.elim` compute definitionally on
+both node shapes (`FreeM.elim_pure`, `FreeM.elim_lift_bind`).
 -/
 
 @[expose] public section
@@ -69,42 +86,112 @@ universe u v uA uB
 
 namespace PFunctor
 
--- Disable generation of unneeded lemmas which the simpNF linter would complain about.
-set_option genInjectivity false in
-set_option genSizeOfSpec false in
-/-- The free monad on a polynomial functor.
-This extends `WType` with an extra `pure` constructor. -/
-inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
-  /-- A leaf node wrapping a pure value. -/
-  | protected pure {α} (a : α) : P.FreeM α
-  /-- Invoke the operation `a : P.A` with continuation `cont : P.B a → P.FreeM α`. -/
-  | liftBind {α} (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α
-deriving Inhabited
+/-- The free monad on a polynomial functor: a one-field structure wrapping the W-type of the
+polynomial functor obtained by adjoining a constant shape for each pure value to `P`. -/
+structure FreeM (P : PFunctor.{uA, uB}) (α : Type v) : Type (max uA uB v) where
+  /-- Wrap a W-type tree as a `FreeM` computation. -/
+  ofW ::
+  /-- The underlying W-type tree of the computation. -/
+  toW : PFunctor.W (P.add (.const α))
 
 namespace FreeM
 
 variable {P : PFunctor.{uA, uB}} {α β γ : Type*}
 
+@[simp] lemma ofW_toW (x : P.FreeM α) : ofW x.toW = x := rfl
+
+@[simp] lemma toW_ofW (w : PFunctor.W (P.add (.const α))) : (ofW w).toW = w := rfl
+
+lemma toW_injective : Function.Injective (toW : P.FreeM α → _) :=
+  fun _ _ h => congrArg ofW h
+
+lemma ofW_injective : Function.Injective (ofW : _ → P.FreeM α) :=
+  fun _ _ h => congrArg toW h
+
+@[simp] lemma toW_inj {x y : P.FreeM α} : x.toW = y.toW ↔ x = y := toW_injective.eq_iff
+
+@[ext] lemma ext {x y : P.FreeM α} (h : x.toW = y.toW) : x = y := toW_injective h
+
+/-- The equivalence between the free monad and its underlying W-type, given by `FreeM.toW`
+and `FreeM.ofW`. Both round-trips hold definitionally. -/
+def equivW : P.FreeM α ≃ PFunctor.W (P.add (.const α)) where
+  toFun := toW
+  invFun := ofW
+  left_inv _ := rfl
+  right_inv _ := rfl
+
+@[simp] lemma equivW_apply (x : P.FreeM α) : equivW x = x.toW := rfl
+
+@[simp] lemma equivW_symm_apply (w : PFunctor.W (P.add (.const α))) :
+    equivW.symm w = ofW w := rfl
+
+open Lean.PrettyPrinter Delaborator in
+/-- This prevents `ofW w` being printed as `{ toW := w }` by `delabStructureInstance`. -/
+@[app_delab ofW] meta def delabOfW : Delab := delabApp
+
+/-- A leaf node wrapping a pure value. -/
+protected def pure (a : α) : P.FreeM α := ⟨⟨.inr a, PEmpty.elim⟩⟩
+
+/-- Invoke the operation `a : P.A` with continuation `cont : P.B a → P.FreeM α`. -/
+def liftBind (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α :=
+  ⟨⟨.inl a, fun b => (cont b).toW⟩⟩
+
+/-- Lift a shape of the base polynomial functor into the free monad. -/
+def lift (a : P.A) : P.FreeM (P.B a) := liftBind a FreeM.pure
+
+instance [Inhabited α] : Inhabited (P.FreeM α) := ⟨.pure default⟩
+
 instance : Pure (P.FreeM) where pure := .pure
 
+@[simp] lemma toW_pure (a : α) :
+    (pure a : P.FreeM α).toW = ⟨.inr a, PEmpty.elim⟩ := rfl
+
+/-- All continuations stored at a pure W-node are equal because their domain is empty. -/
+lemma pure_eq_mk_inl (a : α) (cont : PEmpty → PFunctor.W (P.add (.const α))) :
+    FreeM.pure a = (⟨⟨.inr a, cont⟩⟩ : P.FreeM α) :=
+  congrArg (fun f => ofW (WType.mk (Sum.inr a) f)) (funext PEmpty.rec)
+
+@[simp] lemma ofW_mk_inl (a : P.A) (cont : P.B a → PFunctor.W (P.add (.const α))) :
+    (ofW ⟨.inl a, cont⟩ : P.FreeM α) = liftBind a fun b => ofW (cont b) := rfl
+
+@[simp] lemma ofW_mk_inr (a : α) (cont : PEmpty → PFunctor.W (P.add (.const α))) :
+    (ofW ⟨.inr a, cont⟩ : P.FreeM α) = FreeM.pure a :=
+  (pure_eq_mk_inl a cont).symm
+
+/-- Auxiliary recursor consuming the underlying W-type; use `FreeM.elim` instead. -/
+protected def recAux {motive : P.FreeM α → Sort u} (pure : ∀ a, motive (pure a))
+    (liftBind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)),
+      motive (FreeM.liftBind a cont)) :
+    ∀ w : PFunctor.W (P.add (.const α)), motive (ofW w)
+  | ⟨.inr a, cont⟩ => pure_eq_mk_inl a cont ▸ pure a
+  | ⟨.inl a, cont⟩ =>
+    liftBind a (fun b => ofW (cont b)) fun b => FreeM.recAux pure liftBind (cont b)
+
+/-- Recursor for `FreeM`, stated in terms of its pure and effect-node interface (the name
+`FreeM.rec` is taken by the structure's own recursor; compare `WType.elim`).
+Together with `FreeM.recAux` this is the only place the W-type representation is consumed;
+all other definitions factor through it. Definitions made with it compute definitionally on
+both node shapes, see `FreeM.elim_pure` and `FreeM.elim_lift_bind`. -/
+def elim {motive : P.FreeM α → Sort u} (pure : ∀ a, motive (pure a))
+    (liftBind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)),
+      motive (FreeM.liftBind a cont)) (x : P.FreeM α) : motive x :=
+  FreeM.recAux pure liftBind x.toW
+
 @[simp]
 theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl
 
-/-- Lift a shape of the base polynomial functor into the free monad. -/
-def lift (a : P.A) : P.FreeM (P.B a) := FreeM.liftBind a pure
-
 @[simp] lemma lift_ne_pure (a : P.A) (y : P.B a) :
-    (lift a : P.FreeM (P.B a)) ≠ pure y := by simp [lift]
+    (lift a : P.FreeM (P.B a)) ≠ pure y := fun h => by
+  cases congrArg (PFunctor.W.head ∘ toW) h
 
 @[simp] lemma pure_ne_lift (a : P.A) (y : P.B a) :
-    pure y ≠ (lift a : P.FreeM (P.B a)) := by simp [lift]
+    pure y ≠ (lift a : P.FreeM (P.B a)) := (lift_ne_pure a y).symm
 
-/-- Bind operation for the `FreeM` monad.
+/-- Bind operation for the `FreeM` monad, defined via `FreeM.elim`.
 
 The builtin `>>=` notation should be preferred when `α` and `β` are in the same universe. -/
-protected def bind : P.FreeM α → (α → P.FreeM β) → P.FreeM β
-  | FreeM.pure a, f => f a
-  | FreeM.liftBind a cont, f => FreeM.liftBind a (fun u ↦ FreeM.bind (cont u) f)
+protected def bind (x : P.FreeM α) (f : α → P.FreeM β) : P.FreeM β :=
+  FreeM.elim (motive := fun _ => P.FreeM β) f (fun a _ cont => .liftBind a cont) x
 
 instance : Bind (P.FreeM) where bind := .bind
 
@@ -113,12 +200,10 @@ instance : Bind (P.FreeM) where bind := .bind
 theorem bind_eq_bind {α β : Type v} :
     (FreeM.bind : P.FreeM α → _ → P.FreeM β) = Bind.bind := rfl
 
-/-- Map a function over a `FreeM` computation.
+/-- Map a function over a `FreeM` computation, defined in terms of `FreeM.bind`.
 
 The builtin `<$>` notation should be preferred when `α` and `β` are in the same universe. -/
-def map (f : α → β) : P.FreeM α → P.FreeM β
-  | .pure a => .pure (f a)
-  | .liftBind a cont => .liftBind a fun u => FreeM.map f (cont u)
+def map (f : α → β) (x : P.FreeM α) : P.FreeM β := x.bind (FreeM.pure ∘ f)
 
 instance : Functor (P.FreeM) where
   map := .map
@@ -132,6 +217,25 @@ theorem map_eq_map {α β : Type v} :
 lemma liftBind_eq (a : P.A) (cont : P.B a → P.FreeM α) :
     FreeM.liftBind a cont = (FreeM.lift a).bind cont := rfl
 
+/-- `FreeM.toW` on an effect node, stated for the simp-normal form of `FreeM.liftBind`. -/
+@[simp] lemma toW_liftBind (a : P.A) (cont : P.B a → P.FreeM α) :
+    ((FreeM.lift a).bind cont).toW = ⟨.inl a, fun b => (cont b).toW⟩ := rfl
+
+@[simp]
+lemma elim_pure {motive : P.FreeM α → Sort u} (hp : ∀ a, motive (pure a))
+    (hlb : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)),
+      motive (FreeM.liftBind a cont)) (a : α) :
+    FreeM.elim hp hlb (pure a) = hp a := rfl
+
+/-- `FreeM.elim` computes definitionally on effect nodes.
+Stated for the simp-normal form `(FreeM.lift a).bind cont` of `FreeM.liftBind a cont`. -/
+@[simp]
+lemma elim_lift_bind {motive : P.FreeM α → Sort u} (hp : ∀ a, motive (pure a))
+    (hlb : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (_ih : ∀ i, motive (cont i)),
+      motive (FreeM.liftBind a cont)) (a : P.A) (cont : P.B a → P.FreeM α) :
+    FreeM.elim hp hlb ((FreeM.lift a).bind cont) =
+      hlb a cont fun i => FreeM.elim hp hlb (cont i) := rfl
+
 /-- Lift an object of the base polynomial functor into the free monad.
 
 This lifts the shape `x.1` with `lift` and relabels the responses with `x.2`. We use the
@@ -142,14 +246,17 @@ abbrev liftObj (x : P.Obj α) : P.FreeM α := (lift x.1).map x.2
 instance : MonadLift P (P.FreeM) where
   monadLift x := FreeM.liftObj x
 
-@[simp] lemma liftObj_ne_pure (x : P.Obj α) (y : α) :
-    (liftObj x : P.FreeM α) ≠ pure y := by simp [liftObj, lift, map, -liftBind_eq]
-
-@[simp] lemma pure_ne_liftObj (x : P.Obj α) (y : α) :
-    pure y ≠ (liftObj x : P.FreeM α) := by simp [liftObj, lift, map, -liftBind_eq]
-
 lemma monadLift_eq_liftObj (x : P.Obj α) : (x : P.FreeM α) = FreeM.liftObj x := rfl
 
+/-- Case analysis for `FreeM`, stated in terms of its pure and effect-node interface and in
+the same simp-normal form as `FreeM.induction`. -/
+@[cases_eliminator]
+protected def cases {motive : P.FreeM α → Sort u}
+    (pure : ∀ a, motive (pure a))
+    (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α), motive ((FreeM.lift a).bind cont)) :
+    ∀ x, motive x :=
+  FreeM.elim pure fun a cont _ => lift_bind a cont
+
 set_option linter.unusedVariables false in
 /-- An override for the default induction principle that is in simp-normal form.
 
@@ -158,37 +265,40 @@ Note that when `α` and `P.B a` are in the same universe, this simplifies slight
 protected theorem induction {motive : P.FreeM α → Prop}
     (pure : ∀ a, motive (pure a))
     (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (ih : ∀ i, motive (cont i)),
-      motive ((FreeM.lift a).bind cont)) : ∀ x, motive x
-  | .pure a => pure a
-  | liftBind a cont => lift_bind a cont fun u => FreeM.induction pure lift_bind (cont u)
+      motive ((FreeM.lift a).bind cont)) : ∀ x, motive x :=
+  FreeM.elim pure lift_bind
+
+/-- `.pure a` followed by `bind` collapses immediately. -/
+@[simp]
+lemma pure_bind (a : α) (f : α → P.FreeM β) :
+    (pure a : P.FreeM α).bind f = f a := rfl
+
+@[simp]
+lemma liftBind_bind (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) :
+    ((FreeM.lift a).bind cont).bind f = (FreeM.lift a).bind (fun u ↦ (cont u).bind f) := rfl
 
 protected theorem bind_assoc (x : P.FreeM α) (f : α → P.FreeM β) (g : β → P.FreeM γ) :
     (x.bind f).bind g = x.bind (fun a => (f a).bind g) := by
   induction x with
   | pure a => rfl
-  | lift_bind a cont ih => simp [← liftBind_eq, FreeM.bind, ih] at *
+  | lift_bind a cont ih => simp [ih]
 
-/-- `.pure a` followed by `bind` collapses immediately. -/
 @[simp]
-lemma pure_bind (a : α) (f : α → P.FreeM β) :
-    (pure a : P.FreeM α).bind f = f a := rfl
+lemma bind_pure (x : P.FreeM α) : x.bind pure = x := by
+  induction x with
+  | pure a => rfl
+  | lift_bind a cont ih => simp [ih]
 
 @[simp]
-lemma bind_pure : ∀ x : P.FreeM α, x.bind pure = x
-  | .pure a => rfl
-  | .liftBind a cont => by
-    simp only [FreeM.bind]; congr 1; funext u; exact bind_pure (cont u)
+lemma bind_pure_comp (f : α → β) (x : P.FreeM α) : x.bind (pure ∘ f) = map f x := rfl
 
 @[simp]
-lemma bind_pure_comp (f : α → β) : ∀ x : P.FreeM α, x.bind (pure ∘ f) = map f x
-  | .pure a => rfl
-  | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp]
+lemma map_pure (f : α → β) (a : α) :
+    (pure a : P.FreeM α).map f = pure (f a) := rfl
 
 @[simp]
-lemma liftBind_bind (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) :
-    ((FreeM.lift a).bind cont).bind f = (FreeM.lift a).bind (fun u ↦ (cont u).bind f) := by
-  simp only [lift]
-  exact FreeM.bind_assoc (FreeM.liftBind a pure) cont f
+lemma map_lift_bind (f : α → β) (a : P.A) (cont : P.B a → P.FreeM α) :
+    ((FreeM.lift a).bind cont).map f = (FreeM.lift a).bind (fun u ↦ (cont u).map f) := rfl
 
 @[simp]
 lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) :
@@ -198,43 +308,44 @@ lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) :
     x.bind f = pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
   cases x with
   | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩
-  | liftBind a cont =>
+  | lift_bind a cont =>
     constructor
     · intro h
-      cases h
+      cases congrArg (PFunctor.W.head ∘ toW) h
     · rintro ⟨_, h, _⟩
-      cases h
+      cases congrArg (PFunctor.W.head ∘ toW) h
 
 @[simp] lemma pure_eq_bind_iff (x : P.FreeM α) (f : α → P.FreeM β) (b : β) :
     pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by
   cases x with
   | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩
-  | liftBind a cont =>
+  | lift_bind a cont =>
     constructor
     · intro h
-      cases h
+      cases congrArg (PFunctor.W.head ∘ toW) h
     · rintro ⟨_, h, _⟩
-      cases h
+      cases congrArg (PFunctor.W.head ∘ toW) h
+
+lemma lift_bind_ne_pure (a : P.A) (cont : P.B a → P.FreeM α) (y : α) :
+    (FreeM.lift a).bind cont ≠ pure y := by simp
+
+lemma pure_ne_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) (y : α) :
+    pure y ≠ (FreeM.lift a).bind cont := by simp
+
+@[simp] lemma liftObj_ne_pure (x : P.Obj α) (y : α) :
+    (liftObj x : P.FreeM α) ≠ pure y := lift_bind_ne_pure _ _ _
+
+@[simp] lemma pure_ne_liftObj (x : P.Obj α) (y : α) :
+    pure y ≠ (liftObj x : P.FreeM α) := pure_ne_lift_bind _ _ _
 
 instance : Monad (P.FreeM) where
 
 @[simp]
-theorem id_map : ∀ x : P.FreeM α, map id x = x
-  | .pure a => rfl
-  | .liftBind a cont => by
-    simp only [map]
-    congr 1
-    funext u
-    exact id_map (cont u)
+theorem id_map (x : P.FreeM α) : map id x = x := bind_pure x
 
-theorem comp_map (h : β → γ) (g : α → β) :
-    ∀ x : P.FreeM α, map (h ∘ g) x = map h (map g x)
-  | .pure a => rfl
-  | .liftBind a cont => by
-    simp only [map]
-    congr 1
-    funext u
-    exact comp_map h g (cont u)
+theorem comp_map (h : β → γ) (g : α → β) (x : P.FreeM α) :
+    map (h ∘ g) x = map h (map g x) :=
+  (FreeM.bind_assoc x (FreeM.pure ∘ g) (FreeM.pure ∘ h)).symm
 
 instance : LawfulMonad (P.FreeM) := LawfulMonad.mk'
   (bind_pure_comp := bind_pure_comp)
@@ -246,8 +357,7 @@ instance : LawfulMonad (P.FreeM) := LawfulMonad.mk'
 lemma pure_inj (a b : α) : (pure a : P.FreeM α) = pure b ↔ a = b := by
   constructor
   · intro h
-    cases h
-    rfl
+    exact Sum.inr.inj (congrArg (PFunctor.W.head ∘ toW) h)
   · rintro rfl; rfl
 
 lemma liftBind_inj (a a' : P.A)
@@ -255,8 +365,11 @@ lemma liftBind_inj (a a' : P.A)
     FreeM.liftBind a cont = FreeM.liftBind a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by
   constructor
   · intro h
-    cases h
-    exact ⟨rfl, rfl⟩
+    have hW := congrArg toW h
+    injection hW with ha hcont
+    injection ha with ha
+    subst ha
+    exact ⟨rfl, funext fun b => toW_injective (congrFun (eq_of_heq hcont) b)⟩
   · rintro ⟨rfl, rfl⟩
     rfl
 
@@ -266,9 +379,8 @@ variable {m : Type uB → Type v} {α : Type uB}
 
 /-- Interpret a `FreeM P` computation into any monad `m` by providing an interpretation
 `interp : (a : P.A) → m (P.B a)` for each operation. -/
-protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α
-  | .pure a => pure a
-  | .liftBind a cont => interp a >>= fun u ↦ (cont u).liftM interp
+protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α :=
+  FreeM.elim (motive := fun _ => m α) (fun a => pure a) (fun a _ ih => interp a >>= ih)
 
 variable [Monad m] (interp : (a : P.A) → m (P.B a))
 
@@ -278,9 +390,7 @@ lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure
 @[simp]
 lemma liftM_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) :
     FreeM.liftM interp (FreeM.lift a >>= cont) =
-      (do let u ← interp a; (cont u).liftM interp) := by
-  dsimp only [FreeM.liftM, FreeM.bind, FreeM.lift]
-  rfl
+      (do let u ← interp a; (cont u).liftM interp) := rfl
 
 /--
 A predicate stating that `eval : P.FreeM α → m α` is an interpreter for the polynomial
diff --git a/CslibTests.lean b/CslibTests.lean
index 99f1d31f5..51bcb8b7e 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -15,5 +15,6 @@ import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Modal
+import CslibTests.PFunctor
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/PFunctor.lean b/CslibTests/PFunctor.lean
new file mode 100644
index 000000000..f7610576e
--- /dev/null
+++ b/CslibTests/PFunctor.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+
+import Cslib.Foundations.Data.PFunctor.Free
+
+/-!
+# Polynomial Functor Universe Tests
+
+These tests exercise the universe-polymorphic polynomial sum and the W-type representation of
+`PFunctor.FreeM`.
+-/
+
+universe uA₁ uA₂ uB v
+
+namespace CslibTests
+
+open PFunctor
+
+variable {P : PFunctor.{uA₁, uB}} {α : Type v} {β : Type uA₂}
+
+/-- Addition notation remains available when its result universe is fixed by the expected type. -/
+example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
+    PFunctor.{max uA₁ uA₂, uB} := P + Q
+
+private def isPure {P : PFunctor.{uA₁, uB}} {α : Type v} : P.FreeM α → Bool :=
+  FreeM.elim (motive := fun _ => Bool) (fun _ => true) (fun _ _ _ => false)
+
+/-- The `cases` tactic picks up the registered case eliminator. -/
+example (x : P.FreeM α) : isPure x = true ∨ isPure x = false := by
+  cases x with
+  | pure a => left; rfl
+  | lift_bind a cont => right; rfl
+
+/-- The `induction` tactic picks up the registered induction eliminator. -/
+example (x : P.FreeM α) : x.bind FreeM.pure = x := by
+  induction x with
+  | pure a => rfl
+  | lift_bind a cont ih => simp only [FreeM.liftBind_bind, ih]
+
+/-- The `toW`/`ofW` round-trips hold definitionally (eta for structures). -/
+example (x : P.FreeM α) : FreeM.ofW x.toW = x := rfl
+example (w : PFunctor.W (P.add (.const α))) : (FreeM.ofW w).toW = w := rfl
+
+/-- Distinct node shapes are provably distinct, via the simp set. -/
+example (a : α) (b : P.A) (cont : P.B b → P.FreeM α) :
+    FreeM.liftBind b cont ≠ FreeM.pure a := by simp
+
+private def coin : PFunctor.{0, 0} := ⟨Bool, fun b => if b then Bool else Nat⟩
+
+/-- A ground free computation remains small enough to serve as another polynomial's directions. -/
+private def scheduler : PFunctor.{0, 0} := ⟨Unit, fun _ => coin.FreeM Bool⟩
+
+example : scheduler.B () = coin.FreeM Bool := rfl
+
+end CslibTests