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

[Bas Spitters <b.a.w.s...@gmail.com>]

Setoids were introduced by Martin Hofmann 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ín Hötzel Escardó
<escardo...@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 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
>>
> --
> 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.