fact: Definition hsubtype_preserving {X Y : UU} (U : hsubtype X) (V : hsubtype Y) (f : X → Y) : UU := subtype_containedIn (image_hsubtype U f) V.
imports: UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Propositions