The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

My feverish brain does not manage to see under which precise assumption this holds. However, I doubt it'll work for Coq (I'm guessing the fact that the type argument is taken in a predicative sort rather than an impredicative one would be the issue).


Arnaud

On 26 February 2012 13:15, Nils Anders Danielsson <nad AT chalmers.se> wrote:

On 2012-02-24 10:30, Arnaud Spiwack wrote:

I highly doubt it. Take the substitutive equality as an example. It is
defined as:

 Inductive eq (A:Type) (x:A) : A -> Prop := refl : eq x x.

rather than

 Inductive eq (A:Type) : A -> A -> Prop := refl (x:A) : eq x x.

They're not equivalent. The job of K is precisely to make the
difference between parameters and indices moot (appart from side
issues such as universes).

Paulin-Mohring's variant of J is equivalent to Martin-Löf's, even in the
absence of K. See the addendum to Thomas Streicher's
Habilitationsschrift
(http://www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf).

--
/NAD