Again here induction. We have seen it as a way of characterising a set as a least fixed point, but we could have done just as well characterised equality on that object as the least fixed point of another operator. In this case the shape of induction takes a very pleasing form, which is the following. It essentially says that equality is the least Fw congruence. The reason why I am saying that this is very interesting is because the much popular these days principle of co-induction is simply the dual of the following relation whereby you say that something is the union of all the dual of such notions which are by simulations.

---