Of course, "women and men dancing" is just an illustrative example as far as the _theory_ is concerned: the "types" here are just opaque tags that separate otherwise-identical abstract agents into groups. In particular, types are _not_ strategies. In terms of the dancing game, the _strategies_ "lead" and "follow" can't be types: rather, the arbitrary "men" and "women" tags (which might as well be [suggestively-named Lisp tokens](https://www.readthesequences.com/Truly-Part-Of-You)) are a symmetry-breaking hack that lets us turn _many_ complementary coordination games (for _every pair_, who should lead?) into a _single_ correlative coordination game (for the whole population, are we using the "men lead" or the "women lead" convention?).
Of course, "women and men dancing" is just an illustrative example as far as the _theory_ is concerned: the "types" here are just opaque tags that separate otherwise-identical abstract agents into groups. In particular, types are _not_ strategies. In terms of the dancing game, the _strategies_ "lead" and "follow" can't be types: rather, the arbitrary "men" and "women" tags (which might as well be [suggestively-named Lisp tokens](https://www.readthesequences.com/Truly-Part-Of-You)) are a symmetry-breaking hack that lets us turn _many_ complementary coordination games (for _every pair_, who should lead?) into a _single_ correlative coordination game (for the whole population, are we using the "men lead" or the "women lead" convention?).