Lemma disjointl1 (X : UU) : isisolated (coprod X unit) (ii2 tt). Proof. intros. unfold isisolated. intros x'. induction x' as [ x | u ]. apply (ii2 (negpathsii2ii1 x tt)). induction u. apply (ii1 (idpath _)). Defined.