[Agda] 'Dummie' question - why records?

[Peter Hancock]

On 21/10/2011 13:41, Nils Anders Danielsson wrote:
> On 2011-10-18 12:47, Dirk Ullrich wrote:
>> So taking dependent records together with dependent function types
>> (where we have eta-equality in Agda, too, right?)
>
> Yes.
>
>> looks a little bit like Martin-Löf's logical framework where you have,
>> as far as I know, dependent product and function types, both with
>> eta-equality.
>
> I don't think you have (definitional) η-equality in the intensional
> variant of the framework.
>

I think we do, and I'm not sure what you mean by "the intensional
variant of the framework" . (It has no identity type, which I think
there would have to be for there to be an extensional variant.  Nevertheless,
the function types and the pair-types both have eta, as they are
non-weak *limits*, in the categorical sense.  I feel deeply uneasy about
Peter Dybjer and Anton Setzer's extension of the LF with 0 and +,
that they needed to formulate induction-recursion.)

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.

Peter Hancock