From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1f:9706:: with SMTP id z6-v6mr3448140vkd.13.1525471971236; Fri, 04 May 2018 15:12:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:1a41:: with SMTP id a62-v6ls12651294vka.19.gmail; Fri, 04 May 2018 15:12:50 -0700 (PDT) X-Received: by 2002:a1f:1055:: with SMTP id g82-v6mr14111412vki.68.1525471970551; Fri, 04 May 2018 15:12:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525471970; cv=none; d=google.com; s=arc-20160816; b=RXt6si08vnxKC1E12BezRiyGndTUH2/LvF9pASfcjWxE+POcnQw3gpELotvuRQA4WD BpbmuZuaJthinJeacu7C8rmwESBmmqOv0wgbYJYIvLBKA0dLhr9M34vMQ+tN3ZD7tGjJ g3C7ZJoZDfLEa5r2uWO7hWTqosQjglvQoEqbMgdU4sMs3pdRdY6HbEWMMgSHzFmZJJPT UCEr7XkDHEfAIjzhRGwihNasYtXoaW1K7UtRX9c0nayh1nD1jLp8wifXyaRkXizK1DPS 3YT0gOOo6hhcQGNr9o4WD0dssKadwgRzbmMbt+li9JiM+4fnz+5ofjErFUF+JkMWwcmH CqIQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=8KN6yX5TeodcmqhwBxMVS+brYbiGK7eiyoqPoj1FY14=; b=jvVKCyQ/YyCNWZ4Vi4HrcbNNb01h58QS6EjMh6xCjg0OWdQJ+jMyyYv7rlNgupmFUX 2SG6n74wDu2m/z0MlKMK4x3KLhjn5dQsGv5o3dCsU44Z6qGDlg1hopzFQ/pbG5Q6WhEt CuEYu63zlVFk/AP/xRx6pVmQC8i6+qHjDuVAmzdiejXQBSJsjeOp3/eayQRqxfwmU9FW aFnuIpJYoHjvYvtR/HcHSQxfsRBWTBA1x8dwOfN4VqXPlHk8vODJD/sR+eg72ByqZZND nMuNouh1gUxx8bBVYRg2kIAYue5nXsdiAD7FB1n/WDs3NTaJOmAPYF/zN9wK3QNbKGRT ENbw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=vLB7S5PO; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22d as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb0-x22d.google.com (mail-yb0-x22d.google.com. [2607:f8b0:4002:c09::22d]) by gmr-mx.google.com with ESMTPS id g48si512277uaa.5.2018.05.04.15.12.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 15:12:50 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22d as permitted sender) client-ip=2607:f8b0:4002:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=vLB7S5PO; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22d as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yb0-x22d.google.com with SMTP id o14-v6so8186338ybq.3 for ; Fri, 04 May 2018 15:12:50 -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:content-transfer-encoding; bh=8KN6yX5TeodcmqhwBxMVS+brYbiGK7eiyoqPoj1FY14=; b=vLB7S5POWAH0Z/oiyATUqIMREeBRbu0VG0rCMTQEw4BK90RFLeoFLTYP7KdHmV1oXU cHVy1pfwKT6GgsDHQ1n8Lxi0DabQVo5SrWwHcaM4Qkgir9JCj/2m1IJhtHpScPm1Fl80 CuqN6mXyFUOIwoSdpmioY7RHjKwpTV1TYOlUnI683kTpWf84HSk7ZCIA/noMV/JgI+pr KnSko9iHjvlQGpsgylac086onNEOnmK1NgNVqmeYvLSuRlVcNN+G2dumb5ZeMvkARBYm s+EcWLgJVzAQ1S9zbazsSK3x+lgxD+vQAWrlHeFh2Lzz8QW7O1iDGFV58CUfM/TkujpS MBtQ== X-Gm-Message-State: ALKqPwex3oFQfKfv0BV7xhpquwsBnMv3Y4Qwsu0eanM2Yj58tfr3zTne e5KVrKWiBCpSkY9nMYfi/J+3+v6sMaGihxVV/E6HjANy X-Received: by 2002:a25:d2d4:: with SMTP id j203-v6mr722570ybg.135.1525471970192; Fri, 04 May 2018 15:12:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.129.46.151 with HTTP; Fri, 4 May 2018 15:12:29 -0700 (PDT) In-Reply-To: <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> From: Bas Spitters Date: Sat, 5 May 2018 00:12:29 +0200 Message-ID: Subject: Re: [HoTT] Bishop's work on type theory To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Setoids were introduced by Martin Hofmann is his PhD-thesis. They were "inspired" by Bishop; see p8: www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LFCS-95-327.ps On Sat, May 5, 2018 at 12:04 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > Hi Bas, > > Perhaps, to have this in context, we could add it to e.g. the HoTT web pa= ge > and/or the nlab. > > Do you know precise dates for these manuscripts? > > I am looking forward to seeing you in Bonn. > > Also, it would be nice to have Mike Shulman's questions answered or at le= ast > addressed. > > Martin > > On Friday, 4 May 2018 23:57:09 UTC+2, Bas Spitters wrote: >> >> Hi Martin, >> >> These were discussed publically at some point. I've got them at around >> 2000. >> We never put them on the web, because Bishop had decided not to publish >> them. >> Since you are doing this now, it might be good to at least add a note >> to that respect, so that people can put them in context. >> >> See you in Bonn! >> >> Bas >> >> On Fri, May 4, 2018 at 11:01 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 >> wrote: >> > This week I learned two interesting things that seem to be kept as a >> > guarded >> > secret: >> > >> > (1) Errett Bishop reinvented type theory. >> > (2) He also explained how to compile it to Algol. >> > >> > I am adding a link to these two manuscripts. A nice quote from the >> > second >> > paper (Algol.pdf) is this, in my opinion, because it foresees things >> > such as >> > Agda, Coq, NuPrl, ... >> > >> > "The possibility of such a compilation demonstrates the existence of a >> > new >> > type of programming language, one that contains theorems, proofs, >> > quantifications, and implications, in addition to the more conventiona= l >> > facilities for specifying algorithms" >> > >> > This was in the late 1960's (or correct me). Here is a link to both >> > manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/ >> > >> > Greetings from Bonn. >> > Martin >> > -- > 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.