Sporadic use of \colon

[pierrecagne]

There is, here and there, "\colon" instead of the symbol ":"

Was this discussed at some point? IIRC, the symbol ":" in math mode is spaced as a relation, which I think is the intended semantics of is-of-type. On the contrary, "\colon" is spaced as a punctuation symbol (with some tweaks by the amsmath package).

I would vote we use only ":" and never "\colon" to denote is-of-type.

[bidundas]

Ah, goodie. Thanks for letting me go on a rant.

Quoting "In the AMS (American Mathematical Society) Short Math Guide for LaTeX you'll find both a recommendation (page 8) to use f\colon a \to b (rather than f : a \to b) and a general discussion of relation symbols. ”

and in Getting up and running with AMS-LaTeX

"(Note that if we had typed that as “f: X \to Y” then the spacing around the colon would be wrong, since the colon symbol is typeset as a binary relation, with spaces on the two sides equal.)”

The ”:” pun in HoTT was always a bad one, IMHO. As a mathematician I wouldn’t dream of writing ”f:X\to Y”, but would always write ”f\colon X\to Y”. Doing otherwise in HoTT would be an acknowledgement that the case for using the colon as describing membership doesn’t really fit.

Bjorn (who is much more pragmatic than this mail sounds)

On Aug 12, 2021, at 14:23, Pierre Cagne @.***> wrote:

There is, here and there, "\colon" instead of the symbol ":"

Was this discussed at some point? IIRC, the symbol ":" in math mode is spaced as a relation, which I think is the intended semantics of is-of-type. On the contrary, "\colon" is spaced as a punctuation symbol (with some tweaks by the amsmath package).

I would vote we use only ":" and never "\colon" to denote is-of-type.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[pierrecagne]

The problem is that I have found the use of "\colon" in the book mostly with non-function types. Like "S\colon \FinSet_n" or "z\colon \Sc".

Also, I never understood why ":" is not a relation in the denotation of a function. Although I could understand the relunctance in a math book using set-theoretic foundations (again, I don't see what is the colon if not a relation, but I could live with that), here it makes little sense. When we write "f: A\to B" in the book, we really mean f as an element of the type "A \to B", don't we? Then we can not use "z: \Sc" on one hand and "f\colon A\to B" on the other hand.

I can be mistaken about the intended semantics of "f: A\to B" in our book, but then please explain.

[bidundas]

It is possible to set up things so that membership is a binary relation, but that’s not how I think about it (and I don’t think any of us do, given that we usually take membership to be a primitive of our theories rather than som set-theoretic magic putting the term a and the type A to which it belongs in a common type in which we can have a binary relation).

As for f\colon X\to Y I certainly don’t intend \colon to be a binary relation, but rather mathematical notation to be read in one go with the \to.

Ok, I made my case, and I am probably not able to convince anyone that in LaTeX \colon is the right thing (unless, of course, you really intend ”:”). I can live with that. See you in an hour.

Bjorn

On Aug 12, 2021, at 14:58, Pierre Cagne @.***> wrote:

The problem is that I have found the use of "\colon" in the book mostly with non-function types. Like "S\colon \FinSet_n" or "z\colon \Sc".

Also, I never understood why ":" is not a relation in the denotation of a function. Although I could understand the relunctance in a math book using set-theoretic foundations (again, I don't see what is the colon if not a relation, but I could live with that), here it makes little sense. When we write "f: A\to B" in the book, we really mean f as an element of the type "A \to B", don't we? Then we can not use "z: \Sc" on one hand and "f\colon A\to B" on the other hand.

I can be mistaken about the intended semantics of "f: A\to B" in our book, but then please explain.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[DanGrayson]

As a mathematician I wouldn’t dream of writing ”f:X\to Y”, but would always write ”f\colon X\to Y”.

I've used TeX to type a lot of colons, and haven't even heard of \colon before now. Let's just be consistent, and use : because it's quicker to type than \colon.

Also, in x : X it looks good to have the same amount of space on both sides of the colon.

Yes, x : X is not a binary relation, since it's not a proposition, but it is a binary something -- a binary judgment.

[UlrikBuchholtz]

I always used to write f: X → Y as well as recommended, but now it just looks wrong to me (as does “Let x: X be given…”).

There's also the possibility of an ambiguous reading when using \colon, since the colon might actually be confused for punctuation. (“We now consider the case of g: (very large domain) → Y being surjective…”)

But I'm beating a dead horse… (The \colon is dead – long live the colon!)

[bidundas]

On Aug 12, 2021, at 15:46, Daniel R. Grayson @.***> wrote:

As a mathematician I wouldn’t dream of writing ”f:X\to Y”, but would always write ”f\colon X\to Y”.

I've used TeX to type a lot of colons, and haven't even heard of \colon before now. Let's just be consistent, and use : because it's quicker to type than \colon. That IS a valid argument

Also, in x : X it looks good to have the same amount of space on both sides of the colon. This is an opinion with which I disagree: (and not \colon) x and X live in different types and so there is no need for them to have equal space. Also this brings up the really bad thing about using ”:” for membership - you can’t tell the direction which can be nonobvious and which is fine with \in.

Yes, x : X is not a binary relation, since it's not a proposition, but it is a binary something -- a binary judgment. Again, the problem is that x and X live in different types.

Bjorn

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[DanGrayson]

Again, the problem is that x and X live in different types. Bjorn

You're probably content to write r \cdot m when r is an element of a ring R and m is an element of an R-module. And you're probably content to write X \otimes F when X is an algebraic variety over K and F is an extension of K. Those are living in different types.

[marcbezem]

Reading order is essential in many places, even if the types are the same: how to read x \cdot y in non-commutative al-jabr? (IIRC in Hebrew they read mathematical formulas like we do.)

[bidundas]

I’m not going to argue further on this since generations of typesetters, the AMS LaTeX style guide and I seem to be in minority advocating the traditional kerning for typesetting functions, beside adding that since membership is a primitive in the theory we’re free to choose our spacing for just this symbol in that context and sharing the link https://tex.stackexchange.com/questions/37789/using-colon-or-in-formulas (which discusses these mattes and has "If you're trying to typeset a variable-has-type colon in type theory, you want {:} or \mathord{:} (they display the same). For example, you'll get a nice looking STLC identity function with $\lambda x {:} A . x$.” as the second upvoted entry).

Bjorn (who, unless provoked unduly, will be silent on this matter from now on and accept anything)

On Aug 13, 2021, at 10:02, Marc Bezem @.***> wrote:

Reading order is essential in many places, even if the types are the same: how to read x \cdot y in non-commutative al-jabr? (IIRC in Hebrew they read mathematical formulas like we do.)

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android.

[DanGrayson]

Ah, so now we have 3 options to choose among:

[UlrikBuchholtz]

Actually, there are almost unlimited options to choose from, by choosing two math skips, one for each side.

Note that amsmath redefines \colon to have a bit of space to the left, so it's not purely a punctuation mark:

\renewcommand{\colon}{\nobreak\mskip2mu\mathpunct{}\nonscript
  \mkern-\thinmuskip{:}\mskip6muplus1mu\relax}

I've used TeX to type a lot of colons, and haven't even heard of \colon before now. Let's just be consistent, and use : because it's quicker to type than \colon.

That IS a valid argument

Yes, but it's easy to make : an active character, so it can expand to anything we like. In the new commit 137c088, I've done that, and as an experiment replaced : with \,\mathord\ordinarycolon\,, i.e., a version with two thin math skips.

As an added benefit, := now expands to \coloneqq, i.e., \defis.

I think I could get used to it, if it pleases y'all.

Personally, I'd still prefer the larger skips from \mathrel, since I think of the colon in “a : A” as a relation (albeit at the meta-level), but I repeat myself.

The reason to prefer a larger space is to help with grouping: The typing colon is almost always the top-most node when parsing, so it should have the largest spacing. An exception is local type-ascription as referred to above: In “λx : A. t[x]”, the part “x : A” belongs together, so there it actually makes sense to have reduced spacing.

BTW, here's Mike in 2013 on why he changed his mind on this issue

[DanGrayson]

Here's an illustration of Mike's point: