You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Gurkenglas (May 03 2023 at 17:58):Recall that a vector space is an algebra of the free-vector-space monad on Set.
Likewise, a category is an identity-on-objects algebra of the free-category monad on Quiv.
More impressively: Let a precategory be a category that doesn't have to satisfy the algebra laws.
For a precategory on a quiver q, the following are equivalent:
To clarify, here's how to recover that a category C is...
...associative: Let's define precategories C_left and C_right: Let p be a path in C. If it hasn't length 3, it composes as in C. If it does have the form (f,g,h), it composes to C(C(f,g),h) in C_left and to C(f,C(g,h)) in C_right. Since we've now built C_left and C_right from C, they are C.
...unital: You could use C to conjure arrows from empty paths, then sprinkle them into other paths before you compose. By the property of C, those arrows do nothing.
A functor from C to D is then an object map f plus an f-on-objects map from paths in C to arrows in D given which you can only build that one.
In Haskell terms:
data Path q where Nil :: Path q s s; Snoc :: Path q s t -> q t u -> Path q s u
type Precategory q = forall s t. Path q s t -> q s t
type Redefinition = forall q. Precategory q -> Precategory q
-- A category is a precategory on which all redefinitions agree. (id in particular.)
rassoc :: Redefinition
rassoc c (Snoc (Snoc (Snoc Nil f) g) h) = c (Snoc (Snoc Nil f) (c (Snoc (Snoc Nil g) h)))
type Prefunctor f q r = forall s t. Path q s t -> r (f s) (f t)
type Redefinition2 = forall f q r. (Precategory q, Precategory r, Prefunctor f q r) -> Prefunctor f q r
-- A functor is a prefunctor between categories on which all redefinition2s agree.
Remark: There is exactly one "forall q. Precategory (Path q)".
Tom Leinster's "possible to even mention" concept is possible to mention here.
Might one characterize the structure of Quiv by this property corresponding to unitality and associativity?
The jackpot case would be that this is a compact enough seed for category theory that one can calculate out a grid of all sensible math concepts, making clever definitions obsolete and math tractable.
Anyway. Ideas? Prior work?
Oscar Cunningham (May 05 2023 at 18:01):This sounds interesting. Could you explain how it relates to the title 'reflective stability'?
Gurkenglas (May 14 2023 at 13:10):@Oscar Cunningham it's not a term with a formal definition I am importing. Allusions include:
Morgan Rogers (he/him) (May 14 2023 at 13:30):Re "a category is an identity-on-objects algebra of the free-category monad on Quiv": the unit of the free category monad is the identity on objects, and any algebra has to be an inverse to the unit so is the identity on objects too. So a category is an algebra for the free category monad, without caveats.
What is a "category without properties", and how does it fail to be a category?
Gurkenglas (May 14 2023 at 21:34):@Morgan Rogers (he/him) By identity-on-objects I mean that a path from s to t has to be mapped to an arrow from s to t - the quiver morphism's objects-to-objects map is the identity.
A precategory is an identity-on-objects algebra of the free-category endofunctor on Quiv, that is, it does not need to satisfy the algebra-over-a-monad laws. I should have made more obvious that I didn't mean to drop "identity-on-objects". Edited.