@BartoszMilewski@mathstodon.xyz
Post #3023666
2026-05-13 15:48 UTC
@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.
Replies (1)
-
@sjoerd_visscher@types.pl 2026-05-13 19:26
@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