HoTT
Switch to using truncated logic as default in the book
Mike Shulman wrote on the category theory zulip,
It is true that there was some disagreement among the authors of the book as to the importance of truncated vs untruncated logic, and the result is a compromise. Many of us (including me) would have preferred, for instance, to use words like "there exists" and "proposition" in the truncated sense, as that matches ordinary mathematical practice more. And in the past 10 years, that usage seems to have caught on, for the most part, in the HoTT community. But at the time, at least, when truncation in type theory was a more recent innovation, some of the authors were resistant to abandoning the traditional PAT word usage.
Now that a decade has passed and the homotopy type theory community has largely converged with the broader mathematical community to use truncated logic as default, with propositions as (-1)-truncated types and logical operators and quantifers referring to the truncated versions, I think terminology in the HoTT book should be updated to reflect the new reality.
I think this would be too big a change. Moreover there are probably authors of the book who would not agree.
Yes, I agree that this can't be changed now. The thing to do instead is write more books about HoTT using newer perspectives and terminology.
