diff --git a/Cslib.lean b/Cslib.lean
index 8cfe47e010..2b04deb7fc 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -83,6 +83,8 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Control.Monad.IsMonadHom
+public import Cslib.Foundations.Control.Monad.IsMonadHom.List
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 44a703f0bc..2a1384cdc4 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -40,18 +40,14 @@ open List in
 @[simp, grind =]
 theorem ret_mergeM {T} [AddMonoid T] (xs ys : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeM xs ys le⟫ = List.merge xs ys (fun x y => ⟪le x y⟫) := by
-  fun_induction merge with grind [mergeM, nil_merge, merge_right, cons_merge_cons]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeM xs ys le
 
 open List in
 /-- `TimeM.ret` passes through `List.mergeSortM` into the comparator. -/
 @[simp]
 theorem ret_mergeSortM {T} [AddMonoid T] (xs : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeSortM xs le⟫ = List.mergeSort xs (fun x y => ⟪le x y⟫) := by
-  fun_induction List.mergeSortM with
-  | case1 | case2 => simp
-  | case3 a b xs le iha ihb =>
-    simp only [ret_bind, ret_mergeM, mergeSort]
-    rw [iha, ihb]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeSortM xs le
 
 variable [LinearOrder α]
 
diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index 8c571cf86a..33a0e9ce3b 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Eric Wieser
 module
 
 public import Mathlib.Data.List.Sort
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
 import Cslib.Init
 
@@ -18,18 +19,20 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m] (r : α → α → m Bool)
+variable {m n} [Monad m] [Monad n] (r : α → α → m Bool)
 
 /-- A monadic version of `List.orderedInsert`. -/
 def orderedInsertM (a : α) : List α → m (List α)
   | [] => return [a]
   | b :: l => do if ← r a b then return a :: b :: l else return b :: (← orderedInsertM a l)
 
-@[simp] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
+@[simp, grind =] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
   rfl
-@[simp] theorem orderedInsertM_cons (a b : α) (l : List α) :
+@[simp, grind =] theorem orderedInsertM_cons (a b : α) (l : List α) :
     orderedInsertM r a (b :: l) = do
       if ← r a b then return a :: b :: l else return b :: (← orderedInsertM r a l) := by
   rfl
@@ -45,6 +48,12 @@ theorem idRun_orderedInsertM (r : α → α → Id Bool) (a : α) (xs : List α)
     Id.run (orderedInsertM r a xs) = orderedInsert (fun x y => Id.run <| r x y) a xs :=
   orderedInsertM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_orderedInsertM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (a : α) (xs : List α) :
+    f (orderedInsertM r a xs) = orderedInsertM (fun x y => f (r x y)) a xs := by
+  fun_induction orderedInsertM r a xs with grind
+
 /-- A monadic version of `List.insertionSort`. -/
 def insertionSortM : List α → m (List α)
   | [] => return []
@@ -66,4 +75,10 @@ theorem idRun_insertionSortM (xs : List α) (r : α → α → Id Bool) :
     Id.run (insertionSortM r xs) = insertionSort (fun x y => Id.run <| r x y) xs :=
   insertionSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listInsertionSortM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (xs : List α) :
+    f (insertionSortM r xs) = insertionSortM (fun x y => f (r x y)) xs := by
+  fun_induction insertionSortM r xs with simp [hf.map_pure, hf.map_bind, hf.map_orderedInsertM, *]
+
 end List
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index a1f4c68d72..e64c6523b4 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -5,8 +5,9 @@ Authors: Kim Morrison, Eric Wieser
 -/
 module
 
-import all Init.Data.List.Sort.Basic
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
+import all Init.Data.List.Sort.Basic
 import Cslib.Init
 
 /-!
@@ -18,9 +19,11 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m]
+variable {m n} [Monad m] [Monad n]
 
 /-- A monadic version of `List.merge` -/
 def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
@@ -33,9 +36,11 @@ def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
     else
       return y :: (← mergeM (x :: xs) ys le)
 
-@[simp] theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
+@[simp, grind =]
+theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
   simp [mergeM]
-@[simp] theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
+@[simp, grind =]
+theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
   induction xs with
   | nil => simp
   | cons x xs ih => simp [mergeM]
@@ -57,6 +62,14 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
     Id.run (mergeM xs ys le) = merge xs ys (fun x y => Id.run <| le x y) :=
   mergeM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (xs ys : List α) (le : α → α → m Bool) :
+    f (mergeM xs ys le) = mergeM xs ys (fun x y => f (le x y)) := by
+  fun_induction mergeM xs ys le with
+  | case1 | case2 => grind
+  | case3 x xs y ys ihx ihy => simp [hf.map_bind, hf.map_pure, apply_ite f, ihx, ihy]
+
 /-- A monadic version of `List.mergeSortM` -/
 def mergeSortM (xs : List α) (le : α → α → m Bool) : m (List α) :=
   match xs with
@@ -88,4 +101,12 @@ theorem idRun_mergeSortM (xs : List α) (le : α → α → Id Bool) :
     Id.run (mergeSortM xs le) = mergeSort xs (fun x y => Id.run <| le x y) :=
   mergeSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeSortM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (xs : List α) (le : α → α → m Bool) :
+    f (mergeSortM xs le) = mergeSortM xs (fun x y => f (le x y)) := by
+  fun_induction mergeSortM xs le with
+  | case1 | case2 => simp [hf.map_pure]
+  | case3 a b xs le ih1 ih2 => simp only [mergeSortM, hf.map_bind, ih1, ih2, hf.map_listMergeM, le]
+
 end List
diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean
index 389d6945b0..1cf75a4af4 100644
--- a/Cslib/Algorithms/Lean/TimeM.lean
+++ b/Cslib/Algorithms/Lean/TimeM.lean
@@ -7,6 +7,7 @@ Authors: Sorrachai Yingchareonthawornhcai, Eric Wieser
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Mathlib.Algebra.Group.Defs
 
 /-!
@@ -97,6 +98,8 @@ instance [AddZero T] : Monad (TimeM T) where
 @[simp, grind =] theorem ret_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) :
     (m >>= f).ret = (f m.ret).ret := rfl
 @[simp, grind =] theorem ret_map {α β} (f : α → β) (x : TimeM T α) : (f <$> x).ret = f x.ret := rfl
+@[simp, grind =] theorem ret_mapConst {α β} (a : α) (x : TimeM T β) :
+    (Functor.mapConst a x).ret = a := rfl
 @[simp] theorem ret_seqRight {α} (x : TimeM T α) (y : Unit → TimeM T β) [Add T] :
     (SeqRight.seqRight x y).ret = (y ()).ret := rfl
 @[simp] theorem ret_seqLeft {α} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) :
@@ -104,6 +107,15 @@ instance [AddZero T] : Monad (TimeM T) where
 @[simp] theorem ret_seq {α β} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) :
     (Seq.seq f x).ret = f.ret (x ()).ret := rfl
 
+theorem isMonadHom_pure_ret [AddZero T] : Cslib.IsMonadHom (TimeM T) Id (fun x => pure x.ret) where
+  map_map _ _ := Id.ext <| ret_map _ _
+  map_mapConst _ __ := Id.ext <| ret_mapConst _ _
+  map_pure _ := Id.ext <| ret_pure _
+  map_seq _ _ := Id.ext <| ret_seq _ _
+  map_seqLeft _ _ := Id.ext <| ret_seqLeft _ _
+  map_seqRight _ _ := Id.ext <| ret_seqRight _ _
+  map_bind _ _ := Id.ext <| ret_bind _ _
+
 @[simp, grind =] theorem time_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) :
     (m >>= f).time = m.time + (f m.ret).time := rfl
 @[simp, grind =] theorem time_pure {α} [Zero T] (a : α) : (pure a : TimeM T α).time = 0 := rfl
diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 09d550b8bc..74dea4913c 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -7,6 +7,7 @@ Authors: Tanner Duve, Eric Wieser
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
 /-!
 # Free Monad
@@ -243,29 +244,44 @@ lemma liftM_bind [LawfulMonad m]
   | pure a => simp only [liftM_pure, LawfulMonad.pure_bind]
   | lift_bind op cont ih => simp [← ih]
 
+/-- A morphism of monads moves inside `FreeM.liftM`. -/
+theorem _root_.Cslib.IsMonadHom.map_freeMLiftM [Monad n]
+    {f : ∀ {α}, m α → n α} (hf : IsMonadHom m n f)
+    (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) :
+    f (x.liftM interp) = x.liftM (fun op => f (interp op)) := by
+  induction x with
+  | pure a => exact hf.map_pure a
+  | lift_bind op cont ih =>
+    simp only [bind_eq_bind, liftM_lift_bind, hf.map_bind, ih]
+
+/-- `FreeM.liftM interp` is a morphism of monads. -/
+theorem isMonadHom_liftM [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) :
+    IsMonadHom (FreeM F) m (FreeM.liftM interp) :=
+  IsMonadHom.mk' (liftM_pure interp) (liftM_bind interp)
+
 @[simp]
 lemma liftM_map [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) :
-    (f <$> x).liftM interp = f <$> x.liftM interp := by
-  simp_rw [← LawfulMonad.bind_pure_comp, liftM_bind, liftM_pure]
+    (f <$> x).liftM interp = f <$> x.liftM interp :=
+  isMonadHom_liftM interp |>.map_map _ _
 
 @[simp]
 lemma liftM_seq [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F (α → β)) (y : FreeM F α) :
-    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp := by
-  simp [seq_eq_bind_map]
+    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seq _ _
 
 @[simp]
 lemma liftM_seqLeft [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) :
-    (x <* y).liftM interp = x.liftM interp <* y.liftM interp := by
-  simp [seqLeft_eq_bind]
+    (x <* y).liftM interp = x.liftM interp <* y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqLeft _ _
 
 @[simp]
 lemma liftM_seqRight [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) :
-    (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by
-  simp [seqRight_eq_bind]
+    (x *> y).liftM interp = x.liftM interp *> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqRight _ _
 
 /--
 A predicate stating that `interp : FreeM F α → m α` is an interpreter for the effect
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
new file mode 100644
index 0000000000..a515d1a408
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -0,0 +1,318 @@
+/-
+Copyright (c) 2026 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Cslib.Init
+
+public import Batteries.Control.AlternativeMonad
+public import Std.Do.WP.Monad
+
+/-!
+# (unbundled) morphisms of monads
+
+This file defines predicates on functions `f : ∀ {α}, m α → n α` that preserve functor, applicative,
+monadic, and alternative structure (`IsFunctorHom`, `IsApplicativeHom`, `IsMonadHom`,
+`IsAlternativeHom`, `IsAlternativeMonadHom`).
+
+Rather than assuming lawfulness, they explicitly require compatibility with every operator
+defined by the corresponding typeclasses, with helper constructors that dismiss the derived
+operators when the structures are lawful.
+-/
+
+public section
+
+namespace Cslib
+
+/-! ### Functor Homomorphisms -/
+
+/--
+A function `f` is a morphism of functors if it preserves `<$>` and `Functor.mapConst`.
+-/
+structure IsFunctorHom (m n) [Functor m] [Functor n] (f : ∀ {α}, m α → n α) : Prop where
+  map_map {α β} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
+  map_mapConst {α β} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
+
+namespace IsFunctorHom
+variable {m n p : Type _ → Type _} [Functor m] [Functor n] [Functor p]
+
+attribute [grind .] map_map map_mapConst
+
+private theorem map_mapConst_of_map_map
+    [LawfulFunctor m] [LawfulFunctor n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x) :
+    ∀ {α β} (a : α) (x : m β), f (Functor.mapConst a x) = Functor.mapConst a (f x) := by
+  intros α β a x
+  simp [LawfulFunctor.map_const, map_map]
+
+/-- Construct an `IsFunctorHom` for lawful functors from `map_map`. -/
+theorem mk' [LawfulFunctor m] [LawfulFunctor n] {f : ∀ {α}, m α → n α}
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x) :
+    IsFunctorHom m n f where
+  map_map := map_map
+  map_mapConst := map_mapConst_of_map_map f map_map
+
+variable (m) in
+protected theorem id : IsFunctorHom m m id where
+  map_map _ _ := rfl
+  map_mapConst _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsFunctorHom n p f) (hg : IsFunctorHom m n g) :
+    IsFunctorHom m p (f ∘ g) where
+  map_map _ _ := by simp [hf.map_map, hg.map_map]
+  map_mapConst _ _ := by simp [hf.map_mapConst, hg.map_mapConst]
+
+end IsFunctorHom
+
+
+/-! ### Applicative Homomorphisms -/
+
+/--
+A function `f` is a morphism of applicatives if it preserves `pure`, `<$>`, `<*>`, `<*`, and `*>`.
+-/
+structure IsApplicativeHom (m n) [Applicative m] [Applicative n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsFunctorHom m n f where
+  map_pure {α} (a : α) : f (pure a) = pure a
+  map_seq {α β} (x : m (α → β)) (y : Unit → m α) :
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)
+  map_seqLeft {α β} (x : m α) (y : Unit → m β) :
+      f (SeqLeft.seqLeft x y) = SeqLeft.seqLeft (f x) (f <| y ·)
+  map_seqRight {α β} (x : m α) (y : Unit → m β) :
+      f (SeqRight.seqRight x y) = SeqRight.seqRight (f x) (f <| y ·)
+
+
+namespace IsApplicativeHom
+variable {m n p : Type _ → Type _} [Applicative m] [Applicative n] [Applicative p]
+
+attribute [grind .] map_pure map_seq map_seqLeft map_seqRight
+attribute [grind →] toIsFunctorHom
+
+private theorem map_map_of_map_pure_map_seq
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x := by
+  intros α β g x
+  rw [← pure_seq, ← pure_seq]
+  change f (Seq.seq (pure g) (fun _ => x)) = Seq.seq (pure g) (fun _ => f x)
+  rw [map_seq, map_pure]
+
+private theorem map_seqLeft_of_map_seq_map_map
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (x : m α) (y : Unit → m β),
+      f (SeqLeft.seqLeft x y) = SeqLeft.seqLeft (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seqLeft_eq, map_seq, map_map]
+
+private theorem map_seqRight_of_map_seq_map_map
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (x : m α) (y : Unit → m β),
+      f (SeqRight.seqRight x y) = SeqRight.seqRight (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seqRight_eq, map_seq, map_map]
+
+/-- Construct an `IsApplicativeHom` for lawful applicatives from `map_pure` and `map_seq`. -/
+theorem mk' [LawfulApplicative m] [LawfulApplicative n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    IsApplicativeHom m n f where
+  map_pure
+  toIsFunctorHom := .mk' (map_map_of_map_pure_map_seq f map_pure map_seq)
+  map_seq
+  map_seqLeft := map_seqLeft_of_map_seq_map_map f
+    (map_map_of_map_pure_map_seq f map_pure map_seq) map_seq
+  map_seqRight := map_seqRight_of_map_seq_map_map f
+    (map_map_of_map_pure_map_seq f map_pure map_seq) map_seq
+
+variable (m) in
+protected theorem id : IsApplicativeHom m m id where
+  map_pure _ := rfl
+  toIsFunctorHom := IsFunctorHom.id m
+  map_seq _ _ := rfl
+  map_seqLeft _ _ := rfl
+  map_seqRight _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsApplicativeHom n p f) (hg : IsApplicativeHom m n g) :
+    IsApplicativeHom m p (f ∘ g) where
+  map_pure _ := by simp [hf.map_pure, hg.map_pure]
+  toIsFunctorHom := hf.toIsFunctorHom.comp hg.toIsFunctorHom
+  map_seq _ _ := by simp [hf.map_seq, hg.map_seq]
+  map_seqLeft _ _ := by simp [hf.map_seqLeft, hg.map_seqLeft]
+  map_seqRight _ _ := by simp [hf.map_seqRight, hg.map_seqRight]
+
+end IsApplicativeHom
+
+
+/-! ### Monad Homomorphisms -/
+
+/--
+A function `f` is a morphism of monads if it preserves `pure`, `>>=`, `<$>`, `<*>`, `<*`, and `*>`.
+-/
+structure IsMonadHom (m n) [Monad m] [Monad n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsApplicativeHom m n f where
+  map_bind {α β} (x : m α) (y : α → m β) : f (x >>= y) = f x >>= (f <| y ·)
+
+namespace IsMonadHom
+variable {m n p : Type _ → Type _} [Monad m] [Monad n] [Monad p]
+
+attribute [grind .] map_bind
+attribute [grind →] toIsApplicativeHom
+
+private theorem map_map_of_map_pure_map_bind
+    [LawfulMonad m] [LawfulMonad n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x := by
+  intros α β g x
+  simp [← bind_pure_comp, map_bind, map_pure]
+
+private theorem map_seq_of_map_pure_map_bind
+    [LawfulMonad m] [LawfulMonad n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seq_eq_bind_map, map_map_of_map_pure_map_bind f map_pure, map_bind]
+
+/-- Construct an `IsMonadHom` for lawful monads from `map_pure` and `map_bind`. -/
+theorem mk' [LawfulMonad m] [LawfulMonad n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    IsMonadHom m n f where
+  map_bind
+  toIsApplicativeHom := .mk' map_pure (map_seq_of_map_pure_map_bind f map_pure map_bind)
+
+variable (m) in
+protected theorem id : IsMonadHom m m id where
+  toIsApplicativeHom := IsApplicativeHom.id m
+  map_bind _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsMonadHom n p f) (hg : IsMonadHom m n g) :
+    IsMonadHom m p (f ∘ g) where
+  toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
+  map_bind _ _ := by simp [hf.map_bind, hg.map_bind]
+
+protected theorem monadLift [LawfulMonad m] [LawfulMonad n]
+    [MonadLift m n] [LawfulMonadLift m n] :
+    IsMonadHom m n MonadLift.monadLift :=
+  .mk' LawfulMonadLift.monadLift_pure LawfulMonadLift.monadLift_bind
+
+protected theorem monadLiftT [LawfulMonad m] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] :
+    IsMonadHom m n monadLift :=
+  .mk' LawfulMonadLiftT.monadLift_pure LawfulMonadLiftT.monadLift_bind
+
+end IsMonadHom
+
+/-! ### Alternative Homomorphisms -/
+
+/--
+A function `f` is a morphism of alternatives if it preserves `pure`, `<$>`, `<*>`, `<*`, `*>`,
+`failure`, and `orElse`.
+-/
+structure IsAlternativeHom (m n) [Alternative m] [Alternative n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsApplicativeHom m n f where
+  map_failure {α} : f (Alternative.failure : m α) = Alternative.failure
+  map_orElse {α} (x : m α) (y : Unit → m α) :
+    f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)
+
+namespace IsAlternativeHom
+variable {m n p : Type _ → Type _} [Alternative m] [Alternative n] [Alternative p]
+
+attribute [grind .] map_failure map_orElse
+attribute [grind →] toIsApplicativeHom
+
+/-- Construct an `IsAlternativeHom` for lawful applicatives from `map_pure`, `map_seq`,
+`map_failure`, and `map_orElse`. -/
+theorem mk' [LawfulApplicative m] [LawfulApplicative n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·))
+    (map_failure : ∀ {α}, f (Alternative.failure : m α) = Alternative.failure)
+    (map_orElse : ∀ {α} (x : m α) (y : Unit → m α),
+      f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)) :
+    IsAlternativeHom m n f where
+  toIsApplicativeHom := .mk' map_pure map_seq
+  map_failure
+  map_orElse
+
+variable (m) in
+protected theorem id : IsAlternativeHom m m id where
+  toIsApplicativeHom := IsApplicativeHom.id m
+  map_failure := rfl
+  map_orElse _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsAlternativeHom n p f) (hg : IsAlternativeHom m n g) :
+    IsAlternativeHom m p (f ∘ g) where
+  toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
+  map_failure := by simp [hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [hf.map_orElse, hg.map_orElse]
+
+end IsAlternativeHom
+
+/-! ### Alternative Monad Homomorphisms -/
+
+/--
+A function `f` is a morphism of alternative monads if it preserves monadic and alternative
+structure.
+-/
+structure IsAlternativeMonadHom (m n) [AlternativeMonad m] [AlternativeMonad n]
+    (f : ∀ {α}, m α → n α) : Prop
+    extends IsMonadHom m n f, IsAlternativeHom m n f
+
+namespace IsAlternativeMonadHom
+variable {m n p : Type _ → Type _} [AlternativeMonad m] [AlternativeMonad n] [AlternativeMonad p]
+
+attribute [grind →] toIsMonadHom toIsAlternativeHom
+
+/-- Construct an `IsAlternativeMonadHom` for lawful monads from `map_pure`, `map_bind`,
+`map_failure`, and `map_orElse`. -/
+theorem mk' [LawfulMonad m] [LawfulMonad n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·))
+    (map_failure : ∀ {α}, f (Alternative.failure : m α) = Alternative.failure)
+    (map_orElse : ∀ {α} (x : m α) (y : Unit → m α),
+      f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)) :
+    IsAlternativeMonadHom m n f where
+  toIsMonadHom := .mk' map_pure map_bind
+  map_failure
+  map_orElse
+
+variable (m) in
+protected theorem id : IsAlternativeMonadHom m m id where
+  toIsMonadHom := IsMonadHom.id m
+  map_failure := rfl
+  map_orElse _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsAlternativeMonadHom n p f) (hg : IsAlternativeMonadHom m n g) :
+    IsAlternativeMonadHom m p (f ∘ g) where
+  toIsMonadHom := hf.toIsMonadHom.comp hg.toIsMonadHom
+  map_failure := by simp [hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [hf.map_orElse, hg.map_orElse]
+
+end IsAlternativeMonadHom
+
+open Std.Do WPMonad in
+theorem IsMonadHom.wp [Monad m] [WPMonad m ps] : IsMonadHom m (PredTrans ps) WP.wp :=
+  .mk' wp_pure wp_bind
+
+end Cslib
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
new file mode 100644
index 0000000000..44e3cc6583
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -0,0 +1,217 @@
+/-
+Copyright (c) 2026 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
+public import Mathlib.Data.List.Monad
+
+import all Init.Data.List.Control
+import Mathlib.Data.List.Basic
+
+/-!
+# List operations and monad morphisms
+
+This file proves that monadic operations on lists commute with monad homomorphisms
+(and applicative homomorphisms), and that `List.reverse` is a monad homomorphism on `List`.
+-/
+
+public section
+
+namespace Cslib
+
+universe u um un v
+variable {m : Type u → Type um} {n : Type u → Type un}
+
+/-! ### Preservation of list operations under applicative homomorphisms -/
+
+namespace IsApplicativeHom
+variable [Applicative m] [Applicative n]
+
+@[grind .]
+theorem map_listMapA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapA f) = l.mapA (F ∘ f) := by
+  induction l with grind [List.mapA]
+
+@[grind .]
+theorem map_listForA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
+    {α : Type v} (l : List α) (f : α → m PUnit) :
+    F (l.forA f) = l.forA (F ∘ f) := by
+  induction l with grind [List.forA]
+
+end IsApplicativeHom
+
+/-! ### Preservation of list operations under monad homomorphisms -/
+
+namespace IsMonadHom
+variable [Monad m] [Monad n]
+
+@[grind .]
+theorem map_listMapM'
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM' f) = l.mapM' (F ∘ f) := by
+  induction l with grind [List.mapM']
+
+@[grind .]
+theorem map_listMapMLoop
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) (acc : List β) :
+    F (List.mapM.loop f l acc) = List.mapM.loop (F ∘ f) l acc := by
+  induction l generalizing acc with
+  | nil => exact hf.map_pure _
+  | cons a l ih => simp only [List.mapM.loop, hf.map_bind, ih, Function.comp_def]
+
+@[grind .]
+theorem map_listMapM
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM f) = l.mapM (F ∘ f) := by
+  grind [List.mapM]
+
+@[grind .]
+theorem map_listForM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} (l : List α) (f : α → m PUnit) :
+    F (l.forM f) = l.forM (F ∘ f) := by
+  induction l with grind [List.forM]
+
+@[grind .]
+theorem map_listFoldlM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {s : Type u} {α : Type v} (f : s → α → m s) (init : s) (l : List α) :
+    F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := by
+  induction l generalizing init with grind [List.foldlM]
+
+@[grind .]
+theorem map_listFoldrM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {s : Type u} {α : Type v} (f : α → s → m s) (init : s) (l : List α) :
+    F (l.foldrM f init) = l.foldrM (fun a s => F (f a s)) init := by
+  simp only [List.foldrM]
+  exact hf.map_listFoldlM (fun s a => f a s) init l.reverse
+
+@[grind .]
+theorem map_listFindSomeM?
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} {β : Type u} (f : α → m (Option β)) (l : List α) :
+    F (l.findSomeM? f) = l.findSomeM? (F ∘ f) := by
+  induction l with grind
+
+@[grind .]
+theorem map_listFindM? {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l : List α) :
+    F (l.findM? p) = l.findM? (F ∘ p) := by
+  induction l with grind [List.findM?]
+
+@[grind .]
+theorem map_listAnyM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} (p : α → m Bool) (l : List α) :
+    F (l.anyM p) = l.anyM (F ∘ p) := by
+  induction l with grind [List.anyM]
+
+@[grind .]
+theorem map_listAllM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} (p : α → m Bool) (l : List α) :
+    F (l.allM p) = l.allM (F ∘ p) := by
+  induction l with grind [List.allM]
+
+@[grind .]
+theorem map_listFilterAuxM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l acc : List α) :
+    F (List.filterAuxM p l acc) = List.filterAuxM (F ∘ p) l acc := by
+  induction l generalizing acc with grind [List.filterAuxM]
+
+@[grind .]
+theorem map_listFilterM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l : List α) :
+    F (l.filterM p) = l.filterM (F ∘ p) := by
+  grind [List.filterM]
+
+end IsMonadHom
+
+/-! ### Preservation of list operations under alternative homomorphisms -/
+
+namespace IsAlternativeHom
+variable [Alternative m] [Alternative n]
+
+@[grind .]
+theorem map_listFirstM {F : ∀ {α}, m α → n α} (hf : IsAlternativeHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.firstM f) = l.firstM (F ∘ f) := by
+  induction l with grind [List.firstM]
+
+end IsAlternativeHom
+
+/-! ### Monad homomorphisms on the `List` monad -/
+
+@[grind .]
+theorem IsApplicativeHom.map_listSingleton
+    {F : ∀ {α}, List α → List α} (hf : IsApplicativeHom List List F) {α} (a : α) :
+    F ([a] : List α) = [a] := hf.map_pure _
+
+theorem IsMonadHom.map_listFlatMap
+    {F : ∀ {α}, List α → List α} (hf : IsMonadHom List List F) {α β} (l : List α) (g : α → List β) :
+    F (l.flatMap g) = (F l).flatMap (F <| g ·) := hf.map_bind _ _
+
+@[grind .]
+theorem IsFunctorHom.map_listNil {F : ∀ {α}, List α → List α} (hf : IsFunctorHom List List F) {α} :
+    F ([] : List α) = [] := by
+  simpa [Subsingleton.elim (F ([] : List PEmpty)) []]
+    using (hf.map_map PEmpty.elim []).symm
+
+protected theorem _root_.List.isMonadHom_reverse : IsMonadHom List List List.reverse :=
+  .mk' (fun _ => rfl) (fun _ _ => List.reverse_flatMap)
+
+section uniqueness
+
+/-- A property holds on all lists if it holds on the nil list, the singleton list,
+and concatenations thereof. -/
+private theorem List.nil_singleton_append_induction {α : Type*} {motive : List α → Prop}
+    (nil : motive []) (singleton : ∀ a, motive [a])
+    (append : ∀ xs ys, motive xs → motive ys → motive (xs ++ ys)) :
+    ∀ l, motive l
+  | [] => nil
+  | x :: xs => append [x] xs (singleton x) (nil_singleton_append_induction nil singleton append xs)
+
+/-- Universe-generic type with two elements. This is used only internally in a proof, and keeps
+things more concise than `ULift Bool`. -/
+private inductive Two : Type u | a | b
+
+private theorem eq_ab_or_ba : ∀ (l : List Two),
+    l.flatMap (fun | .a => [.a] | .b => []) = [Two.a] →
+    l.flatMap (fun | .a => [] | .b => [.b]) = [Two.b] →
+    l = [Two.a, Two.b] ∨ l = [Two.b, Two.a]
+  | [.a, .b], _, _ => .inl rfl
+  | [.b, .a], _, _ => .inr rfl
+
+/-- The only monad morphisms on lists are the identity and reversal. -/
+theorem isMonadHom_list_iff (f : ∀ {α : Type u}, List α → List α) :
+    IsMonadHom List List @f ↔ @f = (@id <| List ·) ∨ @f = @List.reverse := by
+  refine ⟨fun h => ?_, ?_⟩
+  · have h_append {α} (xs ys : List α) :
+        f (xs ++ ys) = (f [Two.a, Two.b]).flatMap (fun | .a => f xs | .b => f ys) := by
+      have : xs ++ ys = [Two.a, Two.b].flatMap (fun | .a => xs | .b => ys) := by
+        simp
+      rw [this, h.map_listFlatMap]
+      congr 1; funext x; cases x <;> rfl
+    refine (eq_ab_or_ba (f [Two.a, Two.b]) ?_ ?_).imp (fun hL => ?_) (fun hL => ?_)
+    · simpa [h.map_listNil, h.map_listSingleton] using (h_append [Two.a] []).symm
+    · simpa [h.map_listNil, h.map_listSingleton] using (h_append [] [Two.b]).symm
+    · funext α l
+      induction l using List.nil_singleton_append_induction with grind
+    · funext α l
+      induction l using List.nil_singleton_append_induction with grind
+  · rintro (rfl | rfl)
+    · exact .id _
+    · exact List.isMonadHom_reverse
+
+end uniqueness
+
+end Cslib
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index a29e974704..05cb6535d0 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -7,6 +7,7 @@ Authors: Quang Dao
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Mathlib.Data.PFunctor.Univariate.Basic
 
 /-!
@@ -321,6 +322,16 @@ theorem Interprets.iff (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α 
     Interprets handler eval ↔ eval = (·.liftM handler) :=
   ⟨(·.eq), fun h => h ▸ Interprets.liftM _⟩
 
+/-- A morphism of monads moves inside `FreeM.liftM`. -/
+theorem _root_.Cslib.IsMonadHom.map_pfunctorFreeMLiftM [Monad n]
+    {f : ∀ {α}, m α → n α} (hf : Cslib.IsMonadHom m n f) (interp : (a : P.A) → m (P.B a))
+    (x : P.FreeM α) :
+    f (x.liftM interp) = x.liftM (fun op => f (interp op)) := by
+  induction x with
+  | pure a => exact hf.map_pure a
+  | lift_bind op cont ih =>
+    simp only [bind_eq_bind, liftM_lift_bind, hf.map_bind, ih]
+
 variable [LawfulMonad m]
 
 @[simp]
@@ -336,28 +347,32 @@ lemma liftM_bind {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) :
     funext u
     exact h u
 
+/-- `FreeM.liftM interp` is a morphism of monads. -/
+theorem isMonadHom_liftM : Cslib.IsMonadHom P.FreeM m (FreeM.liftM interp) :=
+  .mk' (liftM_pure interp) (liftM_bind interp)
+
 @[simp]
-lemma liftM_map {α β : Type uB} (f : α → β) (x : P.FreeM α) :
-    (f <$> x).liftM interp = f <$> x.liftM interp := by
-  simp_rw [← LawfulMonad.bind_pure_comp, liftM_bind, liftM_pure]
+lemma liftM_map {α β : Type uB} (f : α → β) (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) :
+    (f <$> x).liftM interp = f <$> x.liftM interp :=
+  isMonadHom_liftM interp |>.map_map _ _
 
 @[simp]
 lemma liftM_seq {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM (α → β)) (y : P.FreeM α) :
-    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp := by
-  simp [seq_eq_bind_map]
+    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seq _ _
 
 @[simp]
 lemma liftM_seqLeft {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
-    (x <* y).liftM interp = x.liftM interp <* y.liftM interp := by
-  simp [seqLeft_eq_bind]
+    (x <* y).liftM interp = x.liftM interp <* y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqLeft _ _
 
 @[simp]
 lemma liftM_seqRight {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
-    (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by
-  simp [seqRight_eq_bind]
+    (x *> y).liftM interp = x.liftM interp *> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqRight _ _
 
 @[simp]
 lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (a : P.A) :