  One of the most highly developed approaches to categorial proof theory is due to Došen. He has not only advanced the application of categorial methods in proofs theory (e.g., Došen and Petrić, 2004), but also shown how proof-theoretic methods can be used in category theory itself (Došen, 2000). Most important for categorial logic in relation to proof-theoretic semantics is that in categorial logic, arrows always come together with an identity relation, which in proof-theory corresponds to the identity of proofs. In this way, ideas and results of categorial proof theory pertain to what may be called intensional proof-theoretic semantics, that is, the study of proofs as entities in their own right, not just as vehicles to establish consequences (Došen, 2006, 2016). Another feature of categorial proof-theory is that it is inherently hypothetical in character, which means that it starts from hypothetical entities. It this way it overcomes a paradigm of standard, in particular validity-based, proof-theoretic semantics (see section 3.6 below).