[Agda] Terminology: inductive family

[Peter Hancock]

Peter Dybjer wrote:

> I used the term for the title of my FACS 1994 paper, because I needed a
> short form for "inductively defined indexed family of sets" which is quite
> a mouthful. Although my aim was to delineate a class of definitions which
> is both natural and general, it was clear from the beginning that there
> were a number of choices that needed to be made. It was important to make
> sure that the class of definitions was constructive in the sense of Per
> Martin-Löf. One of the main arguments for the choice of definition was
> that it was essentially a Curry-Howard interpretation of the definition of
> inductive predicate that Per had in his "Hauptsatz for the intuitionistic
> theory of iterated inductive definitions" 1971.

I don't currently have access to this paper, and forgive me if I'm
wrong, but I think Per couched this theory in first order constructive
predicate logic, without any definitional equality (only syntactic
equality) between terms.

It doesn't seem to me entirely obvious that one can
lift Per's schemata into a dependently typed setting,
(at least one can't lift them *blithely*)
especially because there are now curious phenomena
in the computation rules.  For example, in
that for J, the eliminator for the identity type:

    J(C,c,a,a,r(a)) = c(a) : C(a,a,r(a))
          ^ ^   ^
          | |   |

(where C(x:A,y:A,z:I(A,a,b)):Set,
        c(x:A):C(x,x,r(x)),
        a:A)

the non-linear occurrences on the left-hand side raise
the question of whether the definitional equality
of the indicated expressions should be checked,
even if one is only evaluating the left hand side
"at run-time".

Roughly, things have got a lot hairier since 1971.
(Understatement of the century?)

Peter Hancock