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. induction e1. induction e2. 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.