[Agda] dependent mutually inductive types

[Michael Shulman]

Thanks to everyone who replied!  The literature on Inductive-inductive
types is exactly what I wanted.

On Wed, Aug 3, 2011 at 3:05 AM, Peter Hancock <hancock at spamcop.net> wrote:
> May I ask what application you have in mind? (I've a suspicion, probably
> ridiculous, that it's something to do with homotopy types._)

Not really ridiculous, for anything involving me.  (-:  But actually,
not really the case here.

Peter Lumsdaine and I found ourselves wanting to construct a category
freely generated by certain constructors.  The natural way to
represent a category is with the type of arrows dependent over (two
copies of) the type of objects.  But then if the "constructors" we
want to apply to generate our category can take arrows as part of
their input and produce objects, our free category becomes an
inductive-inductive family.

Mike