diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27be..267579dd6 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -69,6 +69,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/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 09d550b8b..74dea4913 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 000000000..90c79b4d8
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -0,0 +1,308 @@
+/-
+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 Mathlib.Logic.Function.Defs
+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]
+
+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 wp_isMonadHom [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 000000000..95fd4d100
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -0,0 +1,208 @@
+/-
+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 v w
+variable {m n : Type u → Type v}
+
+/-! ### 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 w} {β : 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 w} (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 w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM' f) = l.mapM' (F ∘ f) := by
+  induction l with grind [List.mapM']
+
+@[grind .]
+theorem map_listMapM [LawfulMonad m] [LawfulMonad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM f) = l.mapM (F ∘ f) := by
+  induction l with grind
+
+@[grind .]
+theorem map_listForM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} (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 w} (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 w} (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 w} {β : 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 w} (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 w} (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 w} {β : 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 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 {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 a29e97470..05cb6535d 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) :