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

["Ansten Mørch Klev" <"anste..."@gmail.com>]

[-- 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 --]