Lemma weqhfibernoi1 {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (noi : ∏ (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z) (xe : hfiber f z) : (hfiber (sumofmaps f g) z) ≃ (hfiber f z). Proof. intros. set (w1 := invweq (weqhfibersofsumofmaps f g z)). assert (a : neg (hfiber g z)) by (intro ye; apply (noil1 f g noi z xe ye)). set (w2 := invweq (weqii1withneg (hfiber f z) a)). apply (weqcomp w1 w2). Defined.