Post #1846804

2026-04-26 17:46 UTC

@jonmsterling This also touches on another point I like to trawl out on here from time to time, which is that despite technically being mathematics, type theory often doesn't feel very mathematical because it doesn't adopt the standard structuralist methods of ordinary mathematics, i.e. by coming up with simple definitions for a structure capturing a class of mathematical objects, and refining those structures with additional axioms that enable one to prove stronger theorems about them. I suspect that the difficulty of proving initiality in general for "reasonable type theories" is more a matter of defining a "reasonable type theory" than coming up with some truly novel mathematical content. [Edit: I just saw your post about Uemura's thesis; I'll have to take a look.] In the context of HoTT this is extremely ironic, given that one of the most mathematically enticing promises of univalence is enabling structuralism without the accounting overhead of isomorphisms.

Replies (1)

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

@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.

Open ##1846805