[Agda] Self-containing inductive-recursive definitions

[Dan Licata]

On Jun20, Thorsten Altenkirch wrote:

> I don't know wether it is described in the paper you mention but there
> is a systematic translation of such definitions which was also
> suggested by Conor. The basic idea is to define each datatype in an
> unindexed way and then introduce a family (i.e. a predicate)

That's cool!  Just to check, since the running example in this thread is
a little hard to follow: If you take an intrinsically well-typed
inductive-inductive definition of dependently typed syntax

 mutual
   data Ctx : Set

   data Tp : Ctx -> Set

   data Tm : (G : Ctx) -> Tp G -> Set

and apply this transformation, do you recover a syntax with raw
(extrinsically typed) proof terms for contexts, types, and terms?

-Dan