## Untyped Higher Category Theory

I am currently trying to wade through the vast lake of higher category theory, a formidable task,or so it seems.

In the process, it has occurred to me that there is a basic analogy in place with various forms of type theories, typed logic, typed set theory, typed lambda calculus, etc.

In higher cats, one has 1-morphisms, 2-morphisms, and so on.

A fairly hierarchical structure, a ladder to infinity of sorts.

Now, whenever there are types, there is (almost) invariably an un-typed variant of the theory, which "forgets" the types. So I wonder if there is something along these lines already somewhere in the categorical endeavor.

I try to be a bit more precise: imagine you are staring at a N-category (let us stick to a strict one, just for sake of simplicity), from the top, and you forget all the type labels. You see a fairly complicated diagram of maps whose endpoints are other maps, and so on and so forth. Now try to axiomatize such a structure. That would be an untyped higher category (UHC).

Is there a reference for this structure? Now get rid of the strictness, and re-do the experiment. What kind of untyped higher categories are the result of stripping types from general higher cats?

In the example I mentioned, the UHC is well-founded, in the sense that there are some fellows (the ground objects) who only point to themselves (I identify here the objects with their identity maps). Now, eliminate this distinguished role of objects and you will have a not well founded UHC.

Is there a study of not-well-founded categories, in a similar spirit as there is a theory of not well-founded sets?

-
I don't really understand the question, could you make precise what for example untyped category theory (not higher!) would be about? – Martin Brandenburg Jul 7 at 13:10
@MircoMannucci If what you're interested is just an higher category in which there's only one object then I think you're looking for higher monoidal categories. – Giorgio Mossa Jul 7 at 15:00
@Martin: I think Mirco is alluding to the difference between "untyped" set theory such as ZFC and ramified type theories such as Russell's theory of types where sets have a numeral "type" indicating their level in the hierarchy of the universe. – Zhen Lin Jul 7 at 15:54
There is of course a (strict) $\omega$-category version of the single-sorted definition of a category (ncatlab.org/nlab/show/…). You have to be a little careful with it if you want $\omega$-categories rather than $(\omega+1)$-categories, but it works just fine. You can find the $(\omega+1)$-version in Street's paper "The algebra of oriented simplices." – Mike Shulman Jul 9 at 7:02
should be possible to define in a single sorted way, in principle, but oo-categories are trickier. This is all very different to a RW-types approach. When you say "think (I am being terribly sloppy here!) of object as 0-types, ordinary morphisms as 1-types" I encourage you to not be sloppy and figure out what this means for 1- or 2-categories. This would help frame the discussion for higher categories, and how to think of them using RW type theory. – David Roberts Jul 9 at 15:27