We discuss how the concept of equality is used by mathematicians (including Grothendieck), and what effect this has when trying to formalise mathematics. We challenge various reasonable-sounding...