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