Lemma isincltwooutof3a {X Y Z : UU} (f : X -> Y) (g : Y -> Z) (isg : isincl g) (isgf : isincl (funcomp f g)) : isincl f. Proof. intros. apply (isofhlevelff 1 f g isgf). apply (isofhlevelfsnincl 1 g isg). Defined.