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
 | This article has not been added to any content categories. Please help out by adding categories to it so that it can be listed with similar articles. (January 2013) |