Definition assocPathOver {X:Type} {x x' x'' x''':X} {p:x=x'} {p':x'=x''} {p'':x''=x'''} {Y : X -> Type} {y : Y x} {y' : Y x'} {y'' : Y x''} {y''' : Y x'''} (q : PathOver p y y') (q' : PathOver p' y' y'') (q'' : PathOver p'' y'' y''') : transportf (λ ppp, PathOver ppp y y''') (path_assoc p p' p'') (q * (q' * q'')) = (q * q') * q''. Proof. induction p, p', p'', q, q', q''. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.