[Agda] Terminology: inductive family

[Nils Anders Danielsson]

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
perhaps also inductive-recursive definitions), just as e.g. "recursive
data type" is a very general concept (as opposed to "polynomial data
type", "regular data type" etc.). If you want to talk about a specific
form of inductive family, and want to avoid confusion, then you should
probably be more specific ("restricted inductive family á la
Dybjer/Setzer", "IIRD [DS06]", "Agda data type"...).

-- 
/NAD