Always write ap_f(p) instead of f(p)?

[mikeshulman]

For the second edition, perhaps we should reconsider the decision to write f(p) for ap_f(p). It confuses some readers, especially those trying to formalize the arguments in a proof assistant, and it's unclear to me that it has a real benefit. I believe it was motivated by the fact that in category theory we write both F(X) and F(f) for the action of a functor on objects and morphisms, but I'm no longer convinced (if I ever was) that this analogy is important enough to carry the day.

[EgbertRijke]

I agree. In my course I also used ap_f(p) throughout, to not confuse my students, which helped them seeing what was going on.

Similarly for transport, they also preferred trB(p,b) over p*(b), to have an explicit mention of the family with respect to which the transport is taken, and they kept getting mixed up about the order in which we write a path concatenation.

On Wed, Apr 25, 2018 at 12:36 PM, Mike Shulman notifications@github.com wrote:

For the second edition, perhaps we should reconsider the decision to write f(p) for ap_f(p). It confuses some readers, especially those trying to formalize the arguments in a proof assistant, and it's unclear to me that it has a real benefit. I believe it was motivated by the fact that in category theory we write both F(X) and F(f) for the action of a functor on objects and morphisms, but I'm no longer convinced (if I ever was) that this analogy is important enough to carry the day.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HoTT/book/issues/989, or mute the thread https://github.com/notifications/unsubscribe-auth/ABMbuj84d_lc31xX2HAO-AFi2wNg3KRuks5tsKYAgaJpZM4TjxPQ .

-- egbertrijke.com

[mikeshulman]

Good point about transport. Indeed a proof assistant nearly always seems to require the family to be given explicitly, and probably a human reader is in general little better at doing that inference.

I don't know whether we should change the order of path-concatenation, though; I expect that whichever choice we make, someone will be confused. (-:

[awodey]

I don’t think that the fact that a proof assistant requires something is a very good reason to do it informally : - ) isn’t it enough to have a more verbose “official” notation, and then drop the additional decoration informally for readability?

On Apr 25, 2018, at 5:27 PM, Mike Shulman notifications@github.com wrote:

Good point about transport. Indeed a proof assistant nearly always seems to require the family to be given explicitly, and probably a human reader is in general little better at doing that inference.

I don't know whether we should change the order of path-concatenation, though; I expect that whichever choice we make, someone will be confused. (-:

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HoTT/book/issues/989#issuecomment-384439883, or mute the thread https://github.com/notifications/unsubscribe-auth/AAqtSFUzls6oHRgwuBtZYqcLpKKZYftWks5tsOo_gaJpZM4TjxPQ.

[nicolaikraus]

In [ordinary] category theory, when we write F(X) and F(f) it's usually clear which one is an object and which one is a morphism because of the convention with upper and lower case letters. In type theory, it's much harder to distinguish between f(x) and f(p); I guess most of the time p is used for a path, but if P is a proposition, then p: P is not uncommon either (and it doesn't help here that "point" starts with p as well). Thus, I'd prefer ap_f(p). (I agree with Steve @awodey that the argument with proof assistants is not convincing.) I certainly wouldn't find it helpful to change path concatenation (that would create lots of confusion) but I also prefer tr_B(p,b) over p_*(b).

[mikeshulman]

Sorry, I didn't intend the mention of proof assistants to be an argument on its own. It's certainly true that there are situations in which a human is better at inferring implicit arguments than a proof assistant is (and other situations in which a proof assistant is better than a human). That's why I continued the sentence with "and probably a human reader is in general little better at doing that inference" [emphasis added].

Egbert's experience with his students is some evidence of this. My own experience with transport is that there are roughly two situations:

1. The transporting type family is nothing but a variable type family, B : A -> Type. In this case it is generally obvious what the type family should be, but at the same time it costs very little to notate it (since a single variable doesn't take up much space) and can still be helpful to some readers, if for no other reason than maintaining a consistent notation across all uses of transport.
2. The transporting type family is a more complicated family built out of various other families, type constructors, and functions. In this case it may be possible (at least for an expert human -- proof assistants almost never seem able to do this) to figure out from context what the type family must be -- but it's often hard work, and especially in a textbook we can help beginners out by notating the type family. Omitting such information can also be a source of subtle errors in a proof, e.g. if the author thinks it is "obvious" what type family we are transporting in, but then ends up accidentally confusing two transports that actually happen in two different type families (for instance, #942 is a related error).

[nicolaikraus]

Good points! As a reader, I often find it useful when the transporting type families are given explicitly, and if I don't need them, I still don't mind at all if they are written down.

[andrejbauer]

If only we had modern technology so that one could think to oneself "what is the family for this transport?" and suddenly a small annotation would appear next to tr, showing me the hidden implicit arguments. I'd even be satisfied with having to move the cursor over tr with the mouse. We're probably still decades away from such fancy stuff.

[mikeshulman]

It'll certainly be some time before a printed paper book could behave like that. Of course if we had an HTML version of the book, it could behave like that now. I don't know why PDFs don't seem to support such behavior now; there's certainly no reason they couldn't.

[gbaz]

You can generate such PDF behavior from LaTeX: https://tex.stackexchange.com/a/164186

[mikeshulman]

Interesting, thanks! I don't think I'd want to rely on a behavior that only works with a few PDF readers, though.