Thanks, Mike, for reporting your analysis of the paper. I didn't reply earlier because we had a very intensive week with the summer school here at the Hausdorff institute. It seems that this is a sort of two-level type theory, with a logic on top of a formalism for types. (One thing that one should always have in mind is that these two papers were not published. I have lots of private files with tentative ideas, which I wish that if they are ever seen after I die then they will be taken as such - tentative ideas.) I like seeing Bishop offering ideas on what formalism would reflect his thinking. But most of all I like his conviction that "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" as I said before. I am not sure one can use these two papers as a definitive source to try to understand his original, informal "Foundations of constructive analysis". I would guess *not*. Martin On Saturday, 5 May 2018 06:27:29 UTC+2, Michael Shulman wrote: > > 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ín Hötzel Escardó > > wrote: > >> (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ín Hötzel Escardó > >>> > wrote: > >>> > Hi Bas, > >>> > > >>> > Perhaps, to have this in context, we could add it to e.g. the HoTT > web > >>> 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 > at > >>> 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 > 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ín Hötzel Escardó > >>> >> 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 > 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. > >>> > >> > >> -- > >> 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. > >> > > >