proposition: Lemma uni_naturality : naturality [the functor of idfun] [the functor of (U0 \o U) \o (F \o F0)] uni_fun.
proof: Proof. move=> A B h; rewrite FIdE. rewrite -[RHS]compA. rewrite -(natural (AdjointFunctor.eta H0)). rewrite [LHS]compA. rewrite [RHS]compA. congr (_ \o _). rewrite (FCompE U0 F0) -[in RHS](@functor_o U0) -[in LHS](@functor_o U0). congr (_ # _). by rewrite -(natural (AdjointFunctor.eta H)). Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy