# 2.14 Example: equality of structures

We now consider one example to illustrate the interaction between the groupoid^{} structure^{} 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 equivalent^{} 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 theory^{} in such a way that equality
of categories^{} is equivalence, equality of functors^{} is natural
isomorphism, etc. See in particular §9.8 (http://planetmath.org/98thestructureidentityprinciple).
In this section^{}, we describe a very simple example, coming from algebra^{}.

For simplicity, we use *semigroups* as our example, where a
semigroup is a type equipped with an associative “multiplication^{}”
operation^{}. The same ideas apply to other algebraic structures^{}, 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 $\mathrm{\Sigma}$-type.
In the case of semigroups this yields the following.

###### Definition 2.14.1.

Given a type $A$, the type $\mathrm{SemigroupStr}$(A) of semigroup structures with carrier $A$ is defined by

$$\mathrm{\U0001d5b2\U0001d5be\U0001d5c6\U0001d5c2\U0001d5c0\U0001d5cb\U0001d5c8\U0001d5ce\U0001d5c9\U0001d5b2\U0001d5cd\U0001d5cb}(A):\equiv \sum _{(m:A\to A\to A)}\prod _{(x,y,z:A)}m(x,m(y,z))=m(m(x,y),z).$$ |

A semigroup is a type together with such a structure:

$$\mathrm{\U0001d5b2\U0001d5be\U0001d5c6\U0001d5c2\U0001d5c0\U0001d5cb\U0001d5c8\U0001d5ce\U0001d5c9}:\equiv \sum _{A:\mathcal{U}}\mathrm{\U0001d5b2\U0001d5be\U0001d5c6\U0001d5c2\U0001d5c0\U0001d5cb\U0001d5c8\U0001d5ce\U0001d5c9\U0001d5b2\U0001d5cd\U0001d5cb}(A)$$ |

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 |

\metatable |