I'd like to see someone tackle a PhD thesis (or ten) on applying formalism to the concept of migrations. I suspect there's a missing aspect of type/group/category theory that's at least as big and important as variance is.

I think it might already mostly exist, it just isn't organized into a discipline.