The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

> Coq rejects the definition of I2 below saying "Non strictly positive
> occurrence of "I2" in "I1 I2 I2 -> I2".".
>
> Inductive I1 (A:Type) : Type -> Type :=
>   | MkI1 : I1 A A.
>
> Inductive I2 :=
>   | MkI2 : I1 I2 I2 -> I2.
>
> I think this is due to a violation of the Nested Positivity condition, 
> described here:
> https://coq.inria.fr/refman/language/core/inductive.html#nested-positivity
>
> However, I couldn't find a description in the manual for why nested 
> positivity is important.
>
> In particular, if one were to accept a definition in which the type being
> defined (I2 in this case) appears as an index of some other inductive type
> (e.g., I1), do things become inconsistent?

Coq's positivity requirements are stricter than mere positivity
(because of impredicativity), but even for "mere" positivity I think
your above I2 type is only positive if you assume uniqueness of
I1 proofs (i.e. axiom K):

   I1   ≃ Eq
   MkI1 ≃ eq_refl
   I2   ≃ μx . (I1 x x) = μF

I can define

    fmap : (α → β) → F α → F β
    fmap f _ = eq_refl

but then for `fmap id = id` to be true I need axiom K.

I'd be curious to know if admitting such definitions is more or less
soundness-threatening than axiom K.


        Stefan