Definition weqpath_transport {X Y} (w : X ≃ Y) : transportf (idfun UU) (weqtopaths w) = pr1 w. Proof. intros. exact (!pr1_eqweqmap2 _ @ maponpaths pr1 (weqpathsweq w)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.