+-----+
|     |
|     |
|     |
+-----+

forall a b. (a -> b) -> (a -> b)

The empty square is the identity transformation.

+-----+
|     |
p-----p
|     |
+-----+

forall a b. p a b -> p a b

Profunctors are drawn as horizontal lines.

Note that emptySquare is proId for the profunctor (->). We don't draw a line for (->) because it is the identity for profunctor composition.

+--f--+
|  |  |
|  v  |
|  |  |
+--f--+

forall a b. (a -> b) -> (f a -> f b)

Functors are drawn with vertical lines with arrow heads. You will recognize the above type as fmap!

We don't draw lines for the identity functor, because it is the identity for functor composition.

+--f--+
|  |  |
|  @  |
|  |  |
+--g--+

forall a b. (a -> b) -> (f a -> g b)

Non-identity transformations are drawn with an @ in the middle. Natural transformations between haskell functors are usualy given the type forall a. f a -> g a. The type above you get when fmapping before or after. (It doesn't matter which, because of naturality!)

+-----+
|     |
p--@--q
|     |
+-----+

forall a b. p a b -> q a b

Natural transformations between profunctors.

+--f--+
|  v  |
p--@--q
|  v  |
+--g--+

forall a b. p a b -> q (f a) (g b)

The complete definition of a square is a combination of natural transformations between functors and natural transformations between profunctors.

To make type inferencing easier the above type is wrapped by a newtype.

To make composing squares associative, this library uses squares with lists of functors and profunctors, which are composed together.

FList '[] a ~ a
FList '[f, g, h] a ~ h (g (f a))
PList '[] a b ~ a -> b
PList '[p, q, r] a b ~ (p a x, q x y, r y b)

A helper function to add the wrappers needed for PList and FList, if the square has exactly one (pro)functor on each side (which is common).

+--f--+     +--h--+       +--f--h--+
|  v  |     |  v  |       |  v  v  |
p--@--q ||| q--@--r  ==>  p--@--@--r
|  v  |     |  v  |       |  v  v  |
+--g--+     +--i--+       +--g--i--+

Horizontal composition of squares. proId is the identity of `(|||)`. This is regular function composition of the underlying functions.

+--f--+
|  v  |
p--@--q              +--f--+
|  v  |              |  v  |
+--g--+              p--@--q
  ===        ==>     |  v  |
+--g--+              r--@--s
|  v  |              |  v  |
r--@--s              +--h--+
|  v  |
+--h--+

Vertical composition of squares. funId is the identity of `(===)`.

+--f--+
|  v  |
|  \->f
|     |
+-----+

A functor f can be bent to the right to become the profunctor Star f.

+--f--+
|  v  |
f<-/  |
|     |
+-----+

A functor f can be bent to the left to become the profunctor Costar f.

+-----+
|     |
|  /-<f
|  v  |
+--f--+

The profunctor Costar f can be bent down to become the functor f again.

+-----+
|     |
f>-\  |
|  v  |
+--f--+

The profunctor Star f can be bent down to become the functor f again.

+-----+
f>-\  |         fromLeft
|  v  |         ===
f<-/  |         toLeft
+-----+

fromLeft and toLeft can be composed vertically to bend Star f back to Costar f.

+-----+
|  /-<f         fromRight
|  v  |         ===
|  \->f         toRight
+-----+

fromRight and toRight can be composed vertically to bend Costar f to Star f.

+f-f-f+     +--f--+     spiderLemma n =
|v v v|     f> v <f       fromLeft ||| funId ||| fromRight
| \|/ |     | \|/ |       ===
p--@--q ==> p--@--q       n
| /|\ |     | /|\ |       ===
|v v v|     g< v >g       toLeft ||| funId ||| toRight
+g-g-g+     +--g--+

The spider lemma is an example how bending wires can also be seen as sliding functors around corners.

spiderLemma' n = (toRight === proId === fromRight) ||| n ||| (toLeft === proId === fromLeft)

The spider lemma in the other direction.

H²-f--H
|  v  |
p--@--q     H = Hask, H² = Hask x Hask
|  v  |
H²-g--H

Combine two profunctors from Hask to a profunctor from Hask x Hask

Uncurry the kind of a bifunctor.

type UncurryF :: (a -> b -> Type) -> (a, b) -> Type

1--a--H
|  v  |
U--@--q     1 = Hask^0 = (), H = Hask
|  v  |
1--b--H

The boring profunctor from and to the unit category.

Values as a functor from the unit category.