fact: Definition naturality (C D : category) (F G : {functor C -> D}) (f : F ~~> G) := forall a b (h : {hom a, b}), (G # h) \o (f a) = (f b) \o (F # h).
imports: mathcomp(all_ssreflect) mathcomp(boolp) monae_lib HB(structures)