Definition binopPathOver {X:Type} {x x':X} (p:x=x') {Y Z W : X -> Type} (f : ∏ x, Y x -> Z x -> W x) (y : Y x) (y' : Y x') (z : Z x) (z' : Z x') : PathOver p y y' -> PathOver p z z' -> PathOver p (f x y z) (f x' y' z'). Proof. induction p. simpl. intros [] []. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.