[Agda] induction-recursion

[wren ng thornton]

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,
~wren