Some minor stuff, when

\[ \Phi : X^{\text{op}} \times Y \to \mathbf{Bool} \]

we write \\( \Phi : X\nrightarrow Y \\) but nLab, Wikipedia and Borceaux write \\( \Phi : Y\nrightarrow X \\) (from the covariant to the contravariant argument).