Definition makeNattrans {C D:category} {F G:[C,D]} (mor : ∏ x : C, F ◾ x --> G ◾ x) (eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) : F --> G := (mor,,eqn).
Require Import UniMath.MoreFoundations.Tactics.