2.14 Example: equality of structures

We now consider one example to illustrate the interaction between the groupoid structure on a type and the typeformers. In the introduction we remarked that one of theadvantages of univalence is that two isomorphic things are interchangeable,in the sense that every property or construction involving one alsoapplies to the other. Common “abuses of notation” become formallytrue. Univalence itself says that equivalent types are equal, andtherefore interchangeable, which includes e.g. the common practice of identifying isomorphic sets. Moreover, when we define othermathematical objects as sets, or even general types, equipped with structure or properties, wecan derive the correct notion of equality for them from univalence. We will illustrate thispoint with a significant example in http://planetmath.org/node/87583Chapter 9, where wedefine the basic notions of category theory in such a way that equalityof categories is equivalence, equality of functors is naturalisomorphism, 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 asemigroup is a type equipped with an associative “multiplication”operation. The same ideas apply to other algebraic structures, such asmonoids, 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 structureswith carrier $A$ is defined by

$$\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}(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 semigroupis a type together with such a structure:

$$\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉}:\equiv \sum _{A:𝒰}\mathrm{𝖲𝖾𝗆𝗂𝗀𝗋𝗈𝗎𝗉𝖲𝗍𝗋}(A)$$

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