From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1f:3283:: with SMTP id y125-v6mr14182536vky.34.1525471029978; Fri, 04 May 2018 14:57:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.176.17.213 with SMTP id q21ls2963062uac.16.gmail; Fri, 04 May 2018 14:57:09 -0700 (PDT) X-Received: by 10.176.73.169 with SMTP id e38mr14141510uad.3.1525471029320; Fri, 04 May 2018 14:57:09 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525471029; cv=none; d=google.com; s=arc-20160816; b=LX1V6R7V15wAypGePy+xeinCeDvIAIfwJ3wan7lF8kcCRu2LFwYZ6bQHiR3QH2gHY1 oXJrmubA1Zeo/G+PGNpdKmhFuT81UXs5YCmJOlUBH3EVWOD/Q3/Rfwbg2gef2eLDFK3B Dd7dxgpCDoS8vkLi9c3j5fFFhiq11Q3NYdMtaCoqD4Jn3o3Vqv2wDPaKMPw//H1w2Ehd /HEMsWE9xaBust6LOEtYUg2Gkdi5XweBho/WK2SmOmG3T4NRZ4MweHC0Yty3SEvdiBvU FJ+EjL2WdgS7vHPxd08pOma/3UH8GCoZq15/cYNYCL+/ln8f33bK2zQeghmQnybMAtMM ihdA== 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=dBZb6idSZqbLp7//OWUmSeKeeuRpW+iODb3/btYmnB0=; b=BIyqjHZ0KbjUgiVhnsQlZhPAV1qa7UWrpR3jDxY7B+HbN54emV7c/BKH+gyso0FGkc aFawg8T0+NhOg/z+zIcJv6aoQ+5kl+ilYgZJwK6q3ZgzIjQ9FYtkTspD+jrCYv40qcsb MD02vkAQnaxvS3kwpa4fE4jMGLkAE6N5Nbf3Oz8PUj0UveXNpcEEfgV3j0a705I0ldhZ XmvYfrAbXDlUF9Tb2Y6Vamd1n2QPc9UX3uE5E9vqhYT6Lw8/GTEaeO3/wOL0AkUCn/ZG qIzo2hqL+09W1y9kgVQaDFgwowoRAVYi1xIhjg9lf9XaEQu1P5xRB5nE42t8ezDUy7fK UYAg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=PrUxNYXr; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22c 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-x22c.google.com (mail-yb0-x22c.google.com. [2607:f8b0:4002:c09::22c]) by gmr-mx.google.com with ESMTPS id g48si509663uaa.5.2018.05.04.14.57.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 14:57:09 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22c as permitted sender) client-ip=2607:f8b0:4002:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=PrUxNYXr; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c09::22c 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-x22c.google.com with SMTP id y5-v6so8178051ybg.0 for ; Fri, 04 May 2018 14:57:09 -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=dBZb6idSZqbLp7//OWUmSeKeeuRpW+iODb3/btYmnB0=; b=PrUxNYXrjIPITxTXi0CXHwlh0VG00XAPGxHeT4WF/7D1X4iy5Viz6xanypL4XRlAcW y4qa4kKSeLP4fUN9peFgeqNfTtrM6LZExTiVxATG+PAExHP+HFuW+EGNwniT6KvzgkMY qE8xW824kKKWVnKb7AveXOHlujg+m1DSW+7EDHi+hdj1AwvNcPiSKl8HEmLif1xmCvLH V1cg8GJy2LFjGfuudX/erXwruLKAauVX6t38bUwFGW1Bo6NNHFX423/FlLNrcpr3rVOK rCEagnNJo0oXIRZwMXyqV1st8EJ842TmQXx6aaaXfpZb+Rw1yfxEr+NIM3Af8C8DSnAs yBMw== X-Gm-Message-State: ALKqPwfHHaEkk2yI8WDYMKNNv8N0VTcN6MpHN4V0NEJKt3BGNcqrLA+S joNj4WYYMulv8iFsL5Xu2w2c+SskAnUGe2GsJr8= X-Received: by 2002:a25:d2d4:: with SMTP id j203-v6mr694745ybg.135.1525471028925; Fri, 04 May 2018 14:57:08 -0700 (PDT) MIME-Version: 1.0 Received: by 10.129.46.151 with HTTP; Fri, 4 May 2018 14:56:48 -0700 (PDT) In-Reply-To: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> From: Bas Spitters Date: Fri, 4 May 2018 23:56:48 +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 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 the= m. 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 guar= ded > 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 ne= w > type of programming language, one that contains theorems, proofs, > quantifications, and implications, in addition to the more conventional > 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.