proposition: 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: Proof. intros. induction e. induction e'. apply idpath. 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