Definition Pseudolinear map [efr-L5QG]

Let \mathbb {C} be a 2-category, and let (M,C,\cdot ), (N,D,\star ) be internal pseudomonoid actions. A pseudolinear map (or just linear) is a pair of maps F_m: M \to N, F_c: C \to D, equipped with a pseudomonoid pseudohomomorphism structure \phi , \tau on F_m and a natural isomorphism l: F_m(-) \cdot F_c(=) \to F_c(- \cdot =) satisfying the following coherence conditions (note that writing functors using element-notation like this is well-defined)