[Agda] 'Dummie' question - why records?

[Nils Anders Danielsson]

On 2011-10-21 15:00, Peter Hancock wrote:
> 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).

Right. I decided to take a look in "Programming in Martin-Löf's Type
Theory", and the authors do mention that "It is possible to justify"
η-equality for the monomorphic framework described there.

-- 
/NAD