proposition: 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: 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.
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