Theorem isinclfromunit {X : UU} (f : unit -> X) (is : isaset X) : isincl f. Proof. intros. apply (isinclbetweensets f (isofhlevelcontr 2 (iscontrunit)) is). intros. induction x. induction x'. apply idpath. Defined.