[Agda] Big indices for small types?

[Peter Dybjer]

Hi Conor,

Have you got a consistency proof (relative to set theory)?

I don't have anything specific to say about your definition, except that
it goes against certain
intuitions about "predicativity" (relating to concepts such as "before",
"after", "below", and "above").
However, to me "predicativity" is a subjective notion, it's all in your
own mind, and not an objective concept, which is what really counts.

I propose the following plan of action when adding a new construction to
Martin-Löf type theory (Agda).

1. Prove it consistent relative to set theory
2. Give an informal but careful analysis why it is constructive, that is,
why it satisfies Martin-Löf's style meaning explanations.
3. Prove normalization and decidability of type-checking for the extended
system.

It's probably also important to have a good motivating example.

Cheers,
Peter

> Just fiddling about with some ideas about stratification
> and wondering if anyone has anything substantial to say
> about definitions like
>
>    data EQ (S : Set1) : Set1 -> Set where
>      REFL : EQ S S
>
> On the one hand, this doesn't exactly fit with the idea
> of building the hierarchy up from below. On the other
> hand, it doesn't actually store any big things inside
> any small things.
>
> Of course, Agda 2's
>
>    data BEFORE : AFTER -> Set
>
> distinction isn't the usual parameter/index distinction,
> as shown
>
>    data Lam (X : Set) : Set where
>      var : X -> Lam X
>      app : Lam X -> Lam X -> Lam X
>      lam : Lam (Maybe X) -> Lam X
>
> Sizewise, it seems that anything goes as long as there's
> no large payload.
>
> Is this well understood?
>
> Scares me.
>
> Cheers
>
> Conor
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>