Isn't it amazing that these are all different representations of the same thing, each useful in its own way?
Remote
Sjoerd Visscher
@sjoerd_visscher@types.pl
mastodon
4.7.0-alpha.2+glitch
he/him #haskell #categorytheory #lumatone
277
Followers
227
Following
18
Posts
Joined November 14, 2022
Homepage:
I sing:
Posts
Replying to
@mc@mathstodon.xyz
@mc@mathstodon.xyz the red and blue backgrounds in table 1 seem to be missing?
Replying to
@sjoerd_visscher@types.pl
@BartoszMilewski@mathstodon.xyz Oh, and I have Star and Costar swapped. A companion of a functor A -> B is a profunctor A +-> B, which is Bop x A -> Set. That matches with Star f b a being b -> f a, which is a morphism in B.
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz Nice post and thanks for the mention! One nitpick: I don't think the forall is optional in this case.
Replying to
@sjoerd_visscher@types.pl
@BartoszMilewski@mathstodon.xyz I was confused here, the morphisms are always correct too, because the “diagonals” are elements of the profunctor which must be equal in case of a thin profunctor.
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz That’s what I thought too until yesterday. But there’s a subtle difference. A bool enriched profunctor needs to have bool enriched source and target categories. But a thin profunctor doesn’t need thin source and target categories.
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz @6d03@mathstodon.xyz Thanks, I don't have a direct answer to this, but it did gave me an idea. It is possible to encode the graph of a thin profunctor, which has at most one element for a given source and target object. There's still no guarantee that the morphisms are commuting squares, but that's common in Haskell-style category theory. (Requiring the source and target categories to be thin too would fix that.) https://github.com/sjoerdvisscher/proarrow/blob/main/src/Proarrow/Category/Instance/Graph.hs
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz @6d03@mathstodon.xyz Yes a bit. Reading up on graphs of a profunctor, it is a bit like an arrow category. (It is exactly that if the profunctor is a hom functor). Arrow categories are annoying because it has arrows as objects, and commuting squares as morphisms. But in most Haskell encodings objects are types but arrows are values, and Haskell isn’t dependently typed. Cographs on the other hand are easy [1], which is why I only tried defining cotabulators. [1]: https://github.com/sjoerdvisscher/proarrow/blob/main/src/Proarrow/Category/Instance/Collage.hs#L24
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz @6d03@mathstodon.xyz Oh, really curious to see that! I tried cotabulation once, but it was very complicated, an I didn’t keep it up to date with later refactorings: https://github.com/sjoerdvisscher/proarrow/blob/main/src/Proarrow/Category/Bicategory/Prof.hs#L190
Replying to
@BartoszMilewski@mathstodon.xyz
@6d03@mathstodon.xyz @BartoszMilewski@mathstodon.xyz It matches with what I have here: https://hackage.haskell.org/package/squares-0.2.1/docs/Data-Square.html
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz Oof, that's dense! But I think it is something totally different. My idea is to have an expression of optics that works in any proarrow equipment.
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz Just realized you also might be interested in this post: https://types.pl/@sjoerd_visscher/114881107578007749
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz Thanks! More documentation is definitely coming, especially since the design is starting to settle now. I'm for now focussing on the more practical side, like testing, generating diagrams, and trying to be able to do what's in the book Seven Sketches in Compositionality. So the bicategorical stuff will have to wait a bit.
Replying to
@BartoszMilewski@mathstodon.xyz
@BartoszMilewski@mathstodon.xyz This is awesome! I'm very much in the same boat. Although I decided to limit myself to proarrow equipments only. That's why I have been working on my #haskell proarrow library for the last two years: https://github.com/sjoerdvisscher/proarrow
In my case using double categories turned out to be annoying, so I switched to working with a single bicategory of proarrows, seeing the strict arrows as a sub-bicategory of tight/representable proarrows:
https://github.com/sjoerdvisscher/proarrow/blob/main/src/Proarrow/Category/Equipment.hs
But the double categorical view is better for diagrammatic reasoning.
Replying to
@christianp@mathstodon.xyz
@christianp @gregeganSF Listening to the french pronunciation the vowel is "eu", so there the initial "u" and the final "e" are silent, which makes a lot more sense (as far as the French spelling makes sense).
Replying to
@tomlokhorst@mastodon.social
@tomlokhorst Can you make the beeps ultrasonic? Or would that defeat the purpose.
Replying to
@mathijskadijk@mastodon.social
@mathijskadijk @brunoscheele I guess it's fine as long as the aspect ratio of the rounding of the corner doesn't change?
Replying to
@cypnk@mastodon.social
@cypnk@mastodon.social \o\ lol /o/ warding off existential dread waving my arms in the air lol