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?

Arrows: Functions $f:(X,\tau)\to (Y,\sigma)$ that respect type subsumption, i.e. $\tau(x)\leq\tau(y)\ \Rightarrow\ \sigma(f(x))\leq\sigma(f(y))$"? Or perhaps I have misunderstood the goal. – Adam Dec 2 '10 at 3:44iswhat you meant, it would mean a sort of "Equilogical Spaces (andrej.com/papers/equ-paper.pdf) with subtyping", which would be quite interesting. – Adam Dec 2 '10 at 3:47