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