The maximality of Cartesian categories

DOI10.1002/1521-3870(200101)47:1%3C137::AID-MALQ137%3E3.0.CO;2-FMaRDI QIDQ2707078zbMATH OpenFDO

Authors Kosta Došen, Zoran Petrić

Publication date 28 March 2001

Published in Mathematical Logic Quarterly (MLQ) (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/9911059

zbMATH Keywords

Cartesian categorycoherence theoremequations between arrowsfree Cartesian categoryuniqueness in normal form

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Categorical logic, topoi (03G30) Foundations, relations to logic and deductive systems (18A15) Limits and colimits (products, sums, directed limits, pushouts, fiber products, equalizers, kernels, ends and coends, etc.) (18A30) Preorders, orders, domains and lattices (viewed as categories) (18B35) Categorical structures (18D99)

Review text

This article considers the equations between arrows that are assumed in the definition of a Cartesian category, that is a category with binary products and a terminal object. It is shown that extending these equations with any new equation obtained from the language of free Cartesian categories will collapse the Cartesian category into a preorder. Hence the title ``maximality of Cartesian categories.NEWLINENEWLINENEWLINEThe proof utilizes a coherence theorem addressing uniqueness in normal form in the free Cartesian category on a set of objects \({\mathcal O}\). The authors conclude the article with a discussion of the implication of these results for logic.

Recommendations

• Bicartesian coherence
• scientific article; zbMATH DE number 2006632
• scientific article; zbMATH DE number 4108981
• The maximality of the typed lambda calculus and of cartesian closed categories
• Partial Horn logic and Cartesian categories

Cited in

(7)

• Cartesian categories with natural numbers object
• Symmetric bimonoidal intermuting categories and \(\omega\times\omega\) reduced bar constructions
• Coherence in SMCCs and equivalences on derivations in IMML with unit
• Generality of proofs and its Brauerian representation
• Identity of Proofs Based on Normalization and Generality
• Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics
• Representing conjunctive deductions by disjunctive deductions

This page was built for publication: The maximality of Cartesian categories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2707078)