Lemma inversePathOverWeq' {X:Type} {x x':X} {p:x'=x} {Y : X -> Type} {y : Y x} {y' : Y x'} : PathOver (!p) y y' ≃ PathOver p y' y. Proof. exists inversePathOver'. intros s. use tpair. - exists (inversePathOver s). apply inverseInversePathOver1. - cbn. induction p. intros [t []]. induction t. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.