diff --git a/Cslib.lean b/Cslib.lean
index 982b94f5d..9adb3bce6 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -81,6 +81,7 @@ 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.OmegaSequence.Topology
+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..efbb7aba5
--- /dev/null
+++ b/Cslib/Foundations/Data/PFunctor/Basic.lean
@@ -0,0 +1,149 @@
+/-
+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
+
+Definitions of common `PFunctor` constructions:
+- `monomial A B`: constant direction `B` for any shape `a : A`
+- `P + Q`: shapes are a disjoint sum, directions are define by sum elimination on `a : P.A ⊕ Q.A`
+- `P * Q`: shapes are pairs of underlying shapes, directions are a disjoint sum over both shapes.
+
+Special cases `const`, `linear`, `selfMonomial`, `purePower`, the indeterminate `X`,
+and canonical choices of `0` and `1` are defined as `abbrev` or instances over `monomial`.
+-/
+
+@[expose] public section
+
+universe uA uB uA₁ uA₂ uB₁ uB₂
+
+namespace PFunctor
+
+/-- Two polynomial functors are equal if their head types are equal and their child types
+agree over that equality. -/
+@[ext (iff := false)]
+theorem ext {P Q : PFunctor.{uA, uB}} (h : P.A = Q.A) (h' : ∀ a, P.B a = Q.B (h ▸ a)) :
+    P = Q := by
+  cases P; cases Q; simp only [mk.injEq] at h h' ⊢; subst h
+  simp_all only [heq_eq_eq, true_and]; funext; exact h' _
+
+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) -/
+@[simps] instance instZeroPFunctor : Zero PFunctor where zero := monomial PEmpty PEmpty
+
+instance instIsEmptyZeroPFunctor : IsEmpty (0 : PFunctor.{uA, uB}).A :=
+  inferInstanceAs (IsEmpty PEmpty)
+
+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) -/
+@[simps] instance instOnePFunctor : One PFunctor where one := monomial PUnit PEmpty
+
+instance instUniqueOneA : Unique (1 : PFunctor.{uA, uB}).A := inferInstanceAs (Unique PUnit)
+
+instance instIsEmptyOneB (a : (1 : PFunctor.{uA, uB}).A) : IsEmpty ((1 : PFunctor.{uA, uB}).B a) :=
+  inferInstanceAs (IsEmpty PEmpty)
+
+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
+
+/-- The indeterminate polynomial functor `P(X) = X`, the identity with respect to
+composition and tensor product (up to equivalence). -/
+abbrev X : PFunctor := monomial PUnit PUnit
+
+/- Note: no explicit `IsEmpty`/`Unique` instances are needed for the positions and directions
+of the abbreviations above: being reducible, they unfold to `PEmpty`/`PUnit` during instance
+search. Only `0` and `1` need the explicit instances above, since the `Zero`/`One` instance
+projections are not reducible. -/
+
+@[simp] lemma const_pempty : const PEmpty = 0 := rfl
+
+@[simp] lemma const_punit : const PUnit = 1 := rfl
+
+@[simp] lemma linear_punit : linear PUnit = X := rfl
+
+@[simp] lemma selfMonomial_punit : selfMonomial PUnit = X := rfl
+
+@[simp] lemma purePower_punit : purePower PUnit = X := rfl
+
+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.
+
+This is kept as a `def` alongside the `HAdd` instance below, even though that instance is
+exactly as universe-general as `add` itself: the `binop%` elaborator behind `+` eagerly
+unifies the types of both operands with the expected type, so when the expected type carries
+universe metavariables (e.g. inside `PFunctor.W (P.add (.const α))` with `α : Type v`),
+`P + Q` can fail to elaborate where `P.add Q` succeeds; see `CslibTests/PFunctor.lean`. -/
+@[simps] 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⟩
+
+/-- Addition of polynomial functors, defined as the sum construction. -/
+instance instHAddPFunctor :
+    HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where
+  hAdd := add
+
+/-- Normalize addition of `PFunctor`s to avoid `simp` mismatches between the notations. -/
+@[simp] lemma add_def (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
+    P + Q = P.add Q := rfl
+
+end add
+
+section prod
+
+/-- The product of two polynomial functors `P` and `Q`, written as `P * Q`,
+defined as the product of the head types and the sum of the child types.
+Unlike `add`, the child types of `P` and `Q` may live in different universes,
+since they are combined with `⊕` rather than `Sum.elim`. -/
+@[simps] def prod (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
+    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} := ⟨P.A × Q.A, fun ab => P.B ab.1 ⊕ Q.B ab.2⟩
+
+/-- Multiplication of polynomial functors, defined as the product construction.
+As with addition, we deliberately do not add a homogeneous `Mul` instance. -/
+instance instHMulPFunctor :
+    HMul PFunctor.{uA₁, uB₁} PFunctor.{uA₂, uB₂} PFunctor.{max uA₁ uA₂, max uB₁ uB₂} where
+  hMul := prod
+
+/-- Normalize multiplication of `PFunctor`s to avoid `simp` mismatches between the notations. -/
+@[simp] lemma mul_def (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
+    P * Q = P.prod Q := rfl
+
+end prod
+
+end PFunctor
diff --git a/CslibTests.lean b/CslibTests.lean
index b62965a9c..c79bc5a61 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -16,5 +16,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..f77508a9f
--- /dev/null
+++ b/CslibTests/PFunctor.lean
@@ -0,0 +1,88 @@
+/-
+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.Basic
+
+/-!
+# Polynomial Functor Tests
+
+These tests exercise the universe-polymorphic polynomial sum and product, the simp API for
+the basic constructions, and the extensionality lemma.
+-/
+
+universe uA uB uA₁ uA₂ uB₁ uB₂ v
+
+namespace CslibTests
+
+open PFunctor
+
+/-- Addition notation is 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
+
+/-- Multiplication notation is likewise available, including for child types in
+different universes. -/
+example (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
+    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} := P * Q
+
+/-- The `def` spelling `P.add (.const α)` elaborates under `PFunctor.W` even when the
+expected type only determines the universe levels up to a `max`. This is the motivating
+use case for keeping `PFunctor.add` as a `def` alongside the `HAdd` instance. -/
+example (P : PFunctor.{uA₁, uB}) (α : Type v) : Type (max uA₁ uB v) :=
+  PFunctor.W (P.add (.const α))
+
+/- The `+` spelling of the same type fails: the `binop%` elaborator behind `+` commits the
+universe metavariables in the expected type to the first operand's universes before it
+considers the heterogeneous `HAdd` instance. -/
+/--
+error: Type mismatch
+  P + const α
+has type
+  PFunctor.{max uA₁ v, uB}
+of sort
+  Type (max (max (uA₁ + 1) (uB + 1)) (v + 1))
+but is expected to have type
+  PFunctor.{uA₁, uB}
+of sort `Type (max (uA₁ + 1) (uB + 1))`
+---
+error: failed to solve universe constraint
+  max (max uA₁ uB) v =?= max uB uA₁
+while trying to unify
+  Type (max uA₁ uB v) : Type ((max uA₁ uB v) + 1)
+with
+  Type (max uA₁ uB) : Type ((max uA₁ uB) + 1)
+-/
+#guard_msgs in
+example (P : PFunctor.{uA₁, uB}) (α : Type v) : Type (max uA₁ uB v) :=
+  PFunctor.W (P + PFunctor.const α)
+
+/-- The simp set rewrites the head type of a sum through the `+` notation. -/
+example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
+    (P + Q).A = (P.A ⊕ Q.A) := by simp
+
+/-- The simp set computes child types of a sum on both shapes. -/
+example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) :
+    (P.add Q).B (.inl a) = P.B a := by simp
+
+example (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A) :
+    (P.add Q).B (.inr a) = Q.B a := by simp
+
+/-- The simp set computes head and child types of a product. -/
+example (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (a : P.A) (b : Q.A) :
+    (P * Q).B (a, b) = (P.B a ⊕ Q.B b) := by simp
+
+/-- The named monomials reduce to the canonical `0`, `1`, and `X`. -/
+example : (const PUnit : PFunctor.{uA, uB}) = 1 := by simp
+example : (linear PUnit : PFunctor.{uA, uB}) = X := by simp
+
+/-- The `ext` tactic picks up the registered extensionality lemma. -/
+example (P Q : PFunctor.{uA, uB}) (h : P.A = Q.A) (h' : ∀ a, P.B a = Q.B (h ▸ a)) :
+    P = Q := by
+  ext
+  · exact h
+  · exact h' _
+
+end CslibTests