Lemma double_transport_transpose' {C : precategory_ob_mor} {a a' b b' : C} {f : a' --> b'} {g : a --> b} {px : a' = a} {py : b' = b} : f = double_transport (!px) (!py) g -> double_transport px py f = g. Proof. intro H. destruct (!H). destruct px, py. reflexivity. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos.