Jason Gross (Dec 08 2022 at 19:11): Jason Gross (Dec 08 2022 at 19:11):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.
Théo Winterhalter (Dec 08 2022 at 19:25):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.
Jason Gross (Dec 08 2022 at 19:44):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)
Yannick Forster (Dec 08 2022 at 20:10):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
Ali Caglayan (Dec 08 2022 at 21:35):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.
Kenji Maillard (Dec 08 2022 at 21:49):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).
Bas Spitters (Dec 09 2022 at 10:43):There is Voevodsky's notes on type systems that does this reduction.
Bas Spitters (Dec 09 2022 at 11:01):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