  Szlach\'anyi'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.
