To further explore the up-to techniques for bisimulation in the coalgebra setting, we investigate a special kind of functor, i.e., product functor in this paper. Specifically, when F is the product of n sub-functors, in order to generate an up-to proof for bisimulation, it is sufficient to find n functions, where each one is consistent with its corresponding sub-functor, as well as weakly consistent with other sub-functors. The array formed by the n functions is called jointly consistent with F. We also give the analogue of jointly consistent function in traditional set theory. As for applicat...
