[Agda] Terminology: inductive family

[Peter Hancock]

Conor said:
>> I guess what I'm saying is that it would be a
>> useful community contribution (in which I'm very
>> happy to participate), to write, probably not for
>> publication, some sort of article which traces
>> the evolution of these issues, including the
>> directions abandoned. I certainly don't know
>> enough to write such a thing, but I'm keen to
>> gather the data.
>>     
There's a pretty interesting set of slides by a certain P. Dybjer at:

http://www.cs.chalmers.se/~peterd/papers/historyidentitytype.pdf

Actually, I don't think it can be disentangled from the history of
definitional equality.  Of course, that goes back, er, a very long way,
but a sensible starting point is Per's paper "About models for
intuitionistic type theories and the notion of definitional equality"
in Proc. 3rd Scandinavian Logic Symp, 75, pp 81-109.  There it
is introduced with the wonderful rhetorical flourish:

"By definitional equality, I mean the relation which is used on
almost every page of an informal mathematical text ... . As an
example, one can take the first part of this paper  where it has been used
more than 50 times."

His analysis of it when that paper was written was:

"Definitional equality is a relation between linguistic expressions
and *not* between the abstract entities which they denote and are the same.
This is the view that Frege took of the relation of equality of
content (Inhaltsgleichheit) which enters into his Begriffschrift but
which he later abandoned."

And which Per himself quite soon abandoned, in favour of a
typed judgement, rather than a syntactic relation.   As for the
rules governing definitional equality,  in this paper it is
proposed to drop the $\xi$-rule (propagation through
binders), partly because he was (at that time) unable to
(locally) construct the model of computable terms in his
type theory. (See 2.1.4 of the paper.)

Only recently (2005?) did Per find a way around the
difficulty he first encountered pre 1975.  In the intervening
30 years, he tried just about every imaginable avenue for
getting an analysis of definitional equality that would
satisfy him.   As for propositional equality I(A,a,b), that's
of course something else.  But with the equality reflection
rule of extensional type theory (early 80's) it was tied in to judgemental
equality in a rather drastic way.

I agree, it would be good to record what we know about the
twists and turns of equality in dependent type theory (and
category theory).  I'd like to know much more of what
has been going on in dependent type theory outside Sweden
(or even Stockholm).

Peter


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.