proposition: 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: Proof. intro H. destruct (!H). destruct px, py. reflexivity. Qed.
imports: UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos