News for hackers. Stuff that matters.

A comment on With Category Theory, Mathematics Escapes from Equality (2019). Parent comment

Re:With Category Theory, Mathematics Escapes from Equality (... by zozbot234 on Sunday March 27, 2022 @05:58PM (#30824568)
Large cardinals are closely related to what type theorists call "universes". Again, there's a huge amount of equiconsistency and relative consistency results linking type- and set theories. To keep suggesting and implying that type theory cannot possibly be a language for talking about these things is so incredibly careless and obtuse that some people might call it actively misleading.
[ Parent | on HN ]
Re:With Category Theory, Mathematics Escapes from Equality (... by spekcular on Sunday March 27, 2022 @06:16PM (#30824703)
I'm not sure how that comment is responsive to my post. Sure, type theorists talk about universes, and sure, there are relative consistency results linking type and set theories. My claim is just that large cardinals (or some equivalent concept) are essentially necessary to order theories in consistency strength, so is hard to take a response of the form "it doesn't matter whether HoTT can talk about large cardinals" seriously.
[ Parent | on HN ]