[Agda] 'Dummie' question - why records?

[Peter Hancock]

> I don't know about "scholarly", but I was there when Martin-Löf
> presented his logical framework in some lectures in 1986 and 87, e g
>  in a workshop in Marstrand in 87. In that workshop he insisted
> strongly on eta-conversion for the function type (x : A)B in the
> logical framework ("the theory of types"), whereas only
> beta-conversion should be valid for the function set Pi A B in "the
> theory of sets", that is, the theory you obtain by adding rules for
> new set formers. In his approach Martin-Löf distinguishes between the
> function type and the function set.
>
> The book by Nordström, Petersson, and Smith is probably the best
> reference for this as already mentioned by Nisse.

Another rather good reference that I unjustly overlooked is chapter 8 ("Higher-level
type theory and categorial grammar") of Aarne Ranta's
"Type-Theoretical Grammar" (OUP 1994).  Here is a snippet (pp 166-167):

   Abstraction, application and \beta-conversion are analogous to \Pi introduction,
\Pi-elimination, and \Pi-equality, respectively.  But is (x : \alpha)\beta is a
type and (\Pi x: A)B(x) is a set, the conceptual order of these rules is different.
The introduction rules of a set prescribe the canonical forms of all of its elements.
For (\Pi x : A)B(x), there is just one canonical form, (\llambda x)b(x) where
b(x) : B(x) (x : A), as prescribed by \Pi introduction. The operator ap introduced
by \Pi elimination gives rise to non-canonical elements. \Pi equality
justifies \Pi elimination by telling us how ap is computed.
   But types are not restricted by canonical forms.  The abstract form (x)b is just one
of the forms an object of type (x:\alpha)\beta may have.  It is not the abstraction
rule that tells us what it is to be an object of (x : \alpha)\beta but the
application rule.  The \beta conversion rule is thus needed to justify the
abstraction rule, not the application rule.
   The following rule of eta-conversion is also valid.

       c : (x : \alpha)\beta
    ----------------------------------
     c = (x)(c(x)) : (x : \alpha)\beta

The functions c and (x)(c(x)), when applied to a : \alpha, yield the same value c(a).  To
yield the same value for any argument is precisely what it is for objects of type
(x : \alpha)\beta to be equal.  The corresponding lower-level rule... is not valid.

To my (hank's) mind, the important point is that in the logical framework (which Ranta calls
"higher-level type theory"), the *elimination* rules have conceptual priority.  They say
*what can be done with* an object of type \alpha.

Hank