[Agda] Positive but not strictly positive types

[Vilhelm Sjöberg]

On 2015-04-09 11:49, Andrés Sicard-Ramírez wrote:
> 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)?
I'm interested in the answer to this question also. If I correctly 
understand what Thierry Coquand wrote in the thread you mention, the 
answer is no; because Agda is predicative allowing positive datatypes 
would be sound. But it would be interesting to see this fleshed out more.

I wrote up a blog post about using non-strictly positive datatypes to 
get a paradox in Coq: 
http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/

Vilhelm