proposition: Corollary isweqmaponpaths {X Y : UU} (w : X ≃ Y) (x x' : X) : isweq (@maponpaths _ _ w x x').
proof: Proof. intros. apply (isweq_iso (@maponpaths _ _ w x x') (@invmaponpathsweq _ _ w x x') (@pathsweq3 _ _ w x x') (@pathsweq4 _ _ w x x')). Defined.
imports: UniMath.Foundations.Preamble