[Agda] dependent mutually inductive types

[Dan Doel]

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
>