[Agda] Interfacing with Haskell

[Ivan Tomac]

Is there a way to map or import a type like Int from Haskell to Agda? 
There are examples for mapping Maybe and String. I couldn't find a way 
to map something like Int or Integer though. Not in any direct way that 
doesn't involve manual conversion from positive Int-s to ℕ-s.

Also, unrelated to the previous question and not as important, I didn't 
want to spam the message board with another email just to ask about 
this: what is the best way to rewrite the following Haskell code snippet 
in Agda?

f :: a -> (a, a)
f a = ...

g :: a -> a
g a = a'
where
(a', _) = f a

Using the type in Data.Product I can't seem to write this how I would in 
Haskell. So far I found two solutions. One was to use proj₁and proj₂to 
extract values out of a tuple. The other was to introduce an auxiliary 
function and pattern match on the tuple:

g : forall {A} {a : Set A} -> a -> a
g {A} {a} x = aux (f x)
where
aux : a × a -> a
aux (x' , _) = x'

Both seem awkward. Is there a better way to do this?

Ivan