English
For every α, the type constructor PFun α forms a LawfulMonad with the given monad structure.
Русский
Для любого множества α конструкция типа PFun α образует законный монад с заданной структурой монад.
LaTeX
$$$\\forall \\alpha,\\; \\text{LawfulMonad}(\\mathrm{PFun}\\,\\alpha)$$$
Lean4
instance lawfulMonad : LawfulMonad (PFun α) :=
LawfulMonad.mk' (bind_pure_comp := fun _ _ => funext fun _ => Part.bind_some_eq_map _ _) (id_map := fun f => by
funext a; dsimp [Functor.map, PFun.map]; cases f a; rfl) (pure_bind := fun x f =>
funext fun _ => Part.bind_some _ (f x)) (bind_assoc := fun f g k =>
funext fun a => (f a).bind_assoc (fun b => g b a) fun b => k b a)
