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

https://www.linkedin.com/feed/update/urn:li:share:7046083155149103105/

the OPLSS speaker lineup is up, and OH HELL YEAH https://www.cs.uoregon.edu/research/summerschool/summer23/topics.php

@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

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.

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.”

https://qz.com/ipcc-report-on-climate-change-meat-industry-1850261179 #science #food

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

I wrote a blogpost about a proof I like.

https://rachel.cafe/2023/03/06/a-favourite-proof-of-mine.html

Haskell and logic. ~ Rachel Samuelsson (@rachelrosen). https://rachel.cafe/2022/12/15/haskell-and-logic.html #Haskell #FunctionalProgramming #Logic #Math

I moved my website to https://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: https://www.fightforthefuture.org/news/2023-02-23-statement-major-decision-on-libraries-digital-rights-a-step-closer-on-march-20

is this testing whether I'm a lesbian or a replicant mr. deckard?

interested in univalent mathematics, type theory, and category theory.

undergrad at chalmers university of technology.

🏳️⚧️🏳️🌈⚧️💖

Joined May 2021