3

1

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?

flag
Do you mean "**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 2010 at 3:44
If that is what 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 2010 at 3:47
Interesting stuff! It seems quite different from my original intention however, which was to define a category of sets relative to a (fixed) type system and think of a function as a kind of "matching". I.e. for x to be mapped on to f(x), its type must be more general than the type of f(x). – Aleks Kissinger Jan 13 2011 at 12:52
What I have in mind is reasoning about rewrite systems on algebraic structures whose constituents might have types. In its own right, the category T-Set is not that interesting, but consider e.g. the category of graphs that have a typed set of vertices rather than a set. Then the ordering on T plays the role of the type-unification step on the vertices when matching the LHS of a rewrite rule. – Aleks Kissinger Jan 13 2011 at 12:53
Can you explain what do you mean by "type"? – Math-player Sep 25 2011 at 16:03
show 1 more comment

Your Answer

Get an OpenID
or

Browse other questions tagged or ask your own question.