On the proof of the density theorem

Question

I'm trying to understand Leinster's proof of the density theorem. Here's the terminology and the statement.

Below is his proof. Here are some things that I don't understand:

1. This must be silly, but why is the "top" arrow in the triangle diagram labeled as $\alpha_{A',(Xf)(x)}$? It should be labeled $\alpha_{A',x'}$, but for some reason $x'$ is replaced by $(Xf)(x)$? This must have to do with the definition above (under which a map $(A,x)\to (A',x')$ are maps $f:A'\to A$ with $(Xf)(x)=x'$) but I still don't understand why we should apply this definition here. This triangle comes from the definition of cocone, and the definition of cocone doesn't entitle us to apply Definition 6.2.16.
2. I don't see why $\alpha_{A,x}\circ H_f$ corresponds to $(Yf)(y_{A,x})$. I can only see that $\alpha_{A,x}\circ H_f$ is mapped to $(\alpha_{A,x}\circ H_f)_A(1_A)=(\alpha_{A,x})_A(f)$ (and also $y_{A,x}=(\alpha_{A,x})_A(1_A)$). But that's as far as I could go.
3. Leinster says that writing $y_{A,x}$ as $\overline \alpha_A(x)$, we get a family of maps $\overline \alpha_A:X(A)\to Y(A)$. I don't quite understand this. Each $y_{A,x}$ (and so $\overline \alpha_A(x)$) is an element of $Y(A)$, isn't it? How can it be regarded as an arrow $X(A)\to Y(A)$?
4. How exactly does the very last line follow? I understand that we have two isomorphisms:

$$[\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y)\simeq [\textbf A^{op},\textbf {Set}](X,Y)\\ [\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y)\simeq [\textbf A^{op},\textbf {Set}](\text{colim}(H_\bullet \circ P),Y) $$ But why do they imply $X\simeq \text{colim}(H_\bullet \circ P)$?

Answer 1

I'll write the entire proof a little differently than Leinster, along the way addressing my original questions.

First, as Leinster says, note that $H_\bullet \circ P$ is really a diagram.

From the discussion in the comments (and this question), to prove that $X=\text{colim} (H_\bullet\circ P)$, it suffices to prove that there's a bijection

$$[\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y)\simeq [\textbf A^{op},\textbf {Set}](X,Y)$$ which is natural in $Y$.

Let's construct this bijection. A natural transformation from any $G$ to $\Delta Y$ is a cone on $G$ with vertex $\Delta Y$. So an element of the LHS is a family $$(\alpha_{A,x}:H_A=H_\bullet(A)=H_\bullet(P(A,x)))\to Y)_{A\in\mathscr A, x\in X(A)}$$ such that whenever $F:(A,x)\to (A',x')$ is an arrow in $\mathbf E(X)$, the following diagram commutes:

By the definition of morphisms in $\mathbf E(X)$, $F:(A,x)\to (A',x')$ is an arrow $f^{op}:A\to A'$ in $\mathscr A^{op}$ such that $X(f^{op})(x)=x'$. So the above triangle can be written as

Now, by the Yoneda lemma, there is a bijection

$$[\mathscr A^{op},\textbf {Set}](H_A,Y)\simeq Y(A)\\\alpha_{A,x}\mapsto \widehat{\alpha_{A,x}}=y_{A,x}$$ which is natural in $A$ and $X$. (Here, $y_{A,x}$ is defined to be $\widehat{\alpha_{A,x}}$.) Let's use the naturality in $A$. It says that for all arrows $f:A'\to A$ in $\mathscr A$, the following square commutes:

That is, under the Yoneda bijection $$[\mathscr A^{op},\textbf {Set}](H_{A'},Y)\simeq Y(A')$$ we have $$\alpha_{A,x}\circ H_f\mapsto Y(f^{op})(y_{A,x})$$ Therefore, the condition that the above triangle commutes (i.e., $\alpha_{A,x}\circ H_f=\alpha_{A',X(f^{op})(x)}$) translates to the condition $Y(f^{op})(y_{A,x})=y_{A',X(f^{op})(x)}$ after taking the images of both sides under the Yoneda bijection $\theta\mapsto \widehat \theta$.

Now we can define the map

$$\clubsuit: [\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y)\to[\textbf A^{op},\textbf {Set}](X,Y)\\ (\alpha_{A,x}:H_A\to Y)_{A\in\mathscr A, x\in X(A)}\mapsto \overline\alpha$$ where the component of $\overline \alpha $ at $A$ is defined by $\overline \alpha_A: X(A)\to Y(A), x\mapsto \overline \alpha_A(x)=\widehat {\alpha_{A,x}} \text{ }(=y_{A,x})$. We need to prove that $\overline \alpha$ is a natural transformation. This amounts to saying that if $f:A'\to A$ is an arrow in $\mathscr A$, the diagram below commutes:

This diagram indeed commutes, as the equal sign on the diagram indiates (the equal sign was justified above when we wrote the condition that the triangle commutes in a different way, taking the images of both sides under the Yoneda bijection).

Now let's define the map

$$\spadesuit: [\textbf A^{op},\textbf {Set}](X,Y) \to [\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y) $$ Given $\eta$ from the LHS, we need to define a family of arrows $(\eta_{A,x}:H_A\to Y)_{A\in\mathscr A, x\in X(A)}$. But the collection of all $\eta_{A,x}$ is bijective to $Y(A)$ (by Yoneda), so it suffices to define a family $(\widehat{\eta_{A,x}})_{A\in\mathscr A, x\in X(A)}$. Let's define $\widehat{\eta_{A,x}}=\eta_A(x)$.

It can be checked that $\clubsuit$ and $\spadesuit$ are inverses of each other, and so we have a bijection

$$[\textbf E(X),[\textbf A^{op},\textbf {Set}]](H_\bullet\circ P,\Delta Y)\simeq [\textbf A^{op},\textbf {Set}](X,Y)$$

As noted at the beginning, this implies the result.