Unity in nominal equational reasoning: The algebra of equality on nominal sets

There are currently no fewer than four dedicated logics for equality reasoning over nominal sets: nominal algebra, nominal equational logic, nominal equational logic with equality only, and permissive-nominal algebra.In this survey and research paper we present these logics side-by-side in a common notation, survey their similarities and differences, discuss their proof- and model-theories, and discuss in detail what the implications of those differences are for mathematical reasoning in each of them.