proposition: Lemma transport_mor_funextfun {X : UU} {C : precategory_ob_mor} (F F' : X -> ob C) (H : ∏ (x : X), F x = F' x) {x1 x2 : X} (f : F x1 --> F x2) : transportf (λ x : X → C, x x1 --> x x2) (funextfun F F' H) f = transportf (λ x : X → C, F' x1 --> x x2) (funextfun F F' (λ x : X, H x)) (transportf (λ x : X → C, x x1 --> F x2) ((funextfun F F' (λ x : X, H x))) f).
proof: Proof. induction (funextfun F F' (λ x : X, H x)). apply idpath. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos