[Agda] no longer type checks

[Peter Hancock]

On 14/12/2012 19:00, Martin Escardo wrote:
> Thanks, Andreas. This is a helpful explanation.
>
> I think that maybe it is an open research question what kind of
> pattern matching corresponds to (intensional) MLTT (without the K
> axiom). That should be interesting to know for sure. But I am glad
> that there is some preliminary experimental work in Agda going on.

I agree.  Another important thing which does not seem to be clear is:
what is an inductive definition without *any* non-linearity among the indices?
So, one serious question is: what distinguishes an index from a parameter?

To me, it is not unthinkable that such a version of type-theory might exclude the
exciting identity type.  It may, perhaps, be formulated axiomatically,
and justified by a model.  The model construction seems to be difficult and subtle.

Hank