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 $\Sigma$ -type. In the case of semigroups this yields the following.

Definition 2.14.1.

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

$\mathsf{SemigroupStr}(A):\!\!\equiv\mathchoice{\sum_{(m:A\to A\to A)}\,}{% \mathchoice{{\textstyle\sum_{(m:A\to A\to A)}}}{\sum_{(m:A\to A\to A)}}{\sum_{% (m:A\to A\to A)}}{\sum_{(m:A\to A\to A)}}}{\mathchoice{{\textstyle\sum_{(m:A% \to A\to A)}}}{\sum_{(m:A\to A\to A)}}{\sum_{(m:A\to A\to A)}}{\sum_{(m:A\to A% \to A)}}}{\mathchoice{{\textstyle\sum_{(m:A\to A\to A)}}}{\sum_{(m:A\to A\to A% )}}{\sum_{(m:A\to A\to A)}}{\sum_{(m:A\to A\to A)}}}\mathchoice{\prod_{(x,y,z:% A)}\,}{\mathchoice{{\textstyle\prod_{(x,y,z:A)}}}{\prod_{(x,y,z:A)}}{\prod_{(x% ,y,z:A)}}{\prod_{(x,y,z:A)}}}{\mathchoice{{\textstyle\prod_{(x,y,z:A)}}}{\prod% _{(x,y,z:A)}}{\prod_{(x,y,z:A)}}{\prod_{(x,y,z:A)}}}{\mathchoice{{\textstyle% \prod_{(x,y,z:A)}}}{\prod_{(x,y,z:A)}}{\prod_{(x,y,z: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:

$\mathsf{Semigroup}:\!\!\equiv\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{% \textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U% })}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{% \sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{% \mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{% (A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}\mathsf{SemigroupStr}(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