fact: Definition build (C D : category) (F : {functor C -> D}) (G : {functor D -> C}) (A : F -| G) := Monad.Pack (Monad.Class (monad_of_adjoint_mixin A)).
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)