Lemma pathOverEquations {X Y:Type} {f g : X -> Y} {x x' : X} (e : f x = g x) (e' : f x' = g x') (p : x = x') : PathOver (Y := λ x, f x = g x) p e e' = ( e @ maponpaths g p = maponpaths f p @ e' ). Proof. induction p. simpl. apply (maponpaths (λ r, r = e')). apply pathsinv0, pathscomp0rid. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.