Definition weqpath_cast {X Y} (w : X ≃ Y) : cast (weqtopaths w) = w. Proof. intros. exact (pr1_eqweqmap _ @ maponpaths pr1 (weqpathsweq w)). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.