Monad relations

class MonadRelation (m : Type u → Type v) (n : Type u → Type w) : Type (max (max (u + 1) v) w)

• monadRel {α : Type u} : m α → n α → Prop

def MonadRelation.«term_∼ₘ_» : Lean.TrailingParserDescr

Equations

• MonadRelation.«term_∼ₘ_» = Lean.ParserDescr.trailingNode `MonadRelation.«term_∼ₘ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∼ₘ ") (Lean.ParserDescr.cat `term 51))

class LawfulMonadRelation (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n] [MonadRelation m n] : Prop

• monadRel_pure {α : Type u} (a : α) : monadRel (pure a) (pure a)
• monadRel_bind {α β : Type u} {ma : m α} {mb : α → m β} {na : n α} {nb : α → n β} (ha : monadRel ma na) (hb : ∀ (a : α), monadRel (mb a) (nb a)) : monadRel (ma >>= mb) (na >>= nb)

instance MonadRelation.instOfMonadLiftT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLiftT m n] : MonadRelation m n

A (transitive) monad lift defines a monad relation via its graph

Equations

• MonadRelation.instOfMonadLiftT = { monadRel := fun {α : Type ?u.30} (ma : m α) (na : n α) => liftM ma = na }

instance MonadRelation.instOfLawfulMonadLiftT {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [Monad m] [Monad n] [MonadLiftT m n] [LawfulMonadLiftT m n] : LawfulMonadRelation m n

A (transitive) lawful monad lift defines a lawful monad relation via its graph

class MonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁) (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂) : Type (max (max (max (max (u + 1) v₁) v₂) w₁) w₂)

• monadRelHomFst {α : Type u} : m₁ α → m₂ α
• monadRelHomSnd {α : Type u} : n₁ α → n₂ α

class LawfulMonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁) (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂) [MonadRelation m₁ n₁] [MonadRelation m₂ n₂] [MonadRelationHom m₁ n₁ m₂ n₂] : Prop

• monadRel_hom {α : Type u} {ma : m₁ α} {na : n₁ α} (h : monadRel ma na) : monadRel (monadRelHomFst n₁ n₂ ma) (monadRelHomSnd m₁ m₂ na)