Let be a set equipped with a binary relation . Then a bisimulation is a binary relation such that for all and such that , the following conditions hold:
for all such that , there exists a such that and
for all such that , there exists a such that and
In category theory
In Joyal-Nielsen-Winskel (p.13) is given the following definition. For what a “path category in a category of models” is, see there.
Definition
Let be a path category in a category of models . Two objects are called to be -bisimilar if there is a span of -open maps .
The relation of -open maps and open maps is given by Proposition 11, p.32:
Proposition
If is a dense full subcategory of , then -is -open iff is an open map.