Subscripts to \eqto

[marcbezem]

In Ch. 2 there are no subscripts to \eqto, \eq or =, not even in the type of \ap, where the two \eqto's would have subscripts X and Y, that may be different types. I can't recall whether this was a conscious decision, or whether no need was felt. In Ch. 3 there are 48 such occurrences (of gross > 500 occurrences of =), in particular in the parts of Ch. 3 that were written early on. Often there is no need at all, like in $\sum_{a:A} a \eqto_A a$. I propose to remove such subscripts, also in later chapters, unless they really clarify the expression. It would be weird not to have them in the introductory chapter, and introduce them later on. Alternatively, we could say something about this in the sections 2.5 and/or 2.6 (when \ap is defined). Please give me your votes/opinions on this.

[pierrecagne]

If we can effectively remove all subscripts, I would vote that we do.

The only places where they might be important that come to mind right now are:

1. A = B for A and B types, as the identity type a priori depends on the universe as we discussed last time (even thought they are all equivalent a posteriori)
2. x = y when x,y are used abusively to denote elements (x,!) and (y,!) of a subtype of the type of x and y. Here again both interpretations of the identity type are equivalent so it shouldn't be dangerous as long as definitional equality is not involved.

[bidundas]

If we do such a thing, we should be careful of reminding the reader what type things have, especially if there have been a lot of equivalences along the way. As it is, the subscript is often a timely reminder.

[if a typecheck is supposed to help clarify things, the reader better be informed of the type]

Bjorn

On 2 Mar 2023, at 16:11, Pierre Cagne @.***> wrote:

If we can effectively remove all subscripts, I would vote that we do.

The only places where they might be important that come to mind right now are:

• A = B for A and B types, as the identity type a priori depends on the universe as we discussed last time (even thought they are all equivalent a posteriori) • x = y when x,y are used abusively to denote elements (x,!) and (y,!) of a subtype of the type of x and y. Here again both interpretations of the identity type are equivalent so it shouldn't be dangerous as long as definitional equality is not involved. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.