[notyoutube]

I think you're underestimating the amount of very advanced stuff already done in PL theory, and overestimating how applicable pure maths is to that.

Afaik "category theory [as an] underpinning of type theory" is quite far from true: you can model some type theory with category theory, but it's mostly about modelling, the correspondence is very finicky once you get to the details, and it doesn't help _that much_ for practice. Then, knowing the bit of CT that a typical mathematician knows is not going to amount to much or anything very helpful, in practice, and for the things it will help with (probably going to be quite theoretical cutting edge research), you'll have plenty of people that studied exactly that working on it…

I'd like it to be the case, but being able to describe Yoneda and knowing about assembler is, I think, a far cry from getting you anywhere near these jobs.