Re: [HoTT] Bishop's work on type theory

["Martín Hötzel Escardó" <"escardo..."@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 9094 bytes --]

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 <shu...@sandiego.edu <javascript:>> 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ó <escar...@gmail.com <javascript:>> 
> 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ó 
> >>> <escar...@gmail.com <javascript:>> 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ó 
> >>> >> <escar...@gmail.com> 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 
> <javascript:> 
> >>> > <javascript:>. 
> >>> > 
> >>> > 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 <javascript:>. 
>
> >> For more options, visit https://groups.google.com/d/optout. 
> >> 
> > 
>

[-- Attachment #1.2: Type: text/html, Size: 13632 bytes --]