proposition: 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: Proof. intros hfz hgz. induction hfz as [ x fe ]. induction hgz as [ y ge ]. apply (noi x y (pathscomp0 fe (pathsinv0 ge))). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom