一句话:将 Aczel-Mendler 双模拟推广到一般正则范畴与 topos,并在不依赖选择公理时证明其对复合封闭及一致性。
Aczel-Mendler 双模拟是系统间计算关系的一种余代数推广,通常假设底范畴满足选择公理以保证双模拟类对复合封闭。本文将该定义适配到一般正则范畴与 topos。作者证明:在无选择公理下双模拟对复合封闭;在更弱条件下与其他余代数表述一致;当范畴满足正则选择公理时与通常定义一致。对于 topos 情形,论证依赖幂对象,并顺带恢复其若干良好性质。最后给出 Stone 空间、名称传递 topos 与环上模等例子。
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 the axiom of choice, so that the collection of bisimulations 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) coincides with other types of coalgebraic formulations under milder conditions, 3) coincides with the usual definition when the category satisfies the regular axiom of choice. In particular, the case of toposes heavily relies on power-objects, for which we recover some favourable properties along the way. Finally, we describe several examples in Stone spaces, toposes for name-passing, and modules over a ring.