Post #3023663

2026-05-13 11:38 UTC

@sjoerd_visscher@types.pl @6d03@mathstodon.xyz It seems to me like you're defining a subcategory of Hask by imposing a Constraint on objects. So a Tabulator would be a class that takes two categories and a profunctor between them. It would have two projections giving objects in these two categories, and a projection that gives the element of the type given by the profunctor on these two objects. Does it make sense?

Replies (2)

@BartoszMilewski@mathstodon.xyz 2026-05-13 11:49

@sjoerd_visscher@types.pl @6d03@mathstodon.xyz A morphism is built from two pairs of objects (a, b) and (a', b') and a pair of arrows (u: a -> a', v: b -> b'). They have to satisfy a commuting square that uses lmap and rmap.

Open ##3023664
@sjoerd_visscher@types.pl 2026-05-13 14:57

@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

Open ##3023665