Is there a notion of a category with "labelled" or "typed" morphisms?
I imagine that each morphism would belong to a certain class/type, and those classes would form a commutative monoid under composition of the associated morphisms.
As an example, in the category of people and their possessions, this diagram commutes
with the rules
$owns\circ is = is \circ owns = owns$
$owns \circ owns = owns$
$is \circ is = is$
Neither is nor owns is obviously functorial, and it seems that the diagram with labelled morphisms is more informative than separate categories for is and owns, together with a mapping of objects between the two.
(It's also fun to note that this seemingly lets us derive $2^2=4$ distinct "arrow categories", each of which is semantically somewhat meaningful)
This notion does not seem well documented - I couldn't find anything on nlab, at least. Is it inconsistent, less interesting than I expected, or are there better formulations of the same idea?