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. now induction ex. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.