Lemma noil1 {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (noi : ∏ (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z) : hfiber f z -> hfiber g z -> empty. Proof. intros hfz hgz. induction hfz as [ x fe ]. induction hgz as [ y ge ]. apply (noi x y (pathscomp0 fe (pathsinv0 ge))). Defined.