proposition: Lemma natural_hcomp : naturality [the functor of F' \o F] [the functor of G' \o G] hcomp.
proof: Proof. move=> A B h. rewrite [LHS]compA (natural t) -[LHS]compA -[in RHS]compA. by congr (_ \o _); rewrite FCompE -2!functor_o (natural s). Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy