Definition makeFunctor_op {C D:category} (obj : ob C -> ob D) (mor : ∏ a b : C, b --> a -> obj a --> obj b) (identity : ∏ c, mor c c (identity c) = identity (obj c)) (compax : ∏ (a b c : C) (f : b --> a) (g : c --> b), mor a c (f ∘ g) = mor b c g ∘ mor a b f) : C^op ⟶ D := (obj,, mor),, identity,, compax.
Require Import UniMath.MoreFoundations.Tactics.