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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.