Aczel-Mendler bisimulations are a coalgebraic extension of a variety of computational relations between systems. It is usual to assume that the underlying category satisfies some form of axiom of choice, so that the theory enjoys desirable properties, such as closure under composition. In this paper, we accommodate the definition in a general regular category -- which does not necessarily satisfy any form of axiom of choice. We show that this general definition 1) is closed under composition without using the axiom of choice, 2) coincide with other types of coalgebraic formulations under milder conditions, 3) coincide with the usual definition when the category has the regular axiom of choice. We then develop the particular case of toposes, where the formulation becomes nicer thanks to the power-object monad, and extend the formalism to simulations. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.

翻译：Aczel-Mendler互模拟是系统间多种计算关系的余代数扩展。通常假设底范畴满足某种形式的选择公理，以使该理论具备理想性质（如复合封闭性）。本文将该定义推广至一般正则范畴（其无需满足任何形式的选择公理）。我们证明该推广定义：1) 在不依赖选择公理下保持复合封闭性；2) 在较温和条件下与其他余代数公式等价；3) 当范畴具有正则选择公理时与通常定义一致。随后我们发展至拓扑斯这一特例，借助幂对象单子使公式表述更简洁，并将形式体系扩展至模拟。最后在Stone空间、名称传递拓扑斯及环上模中给出若干实例。