Definition weq_pathscomp0r {X} x {y z:X} (p:y = z) : (x = y) ≃ (x = z). Proof. intros. exact (make_weq _ (isweqpathscomp0r _ p)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.