In intuitionistic type theory (ITT), a discipline within mathematical logic, induction-induction is for simultaneously declaring some inductive type and some inductive predicate over this type.

An inductive definition is given by rules for generating elements of some type. One can then define some predicate on that type by providing constructors for forming the elements of the predicate, such inductively on the way the elements of the type are generated. Induction-induction generalizes this situation since one can simultaneously define the type and the predicate, because the rules for generating elements of the type are allowed to refer to the predicate .

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

edit

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

edit

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

edit
  • Induction-recursion – for simultaneously declaring some inductive type and some recursive function on this type .

References

edit
  1. ^ Dybjer, Peter (June 2000). "A general formulation of simultaneous inductive-recursive definitions in type theory" (PDF). Journal of Symbolic Logic. 65 (2): 525–549. CiteSeerX 10.1.1.6.4575. doi:10.2307/2586554. JSTOR 2586554. S2CID 18271311.
edit