proposition: Lemma functor_data_eq (C C': precategory_ob_mor) (F F' : functor_data C C') (H : F ~ F') (H1 : ∏ C1 C2 (f : C1 --> C2), double_transport (H C1) (H C2) (pr2 F C1 C2 f) = pr2 F' C1 C2 f) : F = F'.
proof: Proof. use total2_paths_f. - use funextfun. intros c. exact (H c). - now apply functor_data_eq_prf. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence