category with duals (list of them)
dualizable object (what they have)
ribbon category, a.k.a. tortile category
monoidal dagger-category?
Let be a closed monoidal category. For two objects, the adjunct
of the identity morphism
is the evaluation morphism for the internal hom .
In a cartesian closed category the evaluation map
is the categorical semantics of what in the type theory internal language is the dependent type whose syntax is
expressing function application. On propositions ((-1)-truncated types) this is the modus ponens deduction rule.
Last revised on May 18, 2022 at 06:42:27. See the history of this page for a list of all contributions to it.