I'm currently self-studying category theory and I'm trying to understand how F. Loregian's proof of Fubini theorem in Co/end calculus (1.31) can be generalised to arbitrary category $\mathcal{D}$ (since the proof is done in the category of sets).
I'm working on lemma 1.32 that aims to show that $\int_C F(C,C) \cong \int_{C,C'}\mathcal{C}(C,C')\pitchfork F(C,C')$
I was able to build the wedge $\omega:\Delta_{\int_C F(C,C)}\rightarrow \mathcal{C}(-,?)\pitchfork F(-,?)$ by verifying that $\omega_{C,C'}=F^*_{C,C'}\tilde\psi=F_{*,C,C'}\tilde\psi$ verifies the dinaturality condition where $\tilde\psi$ is the canonical $\int_C F(C,C)\rightarrow \prod_{C\in\mathcal{C}}F(C,C)$ and $F^*_{C,C'},F_{*,C,C'}:\prod_{C\in\mathcal{C}}F(C,C)\rightarrow\prod_{f:C\rightarrow C'}F(C,C')$ are the morphism associated to the equaliser formula of ends presented in 1.27 of the same document.
I am omitting the details of the proof of dinaturality since I would need to introduce the numerous projections and it will be messy.
Now I need to show that $\omega$ is terminal, so given $(\Omega\in\mathcal{D}, \gamma:\Delta_{\Omega}\rightarrow \mathcal{C}(-,?)\pitchfork F(-,?))$ I am trying to build $k:\Omega:\rightarrow\int_C F(C,C)$ s.t. $\forall C,C': \gamma_{C,C'}=\omega_{C,C'}k$.
I thought about considering for every $C\in\mathcal{C}$ the arrow $\Omega\rightarrow \mathcal{C}(C,C)\pitchfork F(C,C)=\prod_{f:C\rightarrow C}F(C,C)\rightarrow F(C,C)$ where the last arrow is the projection of component $1_C$ but I cannot show that it forms a wedge and hence deduce the existence of $k$.
I am unable to find any ways to construct $k$.
$\newcommand{\set}{\mathsf{Set}}\newcommand{\C}{\mathcal{C}}\newcommand{\D}{\mathcal{D}}\newcommand{\E}{\mathcal{E}}\newcommand{\A}{\mathscr{A}}\newcommand{\B}{\mathscr{B}}\newcommand{\op}{{^\mathsf{op}}}\require{AMScd}$I would have to disagree with the author that direct proofs are somehow boring; there is a pretty proof of the Fubini isomorphism in Mac Lane's CWM. Also, to rigorously check all details is quite tedious in this proof. Moreover the author correctly states the theorem is an existence theorem too; one (co)end exists if and only if the other does, in which case they are isomorphic. However the proof crucially uses the existence of other (co)limits and is a little dodgy in the sense that it relies on all (co)ends existing to define the pair of adjoint functors even though this is not necessary. This is fixable by applying the adjunction isomorphisms on specific given objects only and unwinding the proof a little; it works so long as we assume all powers and copowers exist in $\D$. There’s also a minor issue in that they want you to show $H_{\C\times\E}\cong H_\C\circ H_\E$ but in fact this composite doesn't make sense; there is a domain error. I handle this at the end of this post.
That said, this proof is certainly slick and it seems much more amenable to generalisation; the use of the tensor and cotensors $X\otimes D,X\pitchfork D$ is suggestive of an enriched generalisation. You could say that this proof uses the $\mathsf{Set}$-bimodule structure on the (bicomplete and locally small) category $\D$. It's worth noting we never use the details of the explicit construction of $\otimes,\pitchfork$; any bimodule structure would work.
You didn't mention it in your post so here let $\otimes:\set\times\D\to\D$ denote the "tensor" functor $(X,D)\mapsto\bigsqcup_{x\in X}D$ (on objects) and on arrows $f:X\to X',g:D\to D'$ we declare $f\otimes g$ to be the map $X\otimes D\to X'\otimes D'$ whose every $x$th component is $D\overset{g}{\longrightarrow}D'\overset{\iota_{f(x)}}{\hookrightarrow}X'\otimes D'$. It's easy to verify functoriality. We let $\pitchfork:\set\op\times\D\to\D$ denote the "cotensor" functor $(X,D)\mapsto\prod_{x\in X}D$ (on objects) and on arrows $f:X'\to X,g:D\to D'$ we set $f\pitchfork g:X\pitchfork D\to X'\pitchfork D'$ by declaring its every $x'$th projection to be the map $X\pitchfork D\overset{\pi_{f(x')}}{\twoheadrightarrow}D\overset{g}{\longrightarrow}D'$. It is again easy to verify functoriality.
The author didn't explicitly say so, but the isomorphisms: $$\D(X\otimes D,D')\cong\set(X,\D(D,D'))\cong\D(D,X\pitchfork D')$$Can be chosen to be natural in all variables. This is called a two-variable adjunction. We use the naturality of these adjunctions again and again in the below.
It's a good exercise to check the naturality. To focus on $\set(X,\D(D,D'))\cong\D(D,X\pitchfork D')$, for a map $G:X\to\D(D,D')$ we define $D\to X\pitchfork D'$ by setting every $x$th projection to equal $G(x):D\to D'$.
I don't like the way the author picks $\D=\set$ and inexplicitly states their maps. We can define the same things and make all the necessary calculations without the slightest reference to "generalised elements".
It follows from the adjunction that to find a map $\varpi_{C,C'}:\int_{\C}F\to\C(C,C')\pitchfork F(C,C')$ is to find a function from $\C(C,C')\to\D(\int_\C F,F(C,C'))$. Well, $\int_\C F$ comes equipped with a (terminal) wedge to $F$; for any arrow $f\in\C(C,C')$ we can have two choices of arrow $\int_\C F\to F(C,C')$: we could put $\int_\C F\to F(C,C)\overset{F(1,f)}{\longrightarrow}F(C,C')$ or we could put $\int_\C F\to F(C',C')\overset{F(f,1)}{\longrightarrow}F(C,C')$. Thankfully these choices are the same by the definition of wedge! So we have this function $\C(C,C')\to\D(\int_\C F,F(C,C'))$ and obtain an arrow $\int_\C F\to\C(C,C')\pitchfork F(C,C')$.
The functor $\C\pitchfork F$ is really the composite: $$(\C\op\times\C)\op\times(\C\op\times\C)\overset{\C\op\times F}{\longrightarrow}\set\op\times\D\overset{\pitchfork}{\longrightarrow}\D$$
We would like to check the extranaturality of these $\varpi_{C,C'}$. Using the adjunction avoids having to deal with a mess of projections.
Say $f:C_2\to C_1,g:C'_1\to C'_2$ in $\C$. $$\int_\C F\overset{\varpi_{C_1,C_1'}}{\longrightarrow}\C(C_1,C_1')\pitchfork F(C_1,C_1')\overset{1\pitchfork F(f,g)}{\longrightarrow}\C(C_1,C_1')\pitchfork F(C_2,C'_2)$$Transposes to: $$\C(C_1,C_1')\to\D\left(\int_\C F,F(C_1,C_1')\right)\overset{\D(1,F(f,g))}{\longrightarrow}\D\left(\int_\C F,F(C_2,C_2')\right)$$Which maps $h:C_1\to C'_1$ to the arrow: $$\int_\C F\to F(C_1,C_1)\overset{F(1,h)}{\longrightarrow} F(C_1,C'_1)\overset{F(f,g)}{\longrightarrow}F(C_2,C_2')\\=\int_\C F\to F(C_1,C_1)\overset{F(f,1)}{\longrightarrow}F(C_2,C_1)\overset{F(1,gh)}{\longrightarrow}F(C_2,C_2')$$
And the other route:
$$\int_\C F\overset{\varpi_{C_2,C_2'}}{\longrightarrow}\C(C_2,C_2')\pitchfork F(C_2,C_2')\overset{\C(f,g)\pitchfork1}{\longrightarrow}\C(C_1,C_1')\pitchfork F(C_2,C'_2)$$Transposes to: $$\C(C_1,C_1')\overset{\C(f,g)}{\longrightarrow}\C(C_2,C_2')\to\D\left(\int_\C F,F(C_2,C_2')\right)$$Which takes $h:C_1\to C'_1$ to $ghf:C_2\to C'_2$ and further to: $$\int_\C F\to F(C_2,C_2)\overset{F(1,ghf)}{\longrightarrow}F(C_2,C_2')\\=\int_\C F\to F(C_2,C_2)\overset{F(1,f)}{\longrightarrow}F(C_2,C_1)\overset{F(1,gh)}{\longrightarrow}F(C_2,C_2')$$
Using the wedge condition on $\int_\C F\to F(-,-)$ we see these arrows are the same. It follows $\varpi_\bullet$ is a wedge.
Why is it terminal?
In your notation we consider an object $\Omega$ and a wedge $\gamma_{C,C'}:\Omega\to\C(C,C')\pitchfork F(C,C')$. These arrows transpose to arrows $\C(C,C')\to\D(\Omega,F(C,C'))$. I claim that the arrows $\Gamma_C:\Omega\to F(C,C)$, defined by the arrow picked out in $1\overset{\mathrm{Id}_C}{\longrightarrow}\C(C,C)\to\D(\Omega,F(C,C))$ assemble to a wedge. Say $f:C\to C'$.
$F(1,f)\Gamma_C$ is the evaluation of the function: $$\C(C,C)\to\D(\Omega,F(C,C))\overset{\D(1,F(1,f))}{\longrightarrow}\D(\Omega,F(C,C'))$$At $\mathrm{Id}_C$. This function transposes back to the arrow: $$\Omega\overset{\gamma_{C,C}}{\longrightarrow}\C(C,C)\pitchfork F(C,C)\overset{1\pitchfork F(1,f)}{\longrightarrow}\C(C,C)\pitchfork F(C,C')\\=\Omega\overset{\gamma_{C,C'}}{\longrightarrow}\C(C,C')\pitchfork F(C,C')\overset{\C(1,f)\pitchfork 1}{\longrightarrow}\C(C,C)\pitchfork F(C,C')$$ Which is the transpose of the function: $$\C(C,C)\overset{\C(1,f)}{\longrightarrow}\C(C,C')\to\D(\Omega,F(C,C'))$$When evaluated at $\mathrm{Id}_C$ this yields the evaluation of $\C(C,C')\to\D(\Omega,F(C,C'))$ at $f$.
$F(f,1)\Gamma_{C'}$ is the evaluation at $\mathrm{Id}_C$ of the function: $$\C(C',C')\to\D(\Omega,F(C',C'))\overset{\D(1,F(f,1))}{\longrightarrow}\D(\Omega,F(C,C'))$$Which transposes to: $$\Omega\overset{\gamma_{C',C'}}{\longrightarrow}\C(C',C')\pitchfork F(C',C')\overset{1\pitchfork F(f,1)}{\longrightarrow}\C(C',C')\pitchfork F(C,C')\\=\Omega\overset{\gamma_{C,C'}}{\longrightarrow}\C(C,C')\pitchfork F(C,C')\overset{\C(f,1)\pitchfork1}{\longrightarrow}\C(C',C')\pitchfork F(C,C')$$Which transposes back into: $$\C(C',C')\overset{\C(f,1)}{\longrightarrow}\C(C,C')\to\D(\Omega,F(C',C'))$$When evaluated at $\mathrm{Id}_C$ this gives the evaluation of $\C(C,C')\to\D(\Omega,F(C',C'))$ at $f$. That's the same as what we had before! Therefore $\Gamma_\bullet$ defines a wedge.
There is then a unique arrow $\kappa:\Omega\to\int_\C F$ relating $\Gamma_\bullet$ to the unlabelled terminal wedge of $\int_\C F$. This would prove $\varpi_\bullet$ to be terminal if we establish that for general arrows $\lambda:\Omega\to\int_\C F$, $\lambda$ relates $\gamma_\bullet$ to $\varpi_\bullet$ if and only if it relates $\Gamma_\bullet$ to the terminal wedge of $\int_\C F$. Then uniqueness would be inherited; we would infer $\varpi_\bullet\circ\kappa=\gamma_\bullet$ and that $\kappa$ is unique in this respect, as desired.
The equation: $$\Omega\overset{\lambda}{\longrightarrow}\int_\C F\overset{\varpi_{C,C'}}{\longrightarrow}\C(C,C')\pitchfork F(C,C')=\gamma_{C,C'}$$When instantiated with $C=C'$ transposes precisely to the equation: $$\C(C,C)\to\D\left(\int_\C F,F(C,C)\right)\overset{\D(\lambda,1)}{\longrightarrow}\D(\Omega,F(C,C))\\=\C(C,C)\overset{\hat{\gamma_{C,C}}}{\longrightarrow}\D(\Omega,F(C,C))$$Which gives that $\Gamma_C=\Omega\overset{\lambda}{\longrightarrow}\int_\C F\to F(C,C)$ as desired.
In the converse we want to show the function $\hat{\gamma_{C,C'}}$ equals $\C(C,C')\to\D\left(\int_\C F,F(C,C')\right)\overset{\D(\lambda,1)}{\longrightarrow}\D(\Omega,F(C,C'))$. To do so it suffices to check this at every $f:C\to C'$; it then suffices to check the function: $$\C(C,C)\overset{\C(1,f)}{\longrightarrow}\C(C,C')\to\D\left(\int_\C F,F(C,C')\right)\overset{\D(\lambda,1)}{\longrightarrow}\D(\Omega,F(C,C'))\\=\C(C,C)\to\D\left(\int_\C F,F(C,C)\right)\overset{\D(1,F(1,f))}{\longrightarrow}\D\left(\int_\C F,F(C,C')\right)\overset{\D(\lambda,1)}{\longrightarrow}\D(\Omega,F(C,C'))\\=\C(C,C)\to\D\left(\int_\C F,F(C,C)\right)\overset{\D(\lambda,1)}{\longrightarrow}\D(\Omega,F(C,C))\overset{\D(1,F(1,f))}{\longrightarrow}\D(\Omega,F(C,C'))$$Agrees with: $\hat{\gamma_{C,C'}}\C(1,f)$ at $\mathrm{Id}_C$. Its evaluation at $\mathrm{Id}_C$ gives us $F(1,f)\Gamma_C$ by hypothesis.
What about $\hat{\gamma_{C,C'}}\C(1,f)$? This function transposes to: $$\Omega\overset{\gamma_{C,C'}}{\longrightarrow}\C(C,C')\pitchfork F(C,C')\overset{\C(1,f)\pitchfork1}{\longrightarrow}\C(C,C)\pitchfork F(C,C')\\=\Omega\overset{\gamma_{C,C}}{\longrightarrow}\C(C,C)\pitchfork F(C,C)\overset{1\pitchfork F(1,f)}{\longrightarrow}\C(C,C)\pitchfork F(C,C')$$Transposing back to $\D(1,F(1,f))\hat{\gamma_{C,C}}$ so this too evaluates to $F(1,f)\Gamma_C$. $\blacksquare$
It's also important that the resultant isomorphism $\int_\C F\cong\int_{\C\op\times\C}\C\pitchfork F$ is natural in $F$; if $\alpha:F\implies G$ is a natural transformation of functors $F,F':\C\op\times\C\to\D$ then we have: $$\tag{$\ast$}\begin{CD}\int_\C F@>\int_\C\alpha>>\int_\C G\\@V\cong VV@VV\cong V\\\int_{\C\op\times\C}\C\pitchfork F@>>\int_{\C\op\times\C}1\pitchfork\alpha>\int_{\C\op\times\C}\C\pitchfork G\end{CD}$$
This is necessary to claim that, if $\D$ is bicomplete and all (co)ends exist, we truly have an adjunction $\C\otimes(-)\dashv\int_\C(-)$. This adjunction is defined as follows; if $D\in\D$, by computing transposes we have that a family of arrows $\beta_{C,C'}:\C(C,C')\otimes D\to F(C,C')$ is natural $\C(-,-)\otimes D\implies F$ if and only if its transpose $D\to\C\pitchfork F$ defines a wedge. We take any natural transformation $\beta$, map it to its transpose wedge $D\overset{\cdot}{\to}\C\pitchfork F$, map this to its unique arrow $D\to\int_{\C\op\times\C}\C\pitchfork F$ and compose with our canonical isomorphism to get an arrow $D\to\int_\C F$. Given naturality of the isomorphisms $\int_\C F\cong\int_{\C\op\times\C}\C\pitchfork F$, it's not too hard to check the isomorphism $\D^{\C\op\times\C}(\C\otimes D,F)\cong\D(D,\int_\C F)$ is natural in both variables - so, defining an adjunction.
The naturality square $(\ast)$ commutes if and only if it commutes when composed with every $\int_{\C\op\times\C}\C\pitchfork G\to\C(C,C')\pitchfork G(C,C')$. The lefthand route would yield $\int_\C F\to\C(C,C')\pitchfork F(C,C')\overset{1\pitchfork\alpha}{\longrightarrow}\C(C,C')\pitchfork G(C,C')$ which transposes to the function: $$\C(C,C')\to\D\left(\int_\C F,F(C,C')\right)\overset{\D(1,\alpha)}{\longrightarrow}\D\left(\int_\C F,G(C,C')\right)$$ This function takes some $f:C\to C'$ to: $$\int_\C F\to F(C,C)\overset{F(1,f)}{\longrightarrow}F(C,C')\overset{\alpha}{\longrightarrow}G(C,C')\\=\int_\C F\to F(C,C)\overset{\alpha}{\longrightarrow}G(C,C)\overset{G(1,f)}{\longrightarrow}G(C,C')\\=\int_\C F\overset{\int_\C\alpha}{\longrightarrow}\int_\C G\to G(C,C)\overset{G(1,f)}{\longrightarrow}G(C,C')$$In other words, this function equals: $$\C(C,C')\to\D\left(\int_\C G,G(C,C')\right)\overset{D(\int_\C\alpha,1)}{\longrightarrow}\D\left(\int_\C F,G(C,C')\right)$$Which transposes back to exactly the righthand route. Since $C,C'$ is arbitrary, we are done; $(\ast)$ commutes and we have a genuine adjunction.
Denote by $H_\C$ the functor $\D\to\D^{\C\op\times\C}$ given on objects by $D\mapsto\C\otimes D$ and on arrows $f:D\to D'$ by the natural transformation $1\otimes f$; we know from the above that we have an adjunction: $H_\C\dashv\int_\C$, running $\D\rightleftarrows\D^{\C\op\times\C}$.
For $F:(\C\times\E)\op\times(\C\times\E)\to\D$, we would like to show that: $$\int_\C\int_\E F(C,E,C',E')\cong\int_{\C\times\E}F$$The left hand side is the result of the following functor: $$\int_\C\int_\E:\D^{(\C\times\E)^\op\times(\C\times\E)}\cong(\D^{\E\op\times\E})^{\C\op\times\C}\overset{\left(\int_\E\right)^{\C\op\times\C}}{\longrightarrow}\D^{\C\op\times\C}\overset{\int_\C}{\longrightarrow}\D$$
There is the following general and easy theorem:
So, given that $H_\E\dashv\int_\E$ we infer $(H_\E)^{\C\op\times\C}\dashv\left(\int_\E\right)^{\C\op\times\C}$. From this and from the composition of adjoints we deduce that $\int_\C\int_\E$ is right adjoint to: $$H_{\C,\E}:D\overset{H_\C}{\longrightarrow}D^{\C\op\times\C}\overset{(H_\E)^{\C\op\times\C}}{\longrightarrow}(D^{\E\op\times\E})^{\C\op\times\C}\cong\D^{(\C\times\E)\op\times(\C\times\E)}$$
This is the correct composite, not "$H_\C\circ H_\E$". Now, the establishment of a natural isomorphism $H_{\C,\E}\cong H_{\C\times\E}$ would flip to a natural isomorphism $\int_{\C\times\E}\cong\int_\C\int_\E$, which would give the Fubini theorem.
Thankfully, that's quite easy. We still technically don't need knowledge of how $\otimes$ is constructed; in a general bimodule, there will exist a canonical natural isomorphism: $$H_{\C\times\E}(D)(C,E,C',E')=(\C(C,C')\times\E(E,E'))\otimes D\\\cong\E(E,E')\otimes(\C(C,C')\otimes D)=H_{\C,\E}(D)(C,E,C',E')$$