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. use total2_paths_f. - use funextfun. intros c. exact (H c). - now apply functor_data_eq_prf. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.