proposition: Lemma image_hsubtype_emptyhsubtype {X Y : UU} (f : X → Y) : image_hsubtype (emptysubtype X) f = emptysubtype Y.
proof: 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.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions