Toy Haskell implementation of profunctor equipment encodes double-category 2-cells as compiler-verified natural transformations using Profunctor, Star, and Costar.
Key Takeaways
Cell f g h j is typed as forall a c. h a c -> j (f a) (g c), encoding 2-cells with universal quantification enforced by GHC.
Horizontal composition uses Compose and dimap; vertical composition relies on Procompose, a coend encoded as an existential type.
Companion and conjoint map directly to stdlib Costar and Star; unit laws hold up to isomorphism within Hask.
Full correctness requires dependent types; this single-category, endo-functor restriction trades completeness for compiler checkability.
See Sjoerd Visscher’s proarrows library for a more elaborate version beyond this toy scope.
