I'm looking at the nested positivity conditions for inductive types stated in the Coq manual. First off, are there any other references (not necessarily for Coq, but in dependent type theories generally) for the nested positivity conditions and how they come about? I've found older papers like Dybjer's Inductive Families and Coquand and Paulin's Inductively Defined Types, but I believe these only mention the strict positivity condition, and newer papers like the pCuIC one and A Comprehensible Guide to CIC don't mention nested positivity either.
Now, I'm trying to gain an intuitive understanding of why nested positivity is required. In essence, nested positivity states that when defining a constructor C for some inductive type $D$, if the type of an argument to $C$ is something like $I ~ \vec{p} ~ \vec{t}$, then $D$ can only appear strictly positively in $\vec{p}$, and only if $I \neq D$. I understand that allowing $D$ in negative positions of $\vec{p}$ basically allows for proofs of $(D \to \bot) \to \bot$, and allowing $D$ in other positive positions essentially allows for double negation elimination (and some inconsistency stuff with impredicative Prop). What I don't understand are these:
Why can't $D$ appear strictly positively in $\vec{p}$ if $I = D$ (either as constructor argument or return type)? For instance, for a constructor $C$ of an inductive type $D ~ (A: \textrm{Type}): \textrm{Type}$ (with $A$ as the sole parameter), why is $C: D ~ (D ~ A) \to D ~ A$ disallowed?
EDIT: Not only is this accepted in Agda 2.6.1.2, $C: D ~ (D ~ A \to \bot) \to D ~ A$ is also accepted, which seems suspicious to me.
Why can $D$ otherwise appear strictly positively in the parameters $\vec{p}$, but not in the indices $\vec{t}$?
Consider for instance the (rather silly) constructor $C: (D =_{\textrm{Type}} D) \to D$ for the inductive type $D: \textrm{Type}$, where $=$ is the usual equality type.EDIT: It turns out this doesn't type check in Agda for unrelated universe level reasons, so consider instead the following which Agda rejects for positivity reasons:
data Box : (A : Set) → Set where box : (A : Set) → Box A data D : Set where C : Box D → D
This is accepted by Agda if
A
is instead a parameter, as expected from the nested positivity rules.
I'm particularly interested in finding examples where violating nested positivity conditions (specifically these two I've listed) causes inconsistencies and proofs of $\bot$, which personally would be easier to understand than arguments about monotonicity.
neg : C = D -> ...
whereC
occurs negatively elsewhere, but is not subject to the check. I'm not certain why your particular example isn't accepted by Agda, because it has analysis for detecting thatX
is actually like a parameter (that's whyBox
is well-sized). I guess it doesn't take that into account with respect to positivity checking. $\endgroup$ – Dan Doel Jan 6 at 6:25data _≡_ (A : Set) : Set → Set where refl : A ≡ A
,data D : Set where neg : (E : Set) → (E → ⊥) → D ≡ E → D
. This isn't accepted but it's becauseneg
needs to be in the same universe asD
, butE: Set
means that it's actually inSet₁
. Interestingly, with the constructorc: D ≡ ⊤ → D
, Agda complains aboutD
not being strictly positive in≡
, but not if I change the type ofrefl
toA ≡ ⊤
, so it seems Agda doesn't merely check whether it's a parameter or index. $\endgroup$ – ionathanch Jan 6 at 12:00