Follow

So I guess that this is my #introduction

I am a PhD student in Glasgow, in the university of Strathclyde, mostly studying category theory and monoidal category adjacent things. Right now, I am really into Hopf Monads

@jeslie0 Maybe? It haven't thought about it, but the adjunction \(R\)-Mod\(\rightarrow\) Ab might be Hopf?

Essentially, the requirement is that the forgetful functor is strong monoidal. So if

\[U:R-Mod \rightarrow Ab\]

is the forgetful functor, then you need

\[U(A \otimes B) \cong UA \otimes UB\]

Do you know if that is true?

@jeslie0 i see that you are into Agda - most of my colleagues are Agda people, but I’ve unfortunately not learned enough about type theory while I’ve been here to be good conversation 😛

I probably won’t get it, but what kind of stuff are you doing with Hott?

James Leslie@jeslie0@mathstodon.xyz@Jonoidal welcome to Mathstodon! I'll bite, what is a Hopf Monad and how is it different to an ordinary monad?