Lemma transport_swap: ∏ {X Y : UU} (P : X -> Y → UU) {x x':X} {y y' : Y} (e : x = x') (e' : y = y') (p : P x y), transportf (λ a, P _ a) e' (transportf (λ a, P a _) e p) = transportf (λ a, P a _) e (transportf (λ a, P _ a) e' p) . Proof. intros. induction e. induction e'. apply idpath. 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.