An internal language for autonomous categories (Q1320337): Difference between revisions

\textit{J. Lambek} and \textit{P. J. Scott} [Introduction to higher order categorical logic (1986; Zbl 0596.03002)], have shown that \(\lambda\)- calculi (resp., intuitionistic type theories) serve as internal languages for certain closed categories (resp., topoi). The existence of an internal language/logic for a category allows a calculus of diagrams, making, as the authors of the present paper say, ``geometry into equations''. The main contribution of the paper under review is to show that the term assignment language for the multiplicative fragment of intuitionistic linear logic is an internal language for symmetric monoidal closed (autonomous) categories. As an application, the authors give a simplified proof of the coherence theorem of Kelly and MacLane; that every diagram arising in a particular well-defined manner must commute. Finally the authors show how a weak natural numbers object may be introduced in an autonomous category, providing the basis for an internal recursion theory in such a context.