Talk:Induction-recursion

When I wrote the initial version, I contacted Dybjer to make sure it was accurate. This was his reply on 2013 Jan 30:

Hi Mike,

Thanks for writing this article.

"In intuitionistic type theory (ITT), induction-recursion is a feature for declaring a type and function on that type. It allows the creation of larger types, such as universes, than inductive Types. The types created still remains predicative inside ITT."

What you write is fine except that I would emphasize the simultaneity of the declaration of the type and the function. I actually feel inclined to write a bit more. Is the following comprehensible?

"In intuitionistic type theory (ITT), inductive-recursive definitions generalize {\link inductive definitions}.

An inductive definition is given by rules for generating elements of a type. One can then define functions from that type by induction on the way the elements of the type are generated. Induction-recursion generalizes this situation since one can {\it simultaneously} define the type and the function, because the rules for generating elements of the type are allowed to refer to the function.

Induction-recursion can be used to define large types including various universe constructions. It increases the proof-theoretic strength of type theory substantially. Nevertheless, inductive-recursive recursive definitions are still considered {\it predicative}."

One could also include the definition of the universe a la Tarski, the first and prototypical example, of an inductive-recursive definition.

Best wishes, Peter