Post #1846805

2026-04-26 17:49 UTC

@zwarich Yeah. This was also a big part of the frustration in these years... Some people working in this area were very "structuralism-pilled" and did things in the way you mentioned (e.g. the Uemura stuff), but I'll tell you what I found really funny and frustrating. The 'categorical type theorist' camp (people like Awodey, me, Uemura, etc.) were very much pushing in this direction. But whenever we spoke to proper pure mathematicians about it, they would say things like "Hmm, I don't think that will work, let me tell you how I learned logic must work: first you have a set of symbols, then you count the parentheses, and then you give an induction proof with several hundred cases. That is how syntax works. You are welcome!" We were like, "No, we actually want to use mathematics to do this shit. Just like you do when proving things about rings or whatever. But for type theory". The strongest objections to the use of proper mathematics to study type theory came from the pure mathematicians. I found it very bizarre and irritating.

Replies (1)

@jonmsterling@mathstodon.xyz 2026-04-26 17:51

@zwarich Of course, we completely buried them in the end. There was a very silly "collective initiality project" that the pure mathematicians started, where they basically said they were going to try and resolve the conjecture by cosplaying whatever the fuck logicians do when faced with a problem like this. It was really funny to watch them scrambling, saying things like "It's not a proof unless it uses names and capture avoiding substitutions" and then a month later like "oh man that sucks so bad, I think de bruijn indices might actually be valid" and then two months later the project died. And then we resolved all the major conjectures in the syntactic metatheory of HoTT using ..... structural mathematics. (These would be: homotopy canonicity of HoTT, initiality of all conceivable type theories, normalisation and decidability of cubical type theory, not in that order.)

Open ##1846806