From 90278e57cfb8bf336ea6635605a03b7c3b606436 Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Mon, 5 Oct 2026 18:32:51 -0500
Subject: [PATCH 1/5] feat(PFunctor): relate W-types, M-types and free monads
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add the canonical map `PFunctor.W.toM` and identify `P.W` with the
well-founded trees of `P.M`, together with Lambek's lemma `M.destEquiv` and
an induction principle for `PFunctor.W` through `W.mk`. Identify
`P.FreeM α` with the W-type of `C α + P`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Cslib.lean                                  |   1 +
 Cslib/Foundations/Data/PFunctor/Basic.lean  |  17 ++-
 Cslib/Foundations/Data/PFunctor/Free.lean   |   3 +-
 Cslib/Foundations/Data/PFunctor/Free/W.lean |  57 +++++++++-
 Cslib/Foundations/Data/PFunctor/M.lean      | 109 ++++++++++++++++++++
 5 files changed, 182 insertions(+), 5 deletions(-)
 create mode 100644 Cslib/Foundations/Data/PFunctor/M.lean

diff --git a/Cslib.lean b/Cslib.lean
index 5cfc781da..af6a5420a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -139,6 +139,7 @@ public import Cslib.Foundations.Data.PFunctor.Basic
 public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.PFunctor.Free.Fold
 public import Cslib.Foundations.Data.PFunctor.Free.W
+public import Cslib.Foundations.Data.PFunctor.M
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean
index b6418d909..ab050ffd7 100644
--- a/Cslib/Foundations/Data/PFunctor/Basic.lean
+++ b/Cslib/Foundations/Data/PFunctor/Basic.lean
@@ -21,7 +21,8 @@ Special cases `C`, `linear`, `selfMonomial`, `purePower`, the indeterminate `y`,
 and canonical choices of `0` and `1` are defined as abbreviations or instances over `monomial`.
 The scoped notations `A y^ B` and `y^ B` denote `monomial A B` and `purePower B`, respectively.
 
-The child-map API includes `const`, `Unary`, and `DecidableEqChildren`.
+The child-map API includes `const`, `Unary`, and `DecidableEqChildren`. `W.induction` is an
+induction principle for `P.W` through `W.mk`.
 -/
 
 @[expose] public section
@@ -155,6 +156,20 @@ defined as the product of the head types and the sum of the child types. -/
 
 end prod
 
+section W
+
+variable {P : PFunctor.{uA, uB}}
+
+/-- Induction on `P.W` through `W.mk`, keeping subtrees typed as `P.W` rather than `WType P.B`. -/
+@[elab_as_elim, induction_eliminator]
+protected theorem W.induction {motive : P.W → Prop}
+    (mk : ∀ (a : P.A) (f : P.B a → P.W), (∀ i, motive (f i)) → motive (W.mk ⟨a, f⟩))
+    (w : P.W) : motive w := by
+  induction w using WType.rec with
+  | mk a f ih => exact mk a f ih
+
+end W
+
 section Unary
 
 /-- A polynomial functor is unary if all child types have exactly one element. -/
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index a26e39a02..b95829777 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -16,7 +16,8 @@ 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`.
+constructor, yielding a monad that is free over the polynomial functor `P`. `FreeM.equivW`
+identifies `P.FreeM α` with the W-type of `C α + P`.
 
 ## Comparison with `Cslib.FreeM`
 
diff --git a/Cslib/Foundations/Data/PFunctor/Free/W.lean b/Cslib/Foundations/Data/PFunctor/Free/W.lean
index 401df3601..408355afd 100644
--- a/Cslib/Foundations/Data/PFunctor/Free/W.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free/W.lean
@@ -6,13 +6,18 @@ Authors: Quang Dao, Devon Tuma
 
 module
 
+public import Cslib.Foundations.Data.PFunctor.Basic
 public import Cslib.Foundations.Data.PFunctor.Free
 
 /-!
-# Polynomial free monads with an empty result type
+# Polynomial free monads as W-types
 
-When `α` is empty, a tree in `P.FreeM α` has only operation nodes. The equivalence
-`PFunctor.FreeM.equivWOfIsEmpty` identifies these trees with the W-type `P.W`.
+A tree in `P.FreeM α` is a W-tree whose nodes either return a value of `α` or perform an operation
+of `P`: `PFunctor.FreeM.equivW` identifies `P.FreeM α` with the W-type of `C α + P`, the
+polynomial of the functor `X ↦ α ⊕ P X` whose initial algebra is the free monad.
+
+When `α` is empty, a tree has only operation nodes, and `PFunctor.FreeM.equivWOfIsEmpty` identifies
+these trees with the W-type `P.W` itself.
 -/
 
 @[expose] public section
@@ -69,4 +74,50 @@ def FreeM.equivWOfIsEmpty [IsEmpty α] : P.FreeM α ≃ P.W where
   left_inv := W.toFreeM_toWOfIsEmpty
   right_inv := toWOfIsEmpty_toFreeM
 
+/-- Regard a free program as a W-tree of `C α + P`, whose leaves carry the returned values. -/
+def FreeM.toW : P.FreeM α → (C.{u, uB} α + P).W
+  | .pure a => W.mk ⟨.inl a, PEmpty.elim⟩
+  | .liftBind a cont => W.mk ⟨.inr a, fun b => FreeM.toW (cont b)⟩
+
+/-- Read a W-tree of `C α + P` as a free program. -/
+def FreeM.ofW : (C.{u, uB} α + P).W → P.FreeM α
+  | ⟨.inl a, _⟩ => .pure a
+  | ⟨.inr a, cont⟩ => .liftBind a fun b => FreeM.ofW (cont b)
+
+@[simp]
+theorem FreeM.toW_pure (a : α) :
+    toW (pure a : P.FreeM α) = (W.mk ⟨.inl a, PEmpty.elim⟩ : (C.{u, uB} α + P).W) := rfl
+
+@[simp]
+theorem FreeM.toW_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) :
+    toW ((lift a).bind (α := no_index (P.B a)) cont) =
+      (W.mk ⟨.inr a, fun b => toW (cont b)⟩ : (C.{u, uB} α + P).W) := rfl
+
+@[simp]
+theorem FreeM.toW_lift_bind' {α : Type uB} (a : P.A) (cont : P.B a → P.FreeM α) :
+    toW (Bind.bind (α := no_index (P.B a)) (lift a) cont) =
+      (W.mk ⟨.inr a, fun b => toW (cont b)⟩ : (C.{uB, uB} α + P).W) := rfl
+
+@[simp]
+theorem FreeM.ofW_toW (x : P.FreeM α) : ofW (toW x) = x := by
+  induction x with
+  | pure a => rfl
+  | lift_bind a cont ih => exact congrArg (liftBind a) (funext ih)
+
+@[simp]
+theorem FreeM.toW_ofW (w : (C.{u, uB} α + P).W) : toW (ofW w) = w := by
+  induction w with
+  | mk a f ih =>
+    cases a with
+    | inl a => exact congrArg (fun f => (W.mk ⟨.inl a, f⟩ : (C α + P).W)) (funext (·.elim))
+    | inr a => exact congrArg (fun f => (W.mk ⟨.inr a, f⟩ : (C α + P).W)) (funext ih)
+
+/-- Free programs are the W-trees of `C α + P`. -/
+@[simps]
+def FreeM.equivW : P.FreeM α ≃ (C.{u, uB} α + P).W where
+  toFun := toW
+  invFun := ofW
+  left_inv := ofW_toW
+  right_inv := toW_ofW
+
 end PFunctor
diff --git a/Cslib/Foundations/Data/PFunctor/M.lean b/Cslib/Foundations/Data/PFunctor/M.lean
new file mode 100644
index 000000000..a648f17c1
--- /dev/null
+++ b/Cslib/Foundations/Data/PFunctor/M.lean
@@ -0,0 +1,109 @@
+/-
+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.Foundations.Data.PFunctor.Basic
+public import Mathlib.Data.PFunctor.Univariate.M
+
+/-!
+# W-types as well-founded M-types
+
+For a polynomial functor `P`, the W-type `P.W` is its initial algebra (well-founded trees) and the
+M-type `P.M` is its final coalgebra (possibly infinite trees). The canonical map `W.toM` regards a
+well-founded tree as a possibly infinite one, and `W.equivM` identifies `P.W` with the M-trees that
+are accessible for the immediate-subtree relation, i.e. have no infinite descending path.
+
+Lambek's lemma `M.destEquiv` packages the destructor of `P.M` as an equivalence.
+-/
+
+@[expose] public section
+
+universe uA uB
+
+namespace PFunctor
+
+variable {P : PFunctor.{uA, uB}}
+
+/-- Lambek's lemma: the destructor of the final coalgebra is an equivalence. -/
+@[simps]
+def M.destEquiv : P.M ≃ P P.M where
+  toFun := M.dest
+  invFun := M.mk
+  left_inv := M.mk_dest
+  right_inv := M.dest_mk
+
+theorem M.dest_injective : Function.Injective (M.dest (F := P)) := M.destEquiv.injective
+
+@[simp]
+theorem M.dest_inj {x y : P.M} : M.dest x = M.dest y ↔ x = y := M.dest_injective.eq_iff
+
+/-- The canonical map from the initial algebra into the final coalgebra, regarding a well-founded
+tree as a possibly infinite one. -/
+def W.toM : P.W → P.M :=
+  M.corec W.dest
+
+@[simp]
+theorem W.toM_mk (a : P.A) (f : P.B a → P.W) :
+    (W.mk ⟨a, f⟩).toM = M.mk ⟨a, fun i => (f i).toM⟩ :=
+  M.dest_injective (M.dest_corec _ _)
+
+namespace M
+
+/-- `c` is an immediate subtree of `t`. -/
+def IsChild (c t : P.M) : Prop :=
+  ∃ i, (M.dest t).2 i = c
+
+/-- An M-tree is well-founded when it is accessible for the immediate-subtree relation, i.e. it has
+no infinite descending path. Its branches need not have a common depth bound. -/
+abbrev IsWellFounded (t : P.M) : Prop :=
+  Acc IsChild t
+
+theorem isWellFounded_mk {a : P.A} {f : P.B a → P.M} :
+    (M.mk ⟨a, f⟩).IsWellFounded ↔ ∀ i, (f i).IsWellFounded :=
+  ⟨fun h i => h.inv ⟨i, rfl⟩, fun h => ⟨_, fun _ ⟨i, hi⟩ => hi ▸ h i⟩⟩
+
+/-- The W-tree represented by a well-founded M-tree. -/
+def toW (t : P.M) (h : t.IsWellFounded) : P.W :=
+  Acc.rec (motive := fun _ _ => P.W) (fun t _ ih => W.mk ⟨(M.dest t).1, fun i => ih _ ⟨i, rfl⟩⟩) h
+
+@[simp]
+theorem toW_mk (a : P.A) (f : P.B a → P.M) (h : (M.mk ⟨a, f⟩).IsWellFounded) :
+    (M.mk ⟨a, f⟩).toW h = W.mk ⟨a, fun i => (f i).toW (isWellFounded_mk.1 h i)⟩ := by
+  cases h; rfl
+
+end M
+
+theorem W.isWellFounded_toM (w : P.W) : w.toM.IsWellFounded := by
+  induction w with
+  | mk a f ih => simpa [M.isWellFounded_mk] using ih
+
+@[simp]
+theorem M.toW_toM (w : P.W) (h : w.toM.IsWellFounded) : w.toM.toW h = w := by
+  induction w with
+  | mk a f ih => simp [ih]
+
+theorem W.toM_toW (t : P.M) (h : t.IsWellFounded) : (t.toW h).toM = t := by
+  induction h with
+  | intro t _ ih =>
+    induction t using M.cases with
+    | f x =>
+      obtain ⟨a, f⟩ := x
+      rw [M.toW_mk, W.toM_mk]
+      exact congrArg (M.mk ⟨a, ·⟩) (funext fun i => ih _ ⟨i, rfl⟩)
+
+/-- W-trees are exactly the well-founded M-trees. -/
+@[simps]
+def W.equivM : P.W ≃ {t : P.M // t.IsWellFounded} where
+  toFun w := ⟨w.toM, w.isWellFounded_toM⟩
+  invFun t := t.1.toW t.2
+  left_inv w := M.toW_toM w _
+  right_inv t := Subtype.ext (W.toM_toW t.1 t.2)
+
+theorem W.toM_injective : Function.Injective (W.toM (P := P)) :=
+  fun _ _ h => W.equivM.injective (Subtype.ext h)
+
+end PFunctor

From e99137038fa137ec7ea6afb7e1fa7beced2a0b2d Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Mon, 5 Oct 2026 18:36:08 -0500
Subject: [PATCH 2/5] refactor(PFunctor): build polynomial objects with
 `Obj.mk`

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Cslib/Foundations/Data/PFunctor/Basic.lean  |  2 +-
 Cslib/Foundations/Data/PFunctor/Free/W.lean | 18 +++++++++---------
 Cslib/Foundations/Data/PFunctor/M.lean      | 20 +++++++++++---------
 3 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean
index ab050ffd7..7402e31e8 100644
--- a/Cslib/Foundations/Data/PFunctor/Basic.lean
+++ b/Cslib/Foundations/Data/PFunctor/Basic.lean
@@ -163,7 +163,7 @@ variable {P : PFunctor.{uA, uB}}
 /-- Induction on `P.W` through `W.mk`, keeping subtrees typed as `P.W` rather than `WType P.B`. -/
 @[elab_as_elim, induction_eliminator]
 protected theorem W.induction {motive : P.W → Prop}
-    (mk : ∀ (a : P.A) (f : P.B a → P.W), (∀ i, motive (f i)) → motive (W.mk ⟨a, f⟩))
+    (mk : ∀ (a : P.A) (f : P.B a → P.W), (∀ i, motive (f i)) → motive (W.mk (.mk a f)))
     (w : P.W) : motive w := by
   induction w using WType.rec with
   | mk a f ih => exact mk a f ih
diff --git a/Cslib/Foundations/Data/PFunctor/Free/W.lean b/Cslib/Foundations/Data/PFunctor/Free/W.lean
index 408355afd..236ad9e2b 100644
--- a/Cslib/Foundations/Data/PFunctor/Free/W.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free/W.lean
@@ -76,27 +76,27 @@ def FreeM.equivWOfIsEmpty [IsEmpty α] : P.FreeM α ≃ P.W where
 
 /-- Regard a free program as a W-tree of `C α + P`, whose leaves carry the returned values. -/
 def FreeM.toW : P.FreeM α → (C.{u, uB} α + P).W
-  | .pure a => W.mk ⟨.inl a, PEmpty.elim⟩
-  | .liftBind a cont => W.mk ⟨.inr a, fun b => FreeM.toW (cont b)⟩
+  | .pure a => W.mk (.mk (.inl a) PEmpty.elim)
+  | .liftBind a cont => W.mk (.mk (.inr a) fun b => FreeM.toW (cont b))
 
 /-- Read a W-tree of `C α + P` as a free program. -/
 def FreeM.ofW : (C.{u, uB} α + P).W → P.FreeM α
-  | ⟨.inl a, _⟩ => .pure a
-  | ⟨.inr a, cont⟩ => .liftBind a fun b => FreeM.ofW (cont b)
+  | WType.mk (.inl a) _ => .pure a
+  | WType.mk (.inr a) cont => .liftBind a fun b => FreeM.ofW (cont b)
 
 @[simp]
 theorem FreeM.toW_pure (a : α) :
-    toW (pure a : P.FreeM α) = (W.mk ⟨.inl a, PEmpty.elim⟩ : (C.{u, uB} α + P).W) := rfl
+    toW (pure a : P.FreeM α) = (W.mk (.mk (.inl a) PEmpty.elim) : (C.{u, uB} α + P).W) := rfl
 
 @[simp]
 theorem FreeM.toW_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) :
     toW ((lift a).bind (α := no_index (P.B a)) cont) =
-      (W.mk ⟨.inr a, fun b => toW (cont b)⟩ : (C.{u, uB} α + P).W) := rfl
+      (W.mk (.mk (.inr a) fun b => toW (cont b)) : (C.{u, uB} α + P).W) := rfl
 
 @[simp]
 theorem FreeM.toW_lift_bind' {α : Type uB} (a : P.A) (cont : P.B a → P.FreeM α) :
     toW (Bind.bind (α := no_index (P.B a)) (lift a) cont) =
-      (W.mk ⟨.inr a, fun b => toW (cont b)⟩ : (C.{uB, uB} α + P).W) := rfl
+      (W.mk (.mk (.inr a) fun b => toW (cont b)) : (C.{uB, uB} α + P).W) := rfl
 
 @[simp]
 theorem FreeM.ofW_toW (x : P.FreeM α) : ofW (toW x) = x := by
@@ -109,8 +109,8 @@ theorem FreeM.toW_ofW (w : (C.{u, uB} α + P).W) : toW (ofW w) = w := by
   induction w with
   | mk a f ih =>
     cases a with
-    | inl a => exact congrArg (fun f => (W.mk ⟨.inl a, f⟩ : (C α + P).W)) (funext (·.elim))
-    | inr a => exact congrArg (fun f => (W.mk ⟨.inr a, f⟩ : (C α + P).W)) (funext ih)
+    | inl a => exact congrArg (fun f => (W.mk (.mk (.inl a) f) : (C α + P).W)) (funext (·.elim))
+    | inr a => exact congrArg (fun f => (W.mk (.mk (.inr a) f) : (C α + P).W)) (funext ih)
 
 /-- Free programs are the W-trees of `C α + P`. -/
 @[simps]
diff --git a/Cslib/Foundations/Data/PFunctor/M.lean b/Cslib/Foundations/Data/PFunctor/M.lean
index a648f17c1..9cb60fd92 100644
--- a/Cslib/Foundations/Data/PFunctor/M.lean
+++ b/Cslib/Foundations/Data/PFunctor/M.lean
@@ -48,14 +48,14 @@ def W.toM : P.W → P.M :=
 
 @[simp]
 theorem W.toM_mk (a : P.A) (f : P.B a → P.W) :
-    (W.mk ⟨a, f⟩).toM = M.mk ⟨a, fun i => (f i).toM⟩ :=
+    (W.mk (.mk a f)).toM = M.mk (.mk a fun i => (f i).toM) :=
   M.dest_injective (M.dest_corec _ _)
 
 namespace M
 
 /-- `c` is an immediate subtree of `t`. -/
 def IsChild (c t : P.M) : Prop :=
-  ∃ i, (M.dest t).2 i = c
+  ∃ i, (M.dest t).snd i = c
 
 /-- An M-tree is well-founded when it is accessible for the immediate-subtree relation, i.e. it has
 no infinite descending path. Its branches need not have a common depth bound. -/
@@ -63,16 +63,17 @@ abbrev IsWellFounded (t : P.M) : Prop :=
   Acc IsChild t
 
 theorem isWellFounded_mk {a : P.A} {f : P.B a → P.M} :
-    (M.mk ⟨a, f⟩).IsWellFounded ↔ ∀ i, (f i).IsWellFounded :=
+    (M.mk (.mk a f)).IsWellFounded ↔ ∀ i, (f i).IsWellFounded :=
   ⟨fun h i => h.inv ⟨i, rfl⟩, fun h => ⟨_, fun _ ⟨i, hi⟩ => hi ▸ h i⟩⟩
 
 /-- The W-tree represented by a well-founded M-tree. -/
 def toW (t : P.M) (h : t.IsWellFounded) : P.W :=
-  Acc.rec (motive := fun _ _ => P.W) (fun t _ ih => W.mk ⟨(M.dest t).1, fun i => ih _ ⟨i, rfl⟩⟩) h
+  Acc.rec (motive := fun _ _ => P.W)
+    (fun t _ ih => W.mk (.mk (M.dest t).fst fun i => ih _ ⟨i, rfl⟩)) h
 
 @[simp]
-theorem toW_mk (a : P.A) (f : P.B a → P.M) (h : (M.mk ⟨a, f⟩).IsWellFounded) :
-    (M.mk ⟨a, f⟩).toW h = W.mk ⟨a, fun i => (f i).toW (isWellFounded_mk.1 h i)⟩ := by
+theorem toW_mk (a : P.A) (f : P.B a → P.M) (h : (M.mk (.mk a f)).IsWellFounded) :
+    (M.mk (.mk a f)).toW h = W.mk (.mk a fun i => (f i).toW (isWellFounded_mk.1 h i)) := by
   cases h; rfl
 
 end M
@@ -91,9 +92,10 @@ theorem W.toM_toW (t : P.M) (h : t.IsWellFounded) : (t.toW h).toM = t := by
   | intro t _ ih =>
     induction t using M.cases with
     | f x =>
-      obtain ⟨a, f⟩ := x
-      rw [M.toW_mk, W.toM_mk]
-      exact congrArg (M.mk ⟨a, ·⟩) (funext fun i => ih _ ⟨i, rfl⟩)
+      cases x with
+      | mk a f =>
+        rw [M.toW_mk, W.toM_mk]
+        exact congrArg (M.mk <| .mk a ·) (funext fun i => ih _ ⟨i, rfl⟩)
 
 /-- W-trees are exactly the well-founded M-trees. -/
 @[simps]

From 90e958b114b56de52535694721598b5a46ec5592 Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Mon, 5 Oct 2026 18:44:59 -0500
Subject: [PATCH 3/5] feat(PFunctor): add coinductive resumptions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add `PFunctor.Resumption P α`, the M-type of `C α + P`: possibly
non-terminating programs that return an `α` or perform an operation of `P`.
It has a corecursor, a bisimulation principle and a lawful monad structure,
and `FreeM.toResumption` is an injective monad morphism whose image is exactly
the well-founded resumptions.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Cslib.lean                                    |   1 +
 Cslib/Foundations/Data/PFunctor/Basic.lean    |  58 ++-
 Cslib/Foundations/Data/PFunctor/Free.lean     |   3 +-
 .../Foundations/Data/PFunctor/Resumption.lean | 356 ++++++++++++++++++
 CslibTests.lean                               |   1 +
 CslibTests/Resumption.lean                    |  26 ++
 references.bib                                |  32 ++
 7 files changed, 475 insertions(+), 2 deletions(-)
 create mode 100644 Cslib/Foundations/Data/PFunctor/Resumption.lean
 create mode 100644 CslibTests/Resumption.lean

diff --git a/Cslib.lean b/Cslib.lean
index af6a5420a..203739763 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -140,6 +140,7 @@ public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.PFunctor.Free.Fold
 public import Cslib.Foundations.Data.PFunctor.Free.W
 public import Cslib.Foundations.Data.PFunctor.M
+public import Cslib.Foundations.Data.PFunctor.Resumption
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean
index 7402e31e8..dd4f6fc40 100644
--- a/Cslib/Foundations/Data/PFunctor/Basic.lean
+++ b/Cslib/Foundations/Data/PFunctor/Basic.lean
@@ -21,13 +21,14 @@ Special cases `C`, `linear`, `selfMonomial`, `purePower`, the indeterminate `y`,
 and canonical choices of `0` and `1` are defined as abbreviations or instances over `monomial`.
 The scoped notations `A y^ B` and `y^ B` denote `monomial A B` and `purePower B`, respectively.
 
+The extensions of `P + Q` and `C A` are described by `addObjEquiv` and `constObjEquiv`.
 The child-map API includes `const`, `Unary`, and `DecidableEqChildren`. `W.induction` is an
 induction principle for `P.W` through `W.mk`.
 -/
 
 @[expose] public section
 
-universe uA uB uA₁ uA₂ uB₁ uB₂
+universe uA uB uA₁ uA₂ uB₁ uB₂ v w
 
 namespace PFunctor
 
@@ -156,6 +157,61 @@ defined as the product of the head types and the sum of the child types. -/
 
 end prod
 
+section Obj
+
+variable {X : Type v} {Y : Type w}
+
+@[simp]
+theorem map_id' (P : PFunctor.{uA, uB}) : P.map (id : X → X) = id :=
+  funext P.id_map
+
+@[simp]
+theorem map_comp_map (P : PFunctor.{uA, uB}) {Z : Type*} (f : X → Y) (g : Y → Z) :
+    P.map g ∘ P.map f = P.map (g ∘ f) :=
+  funext (P.map_map f g)
+
+/-- The extension of a sum of polynomial functors is the sum of their extensions. -/
+def addObjEquiv (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (X : Type v) :
+    (P + Q).Obj X ≃ P.Obj X ⊕ Q.Obj X where
+  toFun
+    | .mk (.inl a) f => .inl (.mk a f)
+    | .mk (.inr a) f => .inr (.mk a f)
+  invFun
+    | .inl (.mk a f) => .mk (.inl a) f
+    | .inr (.mk a f) => .mk (.inr a) f
+  left_inv x := by cases x with | mk s f => cases s <;> rfl
+  right_inv x := by rcases x with (x | x) <;> cases x <;> rfl
+
+@[simp]
+theorem addObjEquiv_mk_inl (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A)
+    (f : P.B a → X) : addObjEquiv P Q X (.mk (.inl a) f) = .inl (.mk a f) := rfl
+
+@[simp]
+theorem addObjEquiv_mk_inr (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : Q.A)
+    (f : Q.B a → X) : addObjEquiv P Q X (.mk (.inr a) f) = .inr (.mk a f) := rfl
+
+theorem addObjEquiv_map (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (f : X → Y)
+    (x : (P + Q).Obj X) :
+    addObjEquiv P Q Y ((P + Q).map f x) = Sum.map (P.map f) (Q.map f) (addObjEquiv P Q X x) := by
+  cases x with | mk s g => cases s <;> rfl
+
+/-- The extension of a constant polynomial functor is the constant. -/
+def constObjEquiv (A : Type uA) (X : Type v) : (C.{uA, uB} A).Obj X ≃ A where
+  toFun x := x.fst
+  invFun a := .mk a PEmpty.elim
+  left_inv x := by cases x with | mk a f => exact congrArg (Obj.mk a) (funext (·.elim))
+  right_inv _ := rfl
+
+@[simp]
+theorem constObjEquiv_mk (A : Type uA) (a : A) (f : PEmpty.{uB + 1} → X) :
+    constObjEquiv A X (.mk a f) = a := rfl
+
+@[simp]
+theorem constObjEquiv_map (A : Type uA) (f : X → Y) (x : (C.{uA, uB} A).Obj X) :
+    constObjEquiv A Y ((C A).map f x) = constObjEquiv A X x := rfl
+
+end Obj
+
 section W
 
 variable {P : PFunctor.{uA, uB}}
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index b95829777..7a2bb2d39 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -17,7 +17,8 @@ We define the free monad on a **polynomial functor** (`PFunctor`), and prove som
 
 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`. `FreeM.equivW`
-identifies `P.FreeM α` with the W-type of `C α + P`.
+identifies `P.FreeM α` with the W-type of `C α + P`, and the M-type of the same polynomial gives
+the coinductive counterpart `PFunctor.Resumption`, whose programs may run forever.
 
 ## Comparison with `Cslib.FreeM`
 
diff --git a/Cslib/Foundations/Data/PFunctor/Resumption.lean b/Cslib/Foundations/Data/PFunctor/Resumption.lean
new file mode 100644
index 000000000..9391e587c
--- /dev/null
+++ b/Cslib/Foundations/Data/PFunctor/Resumption.lean
@@ -0,0 +1,356 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+
+module
+
+public import Cslib.Foundations.Data.PFunctor.Free.W
+public import Cslib.Foundations.Data.PFunctor.M
+
+/-!
+# Coinductive resumptions
+
+A resumption `r : PFunctor.Resumption P α` is a possibly non-terminating program that either
+returns a value of `α` or performs an operation `a : P.A` and continues with a response
+`b : P.B a`. It is the M-type of the polynomial `C α + P`, i.e. the final coalgebra of
+`X ↦ α ⊕ P X`. The initial algebra of the same functor is the free monad `P.FreeM α`, which is the
+W-type of `C α + P` (`PFunctor.FreeM.equivW`).
+
+`PFunctor.FreeM.toResumption` is an injective monad morphism whose image is exactly the
+well-founded resumptions (`PFunctor.FreeM.equivWellFounded`), so resumptions extend free programs
+by infinite runs. Over the indeterminate `y`, with a single operation and a unit response,
+resumptions form Capretta's delay monad [Capretta2005]. They give semantics to loops whose
+termination is not structural, such as rejection sampling or the execution of a machine.
+
+This is the resumption monad of [PirogGibbons2014], the identity-monad case of the coalgebraic
+resumptions of [GoncharovMiliusRauch2016]. Unlike the cofree comonad, whose one-step view
+`α × P X` labels every node, a resumption returns a value only at a leaf.
+
+## Main definitions
+
+- `PFunctor.Resumption.dest`: the one-step view, an equivalence `destEquiv`, with the constructors
+  `pure` and `query` and a `cases` eliminator.
+- `PFunctor.Resumption.corec`: the corecursor, characterized by `corec_unique`.
+- `PFunctor.Resumption.bisim`: coinduction through the relation lifting `StepRel`.
+- `PFunctor.Resumption.bind`: sequencing, giving a lawful monad.
+- `PFunctor.FreeM.toResumption`: the embedding of free programs.
+
+## References
+
+* [Piróg and Gibbons, *The Coinductive Resumption Monad*][PirogGibbons2014]
+* [Capretta, *General Recursion via Coinductive Types*][Capretta2005]
+* [Goncharov, Milius and Rauch, *Complete Elgot Monads and Coalgebraic
+  Resumptions*][GoncharovMiliusRauch2016]
+-/
+
+@[expose] public section
+
+universe uA uB u v w
+
+namespace PFunctor
+
+/-- Possibly non-terminating programs over `P` returning a value of `α`: the M-type of `C α + P`,
+whose W-type is `P.FreeM α`. -/
+abbrev Resumption (P : PFunctor.{uA, uB}) (α : Type u) : Type (max u uA uB) :=
+  M (C.{u, uB} α + P : PFunctor.{max u uA, uB})
+
+namespace Resumption
+
+variable {P : PFunctor.{uA, uB}} {α : Type u} {β : Type v} {γ : Type w}
+
+/-- One step of a program over `P` returning `α`: a returned value or an operation with its
+continuation. -/
+def stepEquiv (P : PFunctor.{uA, uB}) (α : Type u) (X : Type v) :
+    (C.{u, uB} α + P).Obj X ≃ α ⊕ P.Obj X :=
+  (addObjEquiv _ _ X).trans ((constObjEquiv α X).sumCongr (Equiv.refl _))
+
+@[simp]
+theorem stepEquiv_mk_inl {X : Type v} (a : α) (f : (C.{u, uB} α + P).B (.inl a) → X) :
+    stepEquiv P α X (.mk (.inl a) f) = .inl a := rfl
+
+@[simp]
+theorem stepEquiv_mk_inr {X : Type v} (a : P.A) (f : (C.{u, uB} α + P).B (.inr a) → X) :
+    stepEquiv P α X (.mk (.inr a) f) = .inr (.mk a f) := rfl
+
+theorem stepEquiv_map {X : Type v} {Y : Type w} (f : X → Y) (x : (C.{u, uB} α + P).Obj X) :
+    stepEquiv P α Y ((C α + P).map f x) = Sum.map id (P.map f) (stepEquiv P α X x) := by
+  cases x with | mk s g => cases s <;> rfl
+
+/-- The one-step view of a resumption. -/
+def destEquiv : Resumption P α ≃ α ⊕ P.Obj (Resumption P α) :=
+  M.destEquiv.trans (stepEquiv P α _)
+
+/-- Observe whether a resumption returns a value or performs an operation. -/
+def dest (r : Resumption P α) : α ⊕ P.Obj (Resumption P α) :=
+  destEquiv r
+
+/-- The resumption returning `a` immediately. -/
+protected def pure (a : α) : Resumption P α :=
+  destEquiv.symm (.inl a)
+
+/-- The resumption performing the operation `a` and continuing with `k`. -/
+def query (a : P.A) (k : P.B a → Resumption P α) : Resumption P α :=
+  destEquiv.symm (.inr (.mk a k))
+
+instance : Pure (Resumption P) where
+  pure := Resumption.pure
+
+@[simp]
+theorem pure_eq_pure : (Resumption.pure : α → Resumption P α) = pure := rfl
+
+@[simp]
+theorem dest_mk (x : (C.{u, uB} α + P).Obj (Resumption P α)) :
+    dest (M.mk x) = stepEquiv P α _ x := rfl
+
+@[simp]
+theorem dest_pure (a : α) : dest (pure a : Resumption P α) = .inl a :=
+  destEquiv.apply_symm_apply _
+
+@[simp]
+theorem dest_query (a : P.A) (k : P.B a → Resumption P α) :
+    dest (query a k) = .inr (.mk a k) :=
+  destEquiv.apply_symm_apply _
+
+theorem dest_injective : Function.Injective (dest : Resumption P α → _) :=
+  destEquiv.injective
+
+@[simp]
+theorem dest_inj {r s : Resumption P α} : dest r = dest s ↔ r = s :=
+  dest_injective.eq_iff
+
+/-- Case analysis on whether a resumption returns a value or performs an operation. -/
+@[elab_as_elim, cases_eliminator]
+protected theorem cases {motive : Resumption P α → Prop} (pure : ∀ a, motive (pure a))
+    (query : ∀ a k, motive (query a k)) (r : Resumption P α) : motive r := by
+  rw [← destEquiv.symm_apply_apply r]
+  rcases destEquiv r with a | x
+  · exact pure a
+  · cases x with | mk a k => exact query a k
+
+/-- The resumption unfolding from a state by a step function. -/
+def corec {X : Type v} (f : X → α ⊕ P.Obj X) : X → Resumption P α :=
+  M.corec fun x => (stepEquiv P α X).symm (f x)
+
+@[simp]
+theorem dest_corec {X : Type v} (f : X → α ⊕ P.Obj X) (x : X) :
+    dest (corec f x) = Sum.map id (P.map (corec f)) (f x) := by
+  simp [dest, destEquiv, corec, M.dest_corec, stepEquiv_map]
+
+/-- Finality: `corec f` is the only map into resumptions that unfolds by `f`. -/
+theorem corec_unique {X : Type v} (f : X → α ⊕ P.Obj X) (g : X → Resumption P α)
+    (hg : ∀ x, dest (g x) = Sum.map id (P.map g) (f x)) : g = corec f :=
+  M.corec_unique _ g fun x =>
+    (stepEquiv P α _).injective (by rw [stepEquiv_map, Equiv.apply_symm_apply]; exact hg x)
+
+@[simp]
+theorem corec_dest : corec (dest : Resumption P α → _) = id :=
+  (corec_unique _ _ fun r => by cases r <;> simp).symm
+
+/-- Corecursion is natural in maps of states that commute with the step functions. -/
+theorem corec_comp {X : Type v} {Y : Type w} (f : X → α ⊕ P.Obj X) (g : Y → α ⊕ P.Obj Y)
+    (h : X → Y) (hh : ∀ x, g (h x) = Sum.map id (P.map h) (f x)) : corec g ∘ h = corec f :=
+  corec_unique f _ fun x => by simp [hh, Sum.map_map]
+
+/-- Lift a relation through one step: both sides return the same value, or perform the same
+operation with related continuations. -/
+inductive StepRel {X : Type v} {Y : Type w} (R : X → Y → Prop) :
+    α ⊕ P.Obj X → α ⊕ P.Obj Y → Prop
+  | pure (a : α) : StepRel R (.inl a) (.inl a)
+  | query (a : P.A) {k : P.B a → X} {k' : P.B a → Y} (h : ∀ i, R (k i) (k' i)) :
+      StepRel R (.inr (.mk a k)) (.inr (.mk a k'))
+
+theorem StepRel.refl {X : Type v} {R : X → X → Prop} (hR : ∀ x, R x x) :
+    ∀ s : α ⊕ P.Obj X, StepRel R s s
+  | .inl a => .pure a
+  | .inr (.mk a _) => .query a fun _ => hR _
+
+/-- Coinduction: related resumptions are equal when related resumptions take related steps. -/
+theorem bisim (R : Resumption P α → Resumption P α → Prop)
+    (h : ∀ r s, R r s → StepRel R (dest r) (dest s)) {r s : Resumption P α} (hrs : R r s) :
+    r = s := by
+  have step : ∀ {x y}, StepRel R x y → ∃ a f f', (stepEquiv P α _).symm x = .mk a f ∧
+      (stepEquiv P α _).symm y = .mk a f' ∧ ∀ i, R (f i) (f' i) := by
+    rintro _ _ (⟨a⟩ | ⟨a, hk⟩)
+    exacts [⟨.inl a, PEmpty.elim, PEmpty.elim, rfl, rfl, (·.elim)⟩, ⟨.inr a, _, _, rfl, rfl, hk⟩]
+  refine M.bisim R (fun r s hrs => ?_) r s hrs
+  rw [← (stepEquiv P α _).symm_apply_apply (M.dest r),
+    ← (stepEquiv P α _).symm_apply_apply (M.dest s)]
+  exact step (h r s hrs)
+
+/-- Perform the operation `a`, returning its response. -/
+def lift (a : P.A) : Resumption P (P.B a) :=
+  query a pure
+
+@[simp]
+theorem lift_eq_query (a : P.A) : lift a = query (P := P) a pure := rfl
+
+/-- The step function of `bind`: run the first resumption, then the continuation of its result. -/
+def bindStep (k : α → Resumption P β) :
+    Resumption P α ⊕ Resumption P β → β ⊕ P.Obj (Resumption P α ⊕ Resumption P β)
+  | .inl r => (dest r).elim (fun a => Sum.map id (P.map .inr) (dest (k a)))
+      fun x => .inr (P.map .inl x)
+  | .inr r => Sum.map id (P.map .inr) (dest r)
+
+/-- Sequence a resumption with a continuation for its returned value.
+
+The builtin `>>=` notation should be preferred when `α` and `β` are in the same universe. -/
+protected def bind (r : Resumption P α) (k : α → Resumption P β) : Resumption P β :=
+  corec (bindStep k) (.inl r)
+
+/-- Apply a function to the returned value.
+
+The builtin `<$>` notation should be preferred when `α` and `β` are in the same universe. -/
+protected def map (f : α → β) (r : Resumption P α) : Resumption P β :=
+  r.bind (pure ∘ f)
+
+@[simp]
+theorem corec_bindStep_comp_inr (k : α → Resumption P β) : corec (bindStep k) ∘ Sum.inr = id :=
+  (corec_comp dest (bindStep k) Sum.inr fun _ => rfl).trans corec_dest
+
+@[simp]
+theorem pure_bind (a : α) (k : α → Resumption P β) : (pure a : Resumption P α).bind k = k a :=
+  dest_injective (by simp [Resumption.bind, bindStep, Sum.map_map])
+
+@[simp]
+theorem query_bind (a : P.A) (f : P.B a → Resumption P α) (k : α → Resumption P β) :
+    (query a f).bind k = query a fun i => (f i).bind k :=
+  dest_injective (by simp [Resumption.bind, bindStep]; rfl)
+
+@[simp]
+theorem bind_pure (r : Resumption P α) : r.bind pure = r :=
+  bisim (fun x y => x = y.bind pure) (fun _ y h => by
+    subst h
+    cases y with
+    | pure a => simp only [pure_bind, dest_pure]; exact .pure a
+    | query a k => simp only [query_bind, dest_query]; exact .query a fun _ => rfl) rfl
+
+theorem bind_assoc (r : Resumption P α) (k : α → Resumption P β) (k' : β → Resumption P γ) :
+    (r.bind k).bind k' = r.bind fun a => (k a).bind k' :=
+  bisim (fun x y => x = y ∨ ∃ r, x = (r.bind k).bind k' ∧ y = r.bind fun a => (k a).bind k')
+    (fun x y h => by
+      obtain rfl | ⟨r, rfl, rfl⟩ := h
+      · exact StepRel.refl (fun _ => .inl rfl) _
+      · cases r with
+        | pure a => simp only [pure_bind]; exact StepRel.refl (fun _ => .inl rfl) _
+        | query a f =>
+          simp only [query_bind, dest_query]
+          exact .query a fun i => .inr ⟨f i, rfl, rfl⟩)
+    (.inr ⟨r, rfl, rfl⟩)
+
+@[simp]
+theorem map_pure (f : α → β) (a : α) : (pure a : Resumption P α).map f = pure (f a) :=
+  pure_bind _ _
+
+@[simp]
+theorem map_query (f : α → β) (a : P.A) (k : P.B a → Resumption P α) :
+    (query a k).map f = query a fun i => (k i).map f :=
+  query_bind _ _ _
+
+section Monad
+
+variable {α β : Type u}
+
+instance : Monad (Resumption P) where
+  bind := Resumption.bind
+  map := Resumption.map
+
+/-- Note that this lemma does not always apply, as it is universe-constrained by `Bind.bind`. -/
+@[simp]
+theorem bind_eq_bind : (Resumption.bind : Resumption P α → _ → Resumption P β) = Bind.bind := rfl
+
+/-- Note that this lemma does not always apply, as it is universe-constrained by `Functor.map`. -/
+@[simp]
+theorem map_eq_map : (Resumption.map : (α → β) → Resumption P α → _) = Functor.map := rfl
+
+instance : LawfulMonad (Resumption P) := LawfulMonad.mk'
+  (id_map := bind_pure)
+  (pure_bind := pure_bind)
+  (bind_assoc := bind_assoc)
+  (bind_pure_comp := fun _ _ => rfl)
+
+@[simp]
+theorem query_bind' (a : P.A) (f : P.B a → Resumption P α) (k : α → Resumption P β) :
+    query a f >>= k = query a fun i => f i >>= k :=
+  query_bind a f k
+
+@[simp]
+theorem map_query' (f : α → β) (a : P.A) (k : P.B a → Resumption P α) :
+    f <$> query a k = query a fun i => f <$> k i :=
+  map_query f a k
+
+end Monad
+
+end Resumption
+
+namespace FreeM
+
+variable {P : PFunctor.{uA, uB}} {α : Type u} {β : Type v}
+
+/-- Regard a free program as a resumption. Free programs are exactly the well-founded
+resumptions (`equivWellFounded`). -/
+def toResumption (x : P.FreeM α) : Resumption P α :=
+  (toW x).toM
+
+@[simp]
+theorem toResumption_pure (a : α) : toResumption (pure a : P.FreeM α) = pure a :=
+  Resumption.dest_injective (by rw [toResumption, toW_pure, W.toM_mk]; rfl)
+
+theorem toResumption_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) :
+    toResumption ((lift a).bind cont) = .query a fun b => toResumption (cont b) :=
+  Resumption.dest_injective (by simp [toResumption]; rfl)
+
+@[simp]
+theorem toResumption_lift (a : P.A) :
+    toResumption (α := no_index (P.B a)) (lift a) = .query a pure := by
+  simpa using toResumption_lift_bind a (pure : P.B a → P.FreeM (P.B a))
+
+@[simp]
+theorem toResumption_bind (x : P.FreeM α) (f : α → P.FreeM β) :
+    toResumption (x.bind f) = (toResumption x).bind fun a => toResumption (f a) := by
+  induction x with
+  | pure a => simp
+  | lift_bind a cont ih => simp [toResumption_lift_bind, ih]
+
+@[simp]
+theorem toResumption_map (f : α → β) (x : P.FreeM α) :
+    toResumption (x.map f) = (toResumption x).map f := by
+  simp [← bind_pure_comp, Resumption.map, Function.comp_def]
+
+theorem isMonadHom_toResumption :
+    Cslib.IsMonadHom P.FreeM (Resumption P) toResumption :=
+  .mk' toResumption_pure toResumption_bind
+
+@[simp]
+theorem toResumption_bind' {α β : Type u} (x : P.FreeM α) (f : α → P.FreeM β) :
+    toResumption (x >>= f) = toResumption x >>= fun a => toResumption (f a) :=
+  toResumption_bind x f
+
+@[simp]
+theorem toResumption_map' {α β : Type u} (f : α → β) (x : P.FreeM α) :
+    toResumption (f <$> x) = f <$> toResumption x :=
+  toResumption_map f x
+
+/-- `toResumption` interprets each operation as the corresponding resumption operation. -/
+theorem toResumption_eq_liftM {α : Type uB} (x : P.FreeM α) :
+    toResumption x = x.liftM Resumption.lift := by
+  induction x <;> simp [*]
+
+theorem toResumption_injective : Function.Injective (toResumption : P.FreeM α → _) :=
+  fun _ _ h => equivW.injective (W.toM_injective h)
+
+theorem isWellFounded_toResumption (x : P.FreeM α) : (toResumption x).IsWellFounded :=
+  W.isWellFounded_toM _
+
+/-- Free programs are exactly the well-founded resumptions. -/
+def equivWellFounded : P.FreeM α ≃ {r : Resumption P α // r.IsWellFounded} :=
+  equivW.trans W.equivM
+
+@[simp]
+theorem equivWellFounded_apply (x : P.FreeM α) :
+    (equivWellFounded x : Resumption P α) = toResumption x := rfl
+
+end FreeM
+
+end PFunctor
diff --git a/CslibTests.lean b/CslibTests.lean
index b39a27de5..95585e1a9 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -32,5 +32,6 @@ import CslibTests.PFunctor
 import CslibTests.PFunctorFree
 import CslibTests.PRG
 import CslibTests.Reduction
+import CslibTests.Resumption
 import CslibTests.StatefulProcesses
 import CslibTests.Synthesis
diff --git a/CslibTests/Resumption.lean b/CslibTests/Resumption.lean
new file mode 100644
index 000000000..52cb4ca5e
--- /dev/null
+++ b/CslibTests/Resumption.lean
@@ -0,0 +1,26 @@
+/-
+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.Resumption
+
+/-! Tests for coinductive resumptions. -/
+
+namespace CslibTests.Resumption
+
+open PFunctor
+
+private def flips : (y^ Bool).FreeM Bool := do
+  let b ← FreeM.lift ()
+  let c ← FreeM.lift ()
+  pure (b && !c)
+
+-- Embedding a `do` program, which uses `>>=` and `<$>` rather than the universe-polymorphic
+-- `bind` and `map`, normalizes to explicit queries.
+example : flips.toResumption =
+    Resumption.query () fun b => Resumption.query () fun c => pure (b && !c) := by
+  simp [flips]
+
+end CslibTests.Resumption
diff --git a/references.bib b/references.bib
index afbe3d9b0..653173b81 100644
--- a/references.bib
+++ b/references.bib
@@ -622,3 +622,35 @@ @article{Vardi1989
   pages        = {261--264},
   year         = {1989}
 }
+
+@article{     Capretta2005,
+  author    = {Capretta, Venanzio},
+  title     = {General Recursion via Coinductive Types},
+  journal   = {Logical Methods in Computer Science},
+  volume    = {1},
+  number    = {2},
+  year      = {2005},
+  doi       = {10.2168/LMCS-1(2:1)2005}
+}
+
+@article{     PirogGibbons2014,
+  author    = {Pir{\'o}g, Maciej and Gibbons, Jeremy},
+  title     = {The Coinductive Resumption Monad},
+  journal   = {Electronic Notes in Theoretical Computer Science},
+  volume    = {308},
+  pages     = {273--288},
+  year      = {2014},
+  note      = {Proceedings of MFPS XXX},
+  doi       = {10.1016/j.entcs.2014.10.015}
+}
+
+@article{     GoncharovMiliusRauch2016,
+  author    = {Goncharov, Sergey and Milius, Stefan and Rauch, Christoph},
+  title     = {Complete {E}lgot Monads and Coalgebraic Resumptions},
+  journal   = {Electronic Notes in Theoretical Computer Science},
+  volume    = {325},
+  pages     = {147--168},
+  year      = {2016},
+  note      = {Proceedings of MFPS XXXII},
+  doi       = {10.1016/j.entcs.2016.09.036}
+}

From 0d4434c06f538a238a0c467b13e86105c6540cec Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Mon, 5 Oct 2026 18:49:32 -0500
Subject: [PATCH 4/5] refactor(Resumption): mirror the polynomial free monad
 API

Use `liftBind` as the implementation-detail constructor with simp-normal
form `(lift a).bind k`, as for `PFunctor.FreeM`, and name the cases and
lemmas accordingly (`lift_bind`, `liftBind_bind`, `dest_lift_bind`,
`map_bind`, `bind_pure_comp`).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../Foundations/Data/PFunctor/Resumption.lean | 115 ++++++++++--------
 CslibTests/Resumption.lean                    |   8 +-
 2 files changed, 70 insertions(+), 53 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/Resumption.lean b/Cslib/Foundations/Data/PFunctor/Resumption.lean
index 9391e587c..358648f40 100644
--- a/Cslib/Foundations/Data/PFunctor/Resumption.lean
+++ b/Cslib/Foundations/Data/PFunctor/Resumption.lean
@@ -30,8 +30,9 @@ resumptions of [GoncharovMiliusRauch2016]. Unlike the cofree comonad, whose one-
 
 ## Main definitions
 
-- `PFunctor.Resumption.dest`: the one-step view, an equivalence `destEquiv`, with the constructors
-  `pure` and `query` and a `cases` eliminator.
+- `PFunctor.Resumption.dest`: the one-step view, an equivalence `destEquiv`, with a `cases`
+  eliminator into returned values `pure a` and operations `(lift a).bind k`, as for
+  `PFunctor.FreeM`.
 - `PFunctor.Resumption.corec`: the corecursor, characterized by `corec_unique`.
 - `PFunctor.Resumption.bisim`: coinduction through the relation lifting `StepRel`.
 - `PFunctor.Resumption.bind`: sequencing, giving a lawful monad.
@@ -90,10 +91,16 @@ def dest (r : Resumption P α) : α ⊕ P.Obj (Resumption P α) :=
 protected def pure (a : α) : Resumption P α :=
   destEquiv.symm (.inl a)
 
-/-- The resumption performing the operation `a` and continuing with `k`. -/
-def query (a : P.A) (k : P.B a → Resumption P α) : Resumption P α :=
+/-- The resumption performing the operation `a` and continuing with `k`.
+
+This is an implementation detail; the simp-normal form is `(lift a).bind k` (see `liftBind_eq`). -/
+def liftBind (a : P.A) (k : P.B a → Resumption P α) : Resumption P α :=
   destEquiv.symm (.inr (.mk a k))
 
+/-- Perform the operation `a`, returning its response. -/
+def lift (a : P.A) : Resumption P (P.B a) :=
+  liftBind a .pure
+
 instance : Pure (Resumption P) where
   pure := Resumption.pure
 
@@ -108,11 +115,14 @@ theorem dest_mk (x : (C.{u, uB} α + P).Obj (Resumption P α)) :
 theorem dest_pure (a : α) : dest (pure a : Resumption P α) = .inl a :=
   destEquiv.apply_symm_apply _
 
-@[simp]
-theorem dest_query (a : P.A) (k : P.B a → Resumption P α) :
-    dest (query a k) = .inr (.mk a k) :=
+theorem dest_liftBind (a : P.A) (k : P.B a → Resumption P α) :
+    dest (liftBind a k) = .inr (.mk a k) :=
   destEquiv.apply_symm_apply _
 
+@[simp]
+theorem dest_lift (a : P.A) : dest (lift (P := P) a) = .inr (.mk a pure) :=
+  dest_liftBind _ _
+
 theorem dest_injective : Function.Injective (dest : Resumption P α → _) :=
   destEquiv.injective
 
@@ -120,15 +130,6 @@ theorem dest_injective : Function.Injective (dest : Resumption P α → _) :=
 theorem dest_inj {r s : Resumption P α} : dest r = dest s ↔ r = s :=
   dest_injective.eq_iff
 
-/-- Case analysis on whether a resumption returns a value or performs an operation. -/
-@[elab_as_elim, cases_eliminator]
-protected theorem cases {motive : Resumption P α → Prop} (pure : ∀ a, motive (pure a))
-    (query : ∀ a k, motive (query a k)) (r : Resumption P α) : motive r := by
-  rw [← destEquiv.symm_apply_apply r]
-  rcases destEquiv r with a | x
-  · exact pure a
-  · cases x with | mk a k => exact query a k
-
 /-- The resumption unfolding from a state by a step function. -/
 def corec {X : Type v} (f : X → α ⊕ P.Obj X) : X → Resumption P α :=
   M.corec fun x => (stepEquiv P α X).symm (f x)
@@ -146,7 +147,7 @@ theorem corec_unique {X : Type v} (f : X → α ⊕ P.Obj X) (g : X → Resumpti
 
 @[simp]
 theorem corec_dest : corec (dest : Resumption P α → _) = id :=
-  (corec_unique _ _ fun r => by cases r <;> simp).symm
+  (corec_unique _ _ fun _ => by simp).symm
 
 /-- Corecursion is natural in maps of states that commute with the step functions. -/
 theorem corec_comp {X : Type v} {Y : Type w} (f : X → α ⊕ P.Obj X) (g : Y → α ⊕ P.Obj Y)
@@ -158,13 +159,13 @@ operation with related continuations. -/
 inductive StepRel {X : Type v} {Y : Type w} (R : X → Y → Prop) :
     α ⊕ P.Obj X → α ⊕ P.Obj Y → Prop
   | pure (a : α) : StepRel R (.inl a) (.inl a)
-  | query (a : P.A) {k : P.B a → X} {k' : P.B a → Y} (h : ∀ i, R (k i) (k' i)) :
+  | liftBind (a : P.A) {k : P.B a → X} {k' : P.B a → Y} (h : ∀ i, R (k i) (k' i)) :
       StepRel R (.inr (.mk a k)) (.inr (.mk a k'))
 
 theorem StepRel.refl {X : Type v} {R : X → X → Prop} (hR : ∀ x, R x x) :
     ∀ s : α ⊕ P.Obj X, StepRel R s s
   | .inl a => .pure a
-  | .inr (.mk a _) => .query a fun _ => hR _
+  | .inr (.mk a _) => .liftBind a fun _ => hR _
 
 /-- Coinduction: related resumptions are equal when related resumptions take related steps. -/
 theorem bisim (R : Resumption P α → Resumption P α → Prop)
@@ -179,13 +180,6 @@ theorem bisim (R : Resumption P α → Resumption P α → Prop)
     ← (stepEquiv P α _).symm_apply_apply (M.dest s)]
   exact step (h r s hrs)
 
-/-- Perform the operation `a`, returning its response. -/
-def lift (a : P.A) : Resumption P (P.B a) :=
-  query a pure
-
-@[simp]
-theorem lift_eq_query (a : P.A) : lift a = query (P := P) a pure := rfl
-
 /-- The step function of `bind`: run the first resumption, then the continuation of its result. -/
 def bindStep (k : α → Resumption P β) :
     Resumption P α ⊕ Resumption P β → β ⊕ P.Obj (Resumption P α ⊕ Resumption P β)
@@ -213,10 +207,32 @@ theorem corec_bindStep_comp_inr (k : α → Resumption P β) : corec (bindStep k
 theorem pure_bind (a : α) (k : α → Resumption P β) : (pure a : Resumption P α).bind k = k a :=
   dest_injective (by simp [Resumption.bind, bindStep, Sum.map_map])
 
+theorem liftBind_bind_eq (a : P.A) (f : P.B a → Resumption P α) (k : α → Resumption P β) :
+    (liftBind a f).bind k = liftBind a fun i => (f i).bind k :=
+  dest_injective (by simp [Resumption.bind, bindStep, dest_liftBind]; rfl)
+
 @[simp]
-theorem query_bind (a : P.A) (f : P.B a → Resumption P α) (k : α → Resumption P β) :
-    (query a f).bind k = query a fun i => (f i).bind k :=
-  dest_injective (by simp [Resumption.bind, bindStep]; rfl)
+theorem liftBind_eq (a : P.A) (k : P.B a → Resumption P α) : liftBind a k = (lift a).bind k := by
+  simp [lift, liftBind_bind_eq]
+
+/-- Case analysis on whether a resumption returns a value or performs an operation. -/
+@[elab_as_elim, cases_eliminator]
+protected theorem cases {motive : Resumption P α → Prop} (pure : ∀ a, motive (pure a))
+    (lift_bind : ∀ a k, motive ((lift a).bind k)) (r : Resumption P α) : motive r := by
+  rw [← destEquiv.symm_apply_apply r]
+  rcases destEquiv r with a | x
+  · exact pure a
+  · cases x with | mk a k => exact (liftBind_eq a k ▸ lift_bind a k : motive (liftBind a k))
+
+@[simp]
+theorem dest_lift_bind (a : P.A) (k : P.B a → Resumption P α) :
+    dest ((lift a).bind (α := no_index (P.B a)) k) = .inr (.mk a k) := by
+  rw [← liftBind_eq, dest_liftBind]
+
+@[simp]
+theorem liftBind_bind (a : P.A) (k : P.B a → Resumption P α) (k' : α → Resumption P β) :
+    ((lift a).bind k).bind k' = (lift a).bind fun i => (k i).bind k' := by
+  simp only [← liftBind_eq, liftBind_bind_eq]
 
 @[simp]
 theorem bind_pure (r : Resumption P α) : r.bind pure = r :=
@@ -224,29 +240,33 @@ theorem bind_pure (r : Resumption P α) : r.bind pure = r :=
     subst h
     cases y with
     | pure a => simp only [pure_bind, dest_pure]; exact .pure a
-    | query a k => simp only [query_bind, dest_query]; exact .query a fun _ => rfl) rfl
+    | lift_bind a k => simp only [liftBind_bind, dest_lift_bind]; exact .liftBind a fun _ => rfl)
+    rfl
 
-theorem bind_assoc (r : Resumption P α) (k : α → Resumption P β) (k' : β → Resumption P γ) :
-    (r.bind k).bind k' = r.bind fun a => (k a).bind k' :=
+protected theorem bind_assoc (r : Resumption P α) (k : α → Resumption P β)
+    (k' : β → Resumption P γ) : (r.bind k).bind k' = r.bind fun a => (k a).bind k' :=
   bisim (fun x y => x = y ∨ ∃ r, x = (r.bind k).bind k' ∧ y = r.bind fun a => (k a).bind k')
     (fun x y h => by
       obtain rfl | ⟨r, rfl, rfl⟩ := h
       · exact StepRel.refl (fun _ => .inl rfl) _
       · cases r with
         | pure a => simp only [pure_bind]; exact StepRel.refl (fun _ => .inl rfl) _
-        | query a f =>
-          simp only [query_bind, dest_query]
-          exact .query a fun i => .inr ⟨f i, rfl, rfl⟩)
+        | lift_bind a f =>
+          simp only [liftBind_bind, dest_lift_bind]
+          exact .liftBind a fun i => .inr ⟨f i, rfl, rfl⟩)
     (.inr ⟨r, rfl, rfl⟩)
 
+@[simp]
+theorem bind_pure_comp (f : α → β) (r : Resumption P α) : r.bind (pure ∘ f) = r.map f := rfl
+
 @[simp]
 theorem map_pure (f : α → β) (a : α) : (pure a : Resumption P α).map f = pure (f a) :=
   pure_bind _ _
 
 @[simp]
-theorem map_query (f : α → β) (a : P.A) (k : P.B a → Resumption P α) :
-    (query a k).map f = query a fun i => (k i).map f :=
-  query_bind _ _ _
+theorem map_bind (f : β → γ) (r : Resumption P α) (k : α → Resumption P β) :
+    (r.bind k).map f = r.bind fun a => (k a).map f :=
+  Resumption.bind_assoc _ _ _
 
 section Monad
 
@@ -267,18 +287,13 @@ theorem map_eq_map : (Resumption.map : (α → β) → Resumption P α → _) =
 instance : LawfulMonad (Resumption P) := LawfulMonad.mk'
   (id_map := bind_pure)
   (pure_bind := pure_bind)
-  (bind_assoc := bind_assoc)
-  (bind_pure_comp := fun _ _ => rfl)
-
-@[simp]
-theorem query_bind' (a : P.A) (f : P.B a → Resumption P α) (k : α → Resumption P β) :
-    query a f >>= k = query a fun i => f i >>= k :=
-  query_bind a f k
+  (bind_assoc := Resumption.bind_assoc)
+  (bind_pure_comp := bind_pure_comp)
 
 @[simp]
-theorem map_query' (f : α → β) (a : P.A) (k : P.B a → Resumption P α) :
-    f <$> query a k = query a fun i => f <$> k i :=
-  map_query f a k
+theorem dest_lift_bind' (a : P.A) {α : Type uB} (k : P.B a → Resumption P α) :
+    dest (Bind.bind (α := no_index (P.B a)) (lift a) k) = .inr (.mk a k) :=
+  dest_lift_bind a k
 
 end Monad
 
@@ -298,12 +313,12 @@ theorem toResumption_pure (a : α) : toResumption (pure a : P.FreeM α) = pure a
   Resumption.dest_injective (by rw [toResumption, toW_pure, W.toM_mk]; rfl)
 
 theorem toResumption_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) :
-    toResumption ((lift a).bind cont) = .query a fun b => toResumption (cont b) :=
+    toResumption ((lift a).bind cont) = (Resumption.lift a).bind fun b => toResumption (cont b) :=
   Resumption.dest_injective (by simp [toResumption]; rfl)
 
 @[simp]
 theorem toResumption_lift (a : P.A) :
-    toResumption (α := no_index (P.B a)) (lift a) = .query a pure := by
+    toResumption (α := no_index (P.B a)) (lift a) = Resumption.lift a := by
   simpa using toResumption_lift_bind a (pure : P.B a → P.FreeM (P.B a))
 
 @[simp]
diff --git a/CslibTests/Resumption.lean b/CslibTests/Resumption.lean
index 52cb4ca5e..471db752f 100644
--- a/CslibTests/Resumption.lean
+++ b/CslibTests/Resumption.lean
@@ -18,9 +18,11 @@ private def flips : (y^ Bool).FreeM Bool := do
   pure (b && !c)
 
 -- Embedding a `do` program, which uses `>>=` and `<$>` rather than the universe-polymorphic
--- `bind` and `map`, normalizes to explicit queries.
-example : flips.toResumption =
-    Resumption.query () fun b => Resumption.query () fun c => pure (b && !c) := by
+-- `bind` and `map`, gives the same program over resumptions.
+example : flips.toResumption = (do
+    let b ← Resumption.lift ()
+    let c ← Resumption.lift ()
+    pure (b && !c)) := by
   simp [flips]
 
 end CslibTests.Resumption

From 316d26113c4eab0acf1d3888a3d63340f387b968 Mon Sep 17 00:00:00 2001
From: Devon Tuma <dtumad@gmail.com>
Date: Mon, 5 Oct 2026 18:54:47 -0500
Subject: [PATCH 5/5] feat(PFunctor): relate M-types and never-returning
 resumptions

Add `M.toResumption`, `Resumption.toMOfIsEmpty` and `equivMOfIsEmpty`,
mirroring the W-type embedding of free programs, and show that embedding
W-trees commutes with these maps. Describe the four tree types and the maps
between them in the module documentation.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Cslib/Foundations/Data/PFunctor/M.lean        |   9 ++
 .../Foundations/Data/PFunctor/Resumption.lean | 100 +++++++++++++++---
 2 files changed, 96 insertions(+), 13 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/M.lean b/Cslib/Foundations/Data/PFunctor/M.lean
index 9cb60fd92..8c463b816 100644
--- a/Cslib/Foundations/Data/PFunctor/M.lean
+++ b/Cslib/Foundations/Data/PFunctor/M.lean
@@ -41,6 +41,15 @@ theorem M.dest_injective : Function.Injective (M.dest (F := P)) := M.destEquiv.i
 @[simp]
 theorem M.dest_inj {x y : P.M} : M.dest x = M.dest y ↔ x = y := M.dest_injective.eq_iff
 
+@[simp]
+theorem M.corec_dest : M.corec (M.dest (F := P)) = id :=
+  (M.corec_unique _ _ fun _ => (P.id_map _).symm).symm
+
+/-- Corecursion is natural in maps of states that commute with the step functions. -/
+theorem M.corec_comp {X Y : Type*} (g : X → P X) (h : Y → P Y) (f : X → Y)
+    (hf : ∀ x, h (f x) = P.map f (g x)) : M.corec h ∘ f = M.corec g :=
+  M.corec_unique g _ fun x => by simp [M.dest_corec, hf]
+
 /-- The canonical map from the initial algebra into the final coalgebra, regarding a well-founded
 tree as a possibly infinite one. -/
 def W.toM : P.W → P.M :=
diff --git a/Cslib/Foundations/Data/PFunctor/Resumption.lean b/Cslib/Foundations/Data/PFunctor/Resumption.lean
index 358648f40..91ec7b273 100644
--- a/Cslib/Foundations/Data/PFunctor/Resumption.lean
+++ b/Cslib/Foundations/Data/PFunctor/Resumption.lean
@@ -14,19 +14,28 @@ public import Cslib.Foundations.Data.PFunctor.M
 
 A resumption `r : PFunctor.Resumption P α` is a possibly non-terminating program that either
 returns a value of `α` or performs an operation `a : P.A` and continues with a response
-`b : P.B a`. It is the M-type of the polynomial `C α + P`, i.e. the final coalgebra of
-`X ↦ α ⊕ P X`. The initial algebra of the same functor is the free monad `P.FreeM α`, which is the
-W-type of `C α + P` (`PFunctor.FreeM.equivW`).
-
-`PFunctor.FreeM.toResumption` is an injective monad morphism whose image is exactly the
-well-founded resumptions (`PFunctor.FreeM.equivWellFounded`), so resumptions extend free programs
-by infinite runs. Over the indeterminate `y`, with a single operation and a unit response,
-resumptions form Capretta's delay monad [Capretta2005]. They give semantics to loops whose
-termination is not structural, such as rejection sampling or the execution of a machine.
-
-This is the resumption monad of [PirogGibbons2014], the identity-monad case of the coalgebraic
-resumptions of [GoncharovMiliusRauch2016]. Unlike the cofree comonad, whose one-step view
-`α × P X` labels every node, a resumption returns a value only at a leaf.
+`b : P.B a`. It completes the polynomial tree types: `P.W` and `P.M` are the initial algebra and
+final coalgebra of `P`, while `P.FreeM α` and `Resumption P α` are those of `X ↦ α ⊕ P X`, that
+is, the W-type and M-type of `C α + P` (`PFunctor.FreeM.equivW`).
+
+The representations are related by
+```
+P.W        ──── W.toM ────▶  P.M
+ │ W.toFreeM                  │ M.toResumption
+ ▼                            ▼
+P.FreeM α  ── toResumption ─▶ Resumption P α
+```
+which commutes (`PFunctor.FreeM.toResumption_toFreeM`). The horizontal maps are injective, with
+image the well-founded trees (`W.equivM`, `FreeM.equivWellFounded`), and `FreeM.toResumption` is a
+monad morphism. The vertical maps are equivalences when `α` is empty (`FreeM.equivWOfIsEmpty`,
+`Resumption.equivMOfIsEmpty`).
+
+Resumptions extend free programs by infinite runs. Over the indeterminate `y`, with a single
+operation and a unit response, they form Capretta's delay monad [Capretta2005], and they give
+semantics to loops whose termination is not structural, such as rejection sampling or the
+execution of a machine. This is the resumption monad of [PirogGibbons2014], the identity-monad
+case of the coalgebraic resumptions of [GoncharovMiliusRauch2016]. Unlike the cofree comonad,
+whose one-step view `α × P X` labels every node, a resumption returns a value only at a leaf.
 
 ## Main definitions
 
@@ -37,6 +46,7 @@ resumptions of [GoncharovMiliusRauch2016]. Unlike the cofree comonad, whose one-
 - `PFunctor.Resumption.bisim`: coinduction through the relation lifting `StepRel`.
 - `PFunctor.Resumption.bind`: sequencing, giving a lawful monad.
 - `PFunctor.FreeM.toResumption`: the embedding of free programs.
+- `PFunctor.Resumption.equivMOfIsEmpty`: resumptions with no return value are M-trees.
 
 ## References
 
@@ -368,4 +378,68 @@ theorem equivWellFounded_apply (x : P.FreeM α) :
 
 end FreeM
 
+/-! ### Resumptions that never return -/
+
+section IsEmpty
+
+variable {P : PFunctor.{uA, uB}} {α : Type u}
+
+/-- Regard an M-tree as a resumption that never returns. -/
+def M.toResumption : P.M → Resumption P α :=
+  Resumption.corec fun t => .inr (M.dest t)
+
+@[simp]
+theorem M.toResumption_mk (a : P.A) (f : P.B a → P.M) :
+    (M.mk (.mk a f)).toResumption (α := α) =
+      (Resumption.lift a).bind fun i => (f i).toResumption :=
+  Resumption.dest_injective (by simp [M.toResumption]; rfl)
+
+/-- Regard a resumption that cannot return as an M-tree. -/
+def Resumption.toMOfIsEmpty [IsEmpty α] : Resumption P α → P.M :=
+  M.corec fun r => (Resumption.dest r).elim isEmptyElim id
+
+@[simp]
+theorem Resumption.toMOfIsEmpty_lift_bind [IsEmpty α] (a : P.A) (k : P.B a → Resumption P α) :
+    toMOfIsEmpty ((lift a).bind (α := no_index (P.B a)) k) =
+      M.mk (.mk a fun i => toMOfIsEmpty (k i)) :=
+  M.dest_injective (by simp [toMOfIsEmpty, M.dest_corec]; rfl)
+
+@[simp]
+theorem Resumption.toMOfIsEmpty_lift_bind' {α : Type uB} [IsEmpty α] (a : P.A)
+    (k : P.B a → Resumption P α) :
+    toMOfIsEmpty (Bind.bind (α := no_index (P.B a)) (lift a) k) =
+      M.mk (.mk a fun i => toMOfIsEmpty (k i)) :=
+  toMOfIsEmpty_lift_bind a k
+
+@[simp]
+theorem Resumption.toMOfIsEmpty_toResumption [IsEmpty α] (t : P.M) :
+    toMOfIsEmpty (t.toResumption (α := α)) = t :=
+  congrFun ((M.corec_comp M.dest _ M.toResumption fun _ => by simp [M.toResumption]).trans
+    M.corec_dest) t
+
+@[simp]
+theorem M.toResumption_toMOfIsEmpty [IsEmpty α] (r : Resumption P α) :
+    (Resumption.toMOfIsEmpty r).toResumption = r :=
+  congrFun ((Resumption.corec_comp Resumption.dest _ Resumption.toMOfIsEmpty fun r => by
+    cases r with
+    | pure a => exact isEmptyElim a
+    | lift_bind a k => simp [Function.comp_def]).trans Resumption.corec_dest) r
+
+/-- With no possible return value, resumptions are exactly the M-trees. -/
+@[simps]
+def Resumption.equivMOfIsEmpty [IsEmpty α] : Resumption P α ≃ P.M where
+  toFun := toMOfIsEmpty
+  invFun := M.toResumption
+  left_inv := M.toResumption_toMOfIsEmpty
+  right_inv := toMOfIsEmpty_toResumption
+
+/-- Embedding W-trees is compatible with the never-returning embeddings into free programs and
+resumptions. -/
+theorem FreeM.toResumption_toFreeM (w : P.W) :
+    (W.toFreeM w : P.FreeM α).toResumption = M.toResumption w.toM := by
+  induction w with
+  | mk a f ih => simp [ih]
+
+end IsEmpty
+
 end PFunctor