Definition image_univ' {X Y : UU} (f : X -> Y) (A : hsubtype Y ) : (forall x:X, A (f x)) <-> (forall y:Y, (image f y) -> A y). Proof. apply image_univ. 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.