Post #3023665
2026-05-13 14:57 UTC
@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
Replies (1)
-
@BartoszMilewski@mathstodon.xyz 2026-05-13 15:48
@sjoerd_visscher@types.pl @6d03@mathstodon.xyz Yes, trying to do dependent types in Haskell is a challenge. How would you encode the simplest category of elements of a functor. An object is a type `a` and a value `x :: f a`. A morphism from (a, x) to (b, y) is a function u: a->b such that `fmap u x = y`. If you can encode this, then tabulation should be relatively easy.