Morphisms Between Monads

A morphism of monads is a family m α → n α, natural in α, preserving pure and bind. There are two useful presentations, and this file is deliberate about which one it owns.

Unbundled: Lean core

When the morphism is canonical for the pair (m, n) and should be found by instance search, it belongs to core's lifting hierarchy: MonadLift / MonadLiftT supply the map and LawfulMonadLift / LawfulMonadLiftT (Init/Control/Lawful/MonadLift/) supply exactly the two laws above. Core carries instances for the standard transformer stack and a liftM_* simp set, so nothing of that shape should be re-derived here.

Bundled: this file

When the morphism is data — chosen at the call site, passed around, composed, or mapped over — instance search is the wrong mechanism and a first-class arrow is needed. Core has no bundled form, so MonadHom (notation m →ᵐ n) is that arrow, with MonadHom.comp (∘ₘ), MonadHom.id, and StateT.mapHom for transporting one along a transformer. NatHom is the underlying natural transformation without the laws; PFunctor.FreeM.liftMHom' consumes it directly.

MonadHom.ofLift is the bridge: any lawful lift induces a bundled morphism. There is deliberately no converse instance — turning an arbitrary MonadHom into a MonadLift would make instance search pick between morphisms that are genuinely different maps.

Why there is no PureHom / BindHom hierarchy

Mathlib splits OneHom from MulHom (and ZeroHom from AddHom) because those component morphisms are useful independently, and because many richer morphism types share their laws through the corresponding HomClass hierarchy. The old sketches in this file proposed the analogous PureHom, BindHom, and MonadHomClass, but PolyFun, VCVio, and ArkLib have no consumer of either partial morphism. A PureHom would only preserve a pointing; a BindHom would only become meaningful after choosing laws for a non-unital semimonad. Neither abstraction exists in this stack.

The neighbouring upstream APIs make the same atomic choice. Lean v4.34's LawfulMonadLift(T) packages the pure and bind laws together, and mathlib's categorical MonadHom packages compatibility with both the unit and multiplication. Batteries adds orthogonal preservation laws, such as LawfulAlternativeLift, alongside a monad lift rather than splitting its two monad laws.

A family-aware analogue of FunLike may become worthwhile once multiple bundled morphism types need common lemmas. The previous (α : Type u) → FunLike F (m α) (n α) sketch did not provide one coherent function-like view of the whole polymorphic family, and there is only one such arrow type today. The decision is therefore to keep MonadHom atomic and not add speculative component structures or hom classes. A real pointed-functor, semimonad, or second bundled-morphism consumer should reopen that decision and arrive with the corresponding laws and generic tests.

The unused MonadEquiv module is omitted for the same reason. If a consumer needs monad equivalences, the minimal design is two inverse MonadHoms, not a parallel hierarchy of unused PureEquiv and BindEquiv structures.

Mathlib's CategoryTheory.MonadHom is a third presentation, at restricted universes and in the categorical idiom; the Type-level form here is what the free-monad and interaction layers actually consume.

structure NatHom (m : Type u → Type v) (n : Type u → Type w) : Type (max (max (u + 1) v) w)

A NatHom m n for two functors m and n is a map m α → n α for each possible type α. This is exactly an element of the category m ⟶ n, but that has more restricted universes

• toFun (α : Type u) : m α → n α

  The underlying family of maps m α → n α, one for each type α.

@[instance_reducible]

instance instCoeFunNatHomForallForall {m : Type u → Type v} {n : Type u → Type w} : CoeFun (NatHom m n) fun (_f : NatHom m n) => {α : Type u} → m α → n α

f mx notation for NatHom m n applied to an element of m α, with implicit α inferred.

structure MonadHom (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] extends NatHom m n : Type (max (max (u + 1) v) w)

A MonadHom m n bundles a monad map m ⟶ n (represented as a NatHom) with proofs that it respects the bind and pure operations in the underlying monad.

• toFun (α : Type u) : m α → n α
• toFun_pure' {α : Type u} (x : α) : self.toFun α (pure x) = pure x
• toFun_bind' {α β : Type u} (x : m α) (y : α → m β) : self.toFun β (x >>= y) = do let x ← self.toFun α x self.toFun β (y x)

theorem MonadHom.ext_iff {m : Type u → Type v} {inst✝ : Pure m} {inst✝¹ : Bind m} {n : Type u → Type w} {inst✝² : Pure n} {inst✝³ : Bind n} {x y : m →ᵐ n} : x = y ↔ x.toFun = y.toFun

theorem MonadHom.ext {m : Type u → Type v} {inst✝ : Pure m} {inst✝¹ : Bind m} {n : Type u → Type w} {inst✝² : Pure n} {inst✝³ : Bind n} {x y : m →ᵐ n} (toFun : x.toFun = y.toFun) : x = y

def «term_→ᵐ_» : Lean.TrailingParserDescr

A MonadHom m n bundles a monad map m ⟶ n (represented as a NatHom) with proofs that it respects the bind and pure operations in the underlying monad.

@[instance_reducible]

instance instCoeFunMonadHomForallForall {m : Type u → Type v} [Pure m] [Bind m] {n : Type u → Type w} [Pure n] [Bind n] : CoeFun (m →ᵐ n) fun (_f : m →ᵐ n) => {α : Type u} → m α → n α

F mx notation for m →ᵐ n applied to an element of m α, with implicit α inferred.

theorem MonadHom.ext' {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {F G : m →ᵐ n} (h : ∀ (α : Type u) (x : m α), (fun {α : Type u} (x : m α) => F.toFun α x) x = (fun {α : Type u} (x : m α) => G.toFun α x) x) : F = G

Extensionality for monad homomorphisms: two morphisms agreeing on every argument at every type are equal.

theorem MonadHom.ext'_iff {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {F G : m →ᵐ n} : F = G ↔ ∀ (α : Type u) (x : m α), (fun {α : Type u} (x : m α) => F.toFun α x) x = (fun {α : Type u} (x : m α) => G.toFun α x) x

theorem MonadHom.mmap_pure {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} (F : m →ᵐ n) (x : α) : (fun {α : Type u} (x : m α) => F.toFun α x) (pure x) = pure x

theorem MonadHom.mmap_bind {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} (F : m →ᵐ n) (mx : m α) (my : α → m β) : (fun {α : Type u} (x : m α) => F.toFun α x) (mx >>= my) = do let x ← (fun {α : Type u} (x : m α) => F.toFun α x) mx (fun {α : Type u} (x : m α) => F.toFun α x) (my x)

@[simp]

theorem MonadHom.mmap_map {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (g : α → β) : (fun {α : Type u} (x : m α) => F.toFun α x) (g <$> x) = g <$> (fun {α : Type u} (x : m α) => F.toFun α x) x

@[simp]

theorem MonadHom.mmap_seq {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m (α → β)) (y : m α) : (fun {α : Type u} (x : m α) => F.toFun α x) (x <*> y) = (fun {α : Type u} (x : m α) => F.toFun α x) x <*> (fun {α : Type u} (x : m α) => F.toFun α x) y

@[simp]

theorem MonadHom.mmap_seqLeft {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (y : m β) : (fun {α : Type u} (x : m α) => F.toFun α x) (x <* y) = (fun {α : Type u} (x : m α) => F.toFun α x) x <* (fun {α : Type u} (x : m α) => F.toFun α x) y

@[simp]

theorem MonadHom.mmap_seqRight {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (y : m β) : (fun {α : Type u} (x : m α) => F.toFun α x) (x *> y) = (fun {α : Type u} (x : m α) => F.toFun α x) x *> (fun {α : Type u} (x : m α) => F.toFun α x) y

@[simp]

theorem MonadHom.mmap_ite {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} (F : m →ᵐ n) (c : Prop) [Decidable c] (x y : m α) : (fun {α : Type u} (x : m α) => F.toFun α x) (if c then x else y) = if c then (fun {α : Type u} (x : m α) => F.toFun α x) x else (fun {α : Type u} (x : m α) => F.toFun α x) y

@[simp]

theorem MonadHom.mmap_dite {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} (F : m →ᵐ n) (c : Prop) [Decidable c] (x : c → m α) (y : ¬c → m α) : (fun {α : Type u} (x : m α) => F.toFun α x) (if h : c then x h else y h) = if h : c then (fun {α : Type u} (x : m α) => F.toFun α x) (x h) else (fun {α : Type u} (x : m α) => F.toFun α x) (y h)

@[simp]

theorem MonadHom.mmap_option_elim {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} {γ : Type x} (F : m →ᵐ n) (o : Option γ) (x : m α) (f : γ → m α) : (fun {α : Type u} (x : m α) => F.toFun α x) (o.elim x f) = o.elim ((fun {α : Type u} (x : m α) => F.toFun α x) x) fun (c : γ) => (fun {α : Type u} (x : m α) => F.toFun α x) (f c)

@[simp]

theorem MonadHom.mmap_sum_elim {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} {γ : Type x} {δ : Type y} (F : m →ᵐ n) (s : γ ⊕ δ) (f : γ → m α) (g : δ → m α) : (fun {α : Type u} (x : m α) => F.toFun α x) (Sum.elim f g s) = Sum.elim (fun (c : γ) => (fun {α : Type u} (x : m α) => F.toFun α x) (f c)) (fun (d : δ) => (fun {α : Type u} (x : m α) => F.toFun α x) (g d)) s

def MonadHom.ofLift (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : m →ᵐ n

Construct a MonadHom from a lawful monad lift.

@[simp]

theorem MonadHom.ofLift_apply {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] {α : Type u} (x : m α) : (fun {α : Type u} (x : m α) => (ofLift m n).toFun α x) x = liftM x

def MonadHom.id (m : Type u → Type v) [Monad m] : m →ᵐ m

The identity morphism between a monad and itself.

@[simp]

theorem MonadHom.id_apply {m : Type u → Type v} [Monad m] {α : Type u} (mx : m α) : (fun {α : Type u} (x : m α) => (id m).toFun α x) mx = mx

def MonadHom.comp {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {n' : Type u → Type x} [Monad n'] (G : n →ᵐ n') (F : m →ᵐ n) : m →ᵐ n'

Compose two MonadHoms together by applying them in sequence.

def MonadHom.«term_∘ₘ_» : Lean.TrailingParserDescr

Infix notation for composition of monad homomorphisms, G ∘ₘ F.

@[simp]

theorem MonadHom.comp_apply {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {n' : Type u → Type x} [Monad n'] {α : Type u} (G : n →ᵐ n') (F : m →ᵐ n) (x : m α) : (fun {α : Type u} (x : m α) => (G ∘ₘ F).toFun α x) x = (fun {α : Type u} (x : n α) => G.toFun α x) ((fun {α : Type u} (x : m α) => F.toFun α x) x)

@[simp]

theorem MonadHom.comp_id {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] (F : m →ᵐ n) : F ∘ₘ id m = F

@[simp]

theorem MonadHom.id_comp {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] (F : m →ᵐ n) : id n ∘ₘ F = F

theorem MonadHom.comp_assoc {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {n' : Type u → Type x} [Monad n'] {n'' : Type u → Type y} [Monad n''] (H : n' →ᵐ n'') (G : n →ᵐ n') (F : m →ᵐ n) : (H ∘ₘ G) ∘ₘ F = H ∘ₘ G ∘ₘ F

def MonadHom.pure (m : Type u_1 → Type u_2) [Monad m] [LawfulMonad m] : Id →ᵐ m

pure/return lawfully embed the Id monad into any lawful monad.

@[simp]

theorem MonadHom.pure_apply {α : Type u} (m : Type u → Type u_1) [Monad m] [LawfulMonad m] (x : Id α) : (fun {α : Type u} (x : Id α) => (MonadHom.pure m).toFun α x) x = pure x.run

def StateT.mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {σ : Type u} (φ : m →ᵐ n) : StateT σ m →ᵐ StateT σ n

StateT σ is functorial on monad morphisms: a monad morphism φ : m →ᵐ n lifts to a monad morphism StateT σ m →ᵐ StateT σ n, acting on the underlying state-run and threading the state unchanged. This transports the naturality of a fold (for example, FreeM.liftM_natural) through a stateful handler — the form a StateT-threaded semantic morphism (such as an evaluation-distribution map) needs.

@[simp]

theorem StateT.run_mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {σ α : Type u} (φ : m →ᵐ n) (x : StateT σ m α) (s : σ) : ((fun {α : Type u} (x : StateT σ m α) => (mapHom φ).toFun α x) x).run s = (fun {α : Type u} (x : m α) => φ.toFun α x) (x.run s)

@[simp]

theorem StateT.mapHom_id {m : Type u → Type v} [Monad m] {σ : Type u} : mapHom (MonadHom.id m) = MonadHom.id (StateT σ m)

@[simp]

theorem StateT.mapHom_comp {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {σ : Type u} {n' : Type u → Type x} [Monad n'] (G : n →ᵐ n') (F : m →ᵐ n) : mapHom (G ∘ₘ F) = mapHom G ∘ₘ mapHom F

def ReaderT.mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ρ : Type u} (φ : m →ᵐ n) : ReaderT ρ m →ᵐ ReaderT ρ n

ReaderT ρ is functorial on monad morphisms, acting under the environment.

@[simp]

theorem ReaderT.run_mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ρ α : Type u} (φ : m →ᵐ n) (x : ReaderT ρ m α) (r : ρ) : ((fun {α : Type u} (x : ReaderT ρ m α) => (mapHom φ).toFun α x) x).run r = (fun {α : Type u} (x : m α) => φ.toFun α x) (x.run r)

@[simp]

theorem ReaderT.mapHom_id {m : Type u → Type v} [Monad m] {ρ : Type u} : mapHom (MonadHom.id m) = MonadHom.id (ReaderT ρ m)

@[simp]

theorem ReaderT.mapHom_comp {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ρ : Type u} {n' : Type u → Type x} [Monad n'] (G : n →ᵐ n') (F : m →ᵐ n) : mapHom (G ∘ₘ F) = mapHom G ∘ₘ mapHom F

def OptionT.mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] (φ : m →ᵐ n) : OptionT m →ᵐ OptionT n

OptionT is functorial on monad morphisms. The failure branch is preserved because a monad morphism commutes with pure, so none is carried to none.

@[simp]

theorem OptionT.run_mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {α : Type u} (φ : m →ᵐ n) (x : OptionT m α) : ((fun {α : Type u} (x : OptionT m α) => (mapHom φ).toFun α x) x).run = (fun {α : Type u} (x : m α) => φ.toFun α x) x.run

@[simp]

theorem OptionT.mapHom_id {m : Type u → Type v} [Monad m] : mapHom (MonadHom.id m) = MonadHom.id (OptionT m)

@[simp]

theorem OptionT.mapHom_comp {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {n' : Type u → Type x} [Monad n'] (G : n →ᵐ n') (F : m →ᵐ n) : mapHom (G ∘ₘ F) = mapHom G ∘ₘ mapHom F

def ExceptT.mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ε : Type u} (φ : m →ᵐ n) : ExceptT ε m →ᵐ ExceptT ε n

ExceptT ε is functorial on monad morphisms. As for OptionT, the error branch survives because a monad morphism preserves pure.

@[simp]

theorem ExceptT.run_mapHom {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ε α : Type u} (φ : m →ᵐ n) (x : ExceptT ε m α) : ((fun {α : Type u} (x : ExceptT ε m α) => (mapHom φ).toFun α x) x).run = (fun {α : Type u} (x : m α) => φ.toFun α x) x.run

@[simp]

theorem ExceptT.mapHom_id {m : Type u → Type v} [Monad m] {ε : Type u} : mapHom (MonadHom.id m) = MonadHom.id (ExceptT ε m)

@[simp]

theorem ExceptT.mapHom_comp {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] {ε : Type u} {n' : Type u → Type x} [Monad n'] (G : n →ᵐ n') (F : m →ᵐ n) : mapHom (G ∘ₘ F) = mapHom G ∘ₘ mapHom F