[Agda] induction-recursion

wren ng thornton wren at freegeek.org
Mon Jan 9 04:52:44 CET 2012

Hello all,

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?

Live well,

More information about the Agda mailing list