Induction-recursion: Difference between revisions

Revision as of 18:23, 26 September 2016

Revision as of 01:19, 30 March 2017

Line 7:

==Background==

Induction-Recursion came out of investigations to the rules of Martin-Löf's [[intuitionistic type theory]]. The type theory has a number of "type formers" and 4four kinds of rules for each one. Martin-Löf had hinted that the rules for each type former followed a pattern, which preserved the properties of the type theory (e.g., [[Normalization property (abstract rewriting)|strong normalization]], [[Impredicativity|predicativity]]). Researchers started looking for the most general description of the pattern, since that would tell what kinds of type formers could be added (or not added!) to extend the type theory.

The "universe" type former was the most interesting, because when the rules were written "ala Tarski", they simultaneously defined the "universe type" ''and ''a function that operated on it. This eventually lead Dybjer to Induction-Recursion.