[-- Attachment #1.1: Type: text/plain, Size: 686 bytes --] In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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: 931 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1348 bytes --] The type checking rules are nonlinear (reuses metavariables). For example, for function application, the type of the argument needs to "equal" the domain of the function. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic equality. But it seems really really hard to have judgmental equality be just syntactic equality, in a dependent type system. It would also be unnatural, from a computational perspective; the judgmental equations are saying something about the computational behavior of the system. On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: > > In section 1.1 of the HoTT book it says "In type theory there is also a > need for an equality judgment." Currently it seems to me like one could, in > principle, replace substitution along judgmental equality with explicit > transports if one added a few sensible rules to the type theory. Is there a > fundamental reason why the equality judgment is still necessary? > > Thanks, > Felix Rech > -- 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: 1740 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1760 bytes --] Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type. -- Anders On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: > > The type checking rules are nonlinear (reuses metavariables). For example, > for function application, the type of the argument needs to "equal" the > domain of the function. What equality is that? It gets called judgmental > equality. It's there in some sense even if it's just syntactic equality. > But it seems really really hard to have judgmental equality be just > syntactic equality, in a dependent type system. It would also be unnatural, > from a computational perspective; the judgmental equations are saying > something about the computational behavior of the system. > > On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could, in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is there a >> fundamental reason why the equality judgment is still necessary? >> >> Thanks, >> Felix Rech >> > -- 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: 2319 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2129 bytes --] I would also like to know an answer to this question. It is true that dependent type theories have been designed using definitional equality. But why would anybody say that there is a *need* for that? Is it impossible to define a sensible dependent type theory (say for the purpose of serving as a foundation for univalent mathematics) that doesn't mention anything like definitional equality? If not, why not? And notice that I am not talking about *usability* of a proof assistant such as the *existing* ones (say Coq, Agda, Lean) were definitional equalities to be removed. I don't care if such hypothetical proof assistants would be impossibly difficult to use for a dependent type theory lacking definitional equalities (if such a thing exists). The question asked by Felix is a very sensible one: why is it claimed that definitional equalities are essential to dependent type theories? (I do understand that they are used to compute, and so if you are interested in constructive mathematics (like I am) then they are useful. But, again, in principle we can think of a dependent type theory with no definitional equalities and instead an existence property like e.g. in Lambek and Scott's "introduction to higher-order categorical logic". And like was discussed in a relatively recent message by Thierry Coquand in this list,) Martin On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: > > In section 1.1 of the HoTT book it says "In type theory there is also a > need for an equality judgment." Currently it seems to me like one could, in > principle, replace substitution along judgmental equality with explicit > transports if one added a few sensible rules to the type theory. Is there a > fundamental reason why the equality judgment is still necessary? > > Thanks, > Felix Rech > -- 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: 2624 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3493 bytes --] If you are not interested in computations and convenience of your type theory, then the definitional equality is not essential in the sense that every type theory T is equivalent to a type theory Q(T) with no computational rules. Now, what do I mean when I say that type theories T and Q(T) are equivalent? I won't give here the formal definition, but the idea is that Q(T) can be interpreted in T and, for every type A of T, there is a type in Q(T) equivalent to A in T and the same is true for terms. This implies that every statement (i.e., type) of Q(T) is provable in Q(T) if and only if it is provable in T and every statement of T has an equivalent statement in Q(T), so the theories are "logically equivalent". Moreover, equivalent theories have equivalent (in an appropriate homotopical sense) categories of models. Regards, Valery Isaev сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <escardo.martin@gmail.com >: > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpose > of serving as a foundation for univalent mathematics) that doesn't mention > anything like definitional equality? If not, why not? And notice that I am > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > The question asked by Felix is a very sensible one: why is it claimed that > definitional equalities are essential to dependent type theories? > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > Martin > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could, in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is there a >> fundamental reason why the equality judgment is still necessary? >> >> Thanks, >> Felix Rech >> > -- > 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: 4556 bytes --]

[-- Attachment #1: Type: text/plain, Size: 6083 bytes --] I agree with everything Martin said below, but I want to go a step further and argue that judgmental equality is potentially holding us back, in terms of meta-theoretical results AND usability of the type theory. I can understand that, for programming, we want built-in computation. However, for a foundational system, I think we should strive for something as minimalistic as possible without arbitrary additional features. It might be a bit controversial to call judgmental equality an "arbitrary additional feature", but there is certainly some arbitrariness involved (why else would Sigma have judgmental eta in some systems and not in others?). It seems to me that the cleanest, most minimalistic, and most canonical choice would be a type theory without judgmental equalities *at all*. This would also be much more in line with the approach of category theory, and I expect that it could make the lives of those of us working with models easier. Is there a deep theoretical reason for the necessity of judgmental equality? Of course, we want convenience and usability. I just fail to see why this means that judgmental equality has to be a built-in thing (one could say: why does it have to be part of the core). It's possible that, if we do *not* insist on built-in judgmental equality, we could even get *more* convenience. What I mean is this: Let's write WTT for a "weak type theory" without any judgmental equalities (since we're doing HoTT, maybe with some axioms such as univalence, but let's not specify this here). Let's say we know that a certain set A of judgmental equalities does not change WTT, i.e. that (WTT+A) is a conservative extension of WTT (conservative in a constructive sense). We could now have a proof assistant which uses WTT as core but which allows us to "load" the conservativity proof of A. Then, at the beginning of a module, a user can tell the proof assistant that in this module, they pretend that the type theory is (WTT+A); i.e. for the user, it looks as if they are working in (WTT+A) but, in the background, the proof assistant translates everything to WTT. In another module, the user can pretend they are working in (WTT+B) instead, if (WTT+B) is conservative over WTT as well. The idea here is that some proofs benefit more from one set of judgmental equalities, while other proofs benefit more from others. Being able to choose which equalities one wants could lead to increased convenience. (I think WTT+A+B is not necessarily conservative over WTT, so we cannot just always assume all equalities for maximum convenience.) For example, let's consider a cubical type theory. I'm aware that we don't really know many conservativity properties of cubical type theories yet, but I would be interested in knowing some. Maybe some cubical type theory gives us a set C which our WTT-based proof assistant can load. In other words, instead of saying "hey, we have found a new cubical type theory with amazing computational behaviour, an implementation is on GitHub", people could say "hey, we have found a new set of judgmental equalities, on GitHub is the conservativity proof that you can load into your proof assistant to use it". I don't think this is something that we will manage to get anytime soon, and I find it very difficult in general to find conservativity results, but is there a theoretical reason which makes this impossible? Nicolai On Fri, Feb 8, 2019 at 9:19 PM Martín Hötzel Escardó < escardo.martin@gmail.com> wrote: > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpose > of serving as a foundation for univalent mathematics) that doesn't mention > anything like definitional equality? If not, why not? And notice that I am > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > The question asked by Felix is a very sensible one: why is it claimed that > definitional equalities are essential to dependent type theories? > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > Martin > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could, in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is there a >> fundamental reason why the equality judgment is still necessary? >> >> Thanks, >> Felix Rech >> > -- > 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: 7175 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3967 bytes --] Hi Valery, On Fri, Feb 8, 2019 at 11:32 PM Valery Isaev <valery.isaev@gmail.com> wrote: > Now, what do I mean when I say that type theories T and Q(T) are > equivalent? I won't give here the formal definition > Would it be correct to say that T is a conservative extension of T, in the sense of Martin Hofmann's thesis? Your description sounds a bit like this, or do you have something different in mind? Nicolai > , but the idea is that Q(T) can be interpreted in T and, for every type A > of T, there is a type in Q(T) equivalent to A in T and the same is true for > terms. This implies that every statement (i.e., type) of Q(T) is provable > in Q(T) if and only if it is provable in T and every statement of T has an > equivalent statement in Q(T), so the theories are "logically equivalent". > Moreover, equivalent theories have equivalent (in an appropriate > homotopical sense) categories of models. > > Regards, > Valery Isaev > > > сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó < > escardo.martin@gmail.com>: > >> I would also like to know an answer to this question. It is true that >> dependent type theories have been designed using definitional equality. >> >> But why would anybody say that there is a *need* for that? Is it >> impossible to define a sensible dependent type theory (say for the purpose >> of serving as a foundation for univalent mathematics) that doesn't mention >> anything like definitional equality? If not, why not? And notice that I am >> not talking about *usability* of a proof assistant such as the *existing* >> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I >> don't care if such hypothetical proof assistants would be impossibly >> difficult to use for a dependent type theory lacking definitional >> equalities (if such a thing exists). >> >> The question asked by Felix is a very sensible one: why is it claimed >> that definitional equalities are essential to dependent type theories? >> >> (I do understand that they are used to compute, and so if you are >> interested in constructive mathematics (like I am) then they are useful. >> But, again, in principle we can think of a dependent type theory with no >> definitional equalities and instead an existence property like e.g. in >> Lambek and Scott's "introduction to higher-order categorical logic". And >> like was discussed in a relatively recent message by Thierry Coquand in >> this list,) >> >> Martin >> >> >> On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: >>> >>> In section 1.1 of the HoTT book it says "In type theory there is also a >>> need for an equality judgment." Currently it seems to me like one could, in >>> principle, replace substitution along judgmental equality with explicit >>> transports if one added a few sensible rules to the type theory. Is there a >>> fundamental reason why the equality judgment is still necessary? >>> >>> Thanks, >>> Felix Rech >>> >> -- >> 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 #2: Type: text/html, Size: 5616 bytes --]

Hi Valery, I'm trying to square what you said with what Anders said. Consider extending MLTT with an interval in two different ways: 1. With judgmental computation rules for the recursor 2. With propositional computation axioms for the recursor I do not expect to obtain a conservativity result for the second version over the first version, since the first one derives function extensionality, and the second one does not (afaict). Can you give a bit more detail about how this algebraic power move that you are describing works, and whether it applies in this case? Thanks! Jon On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote: > If you are not interested in computations and convenience of your type > theory, then the definitional equality is not essential in the sense > that every type theory T is equivalent to a type theory Q(T) with no > computational rules. Now, what do I mean when I say that type theories > T and Q(T) are equivalent? I won't give here the formal definition, but > the idea is that Q(T) can be interpreted in T and, for every type A of > T, there is a type in Q(T) equivalent to A in T and the same is true > for terms. This implies that every statement (i.e., type) of Q(T) is > provable in Q(T) if and only if it is provable in T and every statement > of T has an equivalent statement in Q(T), so the theories are > "logically equivalent". Moreover, equivalent theories have equivalent > (in an appropriate homotopical sense) categories of models. > > Regards, > Valery Isaev > > > сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <escardo.martin@gmail.com>: > > I would also like to know an answer to this question. It is true that dependent type theories have been designed using definitional equality. > > > > But why would anybody say that there is a *need* for that? Is it impossible to define a sensible dependent type theory (say for the purpose of serving as a foundation for univalent mathematics) that doesn't mention anything like definitional equality? If not, why not? And notice that I am not talking about *usability* of a proof assistant such as the *existing* ones (say Coq, Agda, Lean) were definitional equalities to be removed. I don't care if such hypothetical proof assistants would be impossibly difficult to use for a dependent type theory lacking definitional equalities (if such a thing exists). > > > > The question asked by Felix is a very sensible one: why is it claimed that definitional equalities are essential to dependent type theories? > > > > (I do understand that they are used to compute, and so if you are interested in constructive mathematics (like I am) then they are useful. But, again, in principle we can think of a dependent type theory with no definitional equalities and instead an existence property like e.g. in Lambek and Scott's "introduction to higher-order categorical logic". And like was discussed in a relatively recent message by Thierry Coquand in this list,) > > > > Martin > > > > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: > >> In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? > >> > >> Thanks, > >> Felix Rech > > > > > > -- > > 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: Type: text/plain, Size: 5015 bytes --] Hi Nicolai, The notion of a conservative extension is certainly related to the notion of an equivalence of type theories that I'm referring to (I call it Morita equivalence). Hofmann defines various properties of the interpretation |-| : ITT -> ETT, which are weaker than Morita equivalence in general. The statement of Theorem 3.2.5 is almost equivalent to the notion of Morita equivalence. We just need to replace "|P'| = P" with "|P'| and P are propositionally equivalent" and add the condition that, for every \Gamma |-_I and every |\Gamma| |-_E A there is a type \Gamma |-_I A' such that |A'| and A are equivalent in the sense of HoTT (the latter condition follows from Theorem 3.2.5 for ITT and ETT, but not for general type theories). Then we get precisely the notion of Morita equivalence between type theories I and E. Regards, Valery Isaev сб, 9 февр. 2019 г. в 04:41, Nicolai Kraus <nicolai.kraus@gmail.com>: > Hi Valery, > > On Fri, Feb 8, 2019 at 11:32 PM Valery Isaev <valery.isaev@gmail.com> > wrote: > >> Now, what do I mean when I say that type theories T and Q(T) are >> equivalent? I won't give here the formal definition >> > > Would it be correct to say that T is a conservative extension of T, in the > sense of Martin Hofmann's thesis? Your description sounds a bit like this, > or do you have something different in mind? > Nicolai > > > >> , but the idea is that Q(T) can be interpreted in T and, for every type A >> of T, there is a type in Q(T) equivalent to A in T and the same is true for >> terms. This implies that every statement (i.e., type) of Q(T) is provable >> in Q(T) if and only if it is provable in T and every statement of T has an >> equivalent statement in Q(T), so the theories are "logically equivalent". >> Moreover, equivalent theories have equivalent (in an appropriate >> homotopical sense) categories of models. >> >> Regards, >> Valery Isaev >> >> >> сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó < >> escardo.martin@gmail.com>: >> >>> I would also like to know an answer to this question. It is true that >>> dependent type theories have been designed using definitional equality. >>> >>> But why would anybody say that there is a *need* for that? Is it >>> impossible to define a sensible dependent type theory (say for the purpose >>> of serving as a foundation for univalent mathematics) that doesn't mention >>> anything like definitional equality? If not, why not? And notice that I am >>> not talking about *usability* of a proof assistant such as the *existing* >>> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I >>> don't care if such hypothetical proof assistants would be impossibly >>> difficult to use for a dependent type theory lacking definitional >>> equalities (if such a thing exists). >>> >>> The question asked by Felix is a very sensible one: why is it claimed >>> that definitional equalities are essential to dependent type theories? >>> >>> (I do understand that they are used to compute, and so if you are >>> interested in constructive mathematics (like I am) then they are useful. >>> But, again, in principle we can think of a dependent type theory with no >>> definitional equalities and instead an existence property like e.g. in >>> Lambek and Scott's "introduction to higher-order categorical logic". And >>> like was discussed in a relatively recent message by Thierry Coquand in >>> this list,) >>> >>> Martin >>> >>> >>> On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: >>>> >>>> In section 1.1 of the HoTT book it says "In type theory there is also a >>>> need for an equality judgment." Currently it seems to me like one could, in >>>> principle, replace substitution along judgmental equality with explicit >>>> transports if one added a few sensible rules to the type theory. Is there a >>>> fundamental reason why the equality judgment is still necessary? >>>> >>>> Thanks, >>>> Felix Rech >>>> >>> -- >>> 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 #2: Type: text/html, Size: 7187 bytes --]

[-- Attachment #1: Type: text/plain, Size: 5988 bytes --] Hi Jon, It is not true that Q(T) can be obtained from T simply by replacing judgmental equalities with propositional ones (I think this should be true for some theories, but certainly not for all). So, if we denote the theory with an interval and judgmental rules by T_I and the theory with propsoitional axioms by T_a, then Q(T_I) is equivalent to T_I and Q(T_a) is equivalent to T_a, but Q(T_I) is not equivalent to T_a. Theories T_a and Q(T_a) are actually equivalent to the ordinary MLTT (since we simply add another contractible type to it). Functional extensionality is provable in both T_I and Q(T_I). It follows from the existence of the interval type in T_I and it can be added as an axiom to Q(T_I). I believe that theories T_I and Q(T_I) are equivalent to MLTT + functional extensionality, but I don't know how to prove this yet. Regards, Valery Isaev сб, 9 февр. 2019 г. в 05:01, Jon Sterling <jon@jonmsterling.com>: > Hi Valery, > > I'm trying to square what you said with what Anders said. Consider > extending MLTT with an interval in two different ways: > > 1. With judgmental computation rules for the recursor > 2. With propositional computation axioms for the recursor > > I do not expect to obtain a conservativity result for the second version > over the first version, since the first one derives function > extensionality, and the second one does not (afaict). > > Can you give a bit more detail about how this algebraic power move that > you are describing works, and whether it applies in this case? > > Thanks! > Jon > > On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote: > > If you are not interested in computations and convenience of your type > > theory, then the definitional equality is not essential in the sense > > that every type theory T is equivalent to a type theory Q(T) with no > > computational rules. Now, what do I mean when I say that type theories > > T and Q(T) are equivalent? I won't give here the formal definition, but > > the idea is that Q(T) can be interpreted in T and, for every type A of > > T, there is a type in Q(T) equivalent to A in T and the same is true > > for terms. This implies that every statement (i.e., type) of Q(T) is > > provable in Q(T) if and only if it is provable in T and every statement > > of T has an equivalent statement in Q(T), so the theories are > > "logically equivalent". Moreover, equivalent theories have equivalent > > (in an appropriate homotopical sense) categories of models. > > > > Regards, > > Valery Isaev > > > > > > сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó < > escardo.martin@gmail.com>: > > > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > > > > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpose > of serving as a foundation for univalent mathematics) that doesn't mention > anything like definitional equality? If not, why not? And notice that I am > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > > > > > The question asked by Felix is a very sensible one: why is it claimed > that definitional equalities are essential to dependent type theories? > > > > > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > > > > > Martin > > > > > > > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: > > >> In section 1.1 of the HoTT book it says "In type theory there is also > a need for an equality judgment." Currently it seems to me like one could, > in principle, replace substitution along judgmental equality with explicit > transports if one added a few sensible rules to the type theory. Is there a > fundamental reason why the equality judgment is still necessary? > > >> > > >> Thanks, > > >> Felix Rech > > > > > > > > > > -- > > > 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. [-- Attachment #2: Type: text/html, Size: 7707 bytes --]

Working without any judgemental equality was the aim of the original LF where elements of a type A correspond to formal derivations of A in abstract syntax. Also Isabelle works a bit like that. So with a modicum of judgemental equality one uses dependent types for having a syntax for formal derivations. But, of course, this is absolutely useless when you want to execute your proofs! Thomas -- 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: 1419 bytes --] Thank you all for the discussion! One of the motivations for my question was that I actually expect usability benefits if one worked in a dependent type theory without judgmental equality that has good support by a proof assistant. There are primarily two reasons for this: 1. Judgmental equality cannot be taken as assumptions. If one wants to use judgmental equalities then one has to give concrete definitions that satisfy those equalities and cannot hide the definition details. This makes it impossible to change definitions later on without breaking constructions that depend on them. 2. In nontrivial definitions, judgmental equalities seem more arbitrary than natural. If we define addition of natural numbers for example then we can choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot have both. This makes it hard to find the right definitions and to predict their behavior. Another motivation was of course that it would simplify the implementation of proof checkers and parts of the metatheory. I would appreciate any comments on this. -- 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: 1664 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 881 bytes --] On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders Mörtberg wrote: > > Consider the interval HIT, it is contractible and hence equivalent to > Unit. But it also lets you prove function extensionallity which you > definitely don't get from the Unit type. > I have the feeling that function extensionality is special in the sense that the proof that I know of, as well as that of function extensionality in ETT, relies on the fact that we can replace judgmentally equal terms under lambdas, which is like function extensionality for judgmental equality. -- 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: 1228 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 875 bytes --] On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote: > > I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > I agree that the ability to compute canonical forms for terms is essential but one does not need to integrate computation into the type system to do that. At least, one can alway interprete terms of a type theory without an equality judgment in a stronger type theory that has judgmental equalities and do the computations there. -- 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: 1222 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3110 bytes --] Hi, what we need is a strict equality on all types. If we would state the laws of type theory just using the equality type we would also need to add coherence laws. Since I would include the laws for substitution (never understood why substitution is different from application) this would include the laws for infinity categories and this would make even basic type theory certainly much more complicated if not unusable. Instead one introduces a 2-level system with strict equality on one level and weak equality on another. For historic and pragmatic reasons this is combined with the computational aspects of type theory which is expressed as judgemental equality. However, there are reasons to separate these concerns, e.g. to work with higher dimensional constructions in type theory such as semi-simplicial types it is helpful to work with hypothetical strict equalities (see our paper (http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). I do think that the computational behaviour of type theory is important too. However, this can be expressed by demandic a form of computational adequacy, that is for every term there is a strictly equal normal form. It is not necessary that strict equality in general is decidable (indeed different applications of type theory may demand different decision procedures). Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Felix Rech <s9ferech@gmail.com> Date: Wednesday, 30 January 2019 at 11:55 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: [HoTT] Why do we need judgmental equality? In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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: 6179 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1740 bytes --] On 09/02/2019 11:57, Felix Rech wrote:> On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote: > > I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > > > I agree that the ability to compute canonical forms for terms is > essential but one does not need to integrate computation into the type > system to do that. At least, one can alway interprete terms of a type > theory without an equality judgment in a stronger type theory that has > judgmental equalities and do the computations there. Yes, this is what I meant by the sentence that follows the one quoted above, which I quote below. Also, you don't need to compute by reducing equalities. In fact, most functional languages (e.g. Haskell) when compiled *do not* compute by unfolding definitional equalities. On 08/02/2019 21:19, Martín Hötzel Escardó wrote:> (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 2261 bytes --]

Even LF included beta eta hence has a non-trivial judgemental equality. Not to mention the equations for substitution. Thorsten On 09/02/2019, 11:38, "homotopytypetheory@googlegroups.com on behalf of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of streicher@mathematik.tu-darmstadt.de> wrote: Working without any judgemental equality was the aim of the original LF where elements of a type A correspond to formal derivations of A in abstract syntax. Also Isabelle works a bit like that. So with a modicum of judgemental equality one uses dependent types for having a syntax for formal derivations. But, of course, this is absolutely useless when you want to execute your proofs! Thomas -- 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.

[-- Attachment #1.1: Type: text/plain, Size: 3003 bytes --] Hi, To follow on the idea of 2-level type theory. It indeed seems enough to have a strict equality (meaning with UIP and Funext) to pull off an interpretation of weakTT. In fact, I have updated an formalised the work of Nicolas Oury of translating Extensional Type Theory into Intensional Type Theory, and extended the proof so that it can be an instance of a translation from an extensional 2-level type theory into an intensional one. In this work, the treatment of conversion in the target seems to be orthogonal to the result itself. With Simon Boulier we plan to tweak the formalisation a bit so that it allows to target weakTT (and we already conducted informal reasoning to justify it). You can thus give an interpretation to a theory into its weak version, provided you have UIP, funext and enough equalities to interpret for instance β-reduction. I hope this is clear. Théo Le samedi 9 février 2019 14:29:28 UTC+1, Thorsten Altenkirch a écrit : > > Even LF included beta eta hence has a non-trivial judgemental equality. > Not to mention the equations for substitution. > > Thorsten > > On 09/02/2019, 11:38, "homotopyt...@googlegroups.com <javascript:> on > behalf of Thomas Streicher" <homotopyt...@googlegroups.com <javascript:> > on behalf of stre...@mathematik.tu-darmstadt.de <javascript:>> wrote: > > Working without any judgemental equality was the aim of the original > LF where elements of a type A correspond to formal derivations of A in > abstract syntax. Also Isabelle works a bit like that. > > So with a modicum of judgemental equality one uses dependent types for > having a syntax for formal derivations. But, of course, this is > absolutely useless when you want to execute your proofs! > > Thomas > > -- > 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. > > > 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 #1.2: Type: text/html, Size: 4530 bytes --]

[-- Attachment #1: Type: text/plain, Size: 2421 bytes --] On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote: > One of the motivations for my question was that I actually expect > usability benefits if one worked in a dependent type theory without > judgmental equality that has good support by a proof assistant. > Yes, me too (but I think *a lot* of work needs to be done before we can have a proof assistant based on this idea which provides better usability than the current ones). I agree with your points. But I think "x + 0 = x versus 0 + x = x" is an example where I'd expect that one should be able to produce a conservativity proof and use both at the same time instead of choosing one. I think it's not necessary that we restrict ourselves to computation rules that come from actual definitions; anything that is "constructively conservative" over a weak theory should be allowed. In Agda, one can have additional computation rules, but it's not a safe feature. Nicolai > 1. Judgmental equality cannot be taken as assumptions. If one wants to > use judgmental equalities then one has to give concrete definitions that > satisfy those equalities and cannot hide the definition details. This makes > it impossible to change definitions later on without breaking constructions > that depend on them. > 2. In nontrivial definitions, judgmental equalities seem more > arbitrary than natural. If we define addition of natural numbers for > example then we can choose between x + 0 = x and 0 + x = x as judgmental > equality but we cannot have both. This makes it hard to find the right > definitions and to predict their behavior. > > Another motivation was of course that it would simplify the implementation > of proof checkers and parts of the metatheory. > > I would appreciate any comments on this. > > -- > 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: 3305 bytes --]

[-- Attachment #1: Type: text/plain, Size: 3494 bytes --] A relevant citation for this line of thinking (if we reduce implicit computation, can we gain usability some other way?) is the work on the Zombie programming language, which tried to weaken beta-reduction in a dependent language (restricting it to values only, as in F*) to obtain a more automatic form of reasoning upto congruence (definitional equalities can be put in the context and used from there). Programming up to Congruence Vilhelm Sjöberg and Stephanie Weirich, 2015 http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf On Sat, Feb 9, 2019 at 3:05 PM Nicolai Kraus <nicolai.kraus@gmail.com> wrote: > On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote: > >> One of the motivations for my question was that I actually expect >> usability benefits if one worked in a dependent type theory without >> judgmental equality that has good support by a proof assistant. >> > > Yes, me too (but I think *a lot* of work needs to be done before we can > have a proof assistant based on this idea which provides better usability > than the current ones). > I agree with your points. But I think "x + 0 = x versus 0 + x = x" is an > example where I'd expect that one should be able to produce a > conservativity proof and use both at the same time instead of choosing one. > I think it's not necessary that we restrict ourselves to computation rules > that come from actual definitions; anything that is "constructively > conservative" over a weak theory should be allowed. In Agda, one can have > additional computation rules, but it's not a safe feature. > Nicolai > > > >> 1. Judgmental equality cannot be taken as assumptions. If one wants >> to use judgmental equalities then one has to give concrete definitions that >> satisfy those equalities and cannot hide the definition details. This makes >> it impossible to change definitions later on without breaking constructions >> that depend on them. >> 2. In nontrivial definitions, judgmental equalities seem more >> arbitrary than natural. If we define addition of natural numbers for >> example then we can choose between x + 0 = x and 0 + x = x as judgmental >> equality but we cannot have both. This makes it hard to find the right >> definitions and to predict their behavior. >> >> Another motivation was of course that it would simplify the >> implementation of proof checkers and parts of the metatheory. >> >> I would appreciate any comments on this. >> >> -- >> 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 #2: Type: text/html, Size: 4936 bytes --]

Hi all, I think there's two different issues being conflated -- there is the question of whether definitional equalities can be removed, in order to obtain more direct interpretation into weaker models, and then there is the question of whether definitional equalities can be removed as a way to make a proof assistant more modular, exploiting conservativity results locally to add defintional equalities. The first seems more interesting to me, and is indeed the topic of Curien's famous paper. Many interesting coherence theorems lurk underneath the definitional equalities that we take for granted, and we can only see them if we treat definitional equalities as defeasible. The issue about proof assistants seems quite different to me -- the approach that seems to be proposed by some of the people in the room, to replace judgmental equality with a good enough equality *type* seems perfectly good for studying algebra and models (for instance, the discipline of QIITs in the presence of [semantically] extensional equality types seems like a good tool for dependently-sorted algebraic theories). 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 -- usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true). 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. What I mean is that in a proof object for Nuprl, the biggest relation by which you can "purturb" a judgment without needing to update the proof object is alpha equivalence. 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. So how does Nuprl work? "Real" equality is captured purely using the equality type, and not using any judgment except membership in the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi). When you want to reason using beta/eta/xi (and the much richer equations that are also available), you use the equality type and its elimination rules directly, essentially in the same way that Thorsten has advocated. 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. 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. As many of the people on this list are aware, in the years past I was very bullish on this idea, but now after having implemented two separate proof assistants based on this idea, I am not as optimistic about it as I was (but I don't rule it out). Today, I have changed my methodology and embraced strong definitional equality, in order to achieve my actual goals during the very finite historical period of my PhD -- to build usable proof assistants for formalizing mathematics. Best, Jon On Sat, Feb 9, 2019, at 9:05 AM, Nicolai Kraus wrote: > On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote: > > One of the motivations for my question was that I actually expect usability benefits if one worked in a dependent type theory without judgmental equality that has good support by a proof assistant. > > Yes, me too (but I think *a lot* of work needs to be done before we can > have a proof assistant based on this idea which provides better > usability than the current ones). > I agree with your points. But I think "x + 0 = x versus 0 + x = x" is > an example where I'd expect that one should be able to produce a > conservativity proof and use both at the same time instead of choosing > one. I think it's not necessary that we restrict ourselves to > computation rules that come from actual definitions; anything that is > "constructively conservative" over a weak theory should be allowed. In > Agda, one can have additional computation rules, but it's not a safe > feature. > Nicolai > > > > 1. Judgmental equality cannot be taken as assumptions. If one wants to use judgmental equalities then one has to give concrete definitions that satisfy those equalities and cannot hide the definition details. This makes it impossible to change definitions later on without breaking constructions that depend on them. > > 2. In nontrivial definitions, judgmental equalities seem more arbitrary than natural. If we define addition of natural numbers for example then we can choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot have both. This makes it hard to find the right definitions and to predict their behavior. > > Another motivation was of course that it would simplify the implementation of proof checkers and parts of the metatheory. > > > > I would appreciate any comments on this. > > > > > > -- > > 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.

From a semantic point of view, I agree that judgmental equality is about convenience and usability. But that shouldn't be regarded as making it any less important. Indeed, the whole *point* of using type theory as an internal language for a category, rather than simply reasoning about the category directly, is... convenience and usability. Of course there are degrees of convenience, and even type theory without judgmental equality might be slightly more convenient than reasoning directly in categorical language. But I think we need judgmental equality if we really want to get some substantial benefit out of type theory as an internal language. The problem of course is to bridge the gap between the type theory and the category theory, and for that purpose intermediate structures may be useful: categories that are more like type theory (such as tribes and contextual categories) and type theories that are more like category theory (such as ones with fewer judgmental equalities). But I don't think I would want to regard the intermediate structures as fundamental, rather than tools to get from one side to another. From an implementation point of view, I agree that in the long run we should have proof assistants that don't hardcode a fixed set of judgmental equalities. But I don't think that means eliminating all judgmental equalities; it just means making the logical framework more flexible, such as Agda's ability to postulate new reductions or Andromeda's framework with equality reflection. In particular, the new equalities that we postulate should still be *substitutive* (as Jon says, allowing to perturb a judgment without altering the proof object) rather than *transportive* (requiring the proof object to be altered) -- I think Vladimir was the one who suggested words like those. From a computation point of view, of course some kind of reduction is necessary, and it makes sense to consider an object to be "equal" in some sense to the result of computing it. This would presumably be a stronger sense than typal equality inside the system, whether or not it is actually substitutive. Conversely, in order to implement a substitutive equality it seems very useful to have some algorithm that can at least go some part of the way towards deciding it, and computation is likely to play an important role in such an algorithm. From a philosophical point of view, I think definitional/substitutive equality is very important: as Steve Awodey pointed out some time ago, it represents the intensional "equality of sense" rather than the extensional "equality of reference". This explains why it is substitutive: if two terms have the same sense, there is no explanation necessary for why a statement about one also applies to the other, while if they only have the same reference, then some explanation may be required. If I say "I saw the morning star this morning" and you reply "yes, and I saw it last night", it sounds weird because there is a transport necessary along the equality of reference "morning star = evening star", in a way that doesn't happen if instead you reply "yes, and I saw it yesterday morning". Foundations for mathematics based on first-order logic, like ZFC, have no ability to talk about equality of sense; the only equality they know about is reference. A type theory without definitional equality would have the same limitation. Judgmental, definitional, substitutive, and computational equalities are not exactly the same thing. But the fact that there are so many different but related points of view on similar and overlapping concepts, and so many different but related uses and applications for them, suggests to me that there is an important underlying mathematical concept that should not lightly be discarded. On the other hand, the proof of the pudding is in the eating, and this whole discussion would be much more concrete if we had some actual references working out what type theory without judgmental equality looks like, with proofs of whatever properties it may be claimed to have, and perhaps even an implementation of it; so I don't mean to discourage anyone from trying to develop such a thing. -- 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: 2441 bytes --] On Saturday, February 9, 2019 at 6:53:15 AM UTC-5, Felix Rech wrote: > > Judgmental equality cannot be taken as assumptions. If one wants to use > judgmental equalities then one has to give concrete definitions that > satisfy those equalities and cannot hide the definition details. This makes > it impossible to change definitions later on without breaking constructions > that depend on them. > I worry that this will indeed be a modularity problem in practice. You generally can't specify behavior strictly at the interface between subsystems. Semantic purists would point out that such an interface wouldn't make sense anyway, unless the subsystem's type is an hset, and you use paths. In general, you should specify a bunch of coherences. Aside from being way harder though, we don't know how to do it in general, because of the infinite object problem. With a 2-level theory, you could at least have second-class module signatures with strict equality. In nontrivial definitions, judgmental equalities seem more arbitrary than > natural. If we define addition of natural numbers for example then we can > choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot > have both. This makes it hard to find the right definitions and to predict > their behavior. > Another motivation was of course that it would simplify the implementation > of proof checkers and parts of the metatheory. > This problem is solved by the special case of 2-level theories where strict equality is reflective (like extensional type theory (ETT)). What this does for you in practice is that you never have to see coercions between e.g. types (F (x + 0)) and (F (0 + x)), since they can be proven judgmentally equal by induction. (What I mean is that there's no record in terms of rewriting with nat equality. Not that all such reasoning can be done automatically. (It presumably is easy to automate both plus-zero rewrites though.)) Without reflective equality, strict equality doesn't seem to provide any benefit over paths in this case, because you need a coercion, and paths between nats are already unique. -- 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: 2959 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1115 bytes --] If the stronger type theory is not conservative, you generally can't draw mathematical conclusions on the basis of those computations, though. On Saturday, February 9, 2019 at 6:57:51 AM UTC-5, Felix Rech wrote: > > On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote: >> >> I do understand that they are used to compute, and so if you are >> interested in constructive mathematics (like I am) then they are useful. >> > > I agree that the ability to compute canonical forms for terms is essential > but one does not need to integrate computation into the type system to do > that. At least, one can alway interprete terms of a type theory without an > equality judgment in a stronger type theory that has judgmental equalities > and do the computations there. > -- 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: 1587 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 2849 bytes --] I think you're right. From discussions about autophagy, it seems like no one knows how to match judgmental equality using equality types, unless that equality type family is propositionally truncated in some way. Consequently, my guess is that Valery's Q transformation actually yields something rather like a 2-level system. On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch wrote: > > Hi, > > > > what we need is a strict equality on all types. If we would state the laws > of type theory just using the equality type we would also need to add > coherence laws. Since I would include the laws for substitution (never > understood why substitution is different from application) this would > include the laws for infinity categories and this would make even basic > type theory certainly much more complicated if not unusable. Instead one > introduces a 2-level system with strict equality on one level and weak > equality on another. For historic and pragmatic reasons this is combined > with the computational aspects of type theory which is expressed as > judgemental equality. However, there are reasons to separate these > concerns, e.g. to work with higher dimensional constructions in type theory > such as semi-simplicial types it is helpful to work with hypothetical > strict equalities (see our paper ( > http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). > > > > I do think that the computational behaviour of type theory is important > too. However, this can be expressed by demandic a form of computational > adequacy, that is for every term there is a strictly equal normal form. It > is not necessary that strict equality in general is decidable (indeed > different applications of type theory may demand different decision > procedures). > > > > Thorsten > > > > > > *From: *<homotopyt...@googlegroups.com <javascript:>> on behalf of Felix > Rech <s9fe...@gmail.com <javascript:>> > *Date: *Wednesday, 30 January 2019 at 11:55 > *To: *Homotopy Type Theory <homotopyt...@googlegroups.com <javascript:>> > *Subject: *[HoTT] Why do we need judgmental equality? > > > > In section 1.1 of the HoTT book it says "In type theory there is also a > need for an equality judgment." Currently it seems to me like one could, in > principle, replace substitution along judgmental equality with explicit > transports if one added a few sensible rules to the type theory. Is there a > fundamental reason why the equality judgment is still necessary? > > > > Thanks, > > Felix Rech > -- 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: 5143 bytes --]

[-- Attachment #1: Type: text/plain, Size: 4107 bytes --] Hi Matt, I should point out that when I say "a type theory" I mean an ordinary dependently typed language, without any strict equalities or 2-levelness. Any such theory has only (dependent) types and terms and usual structural rules. Any "coherence problem" is solved by simply adding an infinite tower of terms. For example, in MLTT, if f : A -> B -> C, you can define function swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id definitionally. Of course, you cannot have such a definitional equality in Q(MLTT), but instead you have a propositional equality p : Id(swap \circ swap, id) and also an infinite tower of terms, which assure that p is coherent. Any rule that holds definitionally in MLTT will be true in Q(MLTT) propositionally. Regards, Valery Isaev пн, 11 февр. 2019 г. в 10:01, Matt Oliveri <atmacen@gmail.com>: > I think you're right. From discussions about autophagy, it seems like no > one knows how to match judgmental equality using equality types, unless > that equality type family is propositionally truncated in some way. > > Consequently, my guess is that Valery's Q transformation actually yields > something rather like a 2-level system. > > On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch > wrote: >> >> Hi, >> >> >> >> what we need is a strict equality on all types. If we would state the >> laws of type theory just using the equality type we would also need to add >> coherence laws. Since I would include the laws for substitution (never >> understood why substitution is different from application) this would >> include the laws for infinity categories and this would make even basic >> type theory certainly much more complicated if not unusable. Instead one >> introduces a 2-level system with strict equality on one level and weak >> equality on another. For historic and pragmatic reasons this is combined >> with the computational aspects of type theory which is expressed as >> judgemental equality. However, there are reasons to separate these >> concerns, e.g. to work with higher dimensional constructions in type theory >> such as semi-simplicial types it is helpful to work with hypothetical >> strict equalities (see our paper ( >> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). >> >> >> >> I do think that the computational behaviour of type theory is important >> too. However, this can be expressed by demandic a form of computational >> adequacy, that is for every term there is a strictly equal normal form. It >> is not necessary that strict equality in general is decidable (indeed >> different applications of type theory may demand different decision >> procedures). >> >> >> >> Thorsten >> >> >> >> >> >> *From: *<homotopyt...@googlegroups.com> on behalf of Felix Rech < >> s9fe...@gmail.com> >> *Date: *Wednesday, 30 January 2019 at 11:55 >> *To: *Homotopy Type Theory <homotopyt...@googlegroups.com> >> *Subject: *[HoTT] Why do we need judgmental equality? >> >> >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could, in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is there a >> fundamental reason why the equality judgment is still necessary? >> >> >> >> Thanks, >> >> Felix Rech >> > -- > 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: 6043 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 6567 bytes --] 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: 7914 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 3389 bytes --] OK, thanks. I stand corrected. But in that case, I'm with Thorsten: 2-level seems easier. On Monday, February 11, 2019 at 3:04:58 AM UTC-5, Валерий Исаев wrote: > > Hi Matt, > > I should point out that when I say "a type theory" I mean an ordinary > dependently typed language, without any strict equalities or 2-levelness. > Any such theory has only (dependent) types and terms and usual structural > rules. > Any "coherence problem" is solved by simply adding an infinite tower of > terms. For example, in MLTT, if f : A -> B -> C, you can define function > swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id > definitionally. Of course, you cannot have such a definitional equality in > Q(MLTT), but instead you have a propositional equality p : Id(swap \circ > swap, id) and also an infinite tower of terms, which assure that p is > coherent. Any rule that holds definitionally in MLTT will be true in > Q(MLTT) propositionally. > > Regards, > Valery Isaev > > > пн, 11 февр. 2019 г. в 10:01, Matt Oliveri <atm...@gmail.com <javascript:> > >: > >> I think you're right. From discussions about autophagy, it seems like no >> one knows how to match judgmental equality using equality types, unless >> that equality type family is propositionally truncated in some way. >> >> Consequently, my guess is that Valery's Q transformation actually yields >> something rather like a 2-level system. >> >> On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch >> wrote: >>> >>> Hi, >>> >>> >>> >>> what we need is a strict equality on all types. If we would state the >>> laws of type theory just using the equality type we would also need to add >>> coherence laws. Since I would include the laws for substitution (never >>> understood why substitution is different from application) this would >>> include the laws for infinity categories and this would make even basic >>> type theory certainly much more complicated if not unusable. Instead one >>> introduces a 2-level system with strict equality on one level and weak >>> equality on another. For historic and pragmatic reasons this is combined >>> with the computational aspects of type theory which is expressed as >>> judgemental equality. However, there are reasons to separate these >>> concerns, e.g. to work with higher dimensional constructions in type theory >>> such as semi-simplicial types it is helpful to work with hypothetical >>> strict equalities (see our paper ( >>> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). >>> >>> >>> >>> I do think that the computational behaviour of type theory is important >>> too. However, this can be expressed by demandic a form of computational >>> adequacy, that is for every term there is a strictly equal normal form. It >>> is not necessary that strict equality in general is decidable (indeed >>> different applications of type theory may demand different decision >>> procedures). >>> >>> >>> >>> 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: 4944 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1586 bytes --] Come to think of it, that's pretty cool though, that you can systematically produce all the higher coherences for a system of judgmental equations! On Monday, February 11, 2019 at 3:28:53 AM UTC-5, Matt Oliveri wrote: > > OK, thanks. I stand corrected. But in that case, I'm with Thorsten: > 2-level seems easier. > > On Monday, February 11, 2019 at 3:04:58 AM UTC-5, Валерий Исаев wrote: >> >> Hi Matt, >> >> I should point out that when I say "a type theory" I mean an ordinary >> dependently typed language, without any strict equalities or 2-levelness. >> Any such theory has only (dependent) types and terms and usual structural >> rules. >> Any "coherence problem" is solved by simply adding an infinite tower of >> terms. For example, in MLTT, if f : A -> B -> C, you can define function >> swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id >> definitionally. Of course, you cannot have such a definitional equality in >> Q(MLTT), but instead you have a propositional equality p : Id(swap \circ >> swap, id) and also an infinite tower of terms, which assure that p is >> coherent. Any rule that holds definitionally in MLTT will be true in >> Q(MLTT) propositionally. >> >> Regards, >> Valery Isaev >> > -- 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: 2170 bytes --]

I have been thinking about the relationship between type theories with weak or strong computation rules, here is what I currently know about it. Note that in the presence of UIP, type theories with weak and strong computation rules are equivalent. This is a consequence of the conservativity of extensional type theory over intensional type theory. (As Théo said, the proof does not rely on the presence of strong computation rules in ITT) Without UIP, there are coherence theorems to be proven. As explained by Thorsten, we can replace a type theory T (presented by generators (type and term constructors) and relations (definitional equalities)) by a two-level type theory whose outer layer has strict identity types, and in which the definitional equalities of T become generators of the identity types of the outer layer. Here, "strict" means that we either include the equality reflection rule, or the UIP principle. By the same arguments as in Hofmann's conservativity proof, both choices are equivalent. What is interesting is that for some choices of type-theoretic structures and definitional equalities, UIP can be derived in the two-level type theory, rather than taken as an axiom, in which case the strong type theory is a conservative extension of the weak theory. Proving that UIP is derivable is very similar to proving coherence statements of the form "all diagrams commute". (it is an acylicity condition) If F : WTT ---> STT is an extension of a weak type theory WTT by new equations, and W2TT is a two-level type theory associated to WTT, the situation is as follows: WTT -------------------> STT | F | G| H|~ v v W2TT ---> W2TT+UIP ---> W2TT+EXT K L (The objects of this diagram are the initial models of the theories) G and L are always conservative, H is an isomorphism, and if UIP is derivable in W2TT, then K is conservative. I think that I know how to prove that UIP is derivable when considering extensions corresponding to weak computation rules (propositional identity types, ...), although I have not written a detailed proof yet. The core of the proof is a procedure that performs weak head normalization, up to homotopy and coherently, in the weak two-level type theory. Because the strong theory is strongly normalising, repeatedly applying that procedure terminates. -- Rafaël Bocquet -- 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: 2904 bytes --] On Saturday, February 9, 2019 at 3:34:22 PM UTC-5, Michael Shulman wrote: > > From an implementation point of view, I agree that in the long run we > should have proof assistants that don't hardcode a fixed set of > judgmental equalities. But I don't think that means eliminating all > judgmental equalities; it just means making the logical framework more > flexible, such as Agda's ability to postulate new reductions or > Andromeda's framework with equality reflection. In particular, the > new equalities that we postulate should still be *substitutive* (as > Jon says, allowing to perturb a judgment without altering the proof > object) rather than *transportive* (requiring the proof object to be > altered) -- I think Vladimir was the one who suggested words like > those. I first heard those terms was on this list: https://groups.google.com/forum/#!topic/homotopytypetheory/1bUtH8CLGQg It seems from that discussion that they were associated with Vladimir Voevodsky's proposal for HTS. 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. Judgmental, definitional, substitutive, and computational equalities > are not exactly the same thing. But the fact that there are so many > different but related points of view on similar and overlapping > concepts, and so many different but related uses and applications for > them, suggests to me that there is an important underlying > mathematical concept that should not lightly be discarded. > This is too vague. I wouldn't know whether I'm discarding it or not. You seem to be downplaying the differences between these notions. Why? If you don't care about the difference, why don't you just deal with strict or exact equality, and leave the implementation details to someone else? Coherence issues don't penetrate to a lower level than strict equality. Judgmental, definitional, and substitutive equality are special cases of strict equality that differ in their implementation properties. -- 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: 3541 bytes --]

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.

On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atmacen@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.

[-- 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 --]

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: 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 --]

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.

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.

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.

[-- 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 --]

[-- 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 --]

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.

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.

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.

[-- 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 --]

[-- 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: 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: 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 --]

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: 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 --]

[-- 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: Type: text/plain, Size: 5139 bytes --] Hi, I have already written on this topic but I had some thoughts, actually this is related to my explanation of judgemental equality when teaching type theory. In Set Theory we have the element relation and equality and both are propositions, so in some sense dynamic. Eg whether a element relation holds may depend on some assumptions you have made and the same goes for equality. In type theory as in statically typed programming languages typing is a judgement, i.e. it is static (Actually I think there is a nice anology of set theory vs type theory = python vs Haskell). The reason is that we only talk about typed objects and as a consequence a phrase in our language refers to an object whose type is known statically. In particular the type doesn’t depend on some assumptions. If I say that x is a natural number then this is not dependent on some other assumptions I have made. Once I have dependent types this static reasoning needs to be extended. If I define n = 3 and I am checking that (1,2,3) is a vector of size n I need to unfold the definition of n. Actually I am already unfolding the definition of Vec anyway. Hence I am introducing a static equality judgement accompanying my static element judgement. Now what exactly are equalities that are known statically. It seems very natural to include beta equalities and the unfolding of recursive definitions. It is less obvious whether we should include eta equalities because we can only do this for some types and not for all. Hence one of the issues with definitional / judgemental equality is that it is not clear what exactly should be included and what not. With the introduction of HoTT another important aspect of judgemental equality became apparent: it is a universal strict equality. As I have argued it may be a good idea to have a stronger universal strict equality, in particular one which is not a static judgement. However, now we end up with 3 equalities: judgemental, strict and propositional equality (I stick to this term even if propositional equality may not be a proposition). This may make it difficult to convince the non type theorists that type theory is cool. Hence maybe we can only have 2 or 1 equality and reduce judgemental equality to a mere convenience but not a fundamental feature of type theory. Thorsten From: <homotopytypetheory@googlegroups.com> on behalf of Anders Mörtberg <andersmortberg@gmail.com> Date: Wednesday, 6 February 2019 at 04:13 To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type. -- Anders On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: The type checking rules are nonlinear (reuses metavariables). For example, for function application, the type of the argument needs to "equal" the domain of the function. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic equality. But it seems really really hard to have judgmental equality be just syntactic equality, in a dependent type system. It would also be unnatural, from a computational perspective; the judgmental equations are saying something about the computational behavior of the system. On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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: 9060 bytes --]

The supposed arbitrariness of some types having strict eta and others not has been mentioned at least twice. However, I don't find it arbitrary at all: *negative* types have strict eta, while positive types don't. Since negative types are determined by maps *in*, all of their elements, identifications, and so on are determined directly, and strictly; whereas positive types are determined by maps *out*, and in particular their higher groupoid structure must be freely generated for some sense of "free", giving rise to lots of scope for flabbiness. It's quite common in higher category theory for "semi-strictified objects" to admit some strict limits and other "mapping in" universal properties (e.g. the category of algebras and pseudomorphisms for a 2-monad has strict PIE-limits, the category of fibrant objects in a model category has strict pullbacks of fibrations, etc.), but much rarer for them to have strict colimits and other "mapping out" universal properties. In particular, the difference in whether Sigma-types have strict eta or not simply lies in whether we are talking about positive Sigma-types or negative Sigma-types, which are different things, even though they turn out to be equivalent. Type theorists and logicians are familiar by now with the fact that positive and negative binary products / conjunctions are different things, even though they happen to be equivalent in "cartesian" type theory and logic, because they can be disentangled in linear logic. I don't know whether any kind of "linear dependent type theory" can disentangle positive and negative Sigma-types, but both syntactically and semantically it still makes sense to me to consider them as different things that just happen to be equivalent. It also happens sometimes in category theory that a limit and a colimit coincide (e.g. split idempotents, biproducts in an additive category, etc. https://ncatlab.org/nlab/show/absolute+colimit); but depending on whether we consider them as a limit or a colimit, it's natural that we might get different amounts of strictness. On Sat, Feb 16, 2019 at 7:59 AM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > Hi, > > > > I have already written on this topic but I had some thoughts, actually this is related to my explanation of judgemental equality when teaching type theory. > > > > In Set Theory we have the element relation and equality and both are propositions, so in some sense dynamic. Eg whether a element relation holds may depend on some assumptions you have made and the same goes for equality. In type theory as in statically typed programming languages typing is a judgement, i.e. it is static (Actually I think there is a nice anology of set theory vs type theory = python vs Haskell). The reason is that we only talk about typed objects and as a consequence a phrase in our language refers to an object whose type is known statically. In particular the type doesn’t depend on some assumptions. If I say that x is a natural number then this is not dependent on some other assumptions I have made. Once I have dependent types this static reasoning needs to be extended. If I define n = 3 and I am checking that (1,2,3) is a vector of size n I need to unfold the definition of n. Actually I am already unfolding the definition of Vec anyway. Hence I am introducing a static equality judgement accompanying my static element judgement. Now what exactly are equalities that are known statically. It seems very natural to include beta equalities and the unfolding of recursive definitions. It is less obvious whether we should include eta equalities because we can only do this for some types and not for all. Hence one of the issues with definitional / judgemental equality is that it is not clear what exactly should be included and what not. > > > > With the introduction of HoTT another important aspect of judgemental equality became apparent: it is a universal strict equality. As I have argued it may be a good idea to have a stronger universal strict equality, in particular one which is not a static judgement. However, now we end up with 3 equalities: judgemental, strict and propositional equality (I stick to this term even if propositional equality may not be a proposition). This may make it difficult to convince the non type theorists that type theory is cool. Hence maybe we can only have 2 or 1 equality and reduce judgemental equality to a mere convenience but not a fundamental feature of type theory. > > > > Thorsten > > > > > > > > From: <homotopytypetheory@googlegroups.com> on behalf of Anders Mörtberg <andersmortberg@gmail.com> > Date: Wednesday, 6 February 2019 at 04:13 > To: Homotopy Type Theory <homotopytypetheory@googlegroups.com> > Subject: [HoTT] Re: Why do we need judgmental equality? > > > > Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type. > > > > -- > > Anders > > > On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: > > The type checking rules are nonlinear (reuses metavariables). For example, for function application, the type of the argument needs to "equal" the domain of the function. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic equality. But it seems really really hard to have judgmental equality be just syntactic equality, in a dependent type system. It would also be unnatural, from a computational perspective; the judgmental equations are saying something about the computational behavior of the system. > > On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: > > In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? > > > > Thanks, > > Felix Rech > > -- > 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.

On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: However, I don't find it arbitrary at all: *negative* types have strict eta, while positive types don't. This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable. E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally. infix 5 _∷_ record Stream (A : Set) : Set where constructor _∷_ coinductive field hd : A tl : Stream A open Stream etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s etaStream = {!refl!} CCed to the agda list. Maybe somebody can comment on the decidabilty status? 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 #1.1: Type: text/plain, Size: 921 bytes --] What about strict uniqueness for the empty type? In general, what about the "discrete" inductive types of computational HDTT, including HTS-style natural numbers? I understand that this is not something we expect all models to have, but they're useful when available, and they have strict extensionality. On Saturday, February 16, 2019 at 8:25:43 PM UTC-5, Michael Shulman wrote: > > The supposed arbitrariness of some types having strict eta and others > not has been mentioned at least twice. However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. ... > -- 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: 1269 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1918 bytes --] (Since I've already made such a fuss about Nuprl anyway...) Nuprl has a type of streams (of whatever) up to bisimilarity. That is, bisimilar streams are judgmentally equal. Bisimilarity of bit streams is already undecidable. This is essentially the same problem as extensional equality of functions (nat->bool). I think eta *reduction* of streams would be OK to throw in, but it won't get you strict extensionality. On Sunday, February 17, 2019 at 2:56:40 AM UTC-5, Thorsten Altenkirch wrote: > > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on > behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> > on behalf of shu...@sandiego.edu <javascript:>> wrote: > > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. > > This is a very good point. However Streams are negative types but for > example agda doesn't use eta conversion on them, I think for a good reason. > Actually I am not completely sure whether this is undecidable. > > E.g. the following equation cannot be proven using refl (it can be proven > in cubical agda btw). The corresponding equation for Sigma types holds > definitionally. > > infix 5 _∷_ > > record Stream (A : Set) : Set where > constructor _∷_ > coinductive > field > hd : A > tl : Stream A > > open Stream > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s > etaStream = {!refl!} > > CCed to the agda list. Maybe somebody can comment on the decidabilty > status? > > -- 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: 2913 bytes --]

Well, I'm not really convinced that coinductive types should be treated as basic type formers, rather than simply constructed out of inductive types and extensional functions. For one thing, I have no idea how to construct coinductive types as basic type formers in homotopical models. I think the issue that you raise, Thorsten, could be regarded as another argument against treating them basically, or at least against regarding them as really "negative" in the same way that Pis and (negative) Sigmas are. And as for adding random extra strict equalities pertaining certain positive types that happen to hold in some particular model, Matt, I would say similarly that the general perspective gives yet another reason why you shouldn't do that. (-: But the real point is that the general perspective I was proposing doesn't claim to be the *only* way to do things; obviously it isn't. It's just a non-arbitrary "baseline" that is consistent and makes sense and matches a common core of equalities used in many type theories, so that when you deviate from it you're aware that you're being deviant. (-: On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. > > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable. > > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally. > > infix 5 _∷_ > > record Stream (A : Set) : Set where > constructor _∷_ > coinductive > field > hd : A > tl : Stream A > > open Stream > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s > etaStream = {!refl!} > > CCed to the agda list. Maybe somebody can comment on the decidabilty status? > > > > > 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.

For me the idea of inductive vs coinductive or how I called this a while ago data vs codata is an important basic intuition which comes before formal model constructions. Types are defined by constructors or by destructors, eg coproducts are defined by constructors while functions are defined by destructors, namely application. That is a function is something you can apply to arguments obtaining a result. Lambda is a derived construction, I can construct a function if I have a method to compute the result. Similarily natural numbers and lists are given by constructors, while streams are defined by destructors, to give a stream means to be able to say what its head and its tail are. And that is perfectly right Sigma types can be either given by a constructor or by destructors so in this sense they are twitters. There are reductions which just means that certain type formers are universal in that we can define all other from them, e.g. function types together with some inductive types are sufficient to derive a certain class of codata types. That doesn't mean that the dichotomy between data and codata isn't an important basic intuition. On 17/02/2019, 09:19, "Michael Shulman" <shulman@sandiego.edu> wrote: Well, I'm not really convinced that coinductive types should be treated as basic type formers, rather than simply constructed out of inductive types and extensional functions. For one thing, I have no idea how to construct coinductive types as basic type formers in homotopical models. I think the issue that you raise, Thorsten, could be regarded as another argument against treating them basically, or at least against regarding them as really "negative" in the same way that Pis and (negative) Sigmas are. And as for adding random extra strict equalities pertaining certain positive types that happen to hold in some particular model, Matt, I would say similarly that the general perspective gives yet another reason why you shouldn't do that. (-: But the real point is that the general perspective I was proposing doesn't claim to be the *only* way to do things; obviously it isn't. It's just a non-arbitrary "baseline" that is consistent and makes sense and matches a common core of equalities used in many type theories, so that when you deviate from it you're aware that you're being deviant. (-: On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. > > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable. > > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally. > > infix 5 _∷_ > > record Stream (A : Set) : Set where > constructor _∷_ > coinductive > field > hd : A > tl : Stream A > > open Stream > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s > etaStream = {!refl!} > > CCed to the agda list. Maybe somebody can comment on the decidabilty status? > > > > > 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. 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.

> For me the idea of inductive vs coinductive or how I called this a while > ago data vs codata is an important basic intuition which comes before > formal model constructions. Types are defined by constructors or by > destructors, eg coproducts are defined by constructors while functions are > defined by destructors, namely application. That is a function is > something you can apply to arguments obtaining a result. Lambda is a > derived construction, I can construct a function if I have a method to > compute the result. Similarily natural numbers and lists are given by > constructors, while streams are defined by destructors, to give a stream > means to be able to say what its head and its tail are. And that is > perfectly right Sigma types can be either given by a constructor or by > destructors so in this sense they are twitters. > > There are reductions which just means that certain type formers are > universal in that we can define all other from them, e.g. function types > together with some inductive types are sufficient to derive a certain > class of codata types. That doesn't mean that the dichotomy between data > and codata isn't an important basic intuition. > > On 17/02/2019, 09:19, "Michael Shulman" <shulman@sandiego.edu> wrote: > > Well, I'm not really convinced that coinductive types should be > treated as basic type formers, rather than simply constructed out of > inductive types and extensional functions. For one thing, I have no > idea how to construct coinductive types as basic type formers in > homotopical models. I think the issue that you raise, Thorsten, could > be regarded as another argument against treating them basically, or at > least against regarding them as really "negative" in the same way that > Pis and (negative) Sigmas are. > > And as for adding random extra strict equalities pertaining certain > positive types that happen to hold in some particular model, Matt, I > would say similarly that the general perspective gives yet another > reason why you shouldn't do that. (-: > But function types are neither inductive nor conductive. Only N-> (-) ist coinductive. In presence of function types most coinductive types can be implemented. Maybe coinductive is a style of programming but nothing really foundational. Thomas -- 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.

But function types are neither inductive nor conductive. Only N-> (-) ist coinductive. In presence of function types most coinductive types can be implemented. You think of terminal coalgebras - that is not what I mean. To avoid this confusion I am using the term codata but most people in CS understand coinductive better. You can define a type by saying how elements can be constructed, this is data Alternatively you say what you can do with it, i.e. how elements can be destructed. The function type is not data, functions are not understood by the way they are constructed but what you can do with it. A function is something you can apply to an argument and you get a result. Codata types always introduce non-trivial equalities, because all you can do with a function is applying it to arguments two functions which provide the same output for all inputs are equal. Hence functional extensionality should hold. Maybe coinductive is a style of programming but nothing really foundational. I think you miss something important here. 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 #1.1: Type: text/plain, Size: 3379 bytes --] What about infinitary (non-elementary) limits? Are there infinitary homotopy-limits? They are more common than discrete inductive types, right? So what if I considered a stream of A to be essentially an omega-fold product of A. Would that have a strict extensionality principle? More generally, I would try and say that a coinductive type is some limit of an external diagram of elimination spines. This might address Thomas Streicher's objection, since the collection of elimination spines is countable externally. On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman wrote: > > Well, I'm not really convinced that coinductive types should be > treated as basic type formers, rather than simply constructed out of > inductive types and extensional functions. For one thing, I have no > idea how to construct coinductive types as basic type formers in > homotopical models. I think the issue that you raise, Thorsten, could > be regarded as another argument against treating them basically, or at > least against regarding them as really "negative" in the same way that > Pis and (negative) Sigmas are. > > And as for adding random extra strict equalities pertaining certain > positive types that happen to hold in some particular model, Matt, I > would say similarly that the general perspective gives yet another > reason why you shouldn't do that. (-: > > But the real point is that the general perspective I was proposing > doesn't claim to be the *only* way to do things; obviously it isn't. > It's just a non-arbitrary "baseline" that is consistent and makes > sense and matches a common core of equalities used in many type > theories, so that when you deviate from it you're aware that you're > being deviant. (-: > > On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch > <Thorsten....@nottingham.ac.uk <javascript:>> wrote: > > > > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on > behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> > on behalf of shu...@sandiego.edu <javascript:>> wrote: > > > > However, I don't find it > > arbitrary at all: *negative* types have strict eta, while positive > > types don't. > > > > This is a very good point. However Streams are negative types but for > example agda doesn't use eta conversion on them, I think for a good reason. > Actually I am not completely sure whether this is undecidable. > > > > E.g. the following equation cannot be proven using refl (it can be > proven in cubical agda btw). The corresponding equation for Sigma types > holds definitionally. > > > > infix 5 _∷_ > > > > record Stream (A : Set) : Set where > > constructor _∷_ > > coinductive > > field > > hd : A > > tl : Stream A > > > > open Stream > > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s > > etaStream = {!refl!} > > > > CCed to the agda list. Maybe somebody can comment on the decidabilty > status? > -- 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: 4677 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 468 bytes --] On Sunday, February 17, 2019 at 7:08:52 AM UTC-5, Matt Oliveri wrote: > > since the collection of elimination spines is countable externally. > Oh wait, I guess not. -- 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: 822 bytes --]

[-- Attachment #1: Type: text/plain, Size: 819 bytes --] On Sun, Feb 17, 2019 at 1:25 AM Michael Shulman <shulman@sandiego.edu> wrote: > The supposed arbitrariness of some types having strict eta and others > not has been mentioned at least twice. However, I don't find it > arbitrary at all [...] In particular, the difference in whether > Sigma-types have strict eta > or not simply lies in whether we are talking about positive > Sigma-types or negative Sigma-types Since I've mentioned eta for Sigma in this context: thanks for this explanation, Mike! -- Nicolai > -- 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: 1440 bytes --]

> CCed to the agda list. Maybe somebody can comment on the decidabilty status? Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types Talk given at CMCS'18 Thessaloniki, Greece, 15 April 2018 http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf On 2019-02-17 08:56, Thorsten Altenkirch wrote: > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote: > > However, I don't find it > arbitrary at all: *negative* types have strict eta, while positive > types don't. > > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable. > > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally. > > infix 5 _∷_ > > record Stream (A : Set) : Set where > constructor _∷_ > coinductive > field > hd : A > tl : Stream A > > open Stream > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s > etaStream = {!refl!} > > CCed to the agda list. Maybe somebody can comment on the decidabilty status? > > > > > 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. > > > > > _______________________________________________ > Agda mailing list > Agda@lists.chalmers.se > https://lists.chalmers.se/mailman/listinfo/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.

I think Thomas is referring to M-types which can be constructed in HoTT, moreover, they have the right equality in guarded or cubical type theory. I've collected some references here. Please feel free to expand. https://ncatlab.org/nlab/show/M-type On Sun, Feb 17, 2019 at 12:44 PM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: > > > > But function types are neither inductive nor conductive. Only N-> (-) ist > coinductive. > In presence of function types most coinductive types can be implemented. > > You think of terminal coalgebras - that is not what I mean. To avoid this confusion I am using the term codata but most people in CS understand coinductive better. You can define a type by saying how elements can be constructed, this is data Alternatively you say what you can do with it, i.e. how elements can be destructed. The function type is not data, functions are not understood by the way they are constructed but what you can do with it. A function is something you can apply to an argument and you get a result. Codata types always introduce non-trivial equalities, because all you can do with a function is applying it to arguments two functions which provide the same output for all inputs are equal. Hence functional extensionality should hold. > > Maybe coinductive is a style of programming but nothing really foundational. > > I think you miss something important here. > > > > > 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.

admittedly, by coinductive I understand terminal coalgebra in MLTT even function types are inductive though that's a bit of cheating in my eyes so I must say I don't understand what you mean by codata types technically I know positive and negative polarity in the sense of linear logic people presumably, that'scloser to what you have in mind thomas -- 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 tried to explain in common sense term what is a function? And my answer is that it is something you can apply to an element of the domain and you get an element of the codomain. You don’t know how you can inspect the function that is all you know. Hence the function type is explained by what you can do with it. That’s coastal. Compare this with natural numbers. A natural number is 0 or the successor of a natural number. You explain how to produce them. That’s data. What is a stream? A stream is something you can get the head and the tail of. So that is codata as well. Sent from my iPhone > On 17 Feb 2019, at 19:36, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote: > > admittedly, by coinductive I understand terminal coalgebra > > in MLTT even function types are inductive though that's a bit of > cheating in my eyes > > so I must say I don't understand what you mean by codata types > technically > > I know positive and negative polarity in the sense of linear logic people > presumably, that'scloser to what you have in mind > > thomas 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 #1.1: Type: text/plain, Size: 3381 bytes --] On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote: > > why is it claimed that definitional equalities are essential to dependent > type theories? > I've tested what happens if we replace definitional/judgmental equalities in MLTT by identity types, working in the fragment of Agda that only has Π and universes (built-in) and hence my Π has its usual judgemental rules, including the η rule (but this rule could be disabled). In order to switch off definitional equalities for the identity type and Σ types, I work with them given as hypothetical arguments to a module (and no hence with no definitions): _≡_ : {X : 𝓤} → X → X → 𝓤 -- Identity type. refl : {X : 𝓤} (x : X) → x ≡ x J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) → A x (refl x) → (y : X) (r : x ≡ y) → A y r J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) → (a : A x (refl x)) → J x A a x (refl x) ≡ a Σ : {X : 𝓤} → (X → 𝓤) → 𝓤 _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} → ((x : X) (y : Y x) → A (x , y)) → (z : Σ Y) → A z Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} → (f : (x : X) (y : Y x) → A (x , y)) → (x : X) → (y : Y x) → Σ-elim f (x , y) ≡ f x y Everything I try to do with the identity type just works, including the more advanced things of univalent mathematics - but obviously I haven't tried everything that can be tried. However, although I can define both projections pr₁ and pr₂ for Σ, and prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get p : pr₁ (x , y) ≡ x but only pr₂ (x , y) ≡ transport Y (p ⁻¹) y It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further assumptions. But maybe I overlooked something. One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by the the single axiom Σ-single : {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤) → (f : (x : X) (y : Y x) → A (x , y)) → is-contr (Σ λ (g : (z : Σ Y) → A z) → (x : X) (y : Y x) → g (x , y) ≡ f x y) I don't know whether this works. (I suspect the fact that "induction principles ≃ contractibility of the given data with their computation rules" is valid only in the presence of definitional equalities for the induction principle, and that the contractibility version has a better chance to work in the absence of definitional equalities.) One can also wonder whether the presentation taking the projections with their computation rules as primitive, and the η rule would work. But again we can define Σ-elim but not Σ-comp for it. In any case, without further identities, simply replacing definitional equalities by identity types doesn't seem to work, although I may be missing something. Martin -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 4621 bytes --]

Hi, I’m confused — does it even type check to ask pr₂ (x , y) ≡ y ? I would expect x : A y : B(x) (x,y) : Σ A B fst (x,y) : A snd (x,y) : B(fst (x,y)) so if beta for fst is weak, then pr₂ (x , y) ≡ transport Y (p ⁻¹) y is the best you could hope for. I.e., you have a path for the first beta, and a path over it for the second. -Dan > On Feb 18, 2019, at 12:37 PM, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote: > > On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote: > why is it claimed that definitional equalities are essential to dependent type theories? > > I've tested what happens if we replace definitional/judgmental > equalities in MLTT by identity types, working in the fragment of Agda > that only has Π and universes (built-in) and hence my Π has its usual > judgemental rules, including the η rule (but this rule could be disabled). > > In order to switch off definitional equalities for the identity type > and Σ types, I work with them given as hypothetical arguments to a module > (and no hence with no definitions): > > _≡_ : {X : 𝓤} → X → X → 𝓤 -- Identity type. > > refl : {X : 𝓤} (x : X) → x ≡ x > > J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) > → A x (refl x) → (y : X) (r : x ≡ y) → A y r > > J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) > → (a : A x (refl x)) → J x A a x (refl x) ≡ a > > Σ : {X : 𝓤} → (X → 𝓤) → 𝓤 > > _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y > > Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} > → ((x : X) (y : Y x) → A (x , y)) > → (z : Σ Y) → A z > > Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} > → (f : (x : X) (y : Y x) → A (x , y)) > → (x : X) > → (y : Y x) > → Σ-elim f (x , y) ≡ f x y > > Everything I try to do with the identity type just works, including > the more advanced things of univalent mathematics - but obviously I > haven't tried everything that can be tried. > > However, although I can define both projections pr₁ and pr₂ for Σ, and > prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get > > p : pr₁ (x , y) ≡ x > > but only > > pr₂ (x , y) ≡ transport Y (p ⁻¹) y > > It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further > assumptions. But maybe I overlooked something. > > One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by > the the single axiom > > Σ-single : > {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤) > → (f : (x : X) (y : Y x) → A (x , y)) > → is-contr (Σ λ (g : (z : Σ Y) → A z) > → (x : X) (y : Y x) → g (x , y) ≡ f x y) > > I don't know whether this works. (I suspect the fact that "induction > principles ≃ contractibility of the given data with their computation > rules" is valid only in the presence of definitional equalities for > the induction principle, and that the contractibility version has a > better chance to work in the absence of definitional equalities.) > > One can also wonder whether the presentation taking the projections > with their computation rules as primitive, and the η rule would > work. But again we can define Σ-elim but not Σ-comp for it. > > In any case, without further identities, simply replacing definitional > equalities by identity types doesn't seem to work, although I may be > missing something. > > Martin > > > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to 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: 4751 bytes --] Sorry, I was being silly. Martin On Monday, 18 February 2019 19:22:23 UTC, dlicata wrote: > > Hi, > > I’m confused — does it even type check to ask pr₂ (x , y) ≡ y ? > > I would expect > > x : A > y : B(x) > (x,y) : Σ A B > fst (x,y) : A > snd (x,y) : B(fst (x,y)) > > so if beta for fst is weak, then > > pr₂ (x , y) ≡ transport Y (p ⁻¹) y > > is the best you could hope for. I.e., you have a path for the first beta, > and a path over it for the second. > > -Dan > > > On Feb 18, 2019, at 12:37 PM, Martín Hötzel Escardó < > escardo...@gmail.com <javascript:>> wrote: > > > > On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote: > > why is it claimed that definitional equalities are essential to > dependent type theories? > > > > I've tested what happens if we replace definitional/judgmental > > equalities in MLTT by identity types, working in the fragment of Agda > > that only has Π and universes (built-in) and hence my Π has its usual > > judgemental rules, including the η rule (but this rule could be > disabled). > > > > In order to switch off definitional equalities for the identity type > > and Σ types, I work with them given as hypothetical arguments to a > module > > (and no hence with no definitions): > > > > _≡_ : {X : 𝓤} → X → X → 𝓤 -- Identity type. > > > > refl : {X : 𝓤} (x : X) → x ≡ x > > > > J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) > > → A x (refl x) → (y : X) (r : x ≡ y) → A y r > > > > J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) > > → (a : A x (refl x)) → J x A a x (refl x) ≡ a > > > > Σ : {X : 𝓤} → (X → 𝓤) → 𝓤 > > > > _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y > > > > Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} > > → ((x : X) (y : Y x) → A (x , y)) > > → (z : Σ Y) → A z > > > > Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} > > → (f : (x : X) (y : Y x) → A (x , y)) > > → (x : X) > > → (y : Y x) > > → Σ-elim f (x , y) ≡ f x y > > > > Everything I try to do with the identity type just works, including > > the more advanced things of univalent mathematics - but obviously I > > haven't tried everything that can be tried. > > > > However, although I can define both projections pr₁ and pr₂ for Σ, and > > prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get > > > > p : pr₁ (x , y) ≡ x > > > > but only > > > > pr₂ (x , y) ≡ transport Y (p ⁻¹) y > > > > It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further > > assumptions. But maybe I overlooked something. > > > > One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by > > the the single axiom > > > > Σ-single : > > {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤) > > → (f : (x : X) (y : Y x) → A (x , y)) > > → is-contr (Σ λ (g : (z : Σ Y) → A z) > > → (x : X) (y : Y x) → g (x , y) ≡ f x y) > > > > I don't know whether this works. (I suspect the fact that "induction > > principles ≃ contractibility of the given data with their computation > > rules" is valid only in the presence of definitional equalities for > > the induction principle, and that the contractibility version has a > > better chance to work in the absence of definitional equalities.) > > > > One can also wonder whether the presentation taking the projections > > with their computation rules as primitive, and the η rule would > > work. But again we can define Σ-elim but not Σ-comp for it. > > > > In any case, without further identities, simply replacing definitional > > equalities by identity types doesn't seem to work, although I may be > > missing something. > > > > Martin > > > > > > > > > > -- > > You received this message because you are subscribed to the Google > Groups "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to 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: 6213 bytes --]

On Sun, Feb 17, 2019 at 4:08 AM Matt Oliveri <atmacen@gmail.com> wrote: > What about infinitary (non-elementary) limits? Are there infinitary homotopy-limits? They are more common than discrete inductive types, right? So what if I considered a stream of A to be essentially an omega-fold product of A. Would that have a strict extensionality principle? Yes, that might work. I think that the last time I thought about coinductive types in homotopy models I was trying to give them some kind of dependent coinduction principle. But if we take seriously the positive/negative perspective that I advanced before, we would expect coinductive types to have simply a destructor, a non-dependent corecursor, a beta-rule for destructing the corecursor, and an eta-principle saying something like that the endomorphism defined from the destructor and the corecursor is the identity. And that would probably be modeled by the omega-fold product of a type with itself. More generally, if F is a functor that preserves fibrations, fibrant objects, and sequential limits (like F(X) = A x X for streams), then the infinite limit ... -> F(F(F(1))) -> F(F(1)) -> F(1) -> 1 might be a model for the corresponding coinductive type with such an eta-principle. So maybe there's nothing wrong with coinductive types as such, and the point is just that computational considerations like decidability don't always match up with the principled category-theoretic explanations. (-: > On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman wrote: >> >> Well, I'm not really convinced that coinductive types should be >> treated as basic type formers, rather than simply constructed out of >> inductive types and extensional functions. For one thing, I have no >> idea how to construct coinductive types as basic type formers in >> homotopical models. I think the issue that you raise, Thorsten, could >> be regarded as another argument against treating them basically, or at >> least against regarding them as really "negative" in the same way that >> Pis and (negative) Sigmas are. >> >> And as for adding random extra strict equalities pertaining certain >> positive types that happen to hold in some particular model, Matt, I >> would say similarly that the general perspective gives yet another >> reason why you shouldn't do that. (-: >> >> But the real point is that the general perspective I was proposing >> doesn't claim to be the *only* way to do things; obviously it isn't. >> It's just a non-arbitrary "baseline" that is consistent and makes >> sense and matches a common core of equalities used in many type >> theories, so that when you deviate from it you're aware that you're >> being deviant. (-: >> >> On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch >> <Thorsten....@nottingham.ac.uk> wrote: >> > >> > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote: >> > >> > However, I don't find it >> > arbitrary at all: *negative* types have strict eta, while positive >> > types don't. >> > >> > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable. >> > >> > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally. >> > >> > infix 5 _∷_ >> > >> > record Stream (A : Set) : Set where >> > constructor _∷_ >> > coinductive >> > field >> > hd : A >> > tl : Stream A >> > >> > open Stream >> > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s >> > etaStream = {!refl!} >> > >> > CCed to the agda list. Maybe somebody can comment on the decidabilty status? > > -- > 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.