Definition [efr-EGK8]

Let \mathcal {C} be a monoidal category. A selection relation on an object A \in \mathcal {C} is a relation \epsilon \subseteq \mathcal {C}(I,A) \times \mathcal {C}(A,I). We write \epsilon (a,k) for the statement (a,k) \in \epsilon .

Selection relations are ordered by inclusion, and so form a (posetal) category, which we denote \mathbb {S}_\mathcal {C}(A). Given f: A \to B, we define the pushforward on selection relations by f_*\epsilon = \{(fx,k) \mid (x, kf) \in \epsilon \}. In other words, f_*\epsilon (y,k) if and only if there exists x: I \to X so that fx = y and \epsilon (x, kf).

It is clear that pushforward is monotone, so that this defines a functor \mathbb {S}_\mathcal {C} : \mathcal {C} \to \mathsf {Cat}