[Agda] Terminology: inductive family

[Peter Dybjer]

Just a clarification.

Per considers three forms of "productions" for inductively defined
predicate in predicate logic. In addition to the "forall" and "implies"
cases (mentioned in the previous message) for "generalized" inductive
definitions, there is a case for "ordinary" inductive definitions. All
cases collapse to instances of the same schema for inductive families.

> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>