proposition: 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: Proof. rewrite <- functtransportf. unfold pathsinv0. unfold paths_rect. induction e. apply idpath. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos