# Constructing the E-M category of a monad out of inserters and equifiers

As suggested in the answer to another MO question, it seems possible to construct the E-M category of a monad $$T:\mathcal{C}\to\mathcal{C}$$ as an inserter followed by two equifiers as follows (I am having an issue at step 2, please see the diagram there and skip to the end if you would just like the question):

1. We begin by taking the inserter $$\mathcal{E}_0:=Ins(T,1_\mathcal{C})$$ having as objects ordered pairs $$(X,x:T(X)\to X)$$ and as arrows $$f:(X,x)\to(Y,y)$$ arrows $$f:X\to Y$$ in $$\mathcal{C}$$ such that commutes in $$\mathcal{C}$$.

2. We then note that $$T$$ lifts to a functor $$T':Ins(T,1_\mathcal{C})\to Ins(T,1_\mathcal{C}),$$ $$(X,x:T(X)\to X)\mapsto(T(X),T(x):T(T(X))\to T(X)),$$ $$f:X\to Y\mapsto T(f):T(X)\to T(Y)$$ which respects composition and identities since $$T$$ does. $$\eta$$ also lifts to a natural transformation $$\eta':1_{Ins(T,1_\mathcal{C})}\Rightarrow T',$$ $$\eta'_{(X,x)}=\eta_X:(X,x)\to(T(X),T(x)),$$ since $$\eta_X$$ is an arrow in $$Ins(T,1_\mathcal{C})$$ by virtue of the fact that commutes in $$\mathcal{C}$$.

3. Further, we have a natural transformation $${\alpha}:T'\Rightarrow1_{Ins(T,1_\mathcal{C})},$$ $${\alpha}_{(X,x)}=x:T(X)\to X,$$ which is immediately natural by the naturality square in part $$1$$, imposed on all arrows of $$Ins(T,1_\mathcal{C})$$ by definition.

4. We then take the equifier $$\mathcal{E}_1:=Eqf({\alpha}\circ\eta',1_{1_{Ins(F,G)}})$$ consisting of the full subcategory of $$Ins(T,1_\mathcal{C})$$ on objects $$(X,x)$$ such that $$\alpha_{(X,x)}\circ\eta_{(X,x)}=x\circ\eta_X=1_X,$$ so commutes in $$\mathcal{C}$$.

5. We then further take the equifier $$\mathcal{E}_2:=Eqf(\alpha\circ T'\alpha,\alpha\circ\mu')$$ consisting of the full subcategory of $$Eqf(\alpha\circ\eta,1_{1_\mathcal{C}})$$ on objects $$(X,x)$$ such that $$\alpha_{(X,x)}\circ T'\alpha_{(X,x)}=x\circ T(x)=\alpha_{(X,x)}\circ\mu'_{(X,x)}=x\circ\mu_X,$$ so commutes in $$\mathcal{C}$$.

If this all works out we end up with a commutative diagram as below and it's easy to show that the forgetful functor from the inserter category and the inclusions from equifiers create limits and that creation of limits is preserved by composition of functors, so we get that the forgetful functor from the E-M category creates limits.

This is all very nice, but the piece of step 2 where we lift $$\eta:1_\mathcal{C}\Rightarrow T$$ to a transformation $$\eta':1_{Ins(T,1_\mathcal{C})}\Rightarrow T'$$ is giving me trouble. In particular, if that diagram commutes then after step $$4$$ the top path is $$T(x)\circ T(\eta_X)=T(x\circ\eta_X)=T(1_X)=1_{T(X)}$$ by virtue of the $$T$$-algebra equation imposed in step $$4$$, which means the bottom path is also the identity so $$\eta_X\circ x=1_{T(X)}$$ -- this together with the $$T$$-algebra equation $$x\circ\eta_X=1_X$$ implies that $$x$$ and $$\eta_X$$ are isos with $$\eta_X=x^{-1}$$ which I'm almost sure is incorrect, but if this step doesn't work out I don't see how we can obtain the E-M category using this construction.

Is step 2 above correct, and if so how do we show that the diagram in step $$2$$ commutes? If step $$2$$ is not correct, how do we construct the E-M category using inserters and equifiers as suggested in the other linked MO answer?

There is also a piece of step 2 omitted where we lift $$\mu:T\circ T\Rightarrow T$$ to a natural transformation $$\mu':T'\circ T'\Rightarrow T'$$, but I stopped earlier when I realized there was a problem with $$\eta$$.

Step 2 is wrong. You want to take the equifier instead of some pairs of parallel transformations between functors $$\mathcal{E}_0 \to \mathcal{C}$$, not $$\mathcal{E}_0 \to\mathcal{E}_0$$.
As mentioned in the linked answer, for associativity these two functors will be $$T^2 U$$ and $$U$$, where $$U:\mathcal{E}_0 \to \mathcal{C}$$ is the forgetful functor, and the transformations are $$\alpha \circ \mu U$$ and $$\alpha \circ T\alpha$$, where $$\alpha : TU \to U$$ is the universal 2-cell that was inserted by the inserter.
Similarly, for the unit law, the two functors are both $$U$$, and the transformations are $$1_U$$ and $$\alpha \circ \eta U$$.