From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a24:7bc2:: with SMTP id q185-v6mr15152415itc.44.1525445264624; Fri, 04 May 2018 07:47:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:a64f:: with SMTP id r15-v6ls1114111iti.6.gmail; Fri, 04 May 2018 07:47:43 -0700 (PDT) X-Received: by 2002:a24:ed6:: with SMTP id 205-v6mr14928707ite.10.1525445263748; Fri, 04 May 2018 07:47:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525445263; cv=none; d=google.com; s=arc-20160816; b=mMCUMlBhFS9f5ouVWcUYyatYLZ4cFs/9c3Cob1Di2v+fmVDa36go5JKFFDvzYhVJ58 eQoYtBiO4eYwNF1yoinL8paDhYsUBmtSOGKT8+M9K0v4JrPeeZ30Q6qMJHuz1iL3WTWt aCxGhYkc/8qJvoMAghgBV0axCdG9QvQn2mFo5BBZuhUv5GfkwlXw4PXMABBVuO6oBRW+ HD8J+kTOSWLssQ+SGZXRBndo2vcVRwdae/pG6aEaKUqmTXYBwogsIEIDgCFP+eEVpId+ +wWhqoAEKI+rgNXG6UEqFVEH7uO9Wmn5+ymT+bbk1BInisFqBWRTmF9yH24qd18bbv7x tfnw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=3Y7NvG8KJGcgnR6/8q7cEIseditXfmk375qCWRnrgPc=; b=fKANZT8oLbQhQxC/UebKCUPCzpMt5HnMnAFlMJdrh3G9O/XqJ/ChN/E28PSjSR705j 9xL9tOaz/6bZLwAaPzukw3+hvT6nCoFLoFam+gHzt/Ah4uDF+v+OZhS6dqFcect7QwUA Gtl7IJyc3d8whOo1oU8whZRIjA4TZLvohwVS8jeDfXIUhyHkfeIO9rlbIQHmNXS8LAL8 j2UFocw4BaHqI8m6eeWxdN+RX6S1MEMh/6QEfGeCeVcY/4PJEpxJAb3ucTvlJbTRBj2Q 7VevhQ5dTgY0G0Z595UxirNShGJn5jEtvg3Ys3JLWwJe0f7SrQJaqFSWsiuqa/qCIDbF mKDA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=PjjWPzlK; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:400c:c08::22f as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x22f.google.com (mail-ua0-x22f.google.com. [2607:f8b0:400c:c08::22f]) by gmr-mx.google.com with ESMTPS id 2-v6si112800itj.0.2018.05.04.07.47.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 07:47:43 -0700 (PDT) Received-SPF: pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:400c:c08::22f as permitted sender) client-ip=2607:f8b0:400c:c08::22f; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=PjjWPzlK; spf=pass (google.com: domain of anste...@gmail.com designates 2607:f8b0:400c:c08::22f as permitted sender) smtp.mailfrom=anste...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ua0-x22f.google.com with SMTP id d4so5856689ual.10 for ; Fri, 04 May 2018 07:47:43 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=3Y7NvG8KJGcgnR6/8q7cEIseditXfmk375qCWRnrgPc=; b=PjjWPzlKFpbAZfuMdZdOPpZk1eCHBXYOjtus/visr19KRV4FNGbvGdoj6HyiH6AYT5 Up6fLX8YZ4oNYe2Ljs/RqBSnhpsQzpilvrfWxl7owVF5G6HGDjMwymc6KFG34c9HpLmv uhWToB/RHTSId04wINHvx1ycnlihZ8mVfn2sgrJK0ob1b6mCY+HyUtS7Hs5jaE7ZqglG SCfMY1W2RSedjfwwiPCEy6qp6mvvs+KS3HSukVhyHBfK+hN57wSXduXhllJJp7EhTy++ QcB9v72CxTKoLA7QEL6JznELe5OTWLfDlxKnXmP27g+84KPdxYg8VatdLkELBNkAAypE z0vA== X-Gm-Message-State: ALQs6tD5jFBHkLLBA/ypys+sjtree+FT3w4RwOO1wajdUr6HNJXa5r/S 2OMDdoRqKvUUD5rm0KYYg3sRbWcVaskH960a9w8= X-Received: by 10.176.26.146 with SMTP id j18mr21183039uai.4.1525445263154; Fri, 04 May 2018 07:47:43 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.80.93 with HTTP; Fri, 4 May 2018 07:47:42 -0700 (PDT) In-Reply-To: References: From: =?UTF-8?Q?Ansten_M=C3=B8rch_Klev?= Date: Fri, 4 May 2018 16:47:42 +0200 Message-ID: Subject: =?UTF-8?B?UmU6IFtIb1RUXSBNYXJ0aW4tTMO2ZiAnODY=?= To: Colin Zwanziger , homotopyt...@googlegroups.com Content-Type: multipart/alternative; boundary="f403045e6cba08e23a056b626760" --f403045e6cba08e23a056b626760 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=C3=B6f type theory. A good published refe= rence for this is the chapter by Nordstr=C3=B6m, 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=C3=B6f". Ansten Klev On Thu, Apr 26, 2018 at 8:56 PM, Colin Zwanziger wrote: > Dear all, > > Does anyone happen to have a copy of the work > > Martin-L=C3=B6f, P. (1986). Amendment to intuitionistic type theory. *Not= es > from a lecture given in G=C3=B6teborg*. > > 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. > --f403045e6cba08e23a056b626760 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In light of the title and date of this lecture it is natur= al to think that it presented the hierarchy of higher types, what is also s= ometimes called the logical framework of Martin-L=C3=B6f type theory. A goo= d published reference for this is the chapter by Nordstr=C3=B6m, Petersson,= and Smith in vol 5 of the Handbook of Logic in Computer Science. For the t= reatment of Pi, which here allows for an induction principle, see also chap= ter 7 of the book by the same authors and Garner's paper "On the s= trength of dependent products in the type theory of Martin-L=C3=B6f".= =C2=A0

Ansten Klev=C2=A0
=
On Thu, Apr 26, 2018 at 8:56 PM, Colin Zwanz= iger <zwanz...@gmail.com> wrote:
Dear all,

Does an= yone happen to have a copy of the work

Martin-L=C3=B6f, P. (1986). A= mendment to intuitionistic type theory. Notes from a lecture given in G= =C3=B6teborg.

that they could share? Or advice on how to o= btain a copy?

Best regards,

Colin Zwanziger
<= /span>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--f403045e6cba08e23a056b626760--