From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:78c6:: with SMTP id t189-v6mr6927349pgc.6.1525572630240; Sat, 05 May 2018 19:10:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:3545:: with SMTP id c66-v6ls4284714pga.1.gmail; Sat, 05 May 2018 19:10:29 -0700 (PDT) X-Received: by 2002:a65:5187:: with SMTP id h7-v6mr6905245pgq.57.1525572629049; Sat, 05 May 2018 19:10:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525572629; cv=none; d=google.com; s=arc-20160816; b=N4PUYSkxfEStMay2u+Tii39TYuYDnMJPP+MCnk/Ayjx5EX2HycsZMyjs0RWl5qVfTA i1tfd3SP0VHoN61QzCS76WL5qKe8HjzIwWC+f3J/TWhTUAmucLUVKrXbQc/Mt2P7Nuht gTH9Ymvbr1mZXlsaIzSkSlmmKWs+wqvN+TPCNiUM6Nhgkbd8p6OwbI9AlRxjWefollkZ +VH+R55VvIy5Yq92x3zaNnoxvwi9rhHQazOxsf/9XenpBaJPz97a9t05R8Zvx51Efphu pp5kF7oLsWfJZWDioS87rwb2uY15i6nXOfSKw8Rb4o9b7pGV0q64qBnOyGbxw4ptGYTf 5pCw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=q9cID2Wkm+42GtRe8SUWm+rE8iPNAnA/2tyGqgAE1lU=; b=Denf+bpk/9LsThhf5n/SUQn603gdXIWtoqAftwPb+5DXYMl9s+D2v+uC6yZkUJBP7e kKOKT+rsYvmmq2QQCESmLOPEbXCRLDFRqLlBFxfqV0ynqm1NfFKnoDCR8RtiDrpWmUbc 99hOhDbHDHK1B4NYGJvnabusc0xkjNPwLGOqWJmcW+b3UIeocq43udkjJTP0JgO6+VXs sSmEQbTQq6WB4W1g2ihiY3eoCfv6xN24iM9piz9/83akJdaCryDXlNzylvQI/sTeI422 QXp937g5adPUSagcAIgIaxRn30+McJFtrKAv529dX6pswqJu2Yx25FJ+PKOthQHl30EU FQDA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P14B19uh; spf=pass (google.com: domain of zwanz...@gmail.com designates 2607:f8b0:4003:c0f::243 as permitted sender) smtp.mailfrom=zwanz...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ot0-x243.google.com (mail-ot0-x243.google.com. [2607:f8b0:4003:c0f::243]) by gmr-mx.google.com with ESMTPS id o63si1359251pfg.4.2018.05.05.19.10.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 05 May 2018 19:10:29 -0700 (PDT) Received-SPF: pass (google.com: domain of zwanz...@gmail.com designates 2607:f8b0:4003:c0f::243 as permitted sender) client-ip=2607:f8b0:4003:c0f::243; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=P14B19uh; spf=pass (google.com: domain of zwanz...@gmail.com designates 2607:f8b0:4003:c0f::243 as permitted sender) smtp.mailfrom=zwanz...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-ot0-x243.google.com with SMTP id l13-v6so28484189otk.9 for ; Sat, 05 May 2018 19:10:28 -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 :cc; bh=q9cID2Wkm+42GtRe8SUWm+rE8iPNAnA/2tyGqgAE1lU=; b=P14B19uhB0v1mt7f1vtvNW0Cz3sAC5EX4JQs3ZZcHpGVwf2FePxpJHyYHYOkRdE7ok 9hs/S7JcMwqQ6V4dLaawEEfnqhIb7o4EUFxl1dZf5l1oBoitsdwr60m3GbqNCUomR389 Pj0o4VrTYwFeLeKekiiPkweFQ0sHxmn2/SBzLvVvtWthtbXtulzjd6ZfYJ5502muaBn0 cbUM8xu4hiZbmFoIRDqW8FZ8mfiHIYdBfZ4UZ1yOp+B973AW0A8AOAiOB3tg+aejYbkb 24wuYOwr8iO/qjz3Tc1noO8qXjfH9aKEHSxF7FSNigHvA+f+9PnmyjlSzYvTBU4+DSyH SwoA== X-Gm-Message-State: ALQs6tAX9rfphxtfnpxlMAlGLMaRZS3BXp+XEuDuMGpE+legrxcRfzuO kgEBkwhAcNvHMQ1rArcjA4FkX35FNmjTYA6jkBVeow== X-Received: by 2002:a9d:5c4:: with SMTP id 62-v6mr22006222otd.200.1525572628735; Sat, 05 May 2018 19:10:28 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a9d:3409:0:0:0:0:0 with HTTP; Sat, 5 May 2018 19:09:58 -0700 (PDT) In-Reply-To: References: From: Colin Zwanziger Date: Sat, 5 May 2018 22:09:58 -0400 Message-ID: Subject: =?UTF-8?B?UmU6IFtIb1RUXSBNYXJ0aW4tTMO2ZiAnODY=?= To: =?UTF-8?Q?Ansten_M=C3=B8rch_Klev?= Cc: homotopyt...@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000009d6b96056b800e74" --0000000000009d6b96056b800e74 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Yes, this was when Martin-L=C3=B6f introduced his logical framework formula= tion 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=C3=B8rch Klev wrote: > In light of the title and date of this lecture it is natural to think tha= t > 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 re= ference > 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 her= e > 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. *No= tes >> 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >> > > --0000000000009d6b96056b800e74 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Yes, this was when Martin-L=C3=B6f introduced his log= ical framework formulation of type theory. In addition, he returned to inte= nsional type theory in that lecture after some time working with extensiona= l type theory. (I was able to get a good sense of the content of the lectur= e via off-list responses.)

Best,

Colin

On Fri, May 4= , 2018 at 10:47 AM, Ansten M=C3=B8rch 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 f= ramework of Martin-L=C3=B6f type theory. A good published reference for thi= s is the chapter by Nordstr=C3=B6m, Petersson, and Smith in vol 5 of the Ha= ndbook of Logic in Computer Science. For the treatment of Pi, which here al= lows 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".=C2=A0<= font color=3D"#888888">

Ansten Klev=C2=A0

On T= hu, Apr 26, 2018 at 8:56 PM, Colin Zwanziger <zwanz...@gmail.com>= wrote:
Dear all,

Does a= nyone happen to have a copy of the work

Martin-L=C3=B6f, P. (1986). = Amendment 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

--
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.


--0000000000009d6b96056b800e74--