Definition transport_target_funextfun {X : UU} {C : precategory_ob_mor} (F F' : X -> ob C) (H : ∏ (x : X), F x = F' x) {x : X} {c : ob C} (f : c --> F x) : transportf (λ x0 : X → C, c --> x0 x) (funextfun F F' H) f = transportf (λ x0 : C, c --> x0) (H x) f.
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.