Theorem isinclii1 (X Y : UU) : isincl (@ii1 X Y). Proof. intros. set (f := @ii1 X Y). set (g := coprodtoboolsum X Y). set (gf := λ x : X, (g (f x))). set (gf' := λ x : X, tpair (boolsumfun X Y) true x). assert (h : ∏ x : X, paths (gf' x) (gf x)) by (intro; apply idpath). assert (is1 : isofhlevelf (S O) gf') by apply (isofhlevelfsnfib O (boolsumfun X Y) true (isasetbool true true)). 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.