Definition weqonpaths2 {X Y} (w:X ≃ Y) {x x':X} {y y':Y} : w x = y -> w x' = y' -> (x = x') ≃ (y = y'). Proof. intros p q. induction p,q. apply weqonpaths. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.PartA.