Corollary uniqueFiller (X:Type) (x y z : X) (p : x = z) (q : y = z) : ∃! r, r @ q = p. Proof. refine (@iscontrweqf (∑ r, r = p @ !q) _ _ _). { apply weqfibtototal; intro r. exact hornRotation_rr. } { apply iscontrcoconustot. } Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.