proposition: Lemma naturality_mpair (M : monad) (A B : UU0) (f : A -> B) (g : A -> M A): (M # f^`2) \o (mpair \o g^`2) = mpair \o ((M # f) \o g)^`2.
proof: Proof. apply boolp.funext => -[a0 a1]. rewrite compE fmap_bind. rewrite compE mpairE compE bind_fmap; bind_ext => a2. rewrite fcompE fmap_bind 2!compE bind_fmap; bind_ext => a3. by rewrite fcompE -(compE (M # f^`2)) (natural ret) FIdE. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy