Induction-induction
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
|
In intuitionistic type theory (ITT), some discipline within mathematical logic, induction-induction is for simultaneously declaring some inductive type and some inductive predicate over this type.
An
Induction-induction can be used to define larger types including various universe constructions in type theory.[1] and limit constructions in category/topos theory.
Example 1
Present the type as having the following constructors, note the early reference to the predicate :
and-simultaneously present the predicate as having the following constructors :
- if and then
- if and and then .
Example 2
A simple common example is the Universe à la Tarski type former. It creates some inductive type and some inductive predicate . For every type in the type theory (except itself!), there will be some element of which may be seen as some code for this corresponding type; The predicate inductively encodes each possible type to the corresponding element of ; and constructing new codes in will require referring to the decoding-as-type of earlier codes, via the predicate .
See also
- Induction-recursion – for simultaneously declaring some inductive type and some recursive function on this type .
References
- S2CID 18271311.