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