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?