proposition: Lemma bindetaf : BindLaws.left_neutral (bind eps) eta.
proof: Proof. rewrite /BindLaws.left_neutral => A B a h. rewrite /bind /mu. rewrite -(compE ([the functor of g \o f] # h)) (natural eta) -(compE (g # _)) compA. by rewrite AdjointFunctor.tri_right. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy