Is there a translation to W types (or some appropriate strengthening of them) in MetaCoq? (How hard would such a thing be to write?) In particular, I'm wondering if it's possible to show (in MetaCoq) that strong normalisation in any well-formed global environment follows from strong normalisation in a sort-of minimal environment, so long as the minimal environment has enough universes lying around.

Do we now know that indexed W-types are sufficient to express nested inductive types? The short answer I think is no, we haven't done anything in that direction as far as I know.

Is there a version of nested indexed W-types or something that's sufficient to express nested inductive types? (I haven't looked into things much myself, here)

I'd be interested to have a look at this in the future, but I don't see how the question can even be asked without an implemented guard checker

Back when I was investigating various inductive types, I could not find any good literature on nested inductive types. I would be interested in anything you find out. I also concur with Theo's "no" however.

For a reasonable class of nested inductive types you could just mutually define the nesting types together with the original type and then reduce these mutually defined inductive types to a single one and continue the reduction to W + Id + ... There is however this pathological example of an inductive type that @Pierre-Marie Pédrot taught me that cannot be easily unnested:

```
Inductive I := K : forall x : I, x = x -> I
```

Trying to unnest the nested occurence of `=`

will naturally lead to an inductive-inductive family which Coq does not support (and I don't know if that can be reduced to a simple inductive).

There is Voevodsky's notes on type systems that does this reduction.

I've tried to collect some references here before. https://ncatlab.org/nlab/show/inductive-inductive+type

Also, lean does a reduction of inductive types to eliminators.

Last updated: Jan 30 2023 at 17:03 UTC