proposition: Lemma naturality_join : hierarchy.naturality [the functor of F \o F] F join_.
proof: Proof. move=> a b h; rewrite (_ : h = [the {hom a, b} of h])//. rewrite /join_ actmE (category.natural category.join a). congr (_ \o _). by rewrite category.FCompE -2!actmE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures) hierarchy