Definition transportPathOver' {X:Type} {x x':X} (p:x=x') {Y : X -> Type} (y : Y x) (y' : Y x') (q : PathOver p y y') (T : ∏ (a:X) (b:Y a), Type) : T x' y' → T x y. Proof. now induction p, q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.