a figure of speech

[DanGrayson]

Perhaps it would be better to use quantifiers in the traditional way:

[marcbezem]

There is not much difference between the quoted figure of speech and, e.g., "all fibers of f are sets" as used in the same screen shot. The latter also has an implicit quantification, namely over Y, and states that all function values of the function fib_f : Y -> U are sets. I would not object against rephrasing the quoted figure of speech to: "all actions on paths of f are ....", but spelling out this and all similar figures of speech does not seem a good idea to me.

[DanGrayson]

Actually, there is a big difference. In "all fibers of f" we are quantifying over the fibers, and we know what a fiber of f is. But in "each ap_f", we aren't told what we're quantifying over. The latter usage reminds me of a similar misusage: if x is a sequence, some people like to say "each x_i ...", hoping the reader will interpret that correctly as "for each i, x_i ...". That misusage will clash with this misusage, for after reading "each ap_f ...", the reader accustomed to seeing the other misusage will try to interpret as "for each f, ap_f ...", and that is not what is meant.

I sort of like your suggestion about using "all actions on paths of f are ...." -- at least it's not a misusage. But I think the word "action" is overused.

One simple thing we could do is to modify the definition of ap_f to make the two points part of the notation, introducing ap_f,x,x'. Then we could immediately say that ap_f,x,x' can be abbreviated to ap_f if x and x' are clear from the context.

Then here we could adopt the traditional usage, saying "for each x, x', the map ap_f,x,x' ...". This figure of speech is used only 4 times, so replacing it by something immediately understandable will be an improvement.

[marcbezem]

Well, I tell the reader what we're quantifying over in the same sentence. And I don't think the difference with the fibers is that big. And even your example "each x_i ..." would not worry me, although it is indeed a slight abuse of language. The point where I definitely agree is when you say that "each ap_f", without the ensuing definition, can be misunderstood as to quantify over f. There are 51 occurrences of " action" in the book, none in intro-uf.tex, and we should not add more for the sole purpose of clarifying "each ap_f". So my preferred fix would be "all applications on paths of f are ....", but I can live with any other clarification as well.

[DanGrayson]

Re: "all applications on paths of f are ...."

I wonder whether readers will realize that an "application" is a function. Maybe something like "all maps on paths induced by f" instead?

[DanGrayson]

Or "all maps on identity types induced by f"?

[UlrikBuchholtz]

Or "all maps on identity types induced by f"?

I'm fine with that. It also occurred to me that another instance of the “all X of Y” construction that we use a lot in type theory is “all identity types of A”, e.g., “A is a set if all its identity types are propositions”. It's not surprising that when reasoning about functions, we'll need similar constructions. So “f is an injection if all of its maps on identity types are equivalences”.

But it becomes a bit more cumbersome in the next item: “All fibers of f are sets if all fibers of its maps on identity types are propositions.” (This particular case could be alleviated by introducing n-truncatedness of maps: “f is (n+1)-truncated iff all of its maps on identity types are n-truncated.” Or, “f is set-truncated iff all of its maps on identity types are injections.”)

[marcbezem]

I'm also fine with that. I see the (old) footnote 13 has been deleted (which is fine). Is there someting new announcing "maps on identity types"?

[DanGrayson]

The footnote "Another name is the \emph{action on paths} of $f$" has been replaced by this text:

[DanGrayson]

In another location Ulrik framed it this way:

We should probably be consistent.

[DanGrayson]

I've added a footnote:

But now I wonder whether it's a good idea to introduce synonyms, when we could just avoid using them and say "function" every time.

Advice?

[marcbezem]

This can be cultural thing. Some statistics: There are 445 lines in which "map" occurs, including 18 with "mapping". I like "map" since it is short, like "path" for "identification". I could do without "mapping", but not without "function". In writing classes one is sometimes taught to avoid repeated use of the same word and to consider synonyms to make the text less boring. This advice seems less relevant for mathematical prose :-) See you soon!