Lemma transport_source_target {X : UU} {C : precategory} {x y : X} (P : ∏ (x' : X), ob C) (P' : ∏ (x' : X), ob C) (f : ∏ (x' : X), (P x') --> (P' x')) (e : x = y) : transportf (λ (x' : X), (P x') --> (P' x')) e (f x) = transportf (λ (x' : X), precategory_morphisms (P x') (P' y)) e (transportf (precategory_morphisms (P x)) (maponpaths P' e) (f x)). Proof. rewrite <- functtransportf. unfold pathsinv0. unfold paths_rect. induction e. 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.