[Agda] dependent mutually inductive types

[Anthony de Almeida Lopes]

The paper "Equational Theories with Recursive Types"
(http://www.cs.hmc.edu/~stone/papers/recfull.pdf) covers this quite
nicely, as I recall.

- Anthony

2011/8/3 Dan Doel <dan.doel at gmail.com>:
> There was a paper written not long ago about these
> 'inductive-inductive' definitions. Here's a link:
>
>    http://cs.swan.ac.uk/~csfnf/papers/indind_csl2010.pdf
>
> As far as I know, they aren't that widely studied. There's also (as
> the paper mentions, I think) a proposed translation (by Conor McBride)
> into ordinary inductive families. As I recall, it's a two-step process
> where you first define some non-indexed types and then have a second
> set of types that identify the inhabitants of those types that
> correspond to inhabitants of the proposed inductive-inductive
> definition. But I don't have a pointer to the decoding on hand.
>
> -- Dan
>
> On Tue, Aug 2, 2011 at 11:05 PM, Michael Shulman <mshulman at ucsd.edu> wrote:
>> Hi,
>>
>> In Agda, it appears to be possible to mutually-inductively define two
>> types A and B, such that B is dependent on A:
>>
>> mutual
>>  data A : Set where
>>    ...
>>
>>  data B : A -> Set where
>>    ...
>>
>> Is there a mathematical theory of models or consistency for such
>> dependent mutually inductive families?
>>
>> Thanks,
>> Mike
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>