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?