Definition inductionPathOver {X:Type} {x:X} {Y : X -> Type} (y : Y x) (T : ∏ x' (p : x = x') (y' : Y x'), PathOver p y y' → Type) (t : T x (idpath x) y (identityPathOver y)) : ∏ x' (y' : Y x') (p : x = x') (q : PathOver p y y'), T x' p y' q. Proof. intros. induction p, q. exact t. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.