rachel lambda samuelsson @rachelrosen@types.pl

https://github.com/twitter/the-algorithm/blob/main/home-mixer/server/src/main/scala/com/twitter/home_mixer/functional_component/decorator/HomeTweetTypePredicates.scala

?

@maxsnew This shows up quite often when programming with dependent types, indexed by a monoid. I first learned it from a post to the Agda mailing list by Alan Jeffrey years ago. It's quite useful when writing functions like vector reverse: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/wellknown-representation-of-monoids-and-its-application-to-the-function-vector-reverse/929D15452762F6BB0A4A68503026D1C4

@hallasurvivor @de_Jong_Tom

The idea is quite simple and beautiful. As Tom says, you can
analogously use Cayley's theorem for groups or monoids. Functional
programmers use the same trick, there called "difference lists".

Take an expression
((id o (f o g)) o h)
where f,g,h are morphisms in a category 𝓒.
This (up to quotienting) is a morphism in the free category on the
underlying graph of 𝓒, call this F (U 𝓒).

The UMP of the free category says we can define a functor F (U 𝓒) → 𝓓 if
we give a homomorphism of the underlying graphs U 𝓒 → U 𝓓.

So we take 𝓓 = 𝓟o 𝓒, the presheaf category on 𝓒. We define a functor
F (U 𝓒) → 𝓟o 𝓒 by defining it on the graph: U 𝓒 → U (𝓟o 𝓒). To do that
we just use the underlying homomorphsm of the Yoneda embedding, which
we recall is defined on morphisms as
Y(f)(x) = f o x
Then we get a functor ⟦_⟧ : F (U 𝓒) → 𝓟o 𝓒 satisfying
⟦ f ⟧(x) = f o x.

Now let's look at what happens when we take ⟦_⟧ on that expression
from before, and note that all of the following equations are "by
definition" rather than "by an axiom of a category":
⟦ ((id o (f o g)) o h) ⟧(x)
= ⟦ (id o (f o g)) ⟧ (⟦ h ⟧ x)
= id (⟦ (f o g) ⟧ (⟦ h ⟧ x))
= id (⟦ f ⟧ (⟦ g ⟧ (⟦ h ⟧ x)))
= f o (g o (h o x))

So we get that interpreting the morphism in the presheaf category
"automatically" re-associates all of the compositions and removes any
ids.

Finally, we can extract from this a morphism in the original category
by applying this to id:

⟦ ((id o (f o g)) o h) ⟧(id) = f o (g o (h o id))

And we see that what we get back is what we would have defined as a
"normal form" for category expressions.

Okay I just found this strange rabbit hole of... AI generated Bandcamp spam?