3
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$
    – Adam
    Dec 2, 2010 at 3:44
  • $\begingroup$ 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. $\endgroup$
    – Adam
    Dec 2, 2010 at 3:47
  • $\begingroup$ 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). $\endgroup$
    – Aleks Kissinger
    Jan 13, 2011 at 12:52
  • $\begingroup$ 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. $\endgroup$
    – Aleks Kissinger
    Jan 13, 2011 at 12:53
  • $\begingroup$ Can you explain what do you mean by "type"? $\endgroup$
    – user16974
    Sep 25, 2011 at 16:03

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.