From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.176.83.70 with SMTP id y6mr22638117uay.70.1525882510598; Wed, 09 May 2018 09:15:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:2115:: with SMTP id d21-v6ls589099ual.15.gmail; Wed, 09 May 2018 09:15:09 -0700 (PDT) X-Received: by 10.159.48.28 with SMTP id h28mr23787391uab.42.1525882509748; Wed, 09 May 2018 09:15:09 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525882509; cv=none; d=google.com; s=arc-20160816; b=OEA6yCBuovxWm+tA8i0i6NNWIymioFpcNvt/jELOVduiBbRa8wgEtKwVKA93UAHhra USt/mE/pGeqPovsRmc+EhxyoTBHszorvTkTPgNq11cE8U1HerCtKUO9tIA+ZlvyjpvIt jeYxbr0HZkD3ex6kb9r8XCXAZG7YMse+bUpK4i/xRdvjYxXW0LlKLxKW6bnGI3UhpOJG UrijwRW04vIL7VAmO22MCXpq7Hil5AwC7X3xodkt60mOShF2jRMSwg0tzZTLP+eHizyx ItenV8f94TA7w+OR8g4ckxjYBWSm03xqS9RIGOMcupOiRVp8u+6EaBZ1yEXg0pNpxEIl 1EEw== 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=zKSIJL7gwiHgVLWQaamA33V5OJWYn9tTdAKPpHzY7EU=; b=j1Tx5MhOPZZhWaUjyR7sWk8dWOMKpWHnMoPXTuOeDArNaEx3YeJGLonJ141tJrJKRd zi8KuXcmZD2BNPomHkF5TS+jp0bCeFYHylEmYC4svNUPI2C21T5y2rpiUs6NfgopXoVu O3bG+Gy+HJk4kDDs/UrEL/XXa1si075RF6ynOmK3TH/GjGakbV/WF4uI6KJWbeLS7+my cQc0R02c208YXFXP9EBDi1AYPIP2TeiMSU6Ue7kRovdU3hpnGlnbZQb3RgutEw0Kh6eS qN828VSHgZ91LxrJgicFaFHWfS+sg2WjaEHwWlzW4JSXwY0wueHk8nlnFTkdauRSB+B+ kcQA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=EBJ8WnYn; spf=neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x232.google.com (mail-yb0-x232.google.com. [2607:f8b0:4002:c09::232]) by gmr-mx.google.com with ESMTPS id 80-v6si2265180vkf.4.2018.05.09.09.15.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 09 May 2018 09:15:09 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::232; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=EBJ8WnYn; spf=neutral (google.com: 2607:f8b0:4002:c09::232 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x232.google.com with SMTP id y5-v6so12540592ybg.0 for ; Wed, 09 May 2018 09:15:09 -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=zKSIJL7gwiHgVLWQaamA33V5OJWYn9tTdAKPpHzY7EU=; b=EBJ8WnYnTi5rjo6poSbYAEiQGTDp6zUd3IsF56KznFiZzd54KTaHbiwcGh8aa54tt/ xRO6gvA+r1aPJvnaslIAvKPUw+FEU9oYXrf1GZywEz2w6pTblWktLH40dSTaIU81IfJV Al2a8HVfHyZWNKt2Q6KGUFDiZDwQAcN/eaqGhndNZG60Sa9HKNH/DUGgFqp/rEZ77aKc 4KNdltPPuCbUVT5HCQLipDP3zwU8LBYND3gcaBey6l+G4wzLiXvoSWzwjGfDR+tishas F0iEkFE8Opjq39MwGDrECwza5JRhwTULXK5YeC6Ycz7BpHVrWJcuw1se3GGSABLZ61Sr +VcQ== X-Gm-Message-State: ALKqPwcW2bJysxEqN8yqP73Kql03mOXOPn+LkmpfRQJorwSn5/XV6M/n JFKl4xaFEvRgt5y8s/xnZe8TdyQY X-Received: by 2002:a25:d44f:: with SMTP id m76-v6mr1070339ybf.165.1525882509209; Wed, 09 May 2018 09:15:09 -0700 (PDT) Return-Path: Received: from mail-yb0-f174.google.com (mail-yb0-f174.google.com. [209.85.213.174]) by smtp.gmail.com with ESMTPSA id q127-v6sm6412876ywb.90.2018.05.09.09.15.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 09 May 2018 09:15:08 -0700 (PDT) Received: by mail-yb0-f174.google.com with SMTP id f3-v6so4125043ybg.13 for ; Wed, 09 May 2018 09:15:08 -0700 (PDT) X-Received: by 2002:a25:e08:: with SMTP id 8-v6mr21277575ybo.71.1525882508353; Wed, 09 May 2018 09:15:08 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Wed, 9 May 2018 09:15:07 -0700 (PDT) In-Reply-To: <12f91785-ff1a-483b-92e2-c2557b5f9d61@googlegroups.com> References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <12f91785-ff1a-483b-92e2-c2557b5f9d61@googlegroups.com> From: Michael Shulman Date: Wed, 9 May 2018 09:15:07 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Bishop's work on type theory To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable You mean something like "if t:A and A=3D=3DB then t:B"? You're right; I'm not even sure how to phrase such a rule with Bishop's setup where "the" type of a term is an *operation* T(t) =3D=3D A, whereas things like beta-reduction are expressed only propositionally in terms of Leibniz equality. On 5/9/18, Matt Oliveri wrote: > There doesn't seem to be anything like a conversion rule. I suspect that = a > lot of the math examples developed in the system don't actually type chec= k. > > If they do, it would seem to be luck. Or maybe not; does anyone know some > key intuition behind this system that I'm missing? > > On Friday, May 4, 2018 at 5:01:53 PM UTC-4, Mart=C3=ADn H=C3=B6tzel Escar= d=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 secon= d >> >> paper (Algol.pdf) is this, in my opinion, because it foresees things suc= h >> >> as Agda, Coq, NuPrl, ... >> >> "The possibility of such a compilation demonstrates the existence of a n= ew >> >> 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. >