From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.24.87 with SMTP id j23mr13391060uag.56.1525468758839; Fri, 04 May 2018 14:19:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:8bc7:: with SMTP id n190-v6ls12352768vkd.18.gmail; Fri, 04 May 2018 14:19:18 -0700 (PDT) X-Received: by 2002:a1f:2fd3:: with SMTP id v202-v6mr14479362vkv.53.1525468758074; Fri, 04 May 2018 14:19:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525468758; cv=none; d=google.com; s=arc-20160816; b=KxOSb5uDf/fg9lets6uW4jkOlxQEj+FKsTFlIWlJD9R+qH06qzqHCAM7vfej0k9TNY SjVRCWCYKdwtekNYFF1w+ZhgZZNn2tdK7CstK7ZWOLMn2WVDTEr36dtuZczJvN1k7q5n SYFA1eiujI1dV67V7KUrLIJ404uaYZerMPTIiPMsa8vxgJQrKoXQM/vkuBoXqRO1W+w+ TnjwNvGXIQBJudoU1Z2jl096aKcpd3sYx7nlDVvAmnCmMYhCIdfQezIN9WNH3LYEmwxG AWeiARF6sp1IWgrGT2K0qSfaBrLu4RTAt0Ll5yMsQozF8qQ6hPPQLQj1f2yDgTuK8YlI rtAA== 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=Q8oo5cUDqTW6yeZFMfcbB2cd5rU0jVeh1exwn0EMRUY=; b=zgvtd6v3PfRbkzUIj9kYC9o9vgfwnJq8LJv8NswU8R707XQw6KsN0uQdv8L5kbLtj7 uuVCzaBP5vL/FgoSKnhHXH/IKLtAM2aJrOruIDVo4yXR4GWv0xpXeQ/+bBdFJ5WcZIRq PAwYYcGJQtyt8TgP7jdIDHkgxbt1vBXMYLeTnRN7gt8bBfDyu0ZHZXPZz5UYZf6aJI2l ZNyoHgnXbjh7he0pmNGbVgum2YGDpNL5oaju/Q8XinLjS1IqjY2vsaDWJHhITZtBhOKl bfEArWQpVZo3wHIw+2kci5/nKkKFFvUXmM4GiWPWRQNk5D1jXMGuZmid3FL1obpUZz4w HTmA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=RQcx3rG0; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x232.google.com (mail-yw0-x232.google.com. [2607:f8b0:4002:c05::232]) by gmr-mx.google.com with ESMTPS id q145-v6si1415471vka.0.2018.05.04.14.19.17 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 14:19:17 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=RQcx3rG0; spf=neutral (google.com: 2607:f8b0:4002:c05::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x232.google.com with SMTP id z198-v6so2863258ywa.2 for ; Fri, 04 May 2018 14:19:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=Q8oo5cUDqTW6yeZFMfcbB2cd5rU0jVeh1exwn0EMRUY=; b=RQcx3rG036ct75CV6w80GhcPPGCZOQoKZCIckZsjnPTjPiw2ayi7PxG5zkeG1q4scS EawBMLfuxHE6/PCRz1VkfbTLi1erO8O/EC9SgYIesYnDA+Y7Qn6JZjonhCofbtimHi8N jxokKajYh5PaQd1hJNgreamE8qjW3e3irIlui/5fnTsAvcdN9cz6A5uRUmTP50SzV/67 +XKdpp1e/P0aa0Q5qIhrSAd53GKQfA4IWPUjnmE/EmEqEuRpEFFqPvEgZINcZTegX3DL P0FI86uxp5+9pLxG1TWH9nTkbRIOJx8ykmoQ1g1mkVRyOW2Ksdb29MYMNchqS914/MLv vw1Q== X-Gm-Message-State: ALQs6tBVFZ2G/6qmfmgCCgp3tN4gaCua6DVOAVTtVLCuiyhY5NSAoQGI NwUcYlj95XcQGWvAdcXwYhhVuVy7 X-Received: by 2002:a81:28d8:: with SMTP id o207-v6mr16125828ywo.100.1525468757376; Fri, 04 May 2018 14:19:17 -0700 (PDT) Return-Path: Received: from mail-yw0-f182.google.com (mail-yw0-f182.google.com. [209.85.161.182]) by smtp.gmail.com with ESMTPSA id v125-v6sm7900371ywg.75.2018.05.04.14.19.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 14:19:16 -0700 (PDT) Received: by mail-yw0-f182.google.com with SMTP id g9-v6so7077155ywb.12 for ; Fri, 04 May 2018 14:19:16 -0700 (PDT) X-Received: by 2002:a81:8102:: with SMTP id r2-v6mr1706920ywf.272.1525468756179; Fri, 04 May 2018 14:19:16 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Fri, 4 May 2018 14:19:15 -0700 (PDT) In-Reply-To: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> From: Michael Shulman Date: Fri, 4 May 2018 14:19:15 -0700 X-Gmail-Original-Message-ID: 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 Very interesting!! I believe it's been said that Martin-Lof developed his type theory explicitly with the goal of providing a foundation for Bishop's constructive mathematics. Was he aware of these manuscripts of Bishop's at the time? Also: does this conclusively prove that Bishop's "sets" coincide with what type theorists generally call "setoids"? On 5/4/18, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrot= e: > 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 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. >