Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: Generalizations of inductive types

Leopold Schlicht (Nov 19 2021 at 21:07):

Section 5.7 of the HoTT book sketches several generalizations of inductive types: inductive type families, mutual inductive types, inductive-inductive types, inductive-recursive types.

In a previous thread I learned that one can construct W-types (with typal computation rule) with very few assumptions (one needs power sets). Now I wonder: which of the above can be constructed and for which does one need to add additional rules of inference to the type theory? For instance, can ZFC prove "justification theorems" for all the above types of induction (when they are made precise)? (In the same way ZFC can construct W-types, i.e., initial algebras for polynomial endofunctors on Set.) Same question for MLTT and HoTT instead of ZFC.

Also, I would be curious if there is some place in ordinary mathematics (i.e., not Chapter 11 in the HoTT book :grinning_face_with_smiling_eyes:) which relies on some of the above generalizations of inductive types (such as an inductive-inductive definition). I only came up with the following example: if $S_\bullet$ is a simplicial set, and $(T_n)_n$ is a family of subsets $T_n\subseteq S_n$, then the definition of the "simplicial subset of $S_\bullet$ generated by $(T_n)_n$" can be phrased as an inductive family. (But one can also phrase it as a usual induction, so this isn't necessary.)

Mike Shulman (Nov 19 2021 at 21:32):

Roughly speaking, all of them except possibly inductive-recursive types can be constructed out of ordinary inductive types. There are some subtleties regarding definitional behavior of the computation rules, simple vs general elimination rules, and intensional vs extensional theory, some of which are areas of active research -- for instance, see this paper by Jasper Hugunin -- but as a general principle I think this claim can be defended.

Mike Shulman (Nov 19 2021 at 21:35):

The situation with induction-recursion is less clear to me. In one of its original formulations, IR is stronger than ZFC because you can use it to construct universes -- roughly speaking, it's about as strong as the large cardinal axiom "the proper-class ordinal is Mahlo". However, many practical uses of IR don't impinge on this size issue, and I expect it should be possible to formulate a general notion of IR type that at least doesn't have this obstacle to constructibility in ZFC. I wouldn't be surprised if someone's already done it, but I'm not familiar enough with the literature to say.

Leopold Schlicht (Nov 20 2021 at 10:19):

Thanks!