You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Reed Mullanix (Aug 23 2020 at 18:03):Hey all, I've been working through Tom Leinster's (excellent) paper, Higher Operads, Higher Categories, and I've gotten a bit stuck working through some of the coherence conditions for 2-cells on page 108, specifically the left-unitor. This is the diagram I've got so far: diagram.png
I can't seem to find any way to construct the dotted arrow. Does anyone have any insight here?
John Baez (Aug 24 2020 at 20:46):I have no idea what's going on here, but if P is the pullback of TM and E', to get a morphism from P to M you need morphisms from TM and E' to M (which must obey a property). If T is a monad and M is an algebra of that monad you have a morphism from TM to M. So then you mainly need a morphism from E' to M. Without any more clues as to what's going on, I get stuck here.
Paolo Capriotti (Aug 26 2020 at 14:44):Since is Cartesian, there is a pullback square similar to the one on the left side of your diagram, but with replaced by . You then get the unitor from the universal property of the pullback.
Reed Mullanix (Aug 31 2020 at 16:08):Well don't I feel silly! I totally forgot that was cartesian. That does make things quite a bit easier.