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 general regular categories and toposes. 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. In particular, the case of toposes heavily relies on power-objects for which we recover some nice properties on the way. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.

翻译：Aczel-Mendler 互模拟是系统间多种计算关系的余代数扩展。通常假设底范畴满足某种形式的选择公理，以使该理论具备理想性质（如复合封闭性）。本文将定义推广至一般正则范畴与拓扑斯中，证明该推广定义：1) 无需选择公理即可实现复合封闭性；2) 在较弱条件下与其他形式的余代数表述等价；3) 当范畴具有正则选择公理时与常规定义一致。特别地，拓扑斯情形高度依赖于幂对象，并由此恢复若干优良性质。最后，我们在 Stone 空间、名称传递拓扑斯及环上模中给出多个实例。