fact: Definition PathOverToPathPair {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y : Y x) (y' : Y x') : PathOver p y y' → PathPair (x,,y) (x',,y').
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA