The Coq mailing list

[Nils Anders Danielsson <nad AT chalmers.se>]

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