Re: [HoTT] Martin-Löf '86

[Colin Zwanziger <zwanz...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1722 bytes --]

Yes, this was when Martin-Löf introduced his logical framework formulation
of type theory. In addition, he returned to intensional type theory in that
lecture after some time working with extensional type theory. (I was able
to get a good sense of the content of the lecture via off-list responses.)

Best,

Colin

On Fri, May 4, 2018 at 10:47 AM, Ansten Mørch Klev <anste...@gmail.com>
wrote:

> In light of the title and date of this lecture it is natural to think that
> it presented the hierarchy of higher types, what is also sometimes called
> the logical framework of Martin-Löf type theory. A good published reference
> for this is the chapter by Nordström, Petersson, and Smith in vol 5 of the
> Handbook of Logic in Computer Science. For the treatment of Pi, which here
> allows for an induction principle, see also chapter 7 of the book by the
> same authors and Garner's paper "On the strength of dependent products in
> the type theory of Martin-Löf".
>
> Ansten Klev
>
> On Thu, Apr 26, 2018 at 8:56 PM, Colin Zwanziger <zwanz...@gmail.com>
> wrote:
>
>> Dear all,
>>
>> Does anyone happen to have a copy of the work
>>
>> Martin-Löf, P. (1986). Amendment to intuitionistic type theory. *Notes
>> from a lecture given in Göteborg*.
>>
>> that they could share? Or advice on how to obtain a copy?
>>
>> Best regards,
>>
>> Colin Zwanziger
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>

[-- Attachment #2: Type: text/html, Size: 2980 bytes --]