Definition toPathOverIdpath {X:Type} {x:X} {Y : X -> Type} (y y' : Y x) : y = y' -> PathOver (idpath x) y y' := idfun _.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.