Agda Example

gistfile1.idr

data Image : (a -> b) -> b -> Type where
  Im : {f : a -> b} -> (x : a) -> Image f (f x)

inv : (f : a -> b) -> (y : b) -> Image f y -> a
inv f y im with (im)
  inv f _ im | Im x = x

{-
  data Image{A B : Set}(f : A → B) : B → Set where
    image : (x : A) → Image f (f x)

  inv : ∀ {A B} (f : A → B) → (y : B) → Image f y → A 
  inv f .(f x) (image x) = x
-}