Definition pair_path_props {X} {P:X->Type} {x y:X} {p:P x} {q:P y} : x = y -> (∏ z, isaprop (P z)) -> x,,p = y,,q.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.