Puzzle 43: The way I would define the pushforward \$$f_!(P)\$$ of a partition \$$P\$$ is by first using \$$f_!: P(X)\to P(Y) \$$ to push forward each part of P, getting a family of subsets of \$$Y\$$, and then taking the finest partition \$$Q\$$ of \$$Y\$$ such that each subset in the family is contained in one of \$$Q\$$'s parts.

On the level of equivalence relations, it would look like this: Given an equivalence relation \$$\approx\$$ on \$$X\$$, first define \$$y_1\sim y_2\$$ in \$$Y\$$ by \$$y_1\sim y_2\iff \$$ (there exist \$$x_1\mapsto y_1\$$ and \$$x_2\mapsto y_2\$$ such that \$$x_1\approx x_2\$$ in \$$X\$$). This relation \$$\sim\$$ is always symmetric, but generally not transitive, and is not even reflexive if \$$f:X\to Y\$$ is not surjective. So make \$$\sim\$$ into an equivalence relation on \$$Y\$$ by generously adding everything it's missing: declare \$$y\approx y'\$$ iff there is a chain of elements \$$y_0,\dots,y_n\$$ in \$$Y\$$ such that \$$y = y_0\sim y_1\sim\ldots\sim y_n=y'\$$.

Each step in this construction is monotone with respect to fineness: if \$$x_1\approx x_2\$$ implies \$$x_1\approx' x_2\$$, then \$$y_1\sim y_2\$$ implies \$$y_1\sim' y_2\$$ and \$$y_1\approx y_2\$$ implies \$$y_1\approx' y_2\$$. So we've produced a monotone map of posets \$$f_! : \mathcal{E}(X)\to \mathcal{E}(Y)\$$.