Content deleted Content added
Citation bot (talk | contribs) Alter: chapter, title, template type. Add: chapter-url, chapter, series. Removed or converted URL. Removed parameters. Some additions/deletions were parameter name changes. | Use this bot. Report bugs. | Suggested by Headbomb | #UCB_toolbar |
rearrange sentence about universes |
||
Line 1:
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
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 ''simultaneously'' define the type and the function, because the rules for generating elements of the type are allowed to refer to the function.<ref name=Dybjer>{{cite journal|last=Dybjer|first=Peter|title=A general formulation of simultaneous inductive-recursive definitions in type theory|journal=Journal of Symbolic Logic|volume=65|issue=2|date=June 2000|pages=525–549|url=http://www.cse.chalmers.se/~peterd/papers/Inductive_Recursive.pdf|doi=10.2307/2586554|jstor=2586554|citeseerx=10.1.1.6.4575|s2cid=18271311 }}</ref>
| |||