Definition makeNatiso {C D:category} {F G:[C,D]} (mor : ∏ x : C, z_iso (F ◾ x) (G ◾ x)) (eqn : ∏ c c' f, mor c' ∘ F ▭ f = G ▭ f ∘ mor c) : nat_iso F G. Proof. refine (makeNattrans mor eqn,,_). apply nat_trafo_z_iso_if_pointwise_z_iso; intro c. apply pr2. Defined.
Require Import UniMath.MoreFoundations.Tactics.