The Curry-Howard correspondence between linear logic and session types is well-known. In this talk, I will discuss some attempts to extend this to a Lambek correspondence, relating categorical models of classical linear logic to the semantics of session types. This crucially relies on an understanding of typed process equivalence or typed bisimulation for session-typed processes, which is necessary to axiomatize the theory of session types. The work is in progress, and I will present some preliminary ideas.