Definition image_univ {X Y : UU} (f : X -> Y) (A : hsubtype Y ) : (∀ x:X, A (f x)) <-> (image f ⊆ A). Proof. split. - intros H_A y Hy. refine (factor_through_squash_hProp _ _ Hy); intros [x e_xy]; destruct e_xy. use H_A. - intros H_A x. use H_A. apply value_in_image. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.