[Agda] induction-recursion

[Anthony de Almeida Lopes]

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.
Several rather clear examples of this can be found in section 1.1 of
[2]. In Agda, I believe it's use is invoked by prefacing a block of
data declarations by the keyword "mutual." If I'm not mistaken,
sections 3 and 4 of [3] approaches similar results but both the
underlying theory and presentation of the feature are quite different,
introducing "type-level pairs." I imagine using a stratified core
theory (i.e. hierarchy of universes) would probably allow us to forgo
adding type-level pairs to a core theory, achieving the same result as
presented in sections 3 and 4 of [3]. Please correct me if I'm wrong,
on both accounts.

- Anthony

n.b. We're talking specifically about the syntax and semantics of
defining types here.

1. http://www.cs.swan.ac.uk/~csetzer/articles/forsbergSetzerInductionInductionCsl2010.pdf
2. http://www.cs.swan.ac.uk/~csetzer/articles/altenkirchForsbergMorrisSetzerCALCO2011.pdf
3. http://www.cs.hmc.edu/~stone/papers/recfull.pdf


2012/1/9 wren ng thornton <wren at freegeek.org>:
> 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,
> ~wren
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>