ยง
Tensor Hom adjunction
(- X A)
witnesses
A
as an output, while
Hom(A, -)
witness A as input.
Similarly, we know that we can contract
A
with
A*
so it makes sense that the
"dual" of multiplying by
A
(ie, how to divide out
A
) is to invert it by
allowing a contraction with
A*
.