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?