One of the most confusing aspects of the Univalence Axiom (UF) is that it seems to assert that, which mathematical students learn early in their education to be a mistake - that isomorphic objects are equal. The source of the confusion is in the failure of the earlier attempts to explain UF to emphasize the existence of two classes of equalities in the theories used to formalize it - substitutional equalities and transportational equalities. The concept of transportational equality is the adaptation to the precise requirements of a formal theory of the philosophical equality principle going back to Leibniz. The concept of the substitutional equality is the one that we all learn at school. In the original formal system used for the Univalent Foundations there was one trans- portational and one substitutional equality. In the more complex formal systems that are being studied now there can be several equalities of each class.

*This lecture takes place in the framework of the ZiF Workshop What are Criteria for a Suitable Foundation of Mathematics? Homotopy Type Theory, a new interesting alternative to set theory? . *