Definition paths3 {X Y Z} {x x':X} {y y':Y} {z z':Z} : x = x' -> y = y' -> z = z' -> @paths (_×_×_) (x,,y,,z) (x',,y',,z'). Proof. intros p q r. induction p, q, r. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.