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?



What is the right notion of generalized element of a category?
**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](https://www.cs.cmu.edu/~rwh/papers/2dtt/mfps.pdf). 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](http://archive.numdam.org/ARCHIVE/CTGDC/CTGDC_1980__21_2/CTGDC_1980__21_2_111_0/CTGDC_1980__21_2_111_0.pdf).


