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.
Keywords: type theory, symmetric monoidal category, prop, coalgebra
2020 MSC: 18M05, 18M85, 03B47
Theory and Applications of Categories, Vol. 37, 2021, No. 25, pp 863-907.
Published 2021-07-14.
TAC Home