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

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

Right, the question more precisely is whether, when transported along
whatever isomorphism there is between Bishop's "general language" and
MLTT (I have not read the manuscript yet to understand this), the
"sets" defined by Bishop on p16 coincide with Hofmann's setoids.  If
so, then it would be some substantial additional evidence for the
claim that setoids are "what Bishop really meant".

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