[Agda] dependent mutually inductive types

[Thorsten Altenkirch]

Additionally we have recently written a paper which suggests a categorical semantics of these inductive-inductive definitions, which has been accepted for CALCO this year. See

http://www.cs.nott.ac.uk/~txa/publ/catind2.pdf

Cheers,
Thorsten

On 3 Aug 2011, at 04:23, Dan Doel wrote:

> 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