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