Theorem isinclbetweensets {X Y : UU} (f : X -> Y) (isx : isaset X) (isy : isaset Y) (inj : ∏ x x' : X , (paths (f x) (f x') -> x = x')) : isincl f. Proof. intros. apply isinclweqonpaths. intros x x'. apply (isweqimplimpl (@maponpaths _ _ f x x') (inj x x') (isx x x') (isy (f x) (f x'))). Defined.