yeet ⊗

src/Cat/Bi/Diagram/Monad.lagda.md

@@ -158,8 +158,8 @@ module _ {o ℓ ℓ'} (B : Prebicategory o ℓ ℓ') where
 Suppose that we have a [[lax functor]] $P$ from the [[terminal bicategory]] to $\cB$.
 Then $P$ identifies a single object $a=P_0(*)$ as well as a morphism $M:a\to a$
 given by $P_1(\id_*)$. The composition operation is a natural transformation
-$$ P_1(\id_*)\otimes P_1(\id_*)\To P_1(\id_*\otimes \id_*) $$
-i.e. a natural transformation $\mu :M\otimes M\To M$. Finally, the unitor gives
+$$ P_1(\id_*) P_1(\id_*)\To P_1(\id_*) $$
+i.e. a natural transformation $\mu :M M\To M$. Finally, the unitor gives
 $\eta:\id\To M$.
 Altogether, this is exactly the same data as an object $a\in\cB$ and a [[monad in]]
 $\cB$ on $a$.