[Agda] induction-recursion

wren ng thornton wren at freegeek.org
Mon Jan 9 07:22:42 CET 2012

On 1/9/12 12:03 AM, Anthony de Almeida Lopes wrote:
> Assuming you read [1], the categorical point of view in [2] may help
> to compare inductive definitions to inductive-inductive definitions.
> The basic premise, as I gather, is that inductive-inductive
> definitions allow for we might call mutually recursive type families;
> specifically, the types may by indexed by values of each other.

Ah, is that all? That makes sense, both of the power and of how it 
differs from simple induction.

I'll take a look at those references and see if it still makes sense 
afterwards :)

Live well,

More information about the Agda mailing list