Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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?

share|improve this question
    
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 '10 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 '10 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 '11 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 '11 at 12:53
    
Can you explain what do you mean by "type"? –  user16974 Sep 25 '11 at 16:03
show 1 more comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.