Definition pullBackPathOver {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 : Y x2'} (q : PathOver s' y1 y2) : PathOver s (pullBackPointOver g r1 y1) (pullBackPointOver g r2 y2). Proof. induction r1, r2. simpl in r; simpl. assert (k' : s' = maponpaths g s). { refine (r @ pathscomp0rid _). } clear r. induction (!k'); clear k'. induction s. simpl in q. simpl. exact q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.