Previously: Profunctor Equipment.

To make things more palatable for programmers, I decided to provide a toy implementation of some of the equipments in Haskell. The advantage of this encoding is that it can be verified by the compiler, and I still trust the compiler more than I trust the AI.

A more adequate implementation would require a full-blown dependently typed language, but if we restrict ourselves to just a single category and work only with endo-functors and endo-profunctors, we can get at least some intuitions. If you want to see a more elaborate version, see the proarrows library by Sjoerd Visscher.

The only 0-cell I’ll be using is the Haskell category of types and functions. For vertical 1-cells I’ll use the standard library implementation of Functor, and for horizontal ones I’ll use Profunctor.

A 2-cell in \mathbb{P}rof:

is implemented as a natural transformation:

type Cell f g h j = forall a c . h a c -> j (f a) (g c)

The forall serves as a universal quantifier.

The horizontal composition of such cells is given by:

hcomp :: (Functor f, Functor f', Functor g, Functor g'
         , Profunctor h, Profunctor j, Profunctor k) =>
    Cell f g h j -> Cell f' g' j k 
                 -> Cell (Compose f' f) (Compose g' g) h k
hcomp fg_hj fg_jk hac = dimap getCompose Compose $ fg_jk (fg_hj hac)

I used the library definition of functor composition:

newtype Compose f g a = Compose { getCompose :: f (g a) }

Vertical composition of cells uses a more elaborate profunctor composition:

vcomp :: (Functor f, Functor g, Functor h
         , Profunctor p, Profunctor q, Profunctor r, Profunctor s) =>
    Cell f g p r -> Cell g h q s 
                 -> Cell f h (Procompose q p) (Procompose s r)
vcomp fg_pr gh_qs (Procompose qxc pax) 
    = Procompose (gh_qs qxc) (fg_pr pax)

Profunctor composition is defined using a coend. In Haskell, we implement a coend:

\int^x P \langle x, c\rangle \times Q \langle d, x \rangle

as an existential type: 

data Procompose p q d c where
  Procompose :: p x c -> q d x -> Procompose p q d c

Here, x is a type that’s not in the argument list, so it’s interpreted using the existential counterpart of forall.

This is the horizontal unit cell:

type Hunit p = Cell Identity Identity p p

hUnit :: Profunctor p => Hunit p
hUnit = dimap runIdentity Identity

and here’s its vertical counterpart:

type Vunit f a b = Cell f f (->) (->)

vUnit :: Functor f => Vunit f a b
vUnit = fmap

I used the library implementation of the Identity functor, and the type constructor (->) for the hom-profunctor–the unit of profunctor composition. The unit laws are satisfied up to isomorphism.

The companion and the conjoint are synonyms of the library types Costar and Star:

newtype Star f d c   = Star   { runStar   :: d -> f c }
newtype Costar f d c = Costar { runCostar :: f d -> c }
type Companion f d c = Costar f d c
type Conjoint f d c  = Star f d c

The companion unit and counit cells:

are given by, respectively:

type CompUnit f   = Cell Identity f (->) (Costar f)

compUnit :: Functor f => CompUnit f
compUnit h = Costar (fmap (h . runIdentity))

and

type CompCoUnit f = Cell f Identity (Costar f) (->)

compCoUnit :: Functor f => CompCoUnit f 
compCoUnit (Costar h) = Identity . h

Similarly for the conjoint:

type ConjUnit f   = Cell f Identity (->) (Star f)

conjUnit :: Functor f => ConjUnit f 
conjUnit h = Star  (fmap (Identity . h))

and:

type ConjCoUnit f = Cell Identity f (Star f) (->)

conjCoUnit :: Functor f => ConjCoUnit f 
conjCoUnit (Star h) = h . runIdentity

More advanced constructions would require the definition of categories internal to Hask and the use of dependent types.

Haskell code is available here.