proposition: Lemma functor_data_eq_from_nat_trans (C C': precategory) (F F' : functor_data C C') (H : F ~ F') (H1 : is_nat_trans F F' (fun c:C => idtomor _ _ (H c))) : F = F'.
proof: Proof. apply (functor_data_eq _ _ _ _ H). intros c1 c2 f. rewrite double_transport_idtoiso. rewrite <- assoc. apply z_iso_inv_on_right. unfold z_iso_mor. do 2 rewrite eq_idtoiso_idtomor. apply H1. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence