Lemma functor_data_eq_prf (C C': precategory_ob_mor) (F F' : functor_data C C') (H : ∏ c, F c = F' c) (H1 : ∏ C1 C2 (f : C1 --> C2), double_transport (H C1) (H C2) (pr2 F C1 C2 f) = pr2 F' C1 C2 f) : transportf (λ x : C → C', ∏ a b : C, C ⟦ a, b ⟧ → C' ⟦ x a, x b ⟧) (funextfun F F' (λ c : C, H c)) (pr2 F) = pr2 F'. Proof. use funextsec. intros C1. use funextsec. intros C2. use funextsec. intros f. assert (e : transportf (λ x, ∏ a b : C, a --> b → x a --> x b) (funextfun F F' (λ c : C, H c)) (pr2 F) C1 C2 f = transportf (λ x, x C1 --> x C2) (funextfun F F' (λ c : C, H c)) (pr2 F C1 C2 f)). { now induction (funextfun F F' (λ c, H c)). } rewrite e, transport_mor_funextfun, transport_source_funextfun, transport_target_funextfun. exact (H1 C1 C2 f). Qed.
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.