Aether 🇺🇦🏳️‍⚧️🇵🇸

theres something so spectacularly intuitive about open interval objects forming cocategories
like. oh yeah. you can just split a line into two along an arbitrary point between them
its a really basic example but its very pleasant how intuitively it explains the concept of bifurcation

(sorry for my absence; was going through a lot of stuff. gonna get back to drawing and programming soon)

okay i am. done diagram-maxing linear equipment hyperfixation arc for now
got as far as all of this stuff!!!! look at it go
pr sure this is more diagrammatic information than what stuff like nlab and wikipedia has
lemme know if ya find any inaccuracies or if you have any questions :3
still studying all of this stuff, but i thought before exploring in-depth some of the applications of cocategory theory maybe having the right theoretical framework for exploring all of that stuff could be useful

the idea behind cocategory theory is that you are studying structures which can be arbitrarily split into segments and then cull away loops. analysing the former point for a moment; decomposition is natural insofar as the reverse of composition, that we can take apart a lego castle the same way we can construct it. cocategory theory provides a different notion however. its not like decomposition of castles into bricks, bricks into molecules, molecules, and so on, because the cocategory theorist wants to split the electron. while infinitely decomposing things seems impossible and foreign at first, its actually just as natural when you recontextualize the arbitrarity of it as fundamental; as long as you only understand two parts of something as components of a larger whole and discard any other of information, then theres no reason as to why you cant describe a thing having an infinite number of parts

a derived example of a cocategory would be if haskell had primitive negations, we can then define cofunctions via tuples, where notationally Not a refers to a variable introduction, while two negations Not (Not a) eliminate each other

ε :: (Not a, a) -> Not ()
ε (Not a, a) = Not () -- @a@ is introduced on the right of the function arguments, and deposited on the left of the tuple

type (a | b) = Not a -> b

δ :: (Not a, c) -> (Not a, b) | (Not b, c)
δ (Not a, c) (Not (Not a, b)) = (Not b, c)

for cofunctors (or unfunctors, or whatever (ideally funny) name you can come up with) the concept of lifting morphisms doesnt make sense. id know this because i thought it did, and then had to redraw all of the cofunctor diagrams once i realized the natural transformation definition looked a bit Off., so in its place you instead have a lowering transformation. that sounds a bit sillay at first, because "where are you going to get the morphism to lower it?"; a morphism which you dont actually need, because any copoint on the hom (comorphism) can be pre-composed with the lowering transformation, and in this way you can think of functors of cocategories as actually lifting comorphism. its not that we cant have functors and natural transformation, its just that they serve a very different purpose in abscense of composition and presence of bifurcation (spelled incorrectly under the cocategorical structure cause i cant spell)

expanding off the previous example, we might write

unmap :: (Not (Maybe a), Maybe b) -> (Not a, b)
unmap (Not (Just a), Just b) = (Not a, b) -- @a@ is introduced on the righthand, and a @Just a@ is deposited on the lefthand; the @Not (Just a)@ here isnt pattern matching on the @Maybe a@, but rather its creating it; we only pattern match on the @Maybe b@ 
unmap (Not Nothing, Nothing) = undefined -- this is completely valid if we attribute @undefined@ as a part of haskell's cocartesianness, in the same way that ignoring an input is just a component of haskell's cartesian nature. more on that duality in a future post

natural exclusions then are essentially the cocategorical equivalents of natural transformations. natural exclusions are essentially comorphisms of the form f x -\> g x for any suitable x. again, going off the previous examples we might arrive at:

j :: (Not (Maybe a), a) -> Not ()
j (Not (Just a), a) = Not ()

these of course are in a *-autonomous setting. what i have in the diagrams describes the far more general notion of a linear equipment. theres plenty of good examples and motivations for doing category theory in a proarrow equipment, but i hope to further study cocategory theory in them too, and more specifically all the extra possibilities given by linear equipments, such as linear adjunctions

in the future i hope to give a clearer specification of why im so interested in enriched category theory; the short answer is metaprogramming. but with regards to equipments more specifically, they give us a lot of the more correct notions of things. maybe in the future ill write more about that too. i already have way too many posts im working on for now lmao

okay i pinkie promise i have two long posts on the way but
im starting to wonder if theres anything like. linear equipments; essentially proarrow equipments but linear bicategory edition

and i think this would be a Suitably Nice place for doing cocategory theory. you have two equipments; one suitable for doing regular category theory, the other suitable for doing cocategory theory, and both related by a structure specific enough to admit duals, but general enough to not equate the two theories (like a *-bicategory would)

you have the structure of an equipment so you can do all the nice things that youd usually be able in small categories. all the nice tidbits like correct weighted limits, relative monads, derived categories (monads of profunctors)

but you can also do the same cocategorically; all that exact same shit is reversible. you take what you know about *-autonomous categories but then you forget the negation, just like you do with linearly distributive categories in the first place, and as such all the same concepts get translated and dualised over from category theory to cocategory theory but it no longer becomes the case that a category is dually equivalent to some cocategory

and since all the concepts translate perfectly over we get the correct notions of profunctors between cocategories, duals of natural transformations (i call them natural exclusions), correct definition of weighted (anti?)(co)limits, etc. but again, while abolishing the equivalence spawned by *-autonomy

then theres of course linear adjunctions which still allow to define linear duals; if you wanted to state that a given category is dual to a particular cocategory in a linear way you can huge fucking cheese wheel

(excuse my shitty handwriting lmao)

first (non-art) cohost post! (lets hope i get this right)

for a decent while now ive been trying to research cocategories and cocategory objects, since nobody else really does much. i dont really think its cause theyre genuinely useless or anything, but more because theyre unfamiliar. im currently writing a paper on the subject, but had a question regarding naming convention.

since this hasnt really been something studied much before there arent any existing conventions regarding cocategorical structures, so i wanted to take the opportunity to get some kind of consensus beforehand. we basically have a choice of naming things either by resemblance or reflection (at least if we intend to avoid prefix soup)

for example, the cocategory homomorphism that tends to be most useful more closely resemble cofunctors in category theory, but then of course they reflect functors as a dual in the same way that cofunctors normally do. if we go by resemblence it allows us to, for example, just call thing which look most like products as products. on the other hand, if we go by reflection the word "functor" better translates that they have the same usage in category theory as they do in cocategory theory.

in any case cocategories are at least conceptually very interesting. a small cocategory, for example has, boolean algebras representing its objects and morphisms, and each coclosed category gives rise to one in a similar way to how closed categories produce new categories. hell, even Hask is a cocategory if you define negations.

heres the intuition i currently have so far (though id be delighted to hear if you have any others!):
cocategories "contract" all endomorphisms. exactly what that means depends on the ambient category, but it may mean the empty set for one example
they also provide a way to take one morphism and split it into two along an arbitrary point
if that point is chosen to be one of the existing points on either side of the original morphism, the endomorphic segment contracts, and the other segment is equal to the original (figure 1)
if you split a morphism into three seperate segments, it does not matter whether you split from the left or right on the second subdivision, because each pair of possible segments must be the same for all three segments (figure 2)

excited to see what people think about this, and cocategory theory in general!