Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more than welcome!
Page 122 of the Coq reference manual describes the strict positivity criteria:
The constant X occurs strictly positively in T in the following cases:
- X does not occur in T
- T converts to (X t1 . . . tn) and X does not occur in any of ti
- T converts to ∀ x : U, V and X does not occur in type U but occurs strictly positively in type V
- T converts to (I a1 . . . am t1 . . . tp) where I is the name of an inductive declaration of the form Ind(Γ)[m](I : A := c1 : ∀p1 : P1, . . . ∀pm : Pm, C1; . . . ; cn : ∀p1 : P1, . . . ∀pm : Pm, Cn ) (in particular, it is not mutually defined and it has m parameters) and X does not occur in any of the ti , and the (instantiated) types of constructor Ci{pj/aj}j=1...m of I satisfy the nested positivity condition for X
The emphasis (i.e., around "not mutually defined") was added by me.
Why is I required to not be mutually defined? If we removed this restriction (i.e., we allowed I to be mutually defined), would this introduce inconsistency into the system? If so, I'd greatly appreciate an example (e.g., where you prove False).
