[Agda] Terminology: inductive family

[Peter Hancock]

Am I right in thinking that the term "inductive family"
covers cases like the following T : A -> Set, defined in a context

A : Set
B : A -> Set
C : (a : A)-> B a -> Set
d : (a : A, b : B a)-> C a b -> A

T (a : A) = data sup (b : B a) (f : (C a b)-> T (d a b c))

?  After all, it is a family (set-valued function), and it
is defined inductively (or more precisely, its values are
defined by simultaneous induction).

I used the word "covers" to suggest that there may be other
definitions of things that one wishes to call inductive
families, such as those in which each constructor is
targeted on a particular "section" of the function domain,
given as the range of a (vector of) function(s).

In the above case, there happens to be one constructor "sup",
but what is important is that it targets the whole function domain.

I had thought that the qualifications "restricted" and
"general" were invented (by Peter Dybjer and/or Anton?)
to be used when one needs to be specific about the two
forms of inductive family.  The distinction is
important, in my opinion.

I should not like to discourage anyone from thinking
about the more liberal kind of inductive family, at least
anyone who is prepared to acquire some mental scar tissue.
But I *would* like to heavily discourage anyone from
using the term "inductive family" as if it meant only
the general form -- because it damages words, and words
are all we have to communicate with.

Peter Hancock