I think the idea is that the model structure is constructed / proved using ideas from type theory (like univalence), rather than that it is a model of type theory. But I agree that the terminology is confusing. The methodology is, I think, due to Christian Sattler — so maybe Sattler model structure is more appropriate? Steve > On Feb 15, 2019, at 7:01 PM, Michael Shulman <shulman@sandiego.edu> wrote: > > Please don't call these "type-theoretic model structures". There are > many other model categories that model type theories in ways unrelated > to cubes, notably the classical simplicial model categories that model > Book HoTT. Maybe something like "cubical-type model structures"? > > On Fri, Feb 15, 2019 at 8:32 AM Anders Mörtberg > <andersmortberg@gmail.com> wrote: >> >> No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). >> >> The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. >> >> -- >> Anders >> >> On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >>> >>> Thanks. This looks very interesting. >>> >>> Did you think about the corresponding model structure? >>> https://ncatlab.org/nlab/show/type-theoretic+model+structure >>> >>> Because, we know that Cartesian cubical sets are not equivalent to >>> simplicial sets, but as far as I know, this is still unclear for the >>> DeMorgan cubical sets. >>> https://ncatlab.org/nlab/show/cubical+type+theory#models >>> >>> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >>> <andersm...@gmail.com> wrote: >>>> >>>> Evan Cavallo and I have worked out a new cartesian cubical type theory >>>> that generalizes the existing work on cubical type theories and models >>>> based on a structural interval: >>>> >>>> http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf >>>> >>>> The main difference from earlier work on similar models is that it >>>> depends neither on diagonal cofibrations nor on connections or >>>> reversals. In the presence of these additional structures, our notion >>>> of fibration coincides with that of the existing cartesian and De >>>> Morgan cubical set models. This work can therefore be seen as a >>>> generalization of the existing models of univalent type theory which >>>> also clarifies the connection between them. >>>> >>>> The key idea is to weaken the notion of fibration from the cartesian >>>> Kan operations com^r->s so that they are not strictly the identity >>>> when r=s. Instead we introduce weak cartesian Kan operations that are >>>> only the identity function up to a path when r=s. Semantically this >>>> should correspond to a weaker form of a lifting condition where the >>>> lifting only satisfies some of the eqations up to homotopy. We verify >>>> in the note that this weaker notion of fibration is closed under the >>>> type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, >>>> U) so that we get a model of univalent type theory. We also verify >>>> that the circle works and we don't expect any substantial problems >>>> with extending it to more complicated HITs (like pushouts). >>>> >>>> -- >>>> Anders and Evan >>>> >>>> -- >>>> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Please don't call these "type-theoretic model structures". There are many other model categories that model type theories in ways unrelated to cubes, notably the classical simplicial model categories that model Book HoTT. Maybe something like "cubical-type model structures"? On Fri, Feb 15, 2019 at 8:32 AM Anders Mörtberg <andersmortberg@gmail.com> wrote: > > No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). > > The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. > > -- > Anders > > On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: >> >> Thanks. This looks very interesting. >> >> Did you think about the corresponding model structure? >> https://ncatlab.org/nlab/show/type-theoretic+model+structure >> >> Because, we know that Cartesian cubical sets are not equivalent to >> simplicial sets, but as far as I know, this is still unclear for the >> DeMorgan cubical sets. >> https://ncatlab.org/nlab/show/cubical+type+theory#models >> >> On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg >> <andersm...@gmail.com> wrote: >> > >> > Evan Cavallo and I have worked out a new cartesian cubical type theory >> > that generalizes the existing work on cubical type theories and models >> > based on a structural interval: >> > >> > http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf >> > >> > The main difference from earlier work on similar models is that it >> > depends neither on diagonal cofibrations nor on connections or >> > reversals. In the presence of these additional structures, our notion >> > of fibration coincides with that of the existing cartesian and De >> > Morgan cubical set models. This work can therefore be seen as a >> > generalization of the existing models of univalent type theory which >> > also clarifies the connection between them. >> > >> > The key idea is to weaken the notion of fibration from the cartesian >> > Kan operations com^r->s so that they are not strictly the identity >> > when r=s. Instead we introduce weak cartesian Kan operations that are >> > only the identity function up to a path when r=s. Semantically this >> > should correspond to a weaker form of a lifting condition where the >> > lifting only satisfies some of the eqations up to homotopy. We verify >> > in the note that this weaker notion of fibration is closed under the >> > type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, >> > U) so that we get a model of univalent type theory. We also verify >> > that the circle works and we don't expect any substantial problems >> > with extending it to more complicated HITs (like pushouts). >> > >> > -- >> > Anders and Evan >> > >> > -- >> > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 3365 bytes --] No, we didn't think about model structures yet. First of all one has to figure out how to write our Kan operations as a lifting condition (this is not entirely obvious because of the additional weakness). The observation that the type theoretic model structure on De Morgan cubical sets is not equivalent to the one on spaces is simpler than for Cartesian cubical sets as we have reversals. The case that is not known AFAIK is for the one based on distributive lattices (so only with connections, but no reversals), i.e. the "Dedekind" cubes. -- Anders On Friday, February 15, 2019 at 3:16:56 AM UTC-5, Bas Spitters wrote: > > Thanks. This looks very interesting. > > Did you think about the corresponding model structure? > https://ncatlab.org/nlab/show/type-theoretic+model+structure > > Because, we know that Cartesian cubical sets are not equivalent to > simplicial sets, but as far as I know, this is still unclear for the > DeMorgan cubical sets. > https://ncatlab.org/nlab/show/cubical+type+theory#models > > On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg > <andersm...@gmail.com <javascript:>> wrote: > > > > Evan Cavallo and I have worked out a new cartesian cubical type theory > > that generalizes the existing work on cubical type theories and models > > based on a structural interval: > > > > http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf > > > > The main difference from earlier work on similar models is that it > > depends neither on diagonal cofibrations nor on connections or > > reversals. In the presence of these additional structures, our notion > > of fibration coincides with that of the existing cartesian and De > > Morgan cubical set models. This work can therefore be seen as a > > generalization of the existing models of univalent type theory which > > also clarifies the connection between them. > > > > The key idea is to weaken the notion of fibration from the cartesian > > Kan operations com^r->s so that they are not strictly the identity > > when r=s. Instead we introduce weak cartesian Kan operations that are > > only the identity function up to a path when r=s. Semantically this > > should correspond to a weaker form of a lifting condition where the > > lifting only satisfies some of the eqations up to homotopy. We verify > > in the note that this weaker notion of fibration is closed under the > > type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, > > U) so that we get a model of univalent type theory. We also verify > > that the circle works and we don't expect any substantial problems > > with extending it to more complicated HITs (like pushouts). > > > > -- > > Anders and Evan > > > > -- > > 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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 6293 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2556 bytes --] On Thursday, February 14, 2019 at 3:06:29 PM UTC-5, Andrew Pitts wrote: > > On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersm...@gmail.com > <javascript:>> wrote: > > The key idea is to weaken the notion of fibration from the cartesian > > Kan operations com^r->s so that they are not strictly the identity > > when r=s. Instead we introduce weak cartesian Kan operations that are > > only the identity function up to a path when r=s. > > I was interested to read this, because I too use that weakened form > of fibration in some work attempting to get a model of univalence > based only on composition of paths rather than more general Kan > filling operations — so far unpublished, because I can't quite see how > to get univalent universes to work (but seem frustratingly close to > it). > > Very interesting that you also considered this form of weakened fibrations! I also thought a bit about basing things on a binary composition operation, but I never could get it to work. I managed to convince myself some year ago that in the presence of connections and reversals (potentially with Boolean structure) homogeneous composition (hcomp^0->1) is equivalent to binary composition, but without this structure on the interval I don't really see what to do. But on the other hand, if you don't have connections then I don't think you need the fibrations to lift against arbitrary subtubes but rather only open boxes in the sense of BCH... Anyway, the univalent universes (in particular fibrancy of Glue types) is by far the hardest thing in our note (as seems to always be the case). The way we do it is an adaptation of what we did back in CCHM, but because of the weakness we have to do additional corrections in the construction which makes it quite a bit longer. Anyway, what I wanted to say is that perhaps one should call these > things "Dold fibrations" by analogy with the classic notion of Dold > fibration in topological spaces > <https://ncatlab.org/nlab/show/Dold+fibration>? > > Andy > Thanks for the pointer! I didn't know about them and will have to think a bit whether what we have could be seen as a cubical variation of them. -- Anders -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3894 bytes --]

Thanks. This looks very interesting. Did you think about the corresponding model structure? https://ncatlab.org/nlab/show/type-theoretic+model+structure Because, we know that Cartesian cubical sets are not equivalent to simplicial sets, but as far as I know, this is still unclear for the DeMorgan cubical sets. https://ncatlab.org/nlab/show/cubical+type+theory#models On Thu, Feb 14, 2019 at 8:05 PM Anders Mortberg <andersmortberg@gmail.com> wrote: > > Evan Cavallo and I have worked out a new cartesian cubical type theory > that generalizes the existing work on cubical type theories and models > based on a structural interval: > > http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf > > The main difference from earlier work on similar models is that it > depends neither on diagonal cofibrations nor on connections or > reversals. In the presence of these additional structures, our notion > of fibration coincides with that of the existing cartesian and De > Morgan cubical set models. This work can therefore be seen as a > generalization of the existing models of univalent type theory which > also clarifies the connection between them. > > The key idea is to weaken the notion of fibration from the cartesian > Kan operations com^r->s so that they are not strictly the identity > when r=s. Instead we introduce weak cartesian Kan operations that are > only the identity function up to a path when r=s. Semantically this > should correspond to a weaker form of a lifting condition where the > lifting only satisfies some of the eqations up to homotopy. We verify > in the note that this weaker notion of fibration is closed under the > type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, > U) so that we get a model of univalent type theory. We also verify > that the circle works and we don't expect any substantial problems > with extending it to more complicated HITs (like pushouts). > > -- > Anders and Evan > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

On Thu, 14 Feb 2019 at 19:05, Anders Mortberg <andersmortberg@gmail.com> wrote: > The key idea is to weaken the notion of fibration from the cartesian > Kan operations com^r->s so that they are not strictly the identity > when r=s. Instead we introduce weak cartesian Kan operations that are > only the identity function up to a path when r=s. I was interested to read this, because I too use that weakened form of fibration in some work attempting to get a model of univalence based only on composition of paths rather than more general Kan filling operations — so far unpublished, because I can't quite see how to get univalent universes to work (but seem frustratingly close to it). Anyway, what I wanted to say is that perhaps one should call these things "Dold fibrations" by analogy with the classic notion of Dold fibration in topological spaces <https://ncatlab.org/nlab/show/Dold+fibration>? Andy -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Evan Cavallo and I have worked out a new cartesian cubical type theory that generalizes the existing work on cubical type theories and models based on a structural interval: http://www.cs.cmu.edu/~ecavallo/works/unifying-cartesian.pdf The main difference from earlier work on similar models is that it depends neither on diagonal cofibrations nor on connections or reversals. In the presence of these additional structures, our notion of fibration coincides with that of the existing cartesian and De Morgan cubical set models. This work can therefore be seen as a generalization of the existing models of univalent type theory which also clarifies the connection between them. The key idea is to weaken the notion of fibration from the cartesian Kan operations com^r->s so that they are not strictly the identity when r=s. Instead we introduce weak cartesian Kan operations that are only the identity function up to a path when r=s. Semantically this should correspond to a weaker form of a lifting condition where the lifting only satisfies some of the eqations up to homotopy. We verify in the note that this weaker notion of fibration is closed under the type formers of cubical type theory (nat, Sigma, Pi, Path, Id, Glue, U) so that we get a model of univalent type theory. We also verify that the circle works and we don't expect any substantial problems with extending it to more complicated HITs (like pushouts). -- Anders and Evan -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1: Type: text/plain, Size: 5150 bytes --] I would object to the characterization of definitional identity as identity of sense. Sense is often glossed as mode of givenness; or one might say that the sense of an expression determines a route to its reference. Now take terms such as 7+5 and 9+3. These are definitionally identical, but they present the number twelve in different ways; qua senses each determines a different route to ssssssssssss(0). Hence they are not the same senses. Identity of sense is, to my mind, a stricter relation than definitional identity. Very often, also in this thread, the notions of judgemental identity and definitional identity seem to be treated as one and the same thing. But by judgemental identity we should mean a certain form of identity assertion that is different from the assertion that an identity proposition/type is true/inhabited; and by definitional identity we should mean one among several relations on terms that may properly be called a relation of identity. Here is an argument for the need of a form of identity assertion other than p : Id(A,a,b). The proposition Id(A,a,b) is formed by applying the function Id to the type of individuals (set in Martin-Löf's terminology) A, and the elements a,b : A. The notion of a function, however, presupposes a notion of identity: f is a function only if, when applied to identical arguments a, b, we get identical results f(a), f(b). On pain of circularity, the notion of identity appealed to here cannot be propositional identity. A notion of identity is also implicit in the notion of domain presupposed by the notion of a function: f is a function from the domain A to the domain B. To have the right to speak of A as a domain we need to know what it is for elements of A to be identical, we need to know a criterion of identity for A. In type theory the alternative form of identity assertion, used for instance in the explanation of what a function is, is the identity judgement a = b : A. There is nothing in the argument just given that forces the relation picked out by this form of identity assertion to be definitional identity; but there may be other arguments why such an interpretation is preferable. On Wed, Feb 13, 2019 at 7:37 AM Matt Oliveri <atmacen@gmail.com> wrote: > OK. So it sounds like definitional equality is another way of thinking > about equality of sense, and is generally not the same as strict equality. > That's a relief. > > But the use of judgmental equality for capturing a system of paths that's > fully coherent is actually about strict equality, in general; not > necessarily judgmental or definitional equality. > > So to bring things back to HoTT, what are people's opinions about the best > use of these three equalities? > > My opinion is that strict equality should be implemented as judgmental > equality, which should be richer than definitional equality, by using a > 2-level system with reflective equality. This is the case in HTS and > computational higher dimensional type theory. We would still probably want > to consider different theories of strict equality, but there would be no > obligation to implement them as equality algorithms. Definitional equality > would be a quite separate issue, pertaining to proof automation. > > On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote: >> >> For sure definitional equality doesn't have to do with models. Like >> all the kinds of equality we are discussing, it is a syntactic notion. >> Actually I would say it is a *philosophical* notion, and as such is >> imprecisely specified; syntactic notions like judgmental equality can >> do a better or worse job of capturing it in different theories (and in >> some cases may not even be intended to capture it at all). >> >> > what's the difference between "denoting by definition" and regular >> denoting? >> >> x+(y+z) and (x+y)+z denote the same natural number for any natural >> numbers x,y,z, because we can prove that they are equal. But they >> don't denote the same natural number *by definition*, because this >> proof is not just unfolding the meanings of definitions; it involves >> at least a little thought and a pair of inductions. >> >> For a more radical example, "1+1=2" and "there do not exist positive >> integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same >> proposition, namely "true". But that's certainly not the case by >> definition! Same reference; different senses. >> > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 6115 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2460 bytes --] OK. So it sounds like definitional equality is another way of thinking about equality of sense, and is generally not the same as strict equality. That's a relief. But the use of judgmental equality for capturing a system of paths that's fully coherent is actually about strict equality, in general; not necessarily judgmental or definitional equality. So to bring things back to HoTT, what are people's opinions about the best use of these three equalities? My opinion is that strict equality should be implemented as judgmental equality, which should be richer than definitional equality, by using a 2-level system with reflective equality. This is the case in HTS and computational higher dimensional type theory. We would still probably want to consider different theories of strict equality, but there would be no obligation to implement them as equality algorithms. Definitional equality would be a quite separate issue, pertaining to proof automation. On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote: > > For sure definitional equality doesn't have to do with models. Like > all the kinds of equality we are discussing, it is a syntactic notion. > Actually I would say it is a *philosophical* notion, and as such is > imprecisely specified; syntactic notions like judgmental equality can > do a better or worse job of capturing it in different theories (and in > some cases may not even be intended to capture it at all). > > > what's the difference between "denoting by definition" and regular > denoting? > > x+(y+z) and (x+y)+z denote the same natural number for any natural > numbers x,y,z, because we can prove that they are equal. But they > don't denote the same natural number *by definition*, because this > proof is not just unfolding the meanings of definitions; it involves > at least a little thought and a pair of inductions. > > For a more radical example, "1+1=2" and "there do not exist positive > integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same > proposition, namely "true". But that's certainly not the case by > definition! Same reference; different senses. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2907 bytes --]

For sure definitional equality doesn't have to do with models. Like all the kinds of equality we are discussing, it is a syntactic notion. Actually I would say it is a *philosophical* notion, and as such is imprecisely specified; syntactic notions like judgmental equality can do a better or worse job of capturing it in different theories (and in some cases may not even be intended to capture it at all). > what's the difference between "denoting by definition" and regular denoting? x+(y+z) and (x+y)+z denote the same natural number for any natural numbers x,y,z, because we can prove that they are equal. But they don't denote the same natural number *by definition*, because this proof is not just unfolding the meanings of definitions; it involves at least a little thought and a pair of inductions. For a more radical example, "1+1=2" and "there do not exist positive integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same proposition, namely "true". But that's certainly not the case by definition! Same reference; different senses. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2481 bytes --] On Tuesday, February 12, 2019 at 10:36:08 AM UTC-5, Thorsten Altenkirch wrote: > > Why do I need to understand objects to understand elements? > As a user of Nuprl, you don't. Objects give you a new way to reason, which you don't have to use. You would only need to understand the object-based semantics of types to fully understand the language. Why do I have to capture all possible constructions if I just want to talk > about some specific ones? > I don't understand this. This is something that irritates me about set theory: if I want to say for > all natural numbers …, I am actually saying for all sets which turn out to > be natural numbers… At least conceptually this is rubbish. Who thinks like > this? > This doesn't seem to have anything to do with Nuprl. In Nuprl, saying for all natural numbers is a Pi type with domain nat, as usual. Yes and in computer science we think about types sorting untyped programs. > But why? > Some computer scientists like untyped programs. Do you understand the untyped lambda calculus? > Yeah, I'd say so. It took Dana Scott a while to come up with a mathematical semantics. > Because understanding this connection between computation and math turned out to be much harder than understanding computation on its own, operationally. Before denotational models, the untyped lambda calculus was already well-understood operationally. Scott deepened our understanding of it, and of general recursive types more generally. It's not all or nothing. I think we should put our mouth where our heart is. Typed objects are > easier to understand, they make sense by themselves so lets refer to them. > Yes we implement them based in intyped things, trees, strings, bit > sequences but we don’t need low level concepts to understand high level > concepts!! Yes we need them to implement them but this is another issue. > I truly believe that it's useful for the type system to let users reason about the implementation of typed elements in terms of untyped or less-typed objects. This is refinement typing, and it's not just Nuprl vs the world. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4239 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2444 bytes --] You are right that you don't need to explain elements in terms of objects. That doesn't necessarily make it a bad idea. Not necessarily but I think it is a bad idea. Why do I need to understand objects to understand elements? Why do I have to capture all possible constructions if I just want to talk about some specific ones? This is something that irritates me about set theory: if I want to say for all natural numbers …, I am actually saying for all sets which turn out to be natural numbers… At least conceptually this is rubbish. Who thinks like this? Yes and in computer science we think about types sorting untyped programs. But why? Why do I need to think about untyped programs to understand typed ones. Untyped programs are just weird. Do you understand the untyped lambda calculus? It’s syntax is simple but its meaning is a headfuck. It took Dana Scott a while to come up with a mathematical semantics. I think we should put our mouth where our heart is. Typed objects are easier to understand, they make sense by themselves so lets refer to them. Yes we implement them based in intyped things, trees, strings, bit sequences but we don’t need low level concepts to understand high level concepts!! Yes we need them to implement them but this is another issue. Thorsten -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>. For more options, visit https://groups.google.com/d/optout. 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. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #2: Type: text/html, Size: 4777 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2964 bytes --] Let's say that "objects" are untyped, and "elements" are typed, by definition. These are semantic entities. Nuprl's (closed) terms are untyped in that you are allowed to think of them as objects. You can also think of them as elements. This is not the same. I'd like to distance Nuprl, based on PERs, from set theory. In set theory, objects are given their final meaning by the universe, and sets are types only in the most boring possible sense that you gather up objects and call them elements. In Nuprl, terms obtain their computational meaning as objects, but their mathematical meaning as elements. Interpreted as PERs, Nuprl's types let you ask whether two objects implement the same element. Equality of elements is not equality of objects, and the way you think about objects and elements is different. A variable has a declared type, and it denotes an arbitrary element of that type. It is meaningless to think of it as an object (unless the declared type is a subtype of the type of objects). You are right that you don't need to explain elements in terms of objects. That doesn't necessarily make it a bad idea. Each PER indicates how its elements are implemented by objects. There's no requirement that an object will have a unique type. Each type can be thought of as an abstract view of certain objects. Constructions in Nuprl are heavily based on types, as in any strong type system. You wouldn't bother with a strong type system if you weren't going to do that. You can construct elements using the usual sorts of rules. Because Nuprl also has objects, you also have the option of constructing objects and then proving they implement elements of one or more types. If you've never felt at all constrained by a strong type system, great; you don't have to do that. But for many people, the intrinsically untyped approach is sometimes helpful. An element is an element; it doesn't matter whether it's an element by construction, or a verified object. I see this as a tremendous benefit for strongly typed programming. On Monday, February 11, 2019 at 1:17:25 PM UTC-5, Thorsten Altenkirch wrote: > > I have got something else against NuPRL. It explains Type Theory via > untyped objects which are then typed. In my view there is no reason why we > need to explain typed things via untyped objects. When we talk about > mathematical objects we think about typed entities, and the formalism of > type theory should reflect this. It is not that we find an untyped object > on the street and then try to find out which type it has. We are thinking > of a type first and then we construct an element. > > Thorsten > > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3366 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3994 bytes --] On Monday, February 11, 2019 at 4:50:19 PM UTC-5, Michael Shulman wrote: > > Well, I can't tell exactly what Jon meant by "I have a proof object D > of a judgment J, if J is definitionally equal to J', then D is also > already a proof of J'.". If he meant that an entire typing judgment > "M:A" is only "definitionally equal" to a typing judgment "N:B" if > *the very same derivation tree* of M:A counts also as a derivation of > N:B, then in the ordinary presentations of *any* ordinary type theory > I don't think any two judgments that differ by anything more than > alpha-equivalence would be considered "definitionally equal". > Right. So I assumed he didn't mean that. I'm pretty sure that for ITT, the terms are the proof objects. But it's not clear what should count as proof objects otherwise. This is a weakness of the definition. I guessed at what the proof objects were for Nuprl, but it looks like Jon had something else in mind. If the proof objects are taken to be whatever notion of formal proof the formalizer needs to produce, then definitional equality is an important consideration for proof engineering. That's what I was thinking about. Crucially, proof automation changes the notion of proof, in practice. But this makes things fuzzy. AML programs do not denote something in a model, > and I can't think of any sense in which two of them could be "equal by > definition". You seem confused. Definitional equality is not a relation on proof objects, it's a relation on expressions appearing in the judgments they prove. AML programs don't appear in judgments. (Well, not any semantically relevant judgments.) For instance, (\lambda x. x^2)(3) is equal by definition > to 3^2, because \lambda x. x^2 denotes by definition the function that > takes its argument and squares it. This sure seems completely different from what Jon was getting at. But anyway, what's the difference between "denoting by definition" and regular denoting? An important aspect of Jon's definition of "definitional equality", which I think is right, is that it doesn't have to do with models. Definitional equality is an intentional issue. An issue tied to implementation. ITT pins definitional equality to judgmental equality, which *does* have to do with models, and I think that's *bad*. I suspect that the discomfort or lack of understanding many mathematicians supposedly have with definitional equality stems from the fact that it is, in fact, an implementation issue. So I would say that Andromeda with its reflection rule does not > include a "definitional equality" as a distinguished notion of the > core language. Agree. However, when using Andromeda as a logical framework > to implement some object language, one might assert a particular class > of substitutional equalities in the object language that are all > definitional. > How would you tell when a class of equalities is definitional? On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > > > Jon's definitional equality is based on proof objects. The Andromeda > terms aren't proof objects, since you can't check just a term. So the fact > that Andromeda terms don't have coercions for strict equality doesn't do > anything for definitional equality. I would guess AML programs should be > considered the relevant proof objects. I'd say definitional equality in > Andromeda is pretty interesting, since algebraic effect handlers let you > locally add new automation for equality. But it can't be as rich as strict > equality (if you have e.g. induction on nats). And globally, it sounds like > it's just alpha conversion. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 5443 bytes --]

Some of you might already have seen the interesting discussion "Set theories without junk theorems" at MO https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems that is very much about these accidents of representation. Jacques On 2019-02-11 17:58 , Thorsten Altenkirch wrote: > I think it is rather misleading to think that 0 and the empty set have something in common because in set theory they are represented by the same construction {}. This is rather an accident of representation, it is like saying that the number 49 and the letter 'a' have something in common because they are both represented by the same bit sequence. > > Indeed, I think having access and being able to talk about the accidental representation of objects as you can do in set theory is detrimental because it stops abstraction and this is precisely one of the main advantages of type theory. > > Thorsten > > On 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on behalf of Alexander Kurz" <homotopytypetheory@googlegroups.com on behalf of axhkrz@gmail.com> wrote: > > Hi Thorsten, > > "When we talk about mathematical objects we think about typed entities" > > I agree, but does it follow that types and not objects come first? > > For example, 0 can simultaneously be the empty set, a natural number, an integer, a boolean, etc etc > > The importance of the "etc etc" is that this list is not fixed in advance. It can change during mathematical course. > > This seems to indicate to me that objects come first and types later. > > Another example happens when I say that the dual category has the same objects and arrows with domain and codomain reversed. The same object then belongs to different categories. > > Do you think that type theory provides enough flexibility to model this aspect of mathematical discourse conveniently? > > All the best, > > Alexander > > > On 11 Feb 2019, at 10:17, Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > > > I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element. > > > > Thorsten > > > > On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > > > FWIW, I think the only thing I have against NuPRL "in principle" is > > that it seems to be closely tied to one particular model, which is the > > opposite of what I want my type theories to achieve. I say "seems" > > because then someone says something like Jon's "Nuprl's underlying > > objects are untyped -- but that is not an essential part of the idea", > > providing an instance of the problem I have with NuPRL "in practice", > > which is that every time I think I understand it someone proves me > > wrong. (-:O > > > > Can you explain the difference between "definitional" (whatever that > > means) and "strict" equality in Andromeda? Of course there is the > > technical difference between judgmental equality and the equality > > type, but that doesn't seem to me to be a "real" difference in the > > presence of equality reflection, particularly at the purely > > philosophical level at which a phrase like "equality of sense" has to > > be interpreted. As far as I know, even beta-reduction has no > > privileged status in the Andromeda core -- although I suppose > > alpha-conversion probably does. > > > > > > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote: > >> > >> It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. > >> > >> So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? > >> > >> Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. > >> > >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: > >>> > >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote: > >>>> As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). > >>>> > >>>> So I think you're misusing those terms. > >>> > >>> Well, after many years I still have not managed to figure out how > >>> NuPRLites use words, so it's possible that I misinterpreted what Jon > >>> meant by "proof object". But if you interpret what I meant in ITT, > >>> where I know what I am talking about, then it makes sense. In ITT the > >>> relevant sort of "witness of a proof" is just a term, so "not > >>> perturbing the proof object" means the same thing as "not causing > >>> coercions". > >>> > >>>> You seem to be downplaying the differences between these notions. Why? > >>> > >>> Maybe things are different in computer science, but in mathematics it > >>> often happens that there are things called "ideas" that are, in fact, > >>> vaguer than anything that can be written down precisely, and can be > >>> realized precisely by a variety of different formal definitions with > >>> different formal properties. The differences -- even conceptual > >>> differences -- between these definitions are not unimportant or > >>> ignorable, but do not detract from the importance of the idea or our > >>> ability to think about it. Indeed, the presence of multiple formal > >>> approaches to the idea with different connections to different > >>> subjects make it *more* important and provide us *more* options to > >>> work with it formally. I am thinking of for instance all the > >>> different constructions of a highly structured category of spectra, or > >>> all the different definitions of (oo,1)-category. > >> > >> -- > >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > > > > > > > > > > > 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. > > > > > > > > > > -- > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > > > > 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. > > > > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

I think it is rather misleading to think that 0 and the empty set have something in common because in set theory they are represented by the same construction {}. This is rather an accident of representation, it is like saying that the number 49 and the letter 'a' have something in common because they are both represented by the same bit sequence. Indeed, I think having access and being able to talk about the accidental representation of objects as you can do in set theory is detrimental because it stops abstraction and this is precisely one of the main advantages of type theory. Thorsten On 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on behalf of Alexander Kurz" <homotopytypetheory@googlegroups.com on behalf of axhkrz@gmail.com> wrote: Hi Thorsten, "When we talk about mathematical objects we think about typed entities" I agree, but does it follow that types and not objects come first? For example, 0 can simultaneously be the empty set, a natural number, an integer, a boolean, etc etc The importance of the "etc etc" is that this list is not fixed in advance. It can change during mathematical course. This seems to indicate to me that objects come first and types later. Another example happens when I say that the dual category has the same objects and arrows with domain and codomain reversed. The same object then belongs to different categories. Do you think that type theory provides enough flexibility to model this aspect of mathematical discourse conveniently? All the best, Alexander > On 11 Feb 2019, at 10:17, Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element. > > Thorsten > > On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > FWIW, I think the only thing I have against NuPRL "in principle" is > that it seems to be closely tied to one particular model, which is the > opposite of what I want my type theories to achieve. I say "seems" > because then someone says something like Jon's "Nuprl's underlying > objects are untyped -- but that is not an essential part of the idea", > providing an instance of the problem I have with NuPRL "in practice", > which is that every time I think I understand it someone proves me > wrong. (-:O > > Can you explain the difference between "definitional" (whatever that > means) and "strict" equality in Andromeda? Of course there is the > technical difference between judgmental equality and the equality > type, but that doesn't seem to me to be a "real" difference in the > presence of equality reflection, particularly at the purely > philosophical level at which a phrase like "equality of sense" has to > be interpreted. As far as I know, even beta-reduction has no > privileged status in the Andromeda core -- although I suppose > alpha-conversion probably does. > > > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote: >> >> It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. >> >> So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? >> >> Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. >> >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: >>> >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote: >>>> As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). >>>> >>>> So I think you're misusing those terms. >>> >>> Well, after many years I still have not managed to figure out how >>> NuPRLites use words, so it's possible that I misinterpreted what Jon >>> meant by "proof object". But if you interpret what I meant in ITT, >>> where I know what I am talking about, then it makes sense. In ITT the >>> relevant sort of "witness of a proof" is just a term, so "not >>> perturbing the proof object" means the same thing as "not causing >>> coercions". >>> >>>> You seem to be downplaying the differences between these notions. Why? >>> >>> Maybe things are different in computer science, but in mathematics it >>> often happens that there are things called "ideas" that are, in fact, >>> vaguer than anything that can be written down precisely, and can be >>> realized precisely by a variety of different formal definitions with >>> different formal properties. The differences -- even conceptual >>> differences -- between these definitions are not unimportant or >>> ignorable, but do not detract from the importance of the idea or our >>> ability to think about it. Indeed, the presence of multiple formal >>> approaches to the idea with different connections to different >>> subjects make it *more* important and provide us *more* options to >>> work with it formally. I am thinking of for instance all the >>> different constructions of a highly structured category of spectra, or >>> all the different definitions of (oo,1)-category. >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > > > > 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. > > > > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. 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. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

Well, I can't tell exactly what Jon meant by "I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'.". If he meant that an entire typing judgment "M:A" is only "definitionally equal" to a typing judgment "N:B" if *the very same derivation tree* of M:A counts also as a derivation of N:B, then in the ordinary presentations of *any* ordinary type theory I don't think any two judgments that differ by anything more than alpha-equivalence would be considered "definitionally equal". Look for instance at appendix A.2 of the HoTT book: coercion along judgmental equality is a rule that alters a derivation tree. What it doesn't alter is the *term*, and since Jon also said "In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi" I assumed that his "proof objects" in a MLTT-like theory would refer to the terms rather than the derivation trees. Regardless of what Jon meant, it seems to me that insofar as "definitional equality" is distinguished from all these other kinds of strict equality, it should refer to pairs of terms (i.e. bits of syntax that denote something in a model) that are *equal by definition*. For instance, (\lambda x. x^2)(3) is equal by definition to 3^2, because \lambda x. x^2 denotes by definition the function that takes its argument and squares it. I think this is roughly the same as what I would mean by "equality of sense", although the latter is a primarily philosophical concept and as such cannot be pinned down with mathematical rigor. AML programs do not denote something in a model, and I can't think of any sense in which two of them could be "equal by definition". A judgmental, strict, exact, or substitutional equality might include only definitional equalities, as in ordinary ITT, or it might include other non-definitional ones, as in ETT with reflection rule. So I would say that Andromeda with its reflection rule does not include a "definitional equality" as a distinguished notion of the core language. However, when using Andromeda as a logical framework to implement some object language, one might assert a particular class of substitutional equalities in the object language that are all definitional. On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atmacen@gmail.com> wrote: > > Jon's definitional equality is based on proof objects. The Andromeda terms aren't proof objects, since you can't check just a term. So the fact that Andromeda terms don't have coercions for strict equality doesn't do anything for definitional equality. I would guess AML programs should be considered the relevant proof objects. I'd say definitional equality in Andromeda is pretty interesting, since algebraic effect handlers let you locally add new automation for equality. But it can't be as rich as strict equality (if you have e.g. induction on nats). And globally, it sounds like it's just alpha conversion. > > On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote: >> >> FWIW, I think the only thing I have against NuPRL "in principle" is >> that it seems to be closely tied to one particular model, which is the >> opposite of what I want my type theories to achieve. I say "seems" >> because then someone says something like Jon's "Nuprl's underlying >> objects are untyped -- but that is not an essential part of the idea", >> providing an instance of the problem I have with NuPRL "in practice", >> which is that every time I think I understand it someone proves me >> wrong. (-:O >> >> Can you explain the difference between "definitional" (whatever that >> means) and "strict" equality in Andromeda? Of course there is the >> technical difference between judgmental equality and the equality >> type, but that doesn't seem to me to be a "real" difference in the >> presence of equality reflection, particularly at the purely >> philosophical level at which a phrase like "equality of sense" has to >> be interpreted. As far as I know, even beta-reduction has no >> privileged status in the Andromeda core -- although I suppose >> alpha-conversion probably does. >> >> >> On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atm...@gmail.com> wrote: >> > >> > It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. >> > >> > So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? >> > >> > Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 2527 bytes --] You'll have to ask Jon about what "idea" Nuprl's intrinsic untypedness is "not an essential part of". I'd say the most important thing about Nuprl is dependent refinement typing. In particular, Nuprl is extrinsic dependent typing, since the intrinsic type system is trivial. That turns out to be very interesting too, but makes the approach less broadly applicable. I have some outlandish views about Nuprl. I don't consider its PER semantics to be a model, in the usual sense of model theory. It's proof-theoretic semantics. It's a semantic justification of some proof principles. Kind of like a strong normalization proof for ITT. You can point out that it's technically a realizability model. But I'd say that's because the terms are realizers. *What are they realizing?* That would be a model. The model theory of Nuprlish systems is currently virtually nonexistent. Somebody ought to fix that. There's a set-theoretic semantics (actually two, and they are different... sort of) for an old version of Nuprl. That's it, AFAIK. On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote: > > FWIW, I think the only thing I have against NuPRL "in principle" is > that it seems to be closely tied to one particular model, which is the > opposite of what I want my type theories to achieve. I say "seems" > because then someone says something like Jon's "Nuprl's underlying > objects are untyped -- but that is not an essential part of the idea", > providing an instance of the problem I have with NuPRL "in practice", > which is that every time I think I understand it someone proves me > wrong. (-:O > > Can you explain the difference between "definitional" (whatever that > means) and "strict" equality in Andromeda? Of course there is the > technical difference between judgmental equality and the equality > type, but that doesn't seem to me to be a "real" difference in the > presence of equality reflection, particularly at the purely > philosophical level at which a phrase like "equality of sense" has to > be interpreted. As far as I know, even beta-reduction has no > privileged status in the Andromeda core -- although I suppose > alpha-conversion probably does. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3039 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3407 bytes --] Jon's definitional equality is based on proof objects. The Andromeda terms aren't proof objects, since you can't check just a term. So the fact that Andromeda terms don't have coercions for strict equality doesn't do anything for definitional equality. I would guess AML programs should be considered the relevant proof objects. I'd say definitional equality in Andromeda is pretty interesting, since algebraic effect handlers let you locally add new automation for equality. But it can't be as rich as strict equality (if you have e.g. induction on nats). And globally, it sounds like it's just alpha conversion. On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote: > > FWIW, I think the only thing I have against NuPRL "in principle" is > that it seems to be closely tied to one particular model, which is the > opposite of what I want my type theories to achieve. I say "seems" > because then someone says something like Jon's "Nuprl's underlying > objects are untyped -- but that is not an essential part of the idea", > providing an instance of the problem I have with NuPRL "in practice", > which is that every time I think I understand it someone proves me > wrong. (-:O > > Can you explain the difference between "definitional" (whatever that > means) and "strict" equality in Andromeda? Of course there is the > technical difference between judgmental equality and the equality > type, but that doesn't seem to me to be a "real" difference in the > presence of equality reflection, particularly at the purely > philosophical level at which a phrase like "equality of sense" has to > be interpreted. As far as I know, even beta-reduction has no > privileged status in the Andromeda core -- although I suppose > alpha-conversion probably does. > > > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > > > It looks like Jon is with you regarding definitional/substitutive > equality, since he considers Nuprl's subtitutive equality to be alpha > conversion. From the old discussion about it, I had figured Nuprl's > substitutive equality was the equality type. I guess I'll avoid that term. > > > > So I'll ask a more concrete question. You seem to be more open to > Andromeda than Nuprl. It has a difference between definitional equality (in > Jon's sense) and the (strict/exact) equality type for approximately the > same reason as Nuprl. If the theory you're using is HTS, then there's also > path types. So I gather path types are what you want to take as equality of > reference. Which is equality of sense? > > > > Regarding the paragraph I said was vague, my complaint really is that I > don't know what you're getting at. I recommended strict or exact equality > as possible (informal) interpretations. This doesn't mean there needs to be > something called "strict equality" in the system definition, for example, > it means you recognize a strict equality notion when you see one. I don't > know how to recognize the kind of equality you were getting at in that > paragraph. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4135 bytes --]

Hi Thorsten, "When we talk about mathematical objects we think about typed entities" I agree, but does it follow that types and not objects come first? For example, 0 can simultaneously be the empty set, a natural number, an integer, a boolean, etc etc The importance of the "etc etc" is that this list is not fixed in advance. It can change during mathematical course. This seems to indicate to me that objects come first and types later. Another example happens when I say that the dual category has the same objects and arrows with domain and codomain reversed. The same object then belongs to different categories. Do you think that type theory provides enough flexibility to model this aspect of mathematical discourse conveniently? All the best, Alexander > On 11 Feb 2019, at 10:17, Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element. > > Thorsten > > On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > FWIW, I think the only thing I have against NuPRL "in principle" is > that it seems to be closely tied to one particular model, which is the > opposite of what I want my type theories to achieve. I say "seems" > because then someone says something like Jon's "Nuprl's underlying > objects are untyped -- but that is not an essential part of the idea", > providing an instance of the problem I have with NuPRL "in practice", > which is that every time I think I understand it someone proves me > wrong. (-:O > > Can you explain the difference between "definitional" (whatever that > means) and "strict" equality in Andromeda? Of course there is the > technical difference between judgmental equality and the equality > type, but that doesn't seem to me to be a "real" difference in the > presence of equality reflection, particularly at the purely > philosophical level at which a phrase like "equality of sense" has to > be interpreted. As far as I know, even beta-reduction has no > privileged status in the Andromeda core -- although I suppose > alpha-conversion probably does. > > > On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote: >> >> It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. >> >> So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? >> >> Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. >> >> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: >>> >>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote: >>>> As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). >>>> >>>> So I think you're misusing those terms. >>> >>> Well, after many years I still have not managed to figure out how >>> NuPRLites use words, so it's possible that I misinterpreted what Jon >>> meant by "proof object". But if you interpret what I meant in ITT, >>> where I know what I am talking about, then it makes sense. In ITT the >>> relevant sort of "witness of a proof" is just a term, so "not >>> perturbing the proof object" means the same thing as "not causing >>> coercions". >>> >>>> You seem to be downplaying the differences between these notions. Why? >>> >>> Maybe things are different in computer science, but in mathematics it >>> often happens that there are things called "ideas" that are, in fact, >>> vaguer than anything that can be written down precisely, and can be >>> realized precisely by a variety of different formal definitions with >>> different formal properties. The differences -- even conceptual >>> differences -- between these definitions are not unimportant or >>> ignorable, but do not detract from the importance of the idea or our >>> ability to think about it. Indeed, the presence of multiple formal >>> approaches to the idea with different connections to different >>> subjects make it *more* important and provide us *more* options to >>> work with it formally. I am thinking of for instance all the >>> different constructions of a highly structured category of spectra, or >>> all the different definitions of (oo,1)-category. >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > > > > > > 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. > > > > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element. Thorsten On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: FWIW, I think the only thing I have against NuPRL "in principle" is that it seems to be closely tied to one particular model, which is the opposite of what I want my type theories to achieve. I say "seems" because then someone says something like Jon's "Nuprl's underlying objects are untyped -- but that is not an essential part of the idea", providing an instance of the problem I have with NuPRL "in practice", which is that every time I think I understand it someone proves me wrong. (-:O Can you explain the difference between "definitional" (whatever that means) and "strict" equality in Andromeda? Of course there is the technical difference between judgmental equality and the equality type, but that doesn't seem to me to be a "real" difference in the presence of equality reflection, particularly at the purely philosophical level at which a phrase like "equality of sense" has to be interpreted. As far as I know, even beta-reduction has no privileged status in the Andromeda core -- although I suppose alpha-conversion probably does. On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote: > > It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. > > So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? > > Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. > > On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: >> >> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote: >> > As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). >> > >> > So I think you're misusing those terms. >> >> Well, after many years I still have not managed to figure out how >> NuPRLites use words, so it's possible that I misinterpreted what Jon >> meant by "proof object". But if you interpret what I meant in ITT, >> where I know what I am talking about, then it makes sense. In ITT the >> relevant sort of "witness of a proof" is just a term, so "not >> perturbing the proof object" means the same thing as "not causing >> coercions". >> >> > You seem to be downplaying the differences between these notions. Why? >> >> Maybe things are different in computer science, but in mathematics it >> often happens that there are things called "ideas" that are, in fact, >> vaguer than anything that can be written down precisely, and can be >> realized precisely by a variety of different formal definitions with >> different formal properties. The differences -- even conceptual >> differences -- between these definitions are not unimportant or >> ignorable, but do not detract from the importance of the idea or our >> ability to think about it. Indeed, the presence of multiple formal >> approaches to the idea with different connections to different >> subjects make it *more* important and provide us *more* options to >> work with it formally. I am thinking of for instance all the >> different constructions of a highly structured category of spectra, or >> all the different definitions of (oo,1)-category. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. 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. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

FWIW, I think the only thing I have against NuPRL "in principle" is that it seems to be closely tied to one particular model, which is the opposite of what I want my type theories to achieve. I say "seems" because then someone says something like Jon's "Nuprl's underlying objects are untyped -- but that is not an essential part of the idea", providing an instance of the problem I have with NuPRL "in practice", which is that every time I think I understand it someone proves me wrong. (-:O Can you explain the difference between "definitional" (whatever that means) and "strict" equality in Andromeda? Of course there is the technical difference between judgmental equality and the equality type, but that doesn't seem to me to be a "real" difference in the presence of equality reflection, particularly at the purely philosophical level at which a phrase like "equality of sense" has to be interpreted. As far as I know, even beta-reduction has no privileged status in the Andromeda core -- although I suppose alpha-conversion probably does. On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote: > > It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. > > So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? > > Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. > > On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: >> >> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote: >> > As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). >> > >> > So I think you're misusing those terms. >> >> Well, after many years I still have not managed to figure out how >> NuPRLites use words, so it's possible that I misinterpreted what Jon >> meant by "proof object". But if you interpret what I meant in ITT, >> where I know what I am talking about, then it makes sense. In ITT the >> relevant sort of "witness of a proof" is just a term, so "not >> perturbing the proof object" means the same thing as "not causing >> coercions". >> >> > You seem to be downplaying the differences between these notions. Why? >> >> Maybe things are different in computer science, but in mathematics it >> often happens that there are things called "ideas" that are, in fact, >> vaguer than anything that can be written down precisely, and can be >> realized precisely by a variety of different formal definitions with >> different formal properties. The differences -- even conceptual >> differences -- between these definitions are not unimportant or >> ignorable, but do not detract from the importance of the idea or our >> ability to think about it. Indeed, the presence of multiple formal >> approaches to the idea with different connections to different >> subjects make it *more* important and provide us *more* options to >> work with it formally. I am thinking of for instance all the >> different constructions of a highly structured category of spectra, or >> all the different definitions of (oo,1)-category. > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 3742 bytes --] It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term. So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense? Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph. On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote: > > On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com > <javascript:>> wrote: > > As a form of extensional type theory without any "built-in" > implementation proposal, it seems like HTS has no notion of "proof object" > in Jon's sense, which seems to be formal, checkable proofs. It's not that > you couldn't come up with one, it just isn't specified. So I don't think > HTS has any "definitional equality", in Jon's sense. But it seems like HTS' > exact equality was considered substitutive nonetheless. In fact, it seems > to me like what Vladimir meant by "substitutional" was that it doesn't > cause coercions. Either because it's definitional, or because it's > subsumptive (my term, from another message in this thread). > > > > So I think you're misusing those terms. > > Well, after many years I still have not managed to figure out how > NuPRLites use words, so it's possible that I misinterpreted what Jon > meant by "proof object". But if you interpret what I meant in ITT, > where I know what I am talking about, then it makes sense. In ITT the > relevant sort of "witness of a proof" is just a term, so "not > perturbing the proof object" means the same thing as "not causing > coercions". > > > You seem to be downplaying the differences between these notions. Why? > > Maybe things are different in computer science, but in mathematics it > often happens that there are things called "ideas" that are, in fact, > vaguer than anything that can be written down precisely, and can be > realized precisely by a variety of different formal definitions with > different formal properties. The differences -- even conceptual > differences -- between these definitions are not unimportant or > ignorable, but do not detract from the importance of the idea or our > ability to think about it. Indeed, the presence of multiple formal > approaches to the idea with different connections to different > subjects make it *more* important and provide us *more* options to > work with it formally. I am thinking of for instance all the > different constructions of a highly structured category of spectra, or > all the different definitions of (oo,1)-category. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4505 bytes --]

Hi Matt, my final comment is just to clarify that even if you take the tactic trees as the proof objects (which is a position that I think is fine to argue), it is not acceptable to say that they are robust to "beta perturbations", because if your tactics run beta rules automatically, it is trivial for me to cook up an example where a beta-perturbation would make your tactic script fail to terminate (even if the theorem is true). This is because in Nuprl, you are often working with fixed points (a very cool feature!), and must be circumspect in the computation rules that you apply to them -- for instance, consider proving something about an infinite stream of binary digits. The "substitutive" or "perturbative equality" in Nuprl is indeed alpha, I can confirm, regardless of whether you are thinking of tactic scripts or finished proofs as the proof objects. I just want to re-emphasize what Mike was saying about "ideas" being so fuzzy that they can be characterized using multiple, conflicting explanations -- definitional equality is one of these things, and is a scientific or philosophical concept rather than a technical concept (as Martin-Lof convincingly argued in the 1970s in his famous paper on definitional equality). You may have your own way to understand what is happening in Nuprl, and that's ok --- but the way that I am propounding in this thread is an analogy that allows us to compare apples with apples, a very difficult thing to do in this context. If there is anything mathematical to be said about these things, we need a common technical basis, and it seems like the simplest way to do that is to analyze what function definitional equality plays in practice -- it is the thing which (1) doesn't require proof, and (2) doesn't add any coercions to the thing that counts as proof. That is the "universal property" of definitional equality. I'm too busy to respond further (paper deadline!), so I would request that people wait a few days to contact me about it :) On Mon, Feb 11, 2019, at 8:22 AM, Matt Oliveri wrote: > I'm not convinced that I've made a mistake about Nuprl. If had > mistakenly taken realizers to be the proof objects, then *all* equality > would be definitional. That's not what I'm saying. The untyped beta > conversion is special because beta normalization can be automatically > used as necessary by all tactics invoked in the proof object. That > means all proof objects (following this approach) are robust to > "perturbations" that are beta conversions. Like I said, I'm not sure > Nuprl folks do that. If not, you are technically correct that > definitional equality is alpha. But they can and should do that. So the > design of the system fully supports definitional beta conversion. (And > nothing more.) > > Your exhortation was not pointless. I agreed with it, and attempted to > explain the reason for the difference in more detail. > > On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling > wrote:Hi Matt, I don't have time to get sucked further into this > conversation, but let me just say that what you are saying about > "untyped definitional equality" and beta about nuprl is not accurate, > or at least, it is not accurate if you take the broad definition of > 'definitional equality' that I set in my message. > > > > The lack of coercions in the realizers is true, but I did (apparently pointlessly) exhort readers to not confuse a realizer with a proof. There are coercions in the proof objects -- we must compare apples with apples. > > > > On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote: > > > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling > > > wrote:But this approach is not likely to yield *proof assistants* that > > > are more usable than existing systems which have replaced definitional > > > equality with propositional equality. > > > > > > > > I am referring to Nuprl -- > > > > > > A discussion of the usability of propositional equality would not be > > > complete without distinguishing equality that's reflective, or at least > > > "subsumptive", from equality that's merely strict. Subsumptive equality > > > is when the equality elimination rule rewrites in the type of a term > > > without changing the term. There are no coercions. The way reflective > > > equality is implemented in Nuprl is essentially a combination of > > > subsumptive equality and extensionality principles. In ITT + UIP or > > > Observational TT (OTT), there's a strict propositional equality, but > > > you still have coercions. > > > > > > I see the avoidance of coercions as the main practical benefit of > > > Nuprl's approach. > > > > > > One's approach to automation of equality checking is somewhat > > > orthogonal, and I'm less opinionated about that. A number of dependent > > > type systems exist based on an idea of Aaron Stump to use a combination > > > of some algorithmic equality, and subsumptive (but non-extensional, > > > non-reflective) equality. My impression is that Zombie is one such > > > system. > > > > > > > usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true). > > > > > > To clarify, it depends on what you take to be judgmental equality. If > > > it's the equality that determines what's well-typed, then Nuprl has > > > equality reflection. Of course no useful system will implement > > > reflective equality as an algorithm, since it's infeasible. So any > > > algorithmic equality will be some other equality judgment. But the > > > "real" judgmental equality is precisely the equality type. (As you say > > > later.) > > > > > > > When I say "definitional equality" for a formalism, what I mean is that if I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'. Definitional equality is the silent equality. In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. > > > > > > Interesting. So you're counting Nuprl's proof trees and, say, Agda's > > > terms as proof objects? > > > > > > But what about Nuprl's direct computation rules? These allow untyped > > > beta reduction and expansion anywhere in a goal. This justifies > > > automatic beta normalization by all tactics. I don't know if Nuprlrs > > > take advantage of this, but I think they should. > > > > > > > Proof objects must NOT be confused with realizers, of course -- just like we do not confuse Coq proofs with the OCaml code that they could be extract to. > > > > > > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what > > > get normalized; they are what appear in goals. The thing in Coq > > > corresponding most closely to Nuprl's proof trees are Coq's proof > > > scripts, not terms. The passage from Nuprl's proofs to terms is called > > > "witness extraction", and is superficially similar to Coq's program > > > extraction, but its role is completely different. A distinction between > > > proof objects and terms is practically necessary to avoid coercions, > > > since you still need to tell the proof assistant how to use equality > > > *somehow*. In other words, whereas Coq's proof scripts are an extra, > > > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the > > > distinction between AML programs and terms is necessary.) > > > > > > > ...the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi). > > > > > > Although you may wish otherwise, Nuprl's judgments all respect > > > computational equivalence, which includes beta conversion. (This is the > > > justification of the direct computation rules.) > > > > > > > Nuprl is in essence what it looks like to remove all definitional equalities and replace them with internal equalities. The main difference between Nuprl and Thorsten's proposal is that Nuprl's underlying objects are untyped -- but that is not an essential part of the idea. > > > > > > This doesn't seem right, since Nuprl effectively has untyped beta > > > conversion as definitional equality. So I would say it *is* essential > > > that Nuprl is intrinsically untyped. Its untyped definitional equality > > > is all about the underlying untyped computation system. > > > > > > > The reason I bring this up is that the question of whether such an idea can be made usable, namely using a formalism with only alpha equivalence regarded silently/definitionally, and all other equations mediated through the equality type, can be essentially reduced to the question of whether Nuprl is practical and usable, or whether it is possible to implement a version of that idea which is practical and usable. > > > > > > This is an interesting comparison. But because I consider Nuprl as > > > having untyped definitional equality, and a powerful approach to > > > avoiding coercions, I have to disagree strongly. By your argument, > > > Thorsten's proposal would be at least as bad as Nuprl. (For practical > > > usability.) But I think it would probably be much worse, because I > > > think Nuprl is pretty good. Some of that is because of beta conversion. > > > But avoiding coercions using subsumptive equality is also really > > > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't > > > use that. > > > > > > (I would really like it if Nuprl could be accurately likened to some > > > other proposal, since it'd probably get more people thinking about it. > > > Oh well. The most similar systems to Nuprl, other than its successors, > > > are Andromeda, with reflective equality, and the Stump lineage I > > > mentioned, with subsumptive equality. PVS, Mizar, and F* might be > > > similar too.) > > > > > > The main purpose of this message is not to disagree with you, Jon. I'm > > > mostly trying to sing the praises of Nuprl, because I feel that you've > > > badly undersold it. > > > > > > I don't know what the best way to deal with dependent types is. But I > > > think avoiding type annotations and coercions while getting extensional > > > equality is really good. I don't know about avoiding *all* type > > > annotations; maybe that makes automation too hard. But I suspect the > > > ideal proof assistant will be more like Nuprl than like Coq or Agda. > > > > -- > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.1: Type: text/plain, Size: 8519 bytes --] I'm not convinced that I've made a mistake about Nuprl. If had mistakenly taken realizers to be the proof objects, then *all* equality would be definitional. That's not what I'm saying. The untyped beta conversion is special because beta normalization can be automatically used as necessary by all tactics invoked in the proof object. That means all proof objects (following this approach) are robust to "perturbations" that are beta conversions. Like I said, I'm not sure Nuprl folks do that. If not, you are technically correct that definitional equality is alpha. But they can and should do that. So the design of the system fully supports definitional beta conversion. (And nothing more.) Your exhortation was not pointless. I agreed with it, and attempted to explain the reason for the difference in more detail. On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling wrote: > > Hi Matt, I don't have time to get sucked further into this conversation, > but let me just say that what you are saying about "untyped definitional > equality" and beta about nuprl is not accurate, or at least, it is not > accurate if you take the broad definition of 'definitional equality' that I > set in my message. > > The lack of coercions in the realizers is true, but I did (apparently > pointlessly) exhort readers to not confuse a realizer with a proof. There > are coercions in the proof objects -- we must compare apples with apples. > > On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote: > > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling > > wrote:But this approach is not likely to yield *proof assistants* that > > are more usable than existing systems which have replaced definitional > > equality with propositional equality. > > > > > > I am referring to Nuprl -- > > > > A discussion of the usability of propositional equality would not be > > complete without distinguishing equality that's reflective, or at least > > "subsumptive", from equality that's merely strict. Subsumptive equality > > is when the equality elimination rule rewrites in the type of a term > > without changing the term. There are no coercions. The way reflective > > equality is implemented in Nuprl is essentially a combination of > > subsumptive equality and extensionality principles. In ITT + UIP or > > Observational TT (OTT), there's a strict propositional equality, but > > you still have coercions. > > > > I see the avoidance of coercions as the main practical benefit of > > Nuprl's approach. > > > > One's approach to automation of equality checking is somewhat > > orthogonal, and I'm less opinionated about that. A number of dependent > > type systems exist based on an idea of Aaron Stump to use a combination > > of some algorithmic equality, and subsumptive (but non-extensional, > > non-reflective) equality. My impression is that Zombie is one such > > system. > > > > > usually Nuprl is characterized as using equality reflection, but this > is not totally accurate (though there is a sense in which it is true). > > > > To clarify, it depends on what you take to be judgmental equality. If > > it's the equality that determines what's well-typed, then Nuprl has > > equality reflection. Of course no useful system will implement > > reflective equality as an algorithm, since it's infeasible. So any > > algorithmic equality will be some other equality judgment. But the > > "real" judgmental equality is precisely the equality type. (As you say > > later.) > > > > > When I say "definitional equality" for a formalism, what I mean is > that if I have a proof object D of a judgment J, if J is definitionally > equal to J', then D is also already a proof of J'. Definitional equality is > the silent equality. In most formalisms, definitional equality includes > some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. > > > > Interesting. So you're counting Nuprl's proof trees and, say, Agda's > > terms as proof objects? > > > > But what about Nuprl's direct computation rules? These allow untyped > > beta reduction and expansion anywhere in a goal. This justifies > > automatic beta normalization by all tactics. I don't know if Nuprlrs > > take advantage of this, but I think they should. > > > > > Proof objects must NOT be confused with realizers, of course -- just > like we do not confuse Coq proofs with the OCaml code that they could be > extract to. > > > > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what > > get normalized; they are what appear in goals. The thing in Coq > > corresponding most closely to Nuprl's proof trees are Coq's proof > > scripts, not terms. The passage from Nuprl's proofs to terms is called > > "witness extraction", and is superficially similar to Coq's program > > extraction, but its role is completely different. A distinction between > > proof objects and terms is practically necessary to avoid coercions, > > since you still need to tell the proof assistant how to use equality > > *somehow*. In other words, whereas Coq's proof scripts are an extra, > > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the > > distinction between AML programs and terms is necessary.) > > > > > ...the equality type (a judgment whose derivations are crucially taken > only up to alpha, rather than up to beta/eta/xi). > > > > Although you may wish otherwise, Nuprl's judgments all respect > > computational equivalence, which includes beta conversion. (This is the > > justification of the direct computation rules.) > > > > > Nuprl is in essence what it looks like to remove all definitional > equalities and replace them with internal equalities. The main difference > between Nuprl and Thorsten's proposal is that Nuprl's underlying objects > are untyped -- but that is not an essential part of the idea. > > > > This doesn't seem right, since Nuprl effectively has untyped beta > > conversion as definitional equality. So I would say it *is* essential > > that Nuprl is intrinsically untyped. Its untyped definitional equality > > is all about the underlying untyped computation system. > > > > > The reason I bring this up is that the question of whether such an > idea can be made usable, namely using a formalism with only alpha > equivalence regarded silently/definitionally, and all other equations > mediated through the equality type, can be essentially reduced to the > question of whether Nuprl is practical and usable, or whether it is > possible to implement a version of that idea which is practical and usable. > > > > This is an interesting comparison. But because I consider Nuprl as > > having untyped definitional equality, and a powerful approach to > > avoiding coercions, I have to disagree strongly. By your argument, > > Thorsten's proposal would be at least as bad as Nuprl. (For practical > > usability.) But I think it would probably be much worse, because I > > think Nuprl is pretty good. Some of that is because of beta conversion. > > But avoiding coercions using subsumptive equality is also really > > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't > > use that. > > > > (I would really like it if Nuprl could be accurately likened to some > > other proposal, since it'd probably get more people thinking about it. > > Oh well. The most similar systems to Nuprl, other than its successors, > > are Andromeda, with reflective equality, and the Stump lineage I > > mentioned, with subsumptive equality. PVS, Mizar, and F* might be > > similar too.) > > > > The main purpose of this message is not to disagree with you, Jon. I'm > > mostly trying to sing the praises of Nuprl, because I feel that you've > > badly undersold it. > > > > I don't know what the best way to deal with dependent types is. But I > > think avoiding type annotations and coercions while getting extensional > > equality is really good. I don't know about avoiding *all* type > > annotations; maybe that makes automation too hard. But I suspect the > > ideal proof assistant will be more like Nuprl than like Coq or Agda. > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 9636 bytes --]