* Bishop's work on type theory @ 2018-05-04 21:01 Martín Hötzel Escardó 2018-05-04 21:19 ` [HoTT] " Michael Shulman ` (2 more replies) 0 siblings, 3 replies; 16+ messages in thread From: Martín Hötzel Escardó @ 2018-05-04 21:01 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 761 bytes --] 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: 953 bytes --] ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 21:01 Bishop's work on type theory Martín Hötzel Escardó @ 2018-05-04 21:19 ` Michael Shulman 2018-05-04 21:56 ` Bas Spitters 2018-05-09 9:04 ` Matt Oliveri 2 siblings, 0 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-04 21:19 UTC (permalink / raw) To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory 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. > ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 21:01 Bishop's work on type theory Martín Hötzel Escardó 2018-05-04 21:19 ` [HoTT] " Michael Shulman @ 2018-05-04 21:56 ` Bas Spitters 2018-05-04 22:04 ` Martín Hötzel Escardó 2018-05-09 9:04 ` Matt Oliveri 2 siblings, 1 reply; 16+ messages in thread From: Bas Spitters @ 2018-05-04 21:56 UTC (permalink / raw) To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory 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ó <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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 21:56 ` Bas Spitters @ 2018-05-04 22:04 ` Martín Hötzel Escardó 2018-05-04 22:12 ` Bas Spitters 0 siblings, 1 reply; 16+ messages in thread From: Martín Hötzel Escardó @ 2018-05-04 22:04 UTC (permalink / raw) To: Homotopy Type Theory [-- 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 --] ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 22:04 ` Martín Hötzel Escardó @ 2018-05-04 22:12 ` Bas Spitters 2018-05-04 22:16 ` Martín Hötzel Escardó 0 siblings, 1 reply; 16+ messages in thread From: Bas Spitters @ 2018-05-04 22:12 UTC (permalink / raw) To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory 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. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 22:12 ` Bas Spitters @ 2018-05-04 22:16 ` Martín Hötzel Escardó 2018-05-04 22:23 ` Michael Shulman 0 siblings, 1 reply; 16+ messages in thread From: Martín Hötzel Escardó @ 2018-05-04 22:16 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2699 bytes --] (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. > [-- Attachment #1.2: Type: text/html, Size: 5057 bytes --] ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 22:16 ` Martín Hötzel Escardó @ 2018-05-04 22:23 ` Michael Shulman 2018-05-05 4:27 ` Michael Shulman 0 siblings, 1 reply; 16+ messages in thread From: Michael Shulman @ 2018-05-04 22:23 UTC (permalink / raw) To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory 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. > ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-04 22:23 ` Michael Shulman @ 2018-05-05 4:27 ` Michael Shulman 2018-05-05 11:35 ` Thorsten Altenkirch 2018-05-09 22:27 ` Martín Hötzel Escardó 0 siblings, 2 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-05 4:27 UTC (permalink / raw) To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory I have now had a chance to read over the first manuscript more carefully. It is quite fascinating! I think that in modern language, his system would be called a higher-order logic over a dependent type theory. There are some warts from a modern perspective, but I think it's quite astonishing how close Bishop's system is to modern dependent type theories and higher-order logics, if in fact there was historically no communication. What nowadays we call "types", Bishop calls "classes"; and what we call "functions" between types he calls "operations". He has "power-classes" and "subclasses" which behave roughly like power-types and sub-types in higher-order logic, along with a separate logic of formulas that depend on classes. In particular, propositions are, as far as I can tell, proof-irrelevant, and *not* identified with types! He uses the Leibniz equality of HOL (two terms are equal if they satisfy the same predicates) to formulate the beta and eta rules for his Pi, Sigma, etc. classes, and includes (p26) the function extensionality and propositional extensionality axioms again using this Leibniz equality. Some other interesting notes about Bishop's system: 1. He has a class of all classes. I think this means his system is vulnerable to Girard's paradox and hence inconsistent. This is amusing given his remark (p15) that "A contradiction would be just an indication that we were indulging in meaningless formalism," although to be fair he also says later (p26) that "If aspects of the formalization are meaningless, experience will sooner or later let us know." Of course, this should be fixable as usual by introducing a hierarchy of universes. 2. His "sets" (p16) are classes (types) equipped with an equivalence relation valued in *propositions* (more precisely, equipped with a subclass of A x A satisfying reflexivity, symmetry, and transitivity). So they are like setoids defined in Coq with Prop-valued equality (where Prop satisfies propositional extensionality), not setoids defined in MLTT with Type-valued equality. 3. He includes the axiom of choice (p12) formulated in terms of his (proof-irrelevant) propositions, as well as what seems to be a Hilbert choice operator (though it's not clear to me whether this applies in open contexts or not). Since he has powerclasses with propositional extensionality, I think this means that Diaconescu's argument proves LEM, which he obviously wouldn't want. It's harder for me to guess how this should be fixed, since without some kind of AC, setoids don't satisfy the principle of unique choice. 4. He makes the class of all sets into a set (p19) with equality meaning the mere existence of an isomorphism. But later (p21) he refers to this set more properly as the set of "cardinal numbers". 5. He also defines a category (p19) to have a class of objects (no equality relation imposed) and dependent *sets* (classes with equality relation) of morphisms between any two objects. 6. As we did informally in the HoTT Book, he first introduces non-dependent function types and then formulates dependent ones (which he calls "guarded") in terms of a type family expressed as a non-dependent function into the universe (rather than as a type expression containing a variable). It's quite possible, though, that I am misinterpreting some or all of this; his notation is so different that it's easy to get confused. If so, I hope someone will set me straight. On 5/4/18, Michael Shulman <shu...@sandiego.edu> wrote: > 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. >> > ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-05 4:27 ` Michael Shulman @ 2018-05-05 11:35 ` Thorsten Altenkirch 2018-05-05 15:13 ` Michael Shulman 2018-05-09 22:27 ` Martín Hötzel Escardó 1 sibling, 1 reply; 16+ messages in thread From: Thorsten Altenkirch @ 2018-05-05 11:35 UTC (permalink / raw) To: Michael Shulman, Martín Hötzel Escardó Cc: Homotopy Type Theory On 05/05/2018, 05:27, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote: >3. He includes the axiom of choice (p12) formulated in terms of his >(proof-irrelevant) propositions, as well as what seems to be a Hilbert >choice operator (though it's not clear to me whether this applies in >open contexts or not). Since he has powerclasses with propositional >extensionality, I think this means that Diaconescu's argument proves >LEM, which he obviously wouldn't want. It's harder for me to guess >how this should be fixed, since without some kind of AC, setoids don't >satisfy the principle of unique choice. Why not? If we identify propositions with setoids that are internally propositions (all elements are equal) and identify propositions upto logical equality we get unique choice. What do I miss here? Thorsten > This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-05 11:35 ` Thorsten Altenkirch @ 2018-05-05 15:13 ` Michael Shulman 2018-05-05 15:21 ` Michael Shulman 2018-05-05 21:27 ` Michael Shulman 0 siblings, 2 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-05 15:13 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Martín Hötzel Escardó, Homotopy Type Theory I think the problem is that it's not consistent about what a "proposition" is. If a "proposition" is a setoid in which all elements are equal, then to be consistent, the equality relations of other setoids should also be valued in "propositions" of *this* sort, not the original collection of "propositions" you started with. Otherwise, I think you won't necessarily be able to take the quotient of a setoid by a "proposition"-valued equivalence relation, which is the whole point of introducing setoids in the first place. But down this route lies infinity. I only know of three ways to get a well-behaved category of setoids: 1. Use propositions as types, as in MLTT Type-valued setoids and the ex/lex completion. 2. Define a morphism of setoids to be not an operation respecting equality but a total functional relation, as in the tripos-to-topos construction and the ex/reg completion. I personally believe this is the correct solution in the most generality, but Bishop-style constructivists don't seem to like it. 3. Assume the axiom of choice, which causes options (1) and (2) to coincide. On 5/5/18, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> wrote: > > > On 05/05/2018, 05:27, "homotopyt...@googlegroups.com on behalf of > Michael Shulman" <homotopyt...@googlegroups.com on behalf of > shu...@sandiego.edu> wrote: > >>3. He includes the axiom of choice (p12) formulated in terms of his >>(proof-irrelevant) propositions, as well as what seems to be a Hilbert >>choice operator (though it's not clear to me whether this applies in >>open contexts or not). Since he has powerclasses with propositional >>extensionality, I think this means that Diaconescu's argument proves >>LEM, which he obviously wouldn't want. It's harder for me to guess >>how this should be fixed, since without some kind of AC, setoids don't >>satisfy the principle of unique choice. > > Why not? If we identify propositions with setoids that are internally > propositions (all elements are equal) and identify propositions upto > logical equality we get unique choice. > > What do I miss here? > Thorsten > > >> > > > > > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment. > > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored > where permitted by law. > > > > > ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-05 15:13 ` Michael Shulman @ 2018-05-05 15:21 ` Michael Shulman 2018-05-05 21:27 ` Michael Shulman 1 sibling, 0 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-05 15:21 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Martín Hötzel Escardó, Homotopy Type Theory Of course, if you have higher-order logic with propositional extensionality, you don't need to use setoids at all, but can instead define quotients as sets of equivalence classes like in ZF. But I suspect Bishop wouldn't have liked that either. On 5/5/18, Michael Shulman <shu...@sandiego.edu> wrote: > I think the problem is that it's not consistent about what a > "proposition" is. If a "proposition" is a setoid in which all > elements are equal, then to be consistent, the equality relations of > other setoids should also be valued in "propositions" of *this* sort, > not the original collection of "propositions" you started with. > Otherwise, I think you won't necessarily be able to take the quotient > of a setoid by a "proposition"-valued equivalence relation, which is > the whole point of introducing setoids in the first place. But down > this route lies infinity. > > I only know of three ways to get a well-behaved category of setoids: > > 1. Use propositions as types, as in MLTT Type-valued setoids and the > ex/lex completion. > > 2. Define a morphism of setoids to be not an operation respecting > equality but a total functional relation, as in the tripos-to-topos > construction and the ex/reg completion. I personally believe this is > the correct solution in the most generality, but Bishop-style > constructivists don't seem to like it. > > 3. Assume the axiom of choice, which causes options (1) and (2) to > coincide. > > > On 5/5/18, Thorsten Altenkirch <Thorsten....@nottingham.ac.uk> > wrote: >> >> >> On 05/05/2018, 05:27, "homotopyt...@googlegroups.com on behalf of >> Michael Shulman" <homotopyt...@googlegroups.com on behalf of >> shu...@sandiego.edu> wrote: >> >>>3. He includes the axiom of choice (p12) formulated in terms of his >>>(proof-irrelevant) propositions, as well as what seems to be a Hilbert >>>choice operator (though it's not clear to me whether this applies in >>>open contexts or not). Since he has powerclasses with propositional >>>extensionality, I think this means that Diaconescu's argument proves >>>LEM, which he obviously wouldn't want. It's harder for me to guess >>>how this should be fixed, since without some kind of AC, setoids don't >>>satisfy the principle of unique choice. >> >> Why not? If we identify propositions with setoids that are internally >> propositions (all elements are equal) and identify propositions upto >> logical equality we get unique choice. >> >> What do I miss here? >> Thorsten >> >> >>> >> >> >> >> >> This message and any attachment are intended solely for the addressee >> and may contain confidential information. If you have received this >> message in error, please contact the sender and delete the email and >> attachment. >> >> Any views or opinions expressed by the author of this email do not >> necessarily reflect the views of the University of Nottingham. Email >> communications with the University of Nottingham may be monitored >> where permitted by law. >> >> >> >> >> > ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-05 15:13 ` Michael Shulman 2018-05-05 15:21 ` Michael Shulman @ 2018-05-05 21:27 ` Michael Shulman 1 sibling, 0 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-05 21:27 UTC (permalink / raw) To: Thorsten Altenkirch Cc: Martín Hötzel Escardó, Homotopy Type Theory On 5/5/18, Michael Shulman <shu...@sandiego.edu> wrote: > I think the problem is that it's not consistent about what a > "proposition" is. If a "proposition" is a setoid in which all > elements are equal, then to be consistent, the equality relations of > other setoids should also be valued in "propositions" of *this* sort, > not the original collection of "propositions" you started with. > Otherwise, I think you won't necessarily be able to take the quotient > of a setoid by a "proposition"-valued equivalence relation, which is > the whole point of introducing setoids in the first place. But down > this route lies infinity. I take that back: this doesn't lead to an infinite sequence, instead it stops after one iteration, at a result that coincides with (1): > 1. Use propositions as types, as in MLTT Type-valued setoids and the > ex/lex completion. After all, "a proposition is a setoid in which any two elements are equal" is essentially the same as "a proposition is a type". This is of course a perfectly good way to get a category of setoids (although from a semantic point of view it is too limiting, restricting you to categories that arise as ex/lex completions), and I believe it's how a lot of people have interpreted Bishop's mathematics inside MLTT (for instance). But unless I'm confused, it's not what Bishop is trying to do in this manuscript; he definitely seems to want the equality relations of his setoids to be proof-irrelevant predicates. ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-05 4:27 ` Michael Shulman 2018-05-05 11:35 ` Thorsten Altenkirch @ 2018-05-09 22:27 ` Martín Hötzel Escardó 2018-05-10 6:35 ` Andrej Bauer 1 sibling, 1 reply; 16+ messages in thread From: Martín Hötzel Escardó @ 2018-05-09 22:27 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 9094 bytes --] Thanks, Mike, for reporting your analysis of the paper. I didn't reply earlier because we had a very intensive week with the summer school here at the Hausdorff institute. It seems that this is a sort of two-level type theory, with a logic on top of a formalism for types. (One thing that one should always have in mind is that these two papers were not published. I have lots of private files with tentative ideas, which I wish that if they are ever seen after I die then they will be taken as such - tentative ideas.) I like seeing Bishop offering ideas on what formalism would reflect his thinking. But most of all I like his conviction that "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" as I said before. I am not sure one can use these two papers as a definitive source to try to understand his original, informal "Foundations of constructive analysis". I would guess *not*. Martin On Saturday, 5 May 2018 06:27:29 UTC+2, Michael Shulman wrote: > > I have now had a chance to read over the first manuscript more > carefully. It is quite fascinating! I think that in modern language, > his system would be called a higher-order logic over a dependent type > theory. There are some warts from a modern perspective, but I think > it's quite astonishing how close Bishop's system is to modern > dependent type theories and higher-order logics, if in fact there was > historically no communication. > > What nowadays we call "types", Bishop calls "classes"; and what we > call "functions" between types he calls "operations". He has > "power-classes" and "subclasses" which behave roughly like power-types > and sub-types in higher-order logic, along with a separate logic of > formulas that depend on classes. In particular, propositions are, as > far as I can tell, proof-irrelevant, and *not* identified with types! > He uses the Leibniz equality of HOL (two terms are equal if they > satisfy the same predicates) to formulate the beta and eta rules for > his Pi, Sigma, etc. classes, and includes (p26) the function > extensionality and propositional extensionality axioms again using > this Leibniz equality. > > Some other interesting notes about Bishop's system: > > 1. He has a class of all classes. I think this means his system is > vulnerable to Girard's paradox and hence inconsistent. This is > amusing given his remark (p15) that "A contradiction would be just an > indication that we were indulging in meaningless formalism," although > to be fair he also says later (p26) that "If aspects of the > formalization are meaningless, experience will sooner or later let us > know." Of course, this should be fixable as usual by introducing a > hierarchy of universes. > > 2. His "sets" (p16) are classes (types) equipped with an equivalence > relation valued in *propositions* (more precisely, equipped with a > subclass of A x A satisfying reflexivity, symmetry, and transitivity). > So they are like setoids defined in Coq with Prop-valued equality > (where Prop satisfies propositional extensionality), not setoids > defined in MLTT with Type-valued equality. > > 3. He includes the axiom of choice (p12) formulated in terms of his > (proof-irrelevant) propositions, as well as what seems to be a Hilbert > choice operator (though it's not clear to me whether this applies in > open contexts or not). Since he has powerclasses with propositional > extensionality, I think this means that Diaconescu's argument proves > LEM, which he obviously wouldn't want. It's harder for me to guess > how this should be fixed, since without some kind of AC, setoids don't > satisfy the principle of unique choice. > > 4. He makes the class of all sets into a set (p19) with equality > meaning the mere existence of an isomorphism. But later (p21) he > refers to this set more properly as the set of "cardinal numbers". > > 5. He also defines a category (p19) to have a class of objects (no > equality relation imposed) and dependent *sets* (classes with equality > relation) of morphisms between any two objects. > > 6. As we did informally in the HoTT Book, he first introduces > non-dependent function types and then formulates dependent ones (which > he calls "guarded") in terms of a type family expressed as a > non-dependent function into the universe (rather than as a type > expression containing a variable). > > It's quite possible, though, that I am misinterpreting some or all of > this; his notation is so different that it's easy to get confused. If > so, I hope someone will set me straight. > > > > On 5/4/18, Michael Shulman <shu...@sandiego.edu <javascript:>> wrote: > > 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ó <escar...@gmail.com <javascript:>> > 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:> > >>> > <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 <javascript:>. > > >> For more options, visit https://groups.google.com/d/optout. > >> > > > [-- Attachment #1.2: Type: text/html, Size: 13632 bytes --] ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Bishop's work on type theory 2018-05-09 22:27 ` Martín Hötzel Escardó @ 2018-05-10 6:35 ` Andrej Bauer 0 siblings, 0 replies; 16+ messages in thread From: Andrej Bauer @ 2018-05-10 6:35 UTC (permalink / raw) To: Homotopy Type Theory Hi, I have had these documents in my office for a while, but forgot about them and never found the time to look at them. Such an opportunity missed. In any case, it looks like I have an earlier vesion, because some of the manuscripts are written in hand in they do look like an incomplete version of the ones that Martin published. If anyone wants to do archeological mathematics, I could scan them in, althogh I hesitate to make them publically available. With kind regards, Andrej ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: Bishop's work on type theory 2018-05-04 21:01 Bishop's work on type theory Martín Hötzel Escardó 2018-05-04 21:19 ` [HoTT] " Michael Shulman 2018-05-04 21:56 ` Bas Spitters @ 2018-05-09 9:04 ` Matt Oliveri 2018-05-09 16:15 ` [HoTT] " Michael Shulman 2 siblings, 1 reply; 16+ messages in thread From: Matt Oliveri @ 2018-05-09 9:04 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 1183 bytes --] There doesn't seem to be anything like a conversion rule. I suspect that a lot of the math examples developed in the system don't actually type check. If they do, it would seem to be luck. Or maybe not; does anyone know some key intuition behind this system that I'm missing? On Friday, May 4, 2018 at 5:01:53 PM UTC-4, Martín Hötzel Escardó 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: 1936 bytes --] ^ permalink raw reply [flat|nested] 16+ messages in thread
* Re: [HoTT] Re: Bishop's work on type theory 2018-05-09 9:04 ` Matt Oliveri @ 2018-05-09 16:15 ` Michael Shulman 0 siblings, 0 replies; 16+ messages in thread From: Michael Shulman @ 2018-05-09 16:15 UTC (permalink / raw) To: Matt Oliveri; +Cc: Homotopy Type Theory You mean something like "if t:A and A==B then t:B"? You're right; I'm not even sure how to phrase such a rule with Bishop's setup where "the" type of a term is an *operation* T(t) == A, whereas things like beta-reduction are expressed only propositionally in terms of Leibniz equality. On 5/9/18, Matt Oliveri <atm...@gmail.com> wrote: > There doesn't seem to be anything like a conversion rule. I suspect that a > lot of the math examples developed in the system don't actually type check. > > If they do, it would seem to be luck. Or maybe not; does anyone know some > key intuition behind this system that I'm missing? > > On Friday, May 4, 2018 at 5:01:53 PM UTC-4, Martín Hötzel Escardó 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. > ^ permalink raw reply [flat|nested] 16+ messages in thread
end of thread, other threads:[~2018-05-10 6:35 UTC | newest] Thread overview: 16+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-05-04 21:01 Bishop's work on type theory Martín Hötzel Escardó 2018-05-04 21:19 ` [HoTT] " Michael Shulman 2018-05-04 21:56 ` Bas Spitters 2018-05-04 22:04 ` Martín Hötzel Escardó 2018-05-04 22:12 ` Bas Spitters 2018-05-04 22:16 ` Martín Hötzel Escardó 2018-05-04 22:23 ` Michael Shulman 2018-05-05 4:27 ` Michael Shulman 2018-05-05 11:35 ` Thorsten Altenkirch 2018-05-05 15:13 ` Michael Shulman 2018-05-05 15:21 ` Michael Shulman 2018-05-05 21:27 ` Michael Shulman 2018-05-09 22:27 ` Martín Hötzel Escardó 2018-05-10 6:35 ` Andrej Bauer 2018-05-09 9:04 ` Matt Oliveri 2018-05-09 16:15 ` [HoTT] " Michael Shulman
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).