With duals for objects
With duals for morphisms
Special sorts of products
In higher category theory
Let be a closed monoidal category. For two objects, the adjunct
of the identity morphism
is the evaluation morphism for the internal hom .
Syntax and semantics
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.
Revised on January 26, 2014 07:08:26
by Urs Schreiber