Lemma negintersectii1ii2 {X Y : UU} (z : coprod X Y) : hfiber (@ii1 X Y) z -> hfiber (@ii2 _ _) z -> empty. Proof. intros X0 X1. induction X0 as [ t x ]. induction X1 as [ t0 x0 ]. set (e := pathscomp0 x (pathsinv0 x0)). apply (negpathsii1ii2 _ _ e). Defined.