natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
In linear logic/linear type theory, one of the two linear versions of conjunction is called the multiplicative conjunction and usually denoted “$\otimes$”. The analogous connective in relevance logic is sometimes called the intensional conjunction or the fusion or cotenability, and sometimes denoted “$\circ$”.
The categorical semantics of the multiplicative conjunction is as the tensor product with respect to a (symmetric) monoidal category structure on the collection of types.
If one retains of all conjunctions in linear logic only the multiplicative conjunction, then one speaks of the fragment of linear logic called multiplicative linear logic or multiplicative intuitionistic linear logic or MILL for short. See also at linear type theory for more on this.