[Agda] Terminology: inductive family

[Peter Dybjer]

>> 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?)

:-)

You are of course quite right about this. Type theory is a lot hairier
than predicate logic.

But if you look at the forms of introduction rules ("forall"-case and
"implies"-case) for generalized inductive definitions and look at them
from the Curry-Howard-Martin-Löf point of view then I think you
inevitably will end up in something rather close to the schema in the
"Inductive Families" paper. First the "forall" and the "implies" cases
collapse into one case of "inductive premise/argument". But you also need
to allow "non-inductive" premises ("side conditions") which don't appear
in Per's predicate logic version. And the conclusion of the elimination
rule
needs to be a dependent type, the predicate logic schema just has a
non-dependent proposition. And then you get the type-theoretic elimination
rules, like the one for equality mentioned above.

What I'm saying is that I felt guided in a certain rather inevitable
direction leading to "catholic" inductive families. Of course, by this I'm
not saying that there weren't a number of detailed choices that needed to
be made, just that essentially we will end up with catholic inductive
families if we take Per's definitions in predicate logic and swing the
magic wand of Curry-Howard.

Peter