An internal language for autonomous categories
\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.
- A note on natural numbers objects in monoidal categories
- An internal language for autonomous categories
- Cartesian categories with natural numbers object
- Coherence in closed categories
- Computational interpretations of linear logic
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 4010480 (Why is no real title available?)
- scientific article; zbMATH DE number 4071154 (Why is no real title available?)
- scientific article; zbMATH DE number 4103051 (Why is no real title available?)
- scientific article; zbMATH DE number 46995 (Why is no real title available?)
- scientific article; zbMATH DE number 177812 (Why is no real title available?)
- scientific article; zbMATH DE number 512773 (Why is no real title available?)
- Languages for monoidal categories
- Linear logic
- Linear logic, coherence and dinaturality
- Monoidal categories with natural numbers object
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Why commutative diagrams coincide with equivalent proofs
- An internal language for autonomous categories
- Relating categorical semantics for intuitionistic linear logic
- Natural number objects in Dialectica categories
- GS theories: a syntax for higher-order graphs
- The power of closed reduction strategies
- Covert movement in logical grammar
- Logical systems. I: Internal calculi.
- Internal diagrams and archetypal reasoning in category theory
- scientific article; zbMATH DE number 1070654 (Why is no real title available?)
- scientific article; zbMATH DE number 1497809 (Why is no real title available?)
- Lilac: a functional programming language based on linear logic
- scientific article; zbMATH DE number 860038 (Why is no real title available?)
- Partial recursive functions and finality
- Strong typed Böhm theorem and functional completeness on the linear lambda calculus
- Aspects of categorical recursion theory
- The syntactic side of autonomous categories enriched over generalised metric spaces
- Linearity and iterator types for Gödel's system \(\mathcal T\)
- Extending computational trinitarianism
- A note on natural numbers objects in monoidal categories
- The logic of message-passing
- Gödel's system T revisited
This page was built for publication: An internal language for autonomous categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1320337)
