proposition: Lemma composite_adjoint : [the functor of F \o F0] -| [the functor of U0 \o U].
proof: Proof. apply: (@AdjointFunctor.mk _ _ uni couni). rewrite /TriangularLaws.left => A. rewrite FCompE -[LHS]compA. rewrite -(@functor_o F). rewrite (_ : @eps0 _ \o F0 # _ = @eta (F0 A)); first exact: (AdjointFunctor.tri_left H). rewrite functor_o [LHS]compA -FCompE. rewrite -(natural (AdjointFunctor.eps H0)) /= FIdE -compA. by rewrite (AdjointFunctor.tri_left H0) compfid. rewrite /TriangularLaws.right => A. rewrite /couni /uni /=. rewrite compA -[RHS](AdjointFunctor.tri_right H0 (U A)); congr (_ \o _). rewrite FCompE -functor_o; congr (_ # _). rewrite functor_o -compA -FCompE. rewrite (natural (AdjointFunctor.eta H)) FIdE. by rewrite compA (AdjointFunctor.tri_right H) compidf. Qed.
imports: ssrmatching mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy