book icon indicating copy to clipboard operation
book copied to clipboard

Published 20 hours ago • verified publisher icon HoTT

parenthesis missing on page 67

Open prime235711 opened this issue 2 years ago • 4 comments

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

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

prime235711 avatar Mar 01 '22 03:03 prime235711

Page 67 of which version?

mikeshulman avatar Mar 01 '22 18:03 mikeshulman

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

Alizter avatar Mar 01 '22 19:03 Alizter

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.

mikeshulman avatar Mar 01 '22 19:03 mikeshulman

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

mikeshulman avatar Mar 01 '22 19:03 mikeshulman

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

prime235711 avatar Dec 03 '22 09:12 prime235711