Definition pullBackPathOverPath {X X':Type} (g : X -> X') {x1 x2:X} {x1' x2':X'} {r1 : g x1 = x1'} {r2 : g x2 = x2'} {s : x1 = x2} {s' : x1' = x2'} (r : r1 @ s' = maponpaths g s @ r2) {Y : X' -> Type} (y1 : Y x1') (y2 y3 : Y x2') (q : PathOver s' y1 y2) (t : y2 = y3) : pullBackPathOver g r (q ⟥ t) = pullBackPathOver g r q ⟥ pullBackPathOverPoint g r2 t. Proof. induction t, r1, r2. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.