[Agda] induction-recursion

Nils Anders Danielsson nad at chalmers.se
Mon Jan 9 12:06:54 CET 2012

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:



More information about the Agda mailing list