[Agda] 'Dummie' question - why records?

[Peter Dybjer]

> Whatever I think, "Martin-Lof's logical framework" is a bit of a
> fictional entity (my impressions are scraped together from various
> photocopied samizdat notes, and second-hand via drafts by Tasistro,
> Bertate, and other people in Chalmers the late 80's and 90's).
> 
> If anyone is able to attach a precise, scholarly meaning to this noun-phrase,
> I think it might be Peter Dybjer.

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.

Peter