parenthesis missing on page 67

Question

parenthesis missing on page 67

prime235711 opened this issue 3 years ago · 6 comments

prime235711 commented 3 years ago

I think it should be changed that first projection of coproduct type should be apparently parenthesized.

\sum_(x:A) P(x) \rightarrow A

Answer 1 · 2022-03-01T18:48:20.000Z

Page 67 of which version?

Answer 2 · 2022-03-01T19:15:04.000Z

Just before lemma 2.3.2 it seems. I'm still not sure what needs to be changed however.

Answer 3 · 2022-03-01T19:20:01.000Z

Ah! I think @prime235711 means it should be (\sum_(x:A) P(x)) \rightarrow A, in accord with the rule that sigmas and pis scope over the rest of the expression unless delimited.

Answer 4 · 2022-03-01T19:20:24.000Z

Would you like to submit a pull request, @prime235711?

Answer 5 · 2022-12-03T09:49:07.000Z

I'm new to github, so I don't understand what'd you mean. Can someone please do that for me?

Answer 6 · 2023-04-07T17:03:21.000Z

Bumping as I think this issue can be closed now.