Fix a poset $T$, which we'll think of as a set of "types," interpreting $a \leq b$ as "$a$ is more general than $b$." Construct a category of TSet as follows.
Objects: Pairs ($X$, $\tau : X \rightarrow T$)
Arrows: Functions $f : X \rightarrow Y$ that respect type subsumption, i.e. $\tau(x) \leq \sigma(f(x))$
In the case where $T$ is a suitably nice poset (e.g. a frame, distributive lattice, cHA, ...), is there a slick formulation for such a category which makes it clear which (co)limits are hanging around and what properties they have?