proposition: 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: Proof. induction p. simpl. apply (maponpaths (λ r, r = e')). apply pathsinv0, pathscomp0rid. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.PartA