[Agda] Image f

[Sergei Meshveliani]

People, 
I define Image for a map:

  record Image {l c' l'} {A : Set l} {B : Setoid c' l'}
                                     (f : A → Setoid.Carrier B) :
                                                   Set (l ⊔L (c' ⊔L l'))
         where
         _≈_ = Setoid._≈_ B
 
         field  elem  : Setoid.Carrier B
                proof : ∃ \ (x : A) → f x ≈ elem


Has Standard library something close to exploit instead?

Thanks,

------
Sergei