I've been working out how the internal language of a category C extends to taking the category itself as a type.

The most obvious way to interpret $X : \mathbf{C}$ is, of course, that $X$ is an object of C. We could ask for generalized elements too; e.g. we could consider functions $S \to \mathbf{Ob}(\mathbf{C})$ (or equivalently, functors $S \to \mathbf{C}$, where $S$ is viewed as a discrete category) as also being generalized elements of C.

Or, we can internalize; taking any object $X$ of C, we can view it as a discrete internal category, and get a corresponding notion that an $X$-shaped generalized element of C is precisely an arrow $Y \to X$. This is extra pleasing, since this is how we interpret dependent types too. (although it is a little unnerving that C/X is both the category of generalized elements of $X$ and the category of $X$-shaped objects of C)

But in some sense, this is all wrong: they are all talking about generalized objects of C, not generalized elements of C. Naively, I would think generalized elements of C should be functors with codomain C, not functions with codomain Ob(C), and that working with such elements would make all constructions automatically functorial/natural when appropriate.

But then, it's not obvious to me it really does all work out, and I've never seen it presented anywhere anyways.

So my questions are:

  • Is the latter notion useful at all?
  • Is the latter notion the "right" way to think about generalized elements of C, and the former notion just a truncation?
  • Is the latter notion the "wrong" way to think about generalized elements of C? (whether or not it is useful for other settings)
  • Is there something else entirely that's better?
  • $\begingroup$ Here's one way to think about it: the naive elements of a category should just be its morphisms. For example, the elements of a group are just its morphisms when thought of as a one-object category. So generalized elements are indeed probably functors into $C$, but you should think of the domain category as being a structured collection of naive elements, i.e., morphisms. $\endgroup$ – Kevin Casto Nov 12 '15 at 3:06

Yes, it works well to take “functors into C” as the notion of “generalised element of C”.

For groupoids, the Hofmann–Streicher model of type theory gives a strong precise statement of this: closed (i.e. non-dependent) types are interpreted exactly as groupoids G; closed elements of such a type are interpreted exactly as functors from 1 to G, i.e. as objects of G; elements in some other context are interpreted as functors from (the interpretation of) that context to G.

For general categories, I don’t quite know any comparable precise statement — finding an internal language for Cat that is as expressive as Martin-Löf I.T.T. is for groupoids is an open problem. The best existing work I know is Licata, Harper, 2-dimensional Directed Type Theory, 2011. However, less formally, much work of the Australian school of higher category theory can be seen as taking the view that a “generalised element” of an object C of a bicategory K is a 1-cell into C; or perhaps I should call these “generalised objects” or “generalised 0-elements”, since 2-cells with 0-codomain C can also be seen as “generalised arrows/1-elements” of C. Your example is then the special case where the ambient bicategory is CAT. I can’t recall any specific discussion of the “generalised element” terminology in this context in the literature, but it may well be out there. One classic of this approach is Ross Street, Fibrations in Bicategories, 1980.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.