jcreed blog > Do Univalent Universes Arise from Higher Adjoints?

Do Univalent Universes Arise from Higher Adjoints?

A 2-Category of Trees

If we let a 2-category be freely generated by postulating that we have

then the string diagrams we can draw for 2-cells in $\C$ look like forests:
We might squint and think that this is kind of like the set of (order-preserving) functions from one finite ordered set to another. For example, the above image is sort of like the function $h$ that takes $\{0,1,2,3,4,5\}$ to $\{a,b,c\}$ by assigning $h(0)=0,h(1)=a,h(2)=a,h(3)=a, h(4)=b$. But it's not exactly that: the string diagram keeps track of more information than the mere function $h$ does. The string diagram keeps track of the fact that we first collapsed 0 and 1, then merged with 2, then merged with 3. The function $h$ knows merely that 0,1,2,3 all collapse together without remembering how they got there.

A 2-Category of Ordered Functions

If we instead let a 2-category be freely generated by postulating that we have
Then naturality naturally equates diagrams that represent equal functions. However, this only captures order-preserving functions between finite ordered sets.

A 3-Category of Braided Functions

We could go up one more dimension, working in a 3-category, postulating
In this case the 2-cells $\rid_{\rid_C} \to \rid_{\rid_C}$ resemble finite sets, and the 3-cells between them resemble arbitrary maps between them --- except they keep track of extra "braiding" information. For example, the following 3-cell would be distinguished from the "identity function on the 2-element set":

An $n$-Category of Functions between Higher Sets

Presumably if we go up to sufficiently high dimensions, these "low-dimensional" phenomena stabilize and disappear, and we're left with a $n$-dimensional category whose $(n-1)$-cells are finite sets and whose $n$-cells are functions between them. Or perhaps this doesn't actually stabilize at some finite stage and $\mathbf{FinSet}$ is attained as some kind of limit.

However, there are more cells we could have added which could give us more interesting structure. Even at the 3-category level, let's imagine throwing in all of:

With these tools we could imagine describing sets with elements with holes in them, just like higher types in homotopy type theory:
And at sufficiently high dimensions it seems conceivable that a wide range of HITs would be attainable, and all functions between them.

Question 1: Exactly what should the postulated set of cells be at each dimension, to recover the category of finite higher sets and maps between them?

It seems like some kind of very strong high-dimensional adjoint equivalence at all dimensions but the highest, but I don't know enough about higher categories to make a concrete conjecture. And, I guess, follow-up question:

Question 2: Does this algebraically created "universe of finite higher sets" satisfy univalence?