Theorem isinclii2 (X Y : UU) : isincl (@ii2 X Y). Proof. intros. set (f := @ii2 X Y). set (g := coprodtoboolsum X Y). set (gf := λ y : Y, (g (f y))). set (gf' := λ y : Y, tpair (boolsumfun X Y) false y). assert (h : ∏ y : Y, paths (gf' y) (gf y)) by (intro; apply idpath). assert (is1 : isofhlevelf (S O) gf') by apply (isofhlevelfsnfib O (boolsumfun X Y) false (isasetbool false false)). assert (is2 : isofhlevelf (S O) gf) by apply (isofhlevelfhomot (S O) gf' gf h is1). apply (isofhlevelff (S O) _ _ is2 (isofhlevelfweq (S (S O)) (weqcoprodtoboolsum X Y))). Defined.