Definition pathsdirprodweq {X Y : UU} {x1 x2 : X} {y1 y2 : Y} : (make_dirprod x1 y1 = make_dirprod x2 y2) ≃ (x1 = x2) × (y1 = y2). Proof. intermediate_weq (make_dirprod x1 y1 ╝ make_dirprod x2 y2). - apply total2_paths_equiv. - unfold PathPair; cbn. use weqfibtototal; intro p; cbn. apply transitive_paths_weq. apply (toforallpaths _ _ _ (transportf_const p Y) y1). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.