After encountering the field of Categorical Logic recently, and more specifically the nLab page on Computational Trilogy as well as this paper, I'm under the impression that we have a pretty complete categorical formalization of at least one of the several equivalent fundamental notions of computation. Given this, I have two probably extremely naive questions:
(i) Have we tried to categorify computational complexity theory?
(ii) If (i) is somehow possible, could we hope that maybe "functorial invariants'' have something to say about identification problems? Like $P = NP$?
I am curious whether the above even make sense and whether any work has been done which could be said to pursue them.