Induction-recursion
In intuitionistic type theory (ITT), 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 remains predicative inside ITT.
External links
- Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, Journal of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525–549.
- A list of Peter Dybjer's publications on induction and induction-recursion