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

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

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)