proposition: Corollary neghfiberii1y (X Y : UU) (y : Y) : neg (hfiber (@ii1 X Y) (ii2 y)).
proof: Proof. intros. intro xe. induction xe as [ x e ]. apply (negpathsii1ii2 _ _ e). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom