6
$\begingroup$

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?

Improve this question
$\endgroup$
21
  • 4
    $\begingroup$ I don't really understand the question, could you make precise what for example untyped category theory (not higher!) would be about? $\endgroup$
    – Martin Brandenburg
    Commented Jul 7, 2012 at 13:10
  • $\begingroup$ @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. $\endgroup$
    – Giorgio Mossa
    Commented Jul 7, 2012 at 15:00
  • 1
    $\begingroup$ @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. $\endgroup$
    – Zhen Lin
    Commented Jul 7, 2012 at 15:54
  • 1
    $\begingroup$ There is of course a (strict) $\omega$-category version of the single-sorted definition of a category (ncatlab.org/nlab/show/single-sorted+definition+of+a+category). 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." $\endgroup$
    – Mike Shulman
    Commented Jul 9, 2012 at 7:02
  • 1
    $\begingroup$ 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. $\endgroup$
    – David Roberts ♦
    Commented Jul 9, 2012 at 15:27

1 Answer 1

Reset to default
4
$\begingroup$

Hi Mirco, I'm putting my comment as an answer in case otherwise you don't find it. I wonder if you need the "n-arrows-only" approach.... where language of partial monoids replace categories. For example where objects and 1-arrows are treated on the same footing as 2-arrows in a double or 2-category in which the identities are provided by the source and target maps. Proposition: A small double category is precisely a set with two commuting partial monoid structures. (And a 2-category similarly but with an extra condition.) Would it be at all useful to you to try to do this for the n-fold or for the n case?

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .