[Agda] Terminology: inductive family

[Peter Hancock]

> The above discussion started by the feeling that maybe the original schema
> was too general. But there is also reason to believe that it is not
> sufficiently general. For example, the definition of categorically
> inspired internal syntax for type theory (cf my 1996 Internal Type Theory
> paper) uses a definition not covered by the schema. We simultaneosly
> define
> 
> Context : Set
> Type : Context -> Set
> Term : (G : Context) -> Type G -> Set
> Subst : Context -> Context -> Set
> 
> etc.
> 
> I tacitly assumed that this is a constructively valid inductive definition
> although it is not covered by the original schema. Other people have used
> similar definitions, but as far as I know nobody has sorted out the
> precise
> syntax and semantics underlying such definitions. Is anyone aware of any
> work in this direction?

It is one of the things Neil, Anton and I hope to work on,
and relate (if possible) to induction-recursion. (As far as
I can see, it looks very different.  Indeed, sometimes I wonder
if it is acceptable at all.  It would be a test of
"meaning explanations" to see if they give any traction
for this question.)

Actually, I can't resist side-tracking a little on this specific
problem.  When I first became excited by the Petersonn-Synek trees,
I looked at the setup:

Context : Set
Type : Context -> Set
Ext  : (G : Context)-> Type G -> Context
Term : (G : Context)-> Type G -> Set
Def  : (G : Context)-> (A : Type G) -> Term G A -> Context

with the idea that "contexts" can contain not only
declarations of typed variables x : A but also definitions
x := a : A.  I had hoped that "definitions" could
play the role of substitutions in the substitution
calculus, and lead to a different formalism that might
be interesting.  (By the way, I know that Conor McBride
has also had similar ideas.)

I soon found that there were quite a few things missing
from this setup, and I'm not sure how best to extend it.
However, let me note that it is only a slight elaboration
on the Petersonn-Synek setup.  If one defines

    Fam (X : Type) : Type  =  (A : Set)>< (A -> X)

then the P-S setup can be expressed

    A : Set,  Phi : A -> Fam(Fam(A))

whereas what we have above is

    Context : Set
    Phi : Context -> Fam(Context >< Fam(Context))

Using essentially the P-S inductive scheme, one
can get various notions of "declaration block", and
"definition block" out of this set up, that resemble
some of the notions we want to analyse when
implementing dependent type theories.

Peter