Definition pullBackPathPathOver {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} (y0 y1 : Y x1') (y2 : Y x2') (q : PathOver s' y1 y2) (t : y0 = y1) : pullBackPathOver g r (t ⟤ q) = pullBackPathOverPoint g r1 t ⟤ pullBackPathOver g r q. Proof. induction t, r1, r2. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.