[Agda] separate definition of constructors?

[Nils Anders Danielsson]

On 24/05/2019 16.16, Ambrus Kaposi wrote:
> There is another workaround discovered recently by Szumi Xie: you can
> reduce any inductive-inductive type to one with only two sorts (using
> essentially the same technique as reducing mutual inductive types to
> an indexed inductive type). Then you can specify the constructors all
> at once.

I think I saw Conor McBride do something like this a long time ago (in a
talk in which he mentioned some building that was constructed by
building one floor at a time on the ground and then hoisting it up,
finishing with the ground floor, or something like that). Thorsten and I
used a similar technique in previous work:

   http://www.cse.chalmers.se/~nad/publications/altenkirch-danielsson-kraus-partiality/Partiality-monad.Inductive.Preliminary-sketch.html

-- 
/NAD