Lemma fillerEquation {X:Type} {x y z : X} {p : x = z} {q : y = z} (r : x = y) (k : r @ q = p) : @paths (∑ r, r@q=p) (r ,, k) ((p @ !q) ,, hornRotation_rr (idpath _)). Proof. apply proofirrelevancecontr. apply uniqueFiller. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.