[Agda] Terminology: inductive family

[Peter Hancock]

Nils Anders Danielsson wrote:
> On Sat, Jun 7, 2008 at 1:09 PM, Peter Hancock <hancock at spamcop.net> wrote:
>> But I *would* like to heavily discourage anyone from
>> using the term "inductive family" as if it meant only
>> the general form
> 
> I think it is reasonable to let "inductive family" mean any form of
> inductively defined family of types (including singleton families, ...

and, I should hope, the restricted form. (Which was my point.)

Peter Hancock