fact: Record Arrow (x y: Object): Type := arrow { map_obj:> obj x → obj y ; Fmap_inst: Fmap map_obj ; Functor_inst: Functor map_obj _ }.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.functors MathClasses.theory.categories