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 -> 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 -> Set := | c1 : Ty nat | c2 : Ty (Ty nat).
In fact, this case is almost verbatim an example from Coq'Art Section 184.108.40.206 of violating strict positivity:
Inductive T : Set -> 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?
mutual data U : Set0 -> Set0 where c : (i : Fin 2) -> U (T i) T : Fin 2 -> Set0 T zero = ℕ T (suc zero) = U ℕ
I'm happy to have pointers to relevant literature.
Thanks in advance.