Skip to content

Commit 77f9a16

Browse files
authored
Fix typoes in Cat.Monoidal.Instances.Day (#485)
# Description There are some confusions in the coend diagram on this page trying to match notation both from the previous equation (of a convolution) and the following agda equations (between F,G/X,Y and x/c). I've chosen to amend the diagram to completely match the one before, since the prose seems to be primarily attempting to compare the two.
1 parent 9eedf3b commit 77f9a16

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

src/Cat/Monoidal/Instances/Day.lagda.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -176,20 +176,20 @@ isomorphism, but this turns out to be too strong: we can simply take the
176176
product with the $\hom$-set into the product:
177177
178178
$$
179-
(F \otimes^D G)(x) = \int^{c_1, c_2 : \cC} \hom_{\cC}(c, c_1 \otimes c_2) \times X(c_1) \times Y(c_2)
179+
(F \otimes^D G)(x) = \int^{x_1, x_2 : \cC} \hom_{\cC}(x, x_1 \otimes x_2) \times F(x_1) \times G(x_2)
180180
$$
181181
182182
::: warning
183183
It's worth taking a second to read the formalised definition, below, if
184184
you are unfamiliar with coends. We must express the "integrand" as a
185185
functor $(C \times C)\op \times C \times C$. This provides us with
186-
"polarised" versions of the variables $c_1, c_2$, which we write
187-
$c_1^-/c_1^+$ and $c_2^-/c_2^+$.
186+
"polarised" versions of the variables $x_1, x_2$, which we write
187+
$x_1^-/x_1^+$ and $x_2^-/x_2^+$.
188188
189189
We then distribute these variables according to the polarities of each
190190
functor. Since $\hom$ is covariant in its second argument, it sees
191191
$c_1^+ \otimes c_2^+$; but the presheaves are contravariant, so we have
192-
factors $X(c_1^-)$ and $Y(c_2^-)$.
192+
factors $F(x_1^-)$ and $G(x_2^-)$.
193193
:::
194194
195195
```agda

0 commit comments

Comments
 (0)