http://www.math.jhu.edu/~eriehl/hocolimits.pdf
前日までの議論をまとめると、
\int^{c \in C}Bn(*,C,C(c,-)) \otimes Fc = \coprod_{\gamma:[n]\to C}F\gamma(0)
であることが証明できる。
実際、これの左辺はc \mapsto N(c/C)nとFcのcoendであり、Setにおけるtensorはcoprodだから\coprod_{N(c/C)}Fcのcoendを計算する。
N(c/C)nの元はc \to c0 \to c1 \to \cdots \to cnであるから、N(c/C)nを\gamma:[n] \to Cとc \to \gamma(0)に分解して、
\int^{c\in C}\coprod_{N(c/C)n}Fc =
\int^{c\in C}\coprod_{\gamma}\coprod_{c\to\gamma(0)}Fc
でcoendとcoprodは交換するので
= \coprod_{\gamma}\int^{c \in C}\coprod_{c \to \gamma(0)}Fc
= \coprod_{\gamma}F\gamma(0)
となる。
