[Agda] 'Dummie' question - why records?

[Peter Dybjer]

> 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.

Yes, I remember Per saying something like that. How the meaning of the function TYPE is determined by the rule of function application, whereas the meaning of the function SET is determined by the introduction rule, stating that 

lambda : (A : Set)(B : (A)Set)(b : (x : A)B x) Pi A B

is a constructor for the function SET.

Peter