Viktor Dukhovni ietf-dane at dukhovni.org
Tue Apr 13 17:06:41 UTC 2021

```On Tue, Apr 13, 2021 at 11:30:10AM -0500, Galaxy Being wrote:

> Is there anything universal to be drawn from these anecdotal examples of
> seeming commutativity? My breakdown of the third equation shows the same
> type definition for both sides. Is this a way to find equality? All in all,
> Bird doesn't indicate that there are any underlying truths, just "almost"
> commutativity.

Yes, but the answer is likely some combination of parametricity and the
Yoneda Lemma.

- Parametricity:  Given two fuctors f and g and some function
`foo` with type signature:

foo :: forall a. f a -> g a

we can conclude that `foo` is a "natural transformation", which
means that for all functions `bar`, we have:

foo . fmap bar = fmap bar . foo

- Yoneda Lemma: Given a functor f and some function `foo`
with signature:

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

we can conclude that for all `bar :: a -> b`:

foo bar = fmap bar (foo id)

It is interesting that you used the word "universal", because that's the
right word to describe some of the underlying category theory notions.

--
Viktor.
```