Lemma image_hsubtype_emptyhsubtype {X Y : UU} (f : X → Y) : image_hsubtype (emptysubtype X) f = emptysubtype Y. Proof. apply funextsec ; intro y. apply hPropUnivalence. - intro yinfEmpty. use (factor_through_squash _ _ yinfEmpty). { apply emptysubtype. } intro x. apply (pr22 x). - intro yinEmpty. apply fromempty. exact (yinEmpty). Qed.