Definition mapPathOver {X:Type} {x x':X} (p:x=x') {Y Y': X -> Type} (f : ∏ x, Y x -> Y' x) (y : Y x) (y' : Y x') : PathOver p y y' -> PathOver p (f x y) (f x' y'). Proof. induction p. simpl. intros []. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.