Deductive Systems and Coherence for Skew Prounital Closed Categories

TL;DR

This paper develops proof theory for skew prounital closed categories, providing equivalent presentations, solving the coherence problem, and formalizing the results in Agda, with implications for non-commutative linear logic.

Contribution

It introduces the proof theory for skew prounital closed categories, including calculus systems, coherence solutions, and formalization in Agda, advancing understanding of non-invertible structural laws.

Findings

Sequent calculus admits focusing and normalization by evaluation.

Natural deduction derivations correspond to focused sequent calculus derivations.

Free skew prounital closed category on a set loses skewness due to left-normality.

Abstract

In this paper, we develop the proof theory of skew prounital closed categories. These are variants of the skew closed categories of Street where the unit is not represented. Skew closed categories in turn are a weakening of the closed categories of Eilenberg and Kelly where no structural law is required to be invertible. The presence of a monoidal structure in these categories is not required. We construct several equivalent presentations of the free skew prounital closed category on a given set of generating objects: a categorical calculus (Hilbert-style system), a cut-free sequent calculus and a natural deduction system corresponding to a variant of planar (= non-commutative linear) typed lambda-calculus. We solve the coherence problem for skew prounital closed categories by showing that the sequent calculus admits focusing and presenting two reduction-free normalization procedures for the natural deduction calculus: normalization by evaluation and hereditary substitutions. Normal natural deduction derivations (beta-eta-long forms) are in one-to-one correspondence with derivations in the focused sequent calculus. Unexpectedly, the free skew prounital closed category on a set satisfies a left-normality condition which makes it lose its skew aspect. This pitfall can be avoided by considering the free skew prounital closed category on a skew multicategory instead. The latter has a presentation as a cut-free sequent calculus for which it is easy to see that the left-normality condition generally fails. The whole development has been fully formalized in the dependently typed programming language Agda.