proposition: Lemma transport_source_target_comm {C : precategory} {x y x' y' : ob C} (f : x --> y) (e1 : x = x') (e2 : y = y') : transportf (λ (x'' : ob C), precategory_morphisms x'' y') e1 (transportf (precategory_morphisms x) e2 f) = transportf (precategory_morphisms x') e2 (transportf (λ (x'' : ob C), precategory_morphisms x'' y) e1 f).
proof: Proof. induction e1. induction e2. apply idpath. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos