Morphisms Between Monads

Basic definitions of maps between monads parameterized over any possible output type. This is implemented with more constrained universes as m ⟶ n in mathlib category theory, but this gives definitions more standardized to a cs context.

TODO: Evaluate more fine-grained PureHom/BintHom/etc, with Class versions as well. Probably should be in the context of upstreaming things.

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 α

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.

Equations

• instCoeFunNatHomForallForall = { coe := fun (f : NatHom m n) {α : Type ?u.24} (x : m α) => f.toFun α x }

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.

Equations

• «term_→ᵐ_» = Lean.ParserDescr.trailingNode `«term_→ᵐ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵐ ") (Lean.ParserDescr.cat `term 25))

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 NatHom m n applied to an element of m α, with implicit α inferred.

Equations

• instCoeFunMonadHomForallForall = { coe := fun (f : m →ᵐ n) {α : Type ?u.40} (x : m α) => f.toFun α x }

class MonadHomClass (F : Type u_1) (m : outParam (Type u → Type v)) [Monad m] (n : outParam (Type u → Type w)) [Monad n] [hf : (α : Type u) → FunLike F (m α) (n α)] : Prop

Similar to AddHomClass but for MonadHom. This becomes more important if we start defining a hierarchy of these types (e.g. for AlternativeMonads). Note that getting FunLike to work has some outParam challenges, may not be workable.

• map_pure {α : Type u} (x : α) (f : F) : f (pure x) = pure x
• map_bind {α β : Type u} (x : m α) (y : α → m β) (f : F) : f (x >>= y) = f x >>= ⇑f ∘ y

def 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

Equations

• ⋯ = ⋯

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

@[simp]

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

@[simp]

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

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.

Equations

• MonadHom.ofLift m n = { toFun := fun (x : Type ?u.32) (mx : m x) => liftM mx, toFun_pure' := ⋯, toFun_bind' := ⋯ }

@[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.

Equations

• MonadHom.id m = { toFun := fun (x : Type ?u.21) (mx : m x) => mx, toFun_pure' := ⋯, toFun_bind' := ⋯ }

@[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.

Equations

• G ∘ₘ F = { toFun := fun (x : Type ?u.41) => G.toFun x ∘ F.toFun x, toFun_pure' := ⋯, toFun_bind' := ⋯ }

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

Equations

• MonadHom.«term_∘ₘ_» = Lean.ParserDescr.trailingNode `MonadHom.«term_∘ₘ_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ₘ ") (Lean.ParserDescr.cat `term 90))

@[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.

Equations

• MonadHom.pure m = { toFun := fun (x : Type ?u.26) (mx : Id x) => pure mx.run, toFun_pure' := ⋯, toFun_bind' := ⋯ }

@[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