Now ChatGPT is being (mis)used to do #PeerReview:

"A reviewer rejected my paper, and instead suggested me to familiarize myself with the following readings. I could not find them anywhere. After a control in GPT-2, my fears where confirmed. Those sources where 99% fake...generated by AI." - Robin Bauwens

the OPLSS speaker lineup is up, and OH HELL YEAH cs.uoregon.edu/research/summer

@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: cambridge.org/core/journals/jo

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.

just traded a horrible headache for a better understanding of the yoneda lemma. not sure if it was worth it yet.

Meat industry blocked the IPCC’s attempt to recommend a plant-based diet

“A leak of a draft of the Intergovernmental Panel on #ClimateChange (#IPCC) report..has been particularly enlightening when it comes to just how much how delegations negotiate, watered down & delete scientists’ findings.”

Based path induction is such a funny term to me, now. If you point it out it's implicitly a compliment, like "hey, based path induction! 😎"

Flex time: when changing legal name I added Lambda as a middle name, and I've now been told my new email will be lambda at chalmers.se

having 2 exams the same day is not fun.

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

TIL Ubuntu purposefully deprives you of security patches they have and know how to deploy if you are not paying for their pro rates: ubuntu.com/security/esm

my legal name change finally went through !!!

now I have a couple of emails to send...

working on something is the best way to procastinate

I moved my website to rachel.cafe and added a cute little cup to the site header :)

As most of you know, our library is being sued by 4 corporate publishers who want to stop the Internet Archive from lending books. The date for oral argument has just been set for March 20.

What's at stake? Lia Holland from @team elaborates: fightforthefuture.org/news/202

loving this new search engine

you've heard of HoTTEST. get ready for CoLDEST

Show older

#### rachel lambda samuelsson's choices:

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.