[Agda] dependent mutually inductive types

[Peter Hancock]

On 03/08/2011 04:05, Michael Shulman 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?

Well, there is a categorical analysis of such things by
Fredrik Forsberg, Thorsten Altenkirch, Peter Morris and Anton Setzer,
under the name "inductive inductive definitions", some of whom will
probably pop up here and tell you more.

The construction seems quite hairy, involving dialgebras and
equalizers in CAT. I'm looking at some slides Fredrik kindly provided
me for a talk he gave in Strathclyde last week, which explain the idea,
and present appropriate elimination rules.  Fredrik's page is here:
http://cs.swan.ac.uk/~csfnf/

I'm not certain it's what you're asking about: the main thing here is
that the codomain types of the constructors for B can mention the
constructors for A.

May I ask what application you have in mind? (I've a suspicion, probably
ridiculous, that it's something to do with homotopy types._)

Hank
PS: One of the motivations for "induction-induction" is to provide an
analysis of attempts to build models of type-theories (after the style of
Peter Dybjer's categories with families) in type-theory itself.  Two such
endeavours, among others, were by Nils Anders Danielsson and James Chapman in their
respective PhD theses.