instLawfulMonad — Mathlib

English

There is a lawful monad structure on Trunc, satisfying the usual monad laws with respect to id, pure, bind, and related operations.

Русский

На Trunc существует законная структура монад, удовлетворяющая обычным законам монадности относительно id, pure, bind и сопутствующих операций.

LaTeX

$$$\\text{LawfulMonad}(\\operatorname{Trunc})$$$

Lean4

instance : LawfulMonad Trunc where
  id_map _ := Trunc.eq _ _
  pure_bind _ _ := rfl
  bind_assoc _ _ _ := Trunc.eq _ _
  map_const := rfl
  seqLeft_eq _ _ := Trunc.eq _ _
  seqRight_eq _ _ := Trunc.eq _ _
  pure_seq _ _ := rfl
  bind_pure_comp _ _ := rfl
  bind_map _ _ := rfl

Похожие утверждения