[Agda] induction-recursion

[Nils Anders Danielsson]

On 2012-01-09 04:52, wren ng thornton wrote:
> I'm quite familiar with induction, and with recursion, however I'm not
> so familiar with induction-recursion and induction-induction. Is there
> any good introduction to IR and II which covers both their definitions
> as well as _how_ they differ in strength from one another and their
> simpler cousins?

As far as I recall adding II to a theory (with certain properties)
doesn't make it stronger, while adding IR does.

Dybjer and Setzer have written a lot about induction-recursion:

   http://www.cse.chalmers.se/~peterd/papers/inductive.html

-- 
/NAD