* Martin-Löf '86 @ 2018-04-26 18:56 Colin Zwanziger 2018-04-27 7:39 ` [HoTT] " Andrej Bauer 2018-05-04 14:47 ` Ansten Mørch Klev 0 siblings, 2 replies; 4+ messages in thread From: Colin Zwanziger @ 2018-04-26 18:56 UTC (permalink / raw) To: HomotopyTypeTheory [-- 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 --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Martin-Löf '86 2018-04-26 18:56 Martin-Löf '86 Colin Zwanziger @ 2018-04-27 7:39 ` Andrej Bauer 2018-05-04 14:47 ` Ansten Mørch Klev 1 sibling, 0 replies; 4+ messages in thread From: Andrej Bauer @ 2018-04-27 7:39 UTC (permalink / raw) To: Colin Zwanziger; +Cc: HomotopyT...@googlegroups.com [-- 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 --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Martin-Löf '86 2018-04-26 18:56 Martin-Löf '86 Colin Zwanziger 2018-04-27 7:39 ` [HoTT] " Andrej Bauer @ 2018-05-04 14:47 ` Ansten Mørch Klev 2018-05-06 2:09 ` Colin Zwanziger 1 sibling, 1 reply; 4+ messages in thread From: Ansten Mørch Klev @ 2018-05-04 14:47 UTC (permalink / raw) To: Colin Zwanziger, homotopyt... [-- 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 --] ^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: [HoTT] Martin-Löf '86 2018-05-04 14:47 ` Ansten Mørch Klev @ 2018-05-06 2:09 ` Colin Zwanziger 0 siblings, 0 replies; 4+ messages in thread From: Colin Zwanziger @ 2018-05-06 2:09 UTC (permalink / raw) To: Ansten Mørch Klev; +Cc: homotopyt... [-- 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 --] ^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2018-05-06 2:10 UTC | newest] Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-04-26 18:56 Martin-Löf '86 Colin Zwanziger 2018-04-27 7:39 ` [HoTT] " Andrej Bauer 2018-05-04 14:47 ` Ansten Mørch Klev 2018-05-06 2:09 ` Colin Zwanziger
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).