[-- Attachment #1: Type: text/plain, Size: 269 bytes --] 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 [-- Attachment #2: Type: text/html, Size: 362 bytes --]
[-- Attachment #1: Type: text/plain, Size: 153 bytes --] Alas, it's not listed at https://github.com/michaelt/martin-lof (which is otherwise a useful resource to be aware of). With kind regards, Andrej [-- Attachment #2: Type: text/html, Size: 290 bytes --]
[-- Attachment #1: Type: text/plain, Size: 1262 bytes --] 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: 2006 bytes --]
[-- 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 --]