An internal language for autonomous categories
type: Item
instance of: scholarly article
title: An internal language for autonomous categories
zbMATH Open document ID: 0806.03044
DOI: 10.1007/BF00873993
author: Ian Mackie
author: Leopoldo Román
author: Samson Abramsky
published in: Applied Categorical Structures
publication date: 1995-02-16T00:00:00Z
review text: \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.
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18D15
Mathematics Subject Classification ID: 03B20
zbMATH DE Number: 554356
zbMATH Keywords: symmetric monoidal closed categories
zbMATH Keywords: term assignment language
zbMATH Keywords: multiplicative fragment of intuitionistic linear logic
zbMATH Keywords: internal language
zbMATH Keywords: coherence
zbMATH Keywords: weak natural numbers object
zbMATH Keywords: autonomous category
zbMATH Keywords: internal recursion theory
reviewed by: Paul Bankston
Wikidata QID: Q57006902
describes a project that uses: Lilac
MaRDI profile type: Publication
cites work: Computational interpretations of linear logic
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q4281466
cites work: Linear logic, coherence and dinaturality
cites work: Q3997112
cites work: Linear logic
cites work: Languages for monoidal categories
cites work: A note on natural numbers objects in monoidal categories
cites work: Coherence in closed categories
cites work: Q3760508
cites work: Q3803296
cites work: Q3727946
cites work: Why commutative diagrams coincide with equivalent proofs
cites work: Q4038690
cites work: Monoidal categories with natural numbers object
cites work: Cartesian categories with natural numbers object
cites work: Q3827993
full work available at URL: https://doi.org/10.1007/bf00873993
OpenAlex ID: W3091815692
DBLP publication ID: journals/acs/MackieRA93
description: scientific article; zbMATH DE number 554356