  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.
