  We give a natural-deduction-style type theory for symmetric monoidal
categories whose judgmental structure directly represents morphisms with tensor
products in their codomain as well as their domain. The syntax is inspired by
Sweedler notation for coalgebras, with variables associated to types in the
domain and terms associated to types in the codomain, allowing types to be
treated informally like "sets with elements" subject to global linearity-like
restrictions. We illustrate the usefulness of this type theory with various
applications to duality, traces, Frobenius monoids, and (weak) Hopf monoids.
