2.14 Example: equality of structures

We now consider one example to illustrate the interaction between the groupoidPlanetmathPlanetmath structureMathworldPlanetmath on a type and the type formers. In the introduction we remarked that one of the advantages of univalence is that two isomorphic things are interchangeable, in the sense that every property or construction involving one also applies to the other. Common “abuses of notation” become formally true. Univalence itself says that equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath types are equal, and therefore interchangeable, which includes e.g. the common practice of identifying isomorphic sets. Moreover, when we define other mathematical objects as sets, or even general types, equipped with structure or properties, we can derive the correct notion of equality for them from univalence. We will illustrate this point with a significant example in http://planetmath.org/node/87583Chapter 9, where we define the basic notions of category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath in such a way that equality of categoriesMathworldPlanetmath is equivalence, equality of functorsMathworldPlanetmath is natural isomorphism, etc. See in particular §9.8 (http://planetmath.org/98thestructureidentityprinciple). In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, we describe a very simple example, coming from algebraMathworldPlanetmathPlanetmath.

For simplicity, we use semigroups as our example, where a semigroup is a type equipped with an associative “multiplicationPlanetmathPlanetmathoperationMathworldPlanetmath. The same ideas apply to other algebraic structuresPlanetmathPlanetmath, such as monoids, groups, and rings. Recall from §1.6 (http://planetmath.org/16dependentpairtypes),§1.11 (http://planetmath.org/111propositionsastypes) that the definition of a kind of mathematical structure should be interpreted as defining the type of such structures as a certain iterated Σ-type. In the case of semigroups this yields the following.

Definition 2.14.1.

Given a type A, the type SemigroupStr(A) of semigroup structures with carrier A is defined by


A semigroup is a type together with such a structure:


In the next two sections, we describe two ways in which univalence makes it easier to work with such semigroups.

Title 2.14 Example: equality of structures