Corollary isweqpathscomp0r' {X : UU} (x : X) {x' x'' : X} (e' : x' = x'') : isweq (λ e : x = x', e @ e'). Proof. intros p. use tpair. exists (p @ !e'). now apply hornRotation_rr. cbn. intros [q l]. apply fillerEquation. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.