Induction-recursion (original) (raw)

In intuitionistic type theory (ITT), a discipline within mathematical logic, induction-recursion is a feature for simultaneously 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 remain predicative inside ITT. 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 predicative.