Is it possible to formalize (higher) category theory as a one-sorted
theory, just like we did with set theory?
Set theory is typically formalized as a one-sorted theory without urelements.
Is it possible to do the same with category theory or higher category
theory, formalizing the whole affair as a theory with only one type of
object?
I know that this runs counter to what some feel is the philosophical
spirit of category theory, but I'm still curious if it's possible anyway,
just as an interesting logical puzzle.
It seems tricky to me at first glance. A "category" has a "set" of
"objects" and another set of "morphisms." That's already four sorts of
thing - category, set, object, morphism.
However, it's possible to identify an "object" with the identity morphism
on that object. So, you could perhaps use this idea to bring you down to
only three sorts of thing - category, set, and morphism.
Alternatively, you could say that "object" and "morphism" are both types
of the more fundamental n-morphism, and arrive at a three-sorted theory of
categories, sets, and n-morphisms.
You could also try to formalize a "set" as a discrete category, and bring
you down to only two sorts of thing - category and (n-)morphism.
If you go with n-morphisms, maybe you could try to identify every
n-morphism with the (n+1)-identity morphism on it, and see if that
simplifies things somehow.
The above are some ideas that I had; I'm not even sure if they'd work. But
assuming they do, that still leaves you with only two things - categories
and morphisms - and I'm not sure if it's possible to go one step further
and get it down to one thing. Thoughts?
No comments:
Post a Comment