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