[Agda] Abstract existential ?

[Jacques Carette]

Is there a way to encode an existential in Agda where the "exists" part 
of the dependent pair is abstract/private?  ∃ from the standard library 
just says that the first part is implicit (i.e. can be uniquely inferred).

I think I could use the same trick as in Haskell (i.e. use a wrapper 
where I don't export the constructor but do provide accessor functions 
that don't leak), but that somehow seems heavy.  Is there something simpler?

I don't mean a fully non-constructive exists here: I mean (informally!) 
"a dependent pair where the first projection is abstract and cannot 
leak". So to build such a thing, a definite type must be used, but once 
it is created, the 'clients' as it were, cannot find out what that type is.

Jacques