Since there will be enough time, I will use the opportunity to start the talk with a general introduction to natural transformations and examples of applications in computer science.

The semantics of a modal formula is an operation assigning to any model (Kripke frame) A, to any valuation of atomic propositions v, and any element a in A a truth value, ie the semantics of a modal formula is an operation

Models x Valuations x Elements --> Truthvalues

We show that invariance of modal formulas under bisimulation corresponds precisely to the requirement that this operation be natural.

As an application of this observation, one obtains a new way of making precise the intuition that modal formulas are a concept dual to equations (equations as known in algebra or from the specification of data types).