I've read somewhere (probably in the nlab) that higher category theory has application in logic. By the way since now the only applications of higher category theory I've seen are in homotopy theory ...
I've seen many different notion of $\infty$-categories, actual I've seen the operadic-globular ones of Batanin and Leinster and the opetopic too and eventually I'll see the simplicial ones too. ...
has there be an effort to categorify first order logic? More particularly, structures in the sense of logic. If so, then every structure of a first order theory is a category. so in particular, the ...