From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Wed, 9 May 2018 15:27:17 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <3b661da9-52d2-43b0-b346-902e610a3057@googlegroups.com> 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> Subject: Re: [HoTT] Bishop's work on type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_101_906004061.1525904837847" ------=_Part_101_906004061.1525904837847 Content-Type: multipart/alternative; boundary="----=_Part_102_135139987.1525904837848" ------=_Part_102_135139987.1525904837848 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thanks, Mike, for reporting your analysis of the paper. I didn't reply=20 earlier because we had a very intensive week with the summer school here at= =20 the Hausdorff institute. It seems that this is a sort of two-level type=20 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=20 were not published. I have lots of private files with tentative ideas,=20 which I wish that if they are ever seen after I die then they will be taken= =20 as such - tentative ideas.) I like seeing Bishop offering ideas on what formalism would reflect his=20 thinking. But most of all I like his conviction that=20 "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= =20 understand his original, informal "Foundations of constructive analysis". I= =20 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=20 > carefully. It is quite fascinating! I think that in modern language,=20 > his system would be called a higher-order logic over a dependent type=20 > theory. There are some warts from a modern perspective, but I think=20 > it's quite astonishing how close Bishop's system is to modern=20 > dependent type theories and higher-order logics, if in fact there was=20 > historically no communication.=20 > > What nowadays we call "types", Bishop calls "classes"; and what we=20 > call "functions" between types he calls "operations". He has=20 > "power-classes" and "subclasses" which behave roughly like power-types=20 > and sub-types in higher-order logic, along with a separate logic of=20 > formulas that depend on classes. In particular, propositions are, as=20 > far as I can tell, proof-irrelevant, and *not* identified with types!=20 > He uses the Leibniz equality of HOL (two terms are equal if they=20 > satisfy the same predicates) to formulate the beta and eta rules for=20 > his Pi, Sigma, etc. classes, and includes (p26) the function=20 > extensionality and propositional extensionality axioms again using=20 > this Leibniz equality.=20 > > Some other interesting notes about Bishop's system:=20 > > 1. He has a class of all classes. I think this means his system is=20 > vulnerable to Girard's paradox and hence inconsistent. This is=20 > amusing given his remark (p15) that "A contradiction would be just an=20 > indication that we were indulging in meaningless formalism," although=20 > to be fair he also says later (p26) that "If aspects of the=20 > formalization are meaningless, experience will sooner or later let us=20 > know." Of course, this should be fixable as usual by introducing a=20 > hierarchy of universes.=20 > > 2. His "sets" (p16) are classes (types) equipped with an equivalence=20 > relation valued in *propositions* (more precisely, equipped with a=20 > subclass of A x A satisfying reflexivity, symmetry, and transitivity).=20 > So they are like setoids defined in Coq with Prop-valued equality=20 > (where Prop satisfies propositional extensionality), not setoids=20 > defined in MLTT with Type-valued equality.=20 > > 3. He includes the axiom of choice (p12) formulated in terms of his=20 > (proof-irrelevant) propositions, as well as what seems to be a Hilbert=20 > choice operator (though it's not clear to me whether this applies in=20 > open contexts or not). Since he has powerclasses with propositional=20 > extensionality, I think this means that Diaconescu's argument proves=20 > LEM, which he obviously wouldn't want. It's harder for me to guess=20 > how this should be fixed, since without some kind of AC, setoids don't=20 > satisfy the principle of unique choice.=20 > > 4. He makes the class of all sets into a set (p19) with equality=20 > meaning the mere existence of an isomorphism. But later (p21) he=20 > refers to this set more properly as the set of "cardinal numbers".=20 > > 5. He also defines a category (p19) to have a class of objects (no=20 > equality relation imposed) and dependent *sets* (classes with equality=20 > relation) of morphisms between any two objects.=20 > > 6. As we did informally in the HoTT Book, he first introduces=20 > non-dependent function types and then formulates dependent ones (which=20 > he calls "guarded") in terms of a type family expressed as a=20 > non-dependent function into the universe (rather than as a type=20 > expression containing a variable).=20 > > It's quite possible, though, that I am misinterpreting some or all of=20 > this; his notation is so different that it's easy to get confused. If=20 > so, I hope someone will set me straight.=20 > > > > On 5/4/18, Michael Shulman > wrote:=20 > > Right, the question more precisely is whether, when transported along= =20 > > whatever isomorphism there is between Bishop's "general language" and= =20 > > MLTT (I have not read the manuscript yet to understand this), the=20 > > "sets" defined by Bishop on p16 coincide with Hofmann's setoids. If=20 > > so, then it would be some substantial additional evidence for the=20 > > claim that setoids are "what Bishop really meant".=20 > >=20 > > On 5/4/18, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 >=20 > wrote:=20 > >> (I know that, and probably Mike knows that too. Martin)=20 > >>=20 > >> On Saturday, 5 May 2018 00:12:51 UTC+2, Bas Spitters wrote:=20 > >>>=20 > >>> Setoids were introduced by Martin Hofmann is his PhD-thesis. They wer= e=20 > >>> "inspired" by Bishop; see p8:=20 > >>> www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LFCS-95-327.ps= =20 > >>>=20 > >>> On Sat, May 5, 2018 at 12:04 AM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3= =20 > >>> > wrote:=20 > >>> > Hi Bas,=20 > >>> >=20 > >>> > Perhaps, to have this in context, we could add it to e.g. the HoTT= =20 > web=20 > >>> page=20 > >>> > and/or the nlab.=20 > >>> >=20 > >>> > Do you know precise dates for these manuscripts?=20 > >>> >=20 > >>> > I am looking forward to seeing you in Bonn.=20 > >>> >=20 > >>> > Also, it would be nice to have Mike Shulman's questions answered or= =20 > at=20 > >>> least=20 > >>> > addressed.=20 > >>> >=20 > >>> > Martin=20 > >>> >=20 > >>> > On Friday, 4 May 2018 23:57:09 UTC+2, Bas Spitters wrote:=20 > >>> >>=20 > >>> >> Hi Martin,=20 > >>> >>=20 > >>> >> These were discussed publically at some point. I've got them at=20 > >>> >> around=20 > >>> >>=20 > >>> >> 2000.=20 > >>> >> We never put them on the web, because Bishop had decided not to=20 > >>> >> publish=20 > >>> >>=20 > >>> >> them.=20 > >>> >> Since you are doing this now, it might be good to at least add a= =20 > note=20 > >>> >> to that respect, so that people can put them in context.=20 > >>> >>=20 > >>> >> See you in Bonn!=20 > >>> >>=20 > >>> >> Bas=20 > >>> >>=20 > >>> >> On Fri, May 4, 2018 at 11:01 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3= =B3=20 > >>> >> wrote:=20 > >>> >> > This week I learned two interesting things that seem to be kept= =20 > as=20 > >>> >> > a=20 > >>> >> >=20 > >>> >> > guarded=20 > >>> >> > secret:=20 > >>> >> >=20 > >>> >> > (1) Errett Bishop reinvented type theory.=20 > >>> >> > (2) He also explained how to compile it to Algol.=20 > >>> >> >=20 > >>> >> > I am adding a link to these two manuscripts. A nice quote from= =20 > the=20 > >>> >> > second=20 > >>> >> > paper (Algol.pdf) is this, in my opinion, because it foresees=20 > >>> >> > things=20 > >>> >> >=20 > >>> >> > such as=20 > >>> >> > Agda, Coq, NuPrl, ...=20 > >>> >> >=20 > >>> >> > "The possibility of such a compilation demonstrates the existenc= e=20 > >>> >> > of=20 > >>> >> >=20 > >>> a=20 > >>> >> > new=20 > >>> >> > type of programming language, one that contains theorems, proofs= ,=20 > >>> >> > quantifications, and implications, in addition to the more=20 > >>> conventional=20 > >>> >> > facilities for specifying algorithms"=20 > >>> >> >=20 > >>> >> > This was in the late 1960's (or correct me). Here is a link to= =20 > both=20 > >>> >> > manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/=20 > >>> >> >=20 > >>> >> > Greetings from Bonn.=20 > >>> >> > Martin=20 > >>> >>=20 > >>> > --=20 > >>> > You received this message because you are subscribed to the Google= =20 > >>> Groups=20 > >>> > "Homotopy Type Theory" group.=20 > >>> > To unsubscribe from this group and stop receiving emails from it,= =20 > send=20 > >>> an=20 > >>> > email to HomotopyTypeThe...@googlegroups.com=20 > =20 > >>> > .=20 > >>> >=20 > >>> > For more options, visit https://groups.google.com/d/optout.=20 > >>>=20 > >>=20 > >> --=20 > >> You received this message because you are subscribed to the Google=20 > Groups=20 > >> "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= =20 > an=20 > >> email to HomotopyTypeThe...@googlegroups.com .=20 > > >> For more options, visit https://groups.google.com/d/optout.=20 > >>=20 > >=20 > ------=_Part_102_135139987.1525904837848 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Thanks, Mike, for reporting your analysis of the paper. I = didn't reply earlier because we had a very intensive week with the summ= er 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 t= wo papers were not published. I have lots of private files with tentative i= deas, which I wish that if they are ever seen after I die then they will be= taken as such - tentative ideas.)

I like seeing B= ishop offering ideas on what formalism would reflect his thinking. But most= of all I like his conviction that=C2=A0

=C2= =A0"The possibility of such a compilation demonstrates the
= =C2=A0 existence of a new type of programming language, one that
= =C2=A0 contains theorems, proofs, quantifications, and implications,
<= div>=C2=A0 in addition to the more conventional facilities for specifying
=C2=A0 algorithms"

as I said b= efore.

I am not sure one can use these two papers = as a definitive source to try to understand his original, informal "Fo= undations 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. =C2=A0It is quite fascinating! =C2=A0I think that in modern = language,
his system would be called a higher-order logic over a dependent type
theory. =C2=A0There are some warts from a modern perspective, but I thi= nk
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&quo= t;; and what we
call "functions" between types he calls "operations"= ;. =C2=A0He has
"power-classes" and "subclasses" which behave rough= ly like power-types
and sub-types in higher-order logic, along with a separate logic of
formulas that depend on classes. =C2=A0In 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. =C2=A0I think this means his system i= s
vulnerable to Girard's paradox and hence inconsistent. =C2=A0This i= s
amusing given his remark (p15) that "A contradiction would be just= an
indication that we were indulging in meaningless formalism," altho= ugh
to be fair he also says later (p26) that "If aspects of the
formalization are meaningless, experience will sooner or later let us
know." =C2=A0Of course, this should be fixable as usual by introdu= cing a
hierarchy of universes.

2. His "sets" (p16) are classes (types) equipped with an equi= valence
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 i= n
open contexts or not). =C2=A0Since he has powerclasses with proposition= al
extensionality, I think this means that Diaconescu's argument prove= s
LEM, which he obviously wouldn't want. =C2=A0It's harder for me= to guess
how this should be fixed, since without some kind of AC, setoids don= 9;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. =C2=A0But later (p21) he
refers to this set more properly as the set of "cardinal numbers&q= uot;.

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. = =C2=A0If
so, I hope someone will set me straight.



On 5/4/18, Michael Shulman <shu...@sandiego.edu> wrote:
> Right, the question more precisely is whether, when transported al= ong
> whatever isomorphism there is between Bishop's "general l= anguage" and
> MLTT (I have not read the manuscript yet to understand this), the
> "sets" defined by Bishop on p16 coincide with Hofmann= 9;s setoids. =C2=A0If
> 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 <escar...@gmail.com<= /a>> 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-thesi= s. They were
>>> "inspired" by Bishop; see p8:
>>> www.lfcs.inf.ed.ac.uk/reports/95/ECS-LFCS-95-327/ECS-LF= CS-95-327.ps
>>>
>>> On Sat, May 5, 2018 at 12:04 AM, Mart=C3=ADn H=C3=B6tzel E= scard=C3=B3
>>> <escar...@gmail.com <javascript:>> wrot= e:
>>> > 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 que= stions answered or at
>>> least
>>> > addressed.
>>> >
>>> > Martin
>>> >
>>> > On Friday, 4 May 2018 23:57:09 UTC+2, Bas Spitters wr= ote:
>>> >>
>>> >> Hi Martin,
>>> >>
>>> >> These were discussed publically at some point. I&= #39;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 c= ontext.
>>> >>
>>> >> See you in Bonn!
>>> >>
>>> >> Bas
>>> >>
>>> >> On Fri, May 4, 2018 at 11:01 PM, Mart=C3=ADn H=C3= =B6tzel Escard=C3=B3
>>> >> <escar...@gmail.com> wrote:
>>> >> > This week I learned two interesting things t= hat seem to be kept as
>>> >> > a
>>> >> >
>>> >> > guarded
>>> >> > secret:
>>> >> >
>>> >> > (1) Errett Bishop reinvented type theory.
>>> >> > (2) He also explained how to compile it to A= lgol.
>>> >> >
>>> >> > I am adding a link to these two manuscripts.= A nice quote from the
>>> >> > second
>>> >> > paper (Algol.pdf) is this, in my opinion, be= cause 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 conta= ins theorems, proofs,
>>> >> > quantifications, and implications, in additi= on 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: HomotopyTypeTheory+unsub...@googlegroups.com=
>>> > <javascript:>.
>>> >
>>> > For more options, visit http= s://groups.google.com/d/optout.
>>>
>>
>> --
>> You received this message because you are subscribed to the Go= ogle Groups
>> "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from = it, send an
>> email to HomotopyTypeTheory+unsub...@googlegroups.com.
>> For more options, visit https://group= s.google.com/d/optout.
>>
>
------=_Part_102_135139987.1525904837848-- ------=_Part_101_906004061.1525904837847--