From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 4 May 2018 15:16:00 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <385f5d47-0656-4a4d-b24c-c2abeab629e7@googlegroups.com> In-Reply-To: References: <6dd2e3fe-fb92-4775-8d36-4a741f6d4826@googlegroups.com> <32baa760-53ed-4fa4-b69c-9537be5b63aa@googlegroups.com> Subject: Re: [HoTT] Bishop's work on type theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_8019_36041614.1525472160144" ------=_Part_8019_36041614.1525472160144 Content-Type: multipart/alternative; boundary="----=_Part_8020_2079840481.1525472160144" ------=_Part_8020_2079840481.1525472160144 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable (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=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 > > 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 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 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 around= =20 > >> 2000.=20 > >> We never put them on the web, because Bishop had decided not to publis= h=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 > >>=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 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= =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 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, send= =20 > an=20 > > email to HomotopyTypeThe...@googlegroups.com .=20 > > For more options, visit https://groups.google.com/d/optout.=20 > ------=_Part_8020_2079840481.1525472160144 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
(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 Hofman= n 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
<escar...@gmail.com> 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 answer= ed 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 th= em at around
>> 2000.
>> We never put them on the web, because Bishop had decided not t= o 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 Escar= d=C3=B3
>> <escar...@gmail.com> wrote:
>> > This week I learned two interesting things that seem to b= e 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 fore= sees 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 mor= e 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 HomotopyTypeTheory+unsub...@googlegroups.com.
> For more options, visit https://groups.go= ogle.com/d/optout.
------=_Part_8020_2079840481.1525472160144-- ------=_Part_8019_36041614.1525472160144--