Definition abgr_image_hsubtype {A B : abgr} (f : monoidfun A B) : hsubtype B := (λ y : B, ∃ x : A, (f x) = y).
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.