Post #3210905
2026-05-15 09:11 UTC
@BartoszMilewski@mathstodon.xyz Nice post and thanks for the mention! One nitpick: I don't think the forall is optional in this case.
Replies (1)
-
@sjoerd_visscher@types.pl 2026-05-15 09:33
@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.