proposition: Lemma weqhfibernoi2 {X Y Z : UU} (f : X -> Z) (g : Y -> Z) (noi : ∏ (x : X) (y : Y), neg (paths (f x) (g y))) (z : Z) (ye : hfiber g z) : (hfiber (sumofmaps f g) z) ≃ (hfiber g z).
proof: Proof. intros. set (w1 := invweq (weqhfibersofsumofmaps f g z)). assert (a : neg (hfiber f z)). intro xe. apply (noil1 f g noi z xe ye). set (w2 := invweq (weqii2withneg (hfiber g z) a)). apply (weqcomp w1 w2). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom