3 ms·

Thanks! I like the "if" "and" example. Do you have any other examples of the "internalization of the category's morphisms?"

• Twisol 6y ago
  Most of the common examples are mathematical widgets. For example, for any two vector spaces V, W, there's a vector space of linear transformations from V to W. Given a vector in V and a transformation W^V, you can get a vector in W -- I think categorically this is called the hom-tensor adjunction? It's a long-standing desire of mine to find categorical examples closer to software engineering. The usual example is the family of cartesian-closed categories corresponding to simply-typed lambda calculi -- "first-class functions" is exactly saying that you can take and return functions themselves as values, which witnesses that the morphisms of the category are "internalized" as elements of some type. I've never found it to give a very visceral intuition for the concept though.