Definition transitive_paths_weq {X : UU} {x y z : X} : x = y -> (x = z ≃ y = z). Proof. intro xeqy. use weq_iso. - intro xeqz. exact (!xeqy @ xeqz). - intro yeqz. exact (xeqy @ yeqz). - intro xeqz. refine (path_assoc _ _ _ @ _). refine (maponpaths (λ p, p @ xeqz) (pathsinv0r xeqy) @ _). reflexivity. - intro yeqz. refine (path_assoc _ _ _ @ _). refine (maponpaths (λ p, p @ yeqz) (pathsinv0l xeqy) @ _). reflexivity. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.