Lemma empty_hsubtype_preserving {X Y : UU} (f : X → Y) : hsubtype_preserving (emptysubtype X) (emptysubtype Y) f. Proof. unfold hsubtype_preserving. rewrite image_hsubtype_emptyhsubtype. apply subtype_containment_isrefl. Qed.