Definition [efr-001X]

Let p: A' \leftrightarrows A be a lens, let T(A')^\infty \leftrightarrows A' be the terminal A'-system, and consider the composite T(A')^\infty \leftrightarrows A' \leftrightarrows A. A A'/A-modal operator is a factorization of this system over A' \leftrightarrows A, i.e some other A'-system with the same state space, \alpha : T(A')^\infty \leftrightarrows A' so that the two composites T(A')^\infty \leftrightarrows A' \leftrightarrows A agree.

Let \xi : TS \to A' be some other system. It has a unique map to the terminal system. After composing with p: A' \leftrightarrows A, we can regard this as a map p\xi \to p\alpha . We can then compose this with the unique map from \alpha to the terminal system, obtaining a new map p(\xi ) \to p((A')^\infty ). This is the operation corresponding to \alpha .