From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 4 May 2018 15:04:12 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> In-Reply-To: References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> Subject: Re: [HoTT] Bishop's work on type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_8268_729267931.1525471452437" ------=_Part_8268_729267931.1525471452437 Content-Type: multipart/alternative; boundary="----=_Part_8269_826849342.1525471452437" ------=_Part_8269_826849342.1525471452437 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Hi Bas, Perhaps, to have this in context, we could add it to e.g. the HoTT web page= =20 and/or the nlab.=20 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=20 least addressed. Martin On Friday, 4 May 2018 23:57:09 UTC+2, Bas Spitters wrote: > > Hi Martin,=20 > > These were discussed publically at some point. I've got them at around=20 > 2000.=20 > We never put them on the web, because Bishop had decided not to publish= =20 > them.=20 > Since you are doing this now, it might be good to at least add a note=20 > to that respect, so that people can put them in context.=20 > > See you in Bonn!=20 > > Bas=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 as a=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 the=20 > second=20 > > paper (Algol.pdf) is this, in my opinion, because it foresees things=20 > such as=20 > > Agda, Coq, NuPrl, ...=20 > >=20 > > "The possibility of such a compilation demonstrates the existence of a= =20 > new=20 > > type of programming language, one that contains theorems, proofs,=20 > > quantifications, and implications, in addition to the more conventional= =20 > > facilities for specifying algorithms"=20 > >=20 > > This was in the late 1960's (or correct me). Here is a link to both=20 > > manuscripts: http://www.cs.bham.ac.uk/~mhe/Bishop/=20 > >=20 > > Greetings from Bonn.=20 > > Martin=20 > > ------=_Part_8269_826849342.1525471452437 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi Bas,

Perhaps, to have this in contex= t, we could add it to e.g. the HoTT web page and/or the nlab.=C2=A0

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 answ= ered or at least addressed.

Martin

On Frida= y, 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 aro= und 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=C3=ADn H=C3=B6tzel Escard=C3=B3
<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 thin= gs such as
> Agda, Coq, NuPrl, ...
>
> "The possibility of such a compilation demonstrates the exist= ence of a new
> type of programming language, one that contains theorems, proofs,
> quantifications, and implications, in addition to the more convent= ional
> 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.a= c.uk/~mhe/Bishop/
>
> Greetings from Bonn.
> Martin

------=_Part_8269_826849342.1525471452437-- ------=_Part_8268_729267931.1525471452437--