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

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

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

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 <javascript:>> 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 
>
>

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