[Agda] Positive but not strictly positive types

[Andrés Sicard-Ramírez]

Hi,

Retaking the discussion in
http://thread.gmane.org/gmane.comp.lang.agda/6008, it's known that
using *negative* types it's possible

a) to prove absurdity or
b) to write non-terminating terms.

Is there some example in *Agda* of a positive but not strictly
positive type which allows a) or b)?

Thanks,

-- 
Andrés