Why do Agda and Coq disagree on strict positivity? I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-recursion, etc.).

In particular, the following definition is accepted by Agda:

  data Ty : Set0 -&gt; Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)


whereas the equivalent Coq definition is rejected because the appearance of [Ty _] as an index of itself in c2 is considered to violate strict positivity.

  Inductive Ty : Set -&gt; Set :=
    | c1 : Ty nat
    | c2 : Ty (Ty nat).


In fact, this case is almost verbatim an example from Coq'Art Section 14.1.2.1 of violating strict positivity:

  Inductive T : Set -&gt; Set := c : (T (T nat)).


But I don't see the reasons for this difference between the type theories.  The classic example of proving False using a negative occurrence of a type in a constructor argument is clear to me, but I can't see how one might derive a contradiction from this style of indexing (regardless of otherwise strictly positive constructor arguments).

Poking around the literature, Dybjer's early Inductive Families paper makes an offhand comment about Paulin-Mohring's solution in the CID paper having slightly different restrictions, and vaguely suggests the differences might be related to impredicativity, but doesn't elaborate further.  Dybjer's paper seems to allow this, while Paulin-Mohring's clearly prohibits it.

Apparently I'm not the first to notice this difference of opinion, and some believe this definition shouldn't be permitted in either system (https://lists.chalmers.se/pipermail/agda/2012/004249.html), but I haven't found any explanations of why it is either sound in one system but not the other, or just a difference of opinion.

So I suppose I have several questions:


Is this an example of a monotone, but non-strictly-positive type? (In Coq; clearly Agda considers it strictly positive)
Why does Agda permit this while Coq rejects it?  It is simply an idiosyncratic difference in the interpretation of "strictly positive," is there a subtle difference between Coq and Agda that makes it sound in Agda and unsound in Coq, or is it a matter of taste driven by particular theoretical preferences?
Is there a meaningful difference between the first definition above, and the equivalent inductive-recursive definition below?


Inductive-recursive definition:

  mutual
    data U : Set0 -&gt; Set0 where
      c : (i : Fin 2) -&gt; U (T i)
    T : Fin 2 -&gt; Set0
    T zero = ℕ
    T (suc zero) = U ℕ


I'm happy to have pointers to relevant literature.

Thanks in advance.
The issue seems to be confusion resulting from a confluence of two factors:


I was using a stale version of Agda (2.3.0.1).  It appears that prior to 2.3.2, Agda simply wasn't checking strict positivity of the indices of constructor results (see the bug I linked elsewhere in the thread).
A closer reading of Dybjer's Inductive Families paper suggests that he may have intended that the inductive type being defined not be bound when typing the indices of a constructor result.  Section 3.2.1 gives the scheme for inductive constructors in prose, and apparently I misread the language describing the binding environments of each portion of the scheme.


This closer reading is of course consistent with the check that Coq and (recent versions of) Agda perform, that prohibit any appearance of T in its own indices.