First, let me say that I have no idea if such a post has its place here. However, I believe that the ideas I'm going to present are important. The goal of this thread is three fold:

1) trying to define morally what is a theory and its stratification process (like set theory) as a collection of higher categories,

2) asking for references about such ideas,

3) listening for constructive criticisms.

To begin, let us notice that the 1-category Sets of all sets cannot discriminate the "deeper" layers of sets: by this, I mean that two different sets of the same cardinalities will be isomorphic even though their elements are non isomorphic **sets**. This means that 1-category theory can only see the first layer of structure of an object, but fails to see its construction process (which can, however, be quite important when one is looking at some "higher level" concepts).

Yet, if one was following the philosophy that arrows are probing the inner structure of an object, one should instantly conclude that in order to discriminate the elements of a set, and their elements, and so on, infinite category theory is needed. However, how to put such higher categorical structure on Sets? Quite simply, by thinking upside down: we have to consider that a set is an object, while an element of a set is probed by an 1-cell, while an elements of an element is probed by a 2-cells, and so on up to some $n$ (we call the height of a set the length of the maximum chain of membership of its elements). With such vocabulary, one needs $n$-category theory in order to probe up to length $n$ sets.

To begin, let us think of a strict $n$-category as something built recursively from $n-1$ categories. An $n$-category has $n+1$ collection of cells such that: Its "collection" of $0$-cell are $n-1$-categories,

Its "collection" of $1$-cells are $(n-1)$-$0$-transfor (that is, $(n-1)$-functors),

Its "collection" of $2$-cells are $(n-1)$-$1$-transfor (that is, $(n-1)$-natural transformation), ...

Its "collection" of $k$-cells are $(n-1)$-$(k-1)$-transfor (for $k \leq n-1$), ...

Its collection of $n$-cells are $(n-1)$-$(n-1)$-transfor.

We also impose that the domain and codomain of an $n$-$k$-transfor is an $n$-$(k-1)$ transfor, and adds all the relevant compositions.

Now, for any $1$-category $\mathcal{C}$, let us define $Pow(\mathcal{C})$ to be the $2$-category whose $0$-cells are the full subcategories of $\mathcal{C}$, $1$-cells are functors between them, and $2$-cells are natural transformations between such functors.

Notice that at this point, with our previous interpretation of $n$-category, taking such "powercat" operation doesn't allow us to see deeper inside the inner structure of sets inside Sets (that it, it doesn't see that the elements of a set are sets). Yet, $Pow(Sets)$ clearly contains a terminal category whose object is $1 = \{*\}$ and unique arrow is $Id_*$. In particular, any $1$-cell from $1$ to $A$ is a way to pickup an element in $A$ (say, a set $S$), while any natural transformation between $S_1, S_2: 1 \rightarrow A$ is like picking up an arrow $S_1 \rightarrow S_2$ "inside" $A$, without having to know what are the constituting elements of $A$.

Also, say that a map $term: 1 \rightarrow A$ is terminal if it is a terminal object in $Hom(1,A)$ (that is, it picks up the terminal object inside $A$). Any natural transformation from $term$ to $S_1$ is a way to look at the elements of $S_1$ inside $A$ from the outside of $A$. Hence, such natural transformation is nothing else than an element of $A$ in the usual sense : an element of some set that is itself a set, but the latter structure seems to be totally inaccessible from the outside.

Here comes the idea: suppose that we are able to take for all $n$ the $Pow^n(X)$ category where $X$ is some syntactic category, hence is "at most" a category representing some sets of height $1$ : the "formal" elements of a syntactic object $A$ in $X$ are arrows $1 \rightarrow A$. Yet, these formal elements have no arrows between them because there is no 2-cells ($X$ is a $1$-cat). As a result, $X$ represents a category of sets where elements are structureless (like, urelements?). Now, let us fix some big enough $n$. Clearly, $Pow^n(Sets)$ is a $n+1$-category in the previous sense (arrows are $n$-$k$-transfors, etc). We interpret such category as a category of sets of height at most $n$, where elements are sets of height at most $n-1$, and so on. In particular, what happens if we restrict such category to a $1$-category by forgetting all $n$-$k$-transfors but the $k = 0$th one ? We are forming a $1$-category whose objects are $n$-categories and arrows are $n$-$0$-transfors representing sets of height at least $n$. However, by doing so, we just forgot that our "elements" of our categories are actually categories too, and this is exactly what happens when one is looking at Sets as a $1$-category: we forgot that the elements of our elements are sets!

Therefore, one can be tempted to say that the "real" category Sets is actually an $\infty$-category built under some operations on categories over a syntactic one $X$. Also, given two $0$-cells $1$ and $A$ of such $\infty$-category interpreted as some sets of some height (1 being the terminal cell), the maximum $n$ such that the $\infty$-$m$-transfors are trivials for $m > n$ is simply the height of the set $A$ for the membership relation.

Following this line of thoughts, it becomes natural to say that a formal theory (like set theory) is a "collection" of higher categories ($1$-cat, $2$-cat, $\ldots$, $n$-cat, $\ldots$) that are "closed" under the following primitive operations:

Powercat operations takes some $n$-category $\mathcal{C}_n$ and send it to the full $(n+1)$-category of all full subcategories of $\mathcal{C}_n$. We write it $Pow(\mathcal{C}_n)$.

Transfor operations takes two $n$-categories $\mathcal{C}_n$, $\mathcal{D}_n$, and sends them to the full $n$-category of $(n-1)$-transfors $Trans(\mathcal{C}_n, \mathcal{D}_n)$,

$Downshift_k$ operation for all positive integers $k$: if $\mathcal{C}_n$ is an $n$-category, then for any $0 \leq k < n$, $Downshift_k(\mathcal{C}_n)$ is the $(n-k)$-category whose $m$-cells for $0 \leq m < (n-k)$ are the $k+m$-cells of $\mathcal{C}_n$,

$Upshift_k$ operation for all positive integers $k$: if $\mathcal{C}_n$ is an $n$-category, then for any $0 \leq k < n$, $Upshift_k(\mathcal{C}_n)$ is the $(n-k)$-category whose $m$-cells for $0 \leq m < (n-k)$ are the $m$-cells of $\mathcal{C}_n$.

Lifting operation: if $\mathcal{C}_n$ is an $n$-category, then $Lift(\mathcal{C}_n)$ is formally a $n+1$-category where the $(n+1)$-$n$-transfors are all identities and other cells are left unchanged.

Restriction by subcategories

Closed under limits inside any $n$-categories containing the previous ones.

Question: Did some people already looked at this kind of things and paradigm? Moreover, can we find a syntactic $1$-category $X$ generating the category nSets, of all sets of height at most $n$ for the membership relation?

edit: Maybe an easier way to "see" the whole structure of Sets is as follow: for any set $A$, we define the small category $\mathcal{A}$ generated by the syntactic objects with the same name as the ones of $A$ (say, $a$, $b$, $c$, $\ldots$), plus a terminal element $1$. Now, the arrows of $\mathcal{A}$ are, for any objects $a$, $! : a \rightarrow 1$, and $a: 1 \rightarrow a$ with $! \circ a = Id_{1}$ and no other relations. That is, the arrow $a \circ !$ is an endoarrow that is not equals to the identity.

Call $1Sets$ the $1$-category whose objects are all such categories, and arrows are the functors preserving limits (that is the terminal element) between them. Note that here, the terminal category is initial, while the arrow category $(1 \rightarrow *)$ with one non trivial endoarrow at $*$ is terminal. This category is obviously equivalent to Sets. Now, if one is taking the powercat operation taking as $0$-cells all (non necessarily full actually) subcategories of $1Sets$, as $1$-cells the functors between such subcategories, and as 2-cells the natural transformations, we obtain $2Sets$: the category of all sets of height $2$. In particular, one can easily iterate such constructions by taking $Pow(nSets)$ to obtain $(n+1)$Sets as the $(n+1)$-category of all sets of height $n+1$.

Now, what I tried to express yesterday is that the "true" set theory is the "collection" of all $n$-categories $nSets$, which can be put together by lifting all nSets categories to infinite-categories where all $m$-cells are trivials for $m > n$.

I hope that it's now clearer.

Setis that functions between sets generally don't respect their internal structure, and so neither doesSet. If you want to inspect the internal structure, you need a different notion of morphism. e.g. there are several different ways of encoding the internal structure of a well-founded set as being a set equipped with a partial order (e.g. the set of all descending membership chains ending at the original set, with $x \leq y$ meaning that $x$ extends $y$), and thus as an object ofPoset. $\endgroup$ – Hurkyl Jul 4 '15 at 19:36