proposition: Lemma JOIN_naturality : naturality _ _ (@JOIN).
proof: Proof. move=> A B g; apply/esym; rewrite {1}/JOIN -[in LHS]compA. transitivity ( Join \o (M # prod \o M # ([the functor of N \o (M \o N)] # g))). by []. rewrite -functor_o Hprod1. rewrite functor_o [LHS]compA /JOIN FCompE -(FCompE M M). rewrite -(natural join). by rewrite -compA. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib