proposition: Lemma transportf2_comp {X : UU} (P : X -> X → UU) (x x' : X) (ex : x = x') (t:P x x) : transportf (λ y, P y y) ex t = transportf (λ y, P y x') ex (transportf (λ y, P x y) ex t).
proof: Proof. now induction ex. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits