Abstract
Szlachányi’s skew monoidal categories are a well-motivated variation of monoidal categories in which the unitors and associator are not required to be natural isomorphisms, but merely natural transformations in a particular direction. We present a sequent calculus for skew monoidal categories, building on the recent formulation by one of the authors of a sequent calculus for the Tamari order (skew semigroup categories). In this calculus, antecedents consist of a stoup (an optional formula) followed by a context, and the connectives behave like in the standard monoidal sequent calculus except that the left rules may only be applied in stoup position. We prove that this calculus is sound and complete with respect to existence of maps in the free skew monoidal category, and moreover that it captures equality of maps once a suitable equivalence relation is imposed on derivations. We then identify a subsystem of focused derivations and establish that it contains exactly one canonical representative from each equivalence class. This coherence theorem leads directly to simple procedures for deciding equality of maps in the free skew monoidal category and for enumerating any homset without duplicates. Finally, and in the spirit of Lambek’s work, we describe the close connection between this proof-theoretic analysis and Bourke and Lack’s recent characterization of skew monoidal categories as left representable skew multicategories. We have formalized this development in the dependently typed programming language Agda.
This article is a revised and extended version of a paper presented at MFPS 2018 [28].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Uustalu, T., Veltri, N., Zeilberger, N. (2021). The Sequent Calculus of Skew Monoidal Categories. In: Casadio, C., Scott, P.J. (eds) Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics. Outstanding Contributions to Logic, vol 20. Springer, Cham. https://doi.org/10.1007/978-3-030-66545-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-66545-6_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-66544-9
Online ISBN: 978-3-030-66545-6
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)