[Agda] dependent mutually inductive types

[Thorsten Altenkirch]

On 3 Aug 2011, at 11:05, Peter Hancock wrote:

> 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.

Sorry for being a bit short but I am just about to set off on a walking trip... :-)

> 
> The construction seems quite hairy, involving dialgebras and
> equalizers in CAT.

I agree. Hopefully some of the hairs can shaved off...

> 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.

Indeed, if this is not the case (which is true for many examples), you have just an endofunctor on Fam(Set) (or equivalently Set^->) and you just want the initial algebra of this functor.

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

That would be cool.

Btw, many proofs rely on UIP. E.g. the construction which derives indexed W-types from W-types (this is used in our paper on indexed containers) uses UIP and ext. I think it can be also done from univalence but it remains to be verified.

Cheers,
Thorsten

> 
> 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.
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda