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} : double_transport px py g = f -> g = double_transport (!px) (!py) f. 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.