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.
David Corfield (May 11 2025 at 09:46):The entry [[higher observational type theory]] has a passage sounding rather judgmental:
Like your doctor saying "Ideally, you'd be exercising every day," when you admit to sitting about all day.
Is this a fair representation of the hope for H.O.T.T., and if so, is the extent to which the hope is being realized properly elucidated in the references?
David Michael Roberts (May 11 2025 at 11:15):That does sound a little "well, I hope the details are in the references on this page, the authors really should have done so"...
David Corfield (May 11 2025 at 11:21):Yeah. If it's written from a position of ignorance, like the doctor before they inquire about your exercise regime, then we could have such a phrase on just about every page. If it's written in a pointed way for this particular entry, even if it's fair at a certain moment, it's unlikely to be updated as people write and add new references.
John Baez (May 11 2025 at 11:39):My only problem is that when people speak of "the hope", they would do better to say who is hoping it. Of course mathematicians try not to be personal, but if there's a hope then someone is hoping it and it matters who!
Madeleine Birchfield (May 11 2025 at 12:50):I believe @Mike Shulman is working on higher observational type theory so maybe he can say something about this topic.
Mike Shulman (May 11 2025 at 16:38):David Corfield said:
Like your doctor saying "Ideally, you'd be exercising every day," when you admit to sitting about all day.
Hmm... it doesn't sound that way to me. But if it sounds that way to you, maybe you can help rephrase it to be better.
This entry has to be somewhat speculative because HOTT is still work in progress. There is no formally specified theory called HOTT in the literature yet. What there is right now is
I would mostly agree with the two hopes currently written on the page, but they have a somewhat different status. The second one is a mathematical hope (although by this point I'm confident enough that I would call it an expectation): that once the theory is formally specified we will be able to prove univalence in it and prove metatheoretically that it computes (e.g. satisfies normalization). The first one is more of a sociological hope: it's a fact that the theory won't have an interval primitive (although I'm not sure what "second-class" means), but whether it's "logically cleaner" is more of an aesthetic judgment, and my hope is that a substantial number of people will feel that way (as I do). (-: (Although I'm not sure that "logically cleaner" is quite how I would describe how I feel, but I suppose it's a reasonable approximation.)
Madeleine Birchfield (May 11 2025 at 17:14):Mike Shulman said:
it's a fact that the theory won't have an interval primitive (although I'm not sure what "second-class" means)
I think "second-class" means simply that the interval is not a type, but is defined externally to the base dependent type theory. But it doesn't matter since that word isn't in the article anymore from what I can see.
Mike Shulman (May 11 2025 at 17:21):Apparently someone named "p" is editing it as we speak.
David Corfield (May 12 2025 at 06:48):Mike Shulman said:
HOTT is still work in progress. There is no formally specified theory called HOTT in the literature yet
That sounds worth specifying on the page, so I have.
David Corfield (May 12 2025 at 10:00):I also added a remark and link to slides for Mike's philosophical motivation. Nice for my discipline to feel useful, even if not from my pen!
While we hope that HOTT will have technical advantages as well, my primary motivation for it was philosophical. [slides]