Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: operator precedence in dependent set syntax

Nathaniel Virgo (Mar 17 2025 at 17:16):

Does anyone know a good "cheat sheet" kind of document for the conventions in type theory / dependent set syntax? e.g. I can never remember whether $\sum_{a: A} B_a\to X$ means $\left(\sum_{a: A} B_a\right)\to X$ or $\sum_{a: A} \left(B_a \to X\right)$ and I'm hoping to find a concise document where I can easily look that sort of thing up. I guess it mostly doesn't matter exactly which type theory we're talking about as this is mostly for my own informal notes.

Kenji Maillard (Mar 17 2025 at 21:01):

As a rule of thumb, I would have all operators binding a variable scope as far as possible on the right. So $\sum_{a: A} B_a\to X$ means $\sum_{a: A} \left(B_a \to X\right)$.

Mike Shulman (Mar 18 2025 at 16:25):

I don't think there is a universal convention about this. When mixing $\Sigma$ with $\to$ I always put parentheses.

Mike Shulman (Mar 18 2025 at 16:27):

Type theorists tend to follow the rule Kenji mentioned, but I think this is pretty unintuitive for mathematicians, who would probably not read $\sum_{i=1}^n k + 1$ as $\sum_{i=1}^n (k + 1)$.

Mike Shulman (Mar 18 2025 at 16:29):

In the HoTT Book we followed the type-theorists' convention at least for $\Pi$, so that $\prod_{a:A} B_a \to X$ means $\prod_{a:A} (B_a \to X)$, but this is probably the bit of notation in that book that is the most confusing to readers and I wouldn't do it again.

(Then again, if we had the whole book to write over again I would probably suggest using NuPRL/Agda syntax $(a:A) \to B_a \to X$ for dependent functions.)

John Baez (Mar 18 2025 at 16:35):

Mike Shulman said:

I don't think there is a universal convention about this. When mixing $\Sigma$ with $\to$ I always put parentheses.

Whew, thanks! Otherwise we're in a sophisticated version of the world where people post puzzles like "What's 3 $\div$ 4 $\times$ 6 - 5?"

Patrick Nicodemus (Mar 19 2025 at 19:58):

John Baez said:

Whew, thanks! Otherwise we're in a sophisticated version of the world where people post puzzles like "What's 3 $\div$ 4 $\times$ 6 - 5?"

I know the one correct convention, but I'm not tellling.