So I'm pretty familiar with homotopy theory but don't know any type theory, homotopy or otherwise. What does determining whether types are homotopy equivalent get you in terms of ML applications?

This sounds really interesting. Can you expand here or link to any resources related to this? I'm most interested in where you would apply these cohomology theories.

I guess I'm separating purely categorical applications from TDA applications, which I agree things like persistent homology will probably be useful.

That looks interesting, and I'm definitely not saying there's no intersection between CT and DS. There's some cool things I've seen with CT and probability theory recently. But to me it often seems like theory in search of a problem, and a far cry from functor becoming a common word among ML practitioners.

I'm someone with a PhD in a field that uses category theory extensively and I now work in DS. I'm finding a lot of ideas in this post unmotivated, I guess I'm pretty bearish on CT being applied to ML. Can you explain what problems you see that category theory will be used to solve?