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

[Michael Shulman <shu...@sandiego.edu>]

Very interesting!!

I believe it's been said that Martin-Lof developed his type theory
explicitly with the goal of providing a foundation for Bishop's
constructive mathematics.  Was he aware of these manuscripts of
Bishop's at the time?

Also: does this conclusively prove that Bishop's "sets" coincide with
what type theorists generally call "setoids"?


On 5/4/18, Martín Hötzel Escardó <escardo...@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
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>