From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:381d:: with SMTP id f29-v6mr6143912pga.69.1525494449936; Fri, 04 May 2018 21:27:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:bf41:: with SMTP id u1-v6ls7161977pls.7.gmail; Fri, 04 May 2018 21:27:28 -0700 (PDT) X-Received: by 2002:a17:902:1763:: with SMTP id i90-v6mr7822122pli.10.1525494448504; Fri, 04 May 2018 21:27:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1525494448; cv=none; d=google.com; s=arc-20160816; b=UpVPMZhwfDqCUN6ovTGZOTIj5UmTL/5cQ/4f7VzKA7HmsbOifOuYRY5rqU4fdFh9Ly bj6iEXCZ+9iV6c6AOkhgfuRCwUppxxOKyCfAtyhE/YGtXJW3MnXU9YEsQs8WP2d+7BmL Tc0TFIu1NlGFgSk/6cKkyyZgIbDRVrsZsPQm48SwHsWrr41J40L3fqnYEd07ntcOqsC7 +g4YISekcZ+4xK9X/AaSIBTv6ypIULurT6QFUeYqCgB6pCoi+YY8moQdNlzWXff8Cd98 PgRVlLyxWCCXsIMuTWfzDGOGcVSzIBy89xD4vYKiZ/TqiHBmEVhrCAooObFR7mURQyIu 8hEQ== 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=2YywMT/xKV6RKPRXHf4xBoY5T3QUUlXlhP/dPEalFJQ=; b=KALXoH3OI+Zmw9S1es2mkv3XuQ5aTbAt2jFbg3seVexz1aKNmwwmdK6vWfTzRDgclK LwxLssmUd3oHu7/fg+Ex77YdZoIUydG7dQd/kXOJ/lRkyLLoONHkyQaAzZu7kl3nta22 euJA1AErH3gjhROwR+Si2nZaS1S+7fYfb6gAoMmQGpT5xN0pFJbTkMlCNV01jrIjPhUq hu893qFJz6R9Ivd5vH590AAL0WY7xGbEiW2CHi5bQXwTertIFdz1I0KcRxB1Wx70bHP7 /Hy+pqN7gfGCPYQPB8uwd9+k1S1zyXwT4OqhXBJrFOITqo9VHUebGEJ31OIm55noVjKy TTMQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZXuvzjWT; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu 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 h10-v6si1289944plr.3.2018.05.04.21.27.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 21:27:28 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ZXuvzjWT; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22c.google.com with SMTP id x145-v6so7520935ybg.10 for ; Fri, 04 May 2018 21:27:28 -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=2YywMT/xKV6RKPRXHf4xBoY5T3QUUlXlhP/dPEalFJQ=; b=ZXuvzjWTAFgx6dKfvQJ9NZe7HjVjDSY9OIsEWKLsDaMzGkabEl2tLtCMdVtLeZpuqY 8ErBcaYrp79PI9L4GlogNuYdedhA8utE7cuV0UJUCkykwgNOg9UA7MCCra5EUHCnFzEB eru9I3/un9v9CDR+OOI15pJOLaB6Jhpgxxk/sFZLUAu1yi054il9kyYsxUzxl2sZ8GU4 O1xRi/3Nbbte4NeAE0uQendru4nKrFgWojYVsLVFawy+l4vFK1VMcfDguAw/TWgNe6k5 MCxuUEGRKZ8EBiPee+LM3oRwmA7ET7FC/doLw2QxiXDsv8G9AH02XoglZAGiYdydnY+E a/Kg== X-Gm-Message-State: ALQs6tD3QbmPZjqo5F3KGGaUXmjACAKBZcC3Jnd8sWvlflTEqjZCG7fr 8pwp/N1cVgb2to7AgISIX3wWDGKa X-Received: by 2002:a25:2508:: with SMTP id l8-v6mr16546471ybl.505.1525494447482; Fri, 04 May 2018 21:27:27 -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 k22-v6sm8251929ywe.60.2018.05.04.21.27.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 04 May 2018 21:27:27 -0700 (PDT) Received: by mail-yb0-f174.google.com with SMTP id f138-v6so725356yba.6 for ; Fri, 04 May 2018 21:27:26 -0700 (PDT) X-Received: by 2002:a5b:108:: with SMTP id 8-v6mr2343283ybx.292.1525494446424; Fri, 04 May 2018 21:27:26 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d297:0:0:0:0:0 with HTTP; Fri, 4 May 2018 21:27:25 -0700 (PDT) In-Reply-To: References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> <385f5d47-0656-4a4d-b24c-c2abeab629e7@googlegroups.com> From: Michael Shulman Date: Fri, 4 May 2018 21:27:25 -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 I have now had a chance to read over the first manuscript more carefully. It is quite fascinating! I think that in modern language, his system would be called a higher-order logic over a dependent type theory. There are some warts from a modern perspective, but I think it's quite astonishing how close Bishop's system is to modern dependent type theories and higher-order logics, if in fact there was historically no communication. What nowadays we call "types", Bishop calls "classes"; and what we call "functions" between types he calls "operations". He has "power-classes" and "subclasses" which behave roughly like power-types and sub-types in higher-order logic, along with a separate logic of formulas that depend on classes. In particular, propositions are, as far as I can tell, proof-irrelevant, and *not* identified with types! He uses the Leibniz equality of HOL (two terms are equal if they satisfy the same predicates) to formulate the beta and eta rules for his Pi, Sigma, etc. classes, and includes (p26) the function extensionality and propositional extensionality axioms again using this Leibniz equality. Some other interesting notes about Bishop's system: 1. He has a class of all classes. I think this means his system is vulnerable to Girard's paradox and hence inconsistent. This is amusing given his remark (p15) that "A contradiction would be just an indication that we were indulging in meaningless formalism," although to be fair he also says later (p26) that "If aspects of the formalization are meaningless, experience will sooner or later let us know." Of course, this should be fixable as usual by introducing a hierarchy of universes. 2. His "sets" (p16) are classes (types) equipped with an equivalence relation valued in *propositions* (more precisely, equipped with a subclass of A x A satisfying reflexivity, symmetry, and transitivity). So they are like setoids defined in Coq with Prop-valued equality (where Prop satisfies propositional extensionality), not setoids defined in MLTT with Type-valued equality. 3. He includes the axiom of choice (p12) formulated in terms of his (proof-irrelevant) propositions, as well as what seems to be a Hilbert choice operator (though it's not clear to me whether this applies in open contexts or not). Since he has powerclasses with propositional extensionality, I think this means that Diaconescu's argument proves LEM, which he obviously wouldn't want. It's harder for me to guess how this should be fixed, since without some kind of AC, setoids don't satisfy the principle of unique choice. 4. He makes the class of all sets into a set (p19) with equality meaning the mere existence of an isomorphism. But later (p21) he refers to this set more properly as the set of "cardinal numbers". 5. He also defines a category (p19) to have a class of objects (no equality relation imposed) and dependent *sets* (classes with equality relation) of morphisms between any two objects. 6. As we did informally in the HoTT Book, he first introduces non-dependent function types and then formulates dependent ones (which he calls "guarded") in terms of a type family expressed as a non-dependent function into the universe (rather than as a type expression containing a variable). It's quite possible, though, that I am misinterpreting some or all of this; his notation is so different that it's easy to get confused. If so, I hope someone will set me straight. On 5/4/18, Michael Shulman wrote: > Right, the question more precisely is whether, when transported along > whatever isomorphism there is between Bishop's "general language" and > MLTT (I have not read the manuscript yet to understand this), the > "sets" defined by Bishop on p16 coincide with Hofmann's setoids. If > so, then it would be some substantial additional evidence for the > claim that setoids are "what Bishop really meant". > > On 5/4/18, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wr= ote: >> (I know that, and probably Mike knows that too. Martin) >> >> On Saturday, 5 May 2018 00:12:51 UTC+2, Bas Spitters wrote: >>> >>> 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 we= b >>> page >>> > 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 a= t >>> least >>> > 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 not= e >>> >> 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 >>> conventional >>> >> > facilities for specifying algorithms" >>> >> > >>> >> > This was in the late 1960's (or correct me). Here is a link to bot= h >>> >> > 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, sen= d >>> an >>> > email to HomotopyTypeThe...@googlegroups.com >>> > . >>> > >>> > For more options, visit https://groups.google.com/d/optout. >>> >> >> -- >> 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. >> >