Lemma composePathOverPathRotate {X:Type} {x x':X} {p:x=x'} {Y : X -> Type} {y : Y x} {y' y'': Y x'} (r : PathOver p y y') (q : y' = y'') (s : PathOver p y y'') : r ⟥ q = s <-> r = s ⟥ (!q). Proof. induction q. simpl. apply isrefl_logeq. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.PartA.