proposition: Lemma join_naturality : naturality _ _ (@JOIN).
proof: Proof. move=> A B g; apply/esym; rewrite {1}/JOIN -compA Hdorp1. rewrite [LHS]compA. rewrite (FCompE M N (N # g)). rewrite -(@functor_o M). rewrite -natural. by rewrite functor_o. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib