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. induction (funextfun F F' (λ x : X, H x)). apply idpath. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos.