Definition Context [efr-K0Y8]

Let X,Y be objects of a symmetric monoidal category \mathcal {C}. A context for X,Y is a tuple M \in \mathcal {C}, s: I \to X \otimes M, k: Y \otimes M \to I. We denote the set of contexts \mathrm {Ctx}(X,Y).

Given a morphism f: P \otimes X \to Y, and a context c = (M,s,k), the costate k(f \otimes 1_M)(1_{P} \otimes s) will be called the induced costate.