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