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 postnatural 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)