# 9.8 The structure identity principle

The simplest kind of single-sorted structure consists of a type with no additional structure. The univalence axiom expresses the structure identity principle for that notion of structure in a strong form: for types $A,B$, the canonical function $(A=B)\to(A\simeq B)$ is an equivalence.

We start with a precategory $X$. In our application to single-sorted first order structures, $X$ will be the category of $\mathcal{U}$-small sets, where $\mathcal{U}$ is a univalent type universe  .

###### Definition 9.8.1.

A notion of structure $(P,H)$ over $X$ consists of the following.

1. 1.

A type family $P:X_{0}\to\mathcal{U}$. For each $x:X_{0}$ the elements of $Px$ are called $(P,H)$-structures on $x$.

2. 2.

For $x,y:X_{0}$ and $\alpha:Px$, $\;\beta:Py$, to each $f:\hom_{X}(x,y)$ a mere proposition

 $H_{\alpha\beta}(f).$

If $H_{\alpha\beta}(f)$ is true, we say that $f$ is a $(P,H)$ from $\alpha$ to $\beta$.

3. 3.

For $x:X_{0}$ and $\alpha:Px$, we have $H_{\alpha\alpha}(1_{x})$.

4. 4.

For $x,y,z:X_{0}$ and $\alpha:Px$, $\;\beta:Py$, $\;\gamma:Pz$, if $f:\hom_{X}(x,y)$, we have

 $H_{\alpha\beta}(f)\to H_{\beta\gamma}(g)\to H_{\alpha\gamma}(g\circ f).$

When $(P,H)$ is a notion of structure, for $\alpha,\beta:Px$ we define

 $(\alpha\leq_{x}\beta):\!\!\equiv H_{\alpha\beta}(1_{x}).$

By 3 and 4, this is a preorder (\autorefct:orders) with $Px$ its type of objects. We say that $(P,H)$ is a standard notion of structure if this preorder is in fact a partial order, for all $x:X$.

Note that for a standard notion of structure, each type $Px$ must actually be a set. We now define, for any notion of structure $(P,H)$, a precategory of $(P,H)$-structures, $A=\mathsf{Str}_{(P,H)}(X)$.

• The type of objects of $A$ is the type $A_{0}:\!\!\equiv\mathchoice{\sum_{x:X}\,}{\mathchoice{{\textstyle\sum_{(x:X)}}% }{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X% )}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(% x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}Px$. If $a\equiv(x,\alpha):A_{0}$, we may write $|a|:\!\!\equiv x$.

• For $(x,\alpha):A_{0}$ and $(y,\beta):A_{0}$, we define

 $\hom_{A}((x,\alpha),(y,\beta)):\!\!\equiv\setof{f:x\to y|H_{\alpha\beta}(f)}.$

The composition and identities are inherited from $X$; conditions 3 and 4 ensure that these lift to $A$.

###### Theorem 9.8.2 (Structure identity principle).

If $X$ is a category and $(P,H)$ is a standard notion of structure over $X$, then the precategory $\mathsf{Str}_{(P,H)}(X)$ is a category.

###### Proof.

By the definition of equality in dependent pair types, to give an equality $(x,\alpha)=(y,\beta)$ consists of

• An equality $p:x=y$, and

• An equality ${p}_{*}\mathopen{}\left({\alpha}\right)\mathclose{}=\beta$.

Since $P$ is set-valued, the latter is a mere proposition. On the other hand, it is easy to see that an isomorphism $(x,\alpha)\cong(y,\beta)$ in $\mathsf{Str}_{(P,H)}(X)$ consists of

• An isomorphism $f:x\cong y$ in $X$, such that

• $H_{\alpha\beta}(f)$ and $H_{\beta\alpha}({f}^{-1})$.

Of course, the second of these is also a mere proposition. And since $X$ is a category, the function $(x=y)\to(x\cong y)$ is an equivalence. Thus, it will suffice to show that for any $p:x=y$ and for any $(\alpha:Px)$, $(\beta:Py)$, we have ${p}_{*}\mathopen{}\left({\alpha}\right)\mathclose{}=\beta$ if and only if both $H_{\alpha\beta}(\mathsf{idtoiso}(p))$ and $H_{\beta\alpha}({\mathsf{idtoiso}(p)}^{-1})$.

The “only if” direction is just the existence of the function $\mathsf{idtoiso}$ for the category $\mathsf{Str}_{(P,H)}(X)$. For the “if” direction, by induction  on $p$ we may assume that $y\equiv x$ and $p\equiv\mathsf{refl}_{x}$. However, in this case $\mathsf{idtoiso}(p)\equiv 1_{x}$ and therefore ${\mathsf{idtoiso}(p)}^{-1}=1_{x}$. Thus, $\alpha\leq_{x}\beta$ and $\beta\leq_{x}\alpha$, which implies $\alpha=\beta$ since $(P,H)$ is a standard notion of structure. ∎

As an example, this methodology gives an alternative way to express the proof of \autorefct:functor-cat.

###### Example 9.8.3.

Let $A$ be a precategory and $B$ a category. There is a precategory $B^{A_{0}}$ whose objects are functions $A_{0}\to B_{0}$, and whose set of morphisms from $F_{0}:A_{0}\to B_{0}$ to $G_{0}:A_{0}\to B_{0}$ is $\mathchoice{\prod_{a:A_{0}}\,}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{% \prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}{\mathchoice{{% \textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:% A_{0})}}}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_% {(a:A_{0})}}{\prod_{(a:A_{0})}}}\hom_{B}(F_{0}a,G_{0}a)$. Composition and identities are inherited directly from those in $B$. It is easy to show that $\gamma:\hom_{B^{A_{0}}}(F_{0},G_{0})$ is an isomorphism exactly when each component   $\gamma_{a}$ is an isomorphism, so that we have $(F_{0}\cong G_{0})\simeq\mathchoice{\prod_{a:A_{0}}\,}{\mathchoice{{\textstyle% \prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}{% \mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})% }}{\prod_{(a:A_{0})}}}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_% {0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}(F_{0}a\cong G_{0}a)$. Moreover, the map $\mathsf{idtoiso}:(F_{0}=G_{0})\to(F_{0}\cong G_{0})$ of $B^{A_{0}}$ is equal to the composite

 $(F_{0}=G_{0})\longrightarrow\mathchoice{\prod_{a:A_{0}}\,}{\mathchoice{{% \textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:% A_{0})}}}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_% {(a:A_{0})}}{\prod_{(a:A_{0})}}}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{% \prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}(F_{0}a=G_{0}a)% \longrightarrow\mathchoice{\prod_{a:A_{0}}\,}{\mathchoice{{\textstyle\prod_{(a% :A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}{% \mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})% }}{\prod_{(a:A_{0})}}}{\mathchoice{{\textstyle\prod_{(a:A_{0})}}}{\prod_{(a:A_% {0})}}{\prod_{(a:A_{0})}}{\prod_{(a:A_{0})}}}(F_{0}a\cong G_{0}a)% \longrightarrow(F_{0}\cong G_{0})$

in which the first map is an equivalence by function extensionality, the second because it is a dependent product of equivalences (since $B$ is a category), and the third as remarked above. Thus, $B^{A_{0}}$ is a category.

Now we define a notion of structure on $B^{A_{0}}$ for which $P(F_{0})$ is the type of operations  $F:\mathchoice{\prod_{a,a^{\prime}:A_{0}}\,}{\mathchoice{{\textstyle\prod_{(a,a% ^{\prime}:A_{0})}}}{\prod_{(a,a^{\prime}:A_{0})}}{\prod_{(a,a^{\prime}:A_{0})}% }{\prod_{(a,a^{\prime}:A_{0})}}}{\mathchoice{{\textstyle\prod_{(a,a^{\prime}:A% _{0})}}}{\prod_{(a,a^{\prime}:A_{0})}}{\prod_{(a,a^{\prime}:A_{0})}}{\prod_{(a% ,a^{\prime}:A_{0})}}}{\mathchoice{{\textstyle\prod_{(a,a^{\prime}:A_{0})}}}{% \prod_{(a,a^{\prime}:A_{0})}}{\prod_{(a,a^{\prime}:A_{0})}}{\prod_{(a,a^{% \prime}:A_{0})}}}\hom_{A}(a,a^{\prime})\to\hom_{B}(F_{0}a,F_{0}a^{\prime})$ which extend $F_{0}$ to a functor  (i.e. preserve composition and identities). This is a set since each $\hom_{B}(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt})$ is so. Given such $F$ and $G$, we define $\gamma:\hom_{B^{A_{0}}}(F_{0},G_{0})$ to be a homomorphism if it forms a natural transformation. In \autorefct:functor-precat we essentially verified that this is a notion of structure. Moreover, if $F$ and $F^{\prime}$ are both structures on $F_{0}$ and the identity is a natural transformation from $F$ to $F^{\prime}$, then for any $f:\hom_{A}(a,a^{\prime})$ we have $F^{\prime}f=F^{\prime}f\circ 1_{F_{0}a}=1_{F_{0}a}\circ Ff=Ff$. Applying function extensionality, we conclude $F=F^{\prime}$. Thus, we have a standard notion of structure, and so by \autorefthm:sip, the precategory $B^{A}$ is a category.

As another example, we consider categories of structures for a first-order signature    . We define a first-order signature, $\Omega$, to consist of sets $\Omega_{0}$ and $\Omega_{1}$ of function symbols, $\omega:\Omega_{0}$, and relation symbols, $\omega:\Omega_{1}$, each having an arity $|\omega|$ that is a set. An $\Omega$-structure $a$ consists of a set $|a|$ together with an assignment of an $|\omega|$-ary function $\omega^{a}:|a|^{|\omega|}\to|a|$ on $|a|$ to each function symbol, $\omega$, and an assignment of an $|\omega|$-ary relation    $\omega^{a}$ on $|a|$, assigning a mere proposition $\omega^{a}x$ to each $x:|a|^{|\omega|}$, to each relation symbol. And given $\Omega$-structures $a,b$, a function $f:|a|\to|b|$ is a homomorphism $a\to b$ if it preserves the structure; i.e. if for each symbol $\omega$ of the signature and each $x:|a|^{|\omega|}$,

1. 1.

$f(\omega^{a}x)=\omega^{b}(f\circ x)$ if $\omega:\Omega_{0}$, and

2. 2.

$\omega^{a}x\to\omega^{b}(f\circ x)$ if $\omega:\Omega_{1}$.

Note that each $x:|a|^{|\omega|}$ is a function $x:|\omega|\to|a|$ so that $f\circ x:b^{\omega}$.

Now we assume given a (univalent) universe $\mathcal{U}$ and a $\mathcal{U}$-small signature $\Omega$; i.e. $|\Omega|$ is a $\mathcal{U}$-small set and, for each $\omega:|\Omega|$, the set $|\omega|$ is $\mathcal{U}$-small. Then we have the category $\mathcal{S}et_{\mathcal{U}}$ of $\mathcal{U}$-small sets. We want to define the precategory of $\mathcal{U}$-small $\Omega$-structures over $\mathcal{S}et_{\mathcal{U}}$ and use \autorefthm:sip to show that it is a category.

We use the first order signature $\Omega$ to give us a standard notion of structure $(P,H)$ over $\mathcal{S}et_{\mathcal{U}}$.

###### Definition 9.8.4.

1. 1.

For each $\mathcal{U}$-small set $x$ define

 $Px:\!\!\equiv P_{0}x\times P_{1}x.$

Here

 $\displaystyle P_{0}x$ $\displaystyle:\!\!\equiv\mathchoice{\prod_{\omega:\Omega_{0}}\,}{\mathchoice{{% \textstyle\prod_{(\omega:\Omega_{0})}}}{\prod_{(\omega:\Omega_{0})}}{\prod_{(% \omega:\Omega_{0})}}{\prod_{(\omega:\Omega_{0})}}}{\mathchoice{{\textstyle% \prod_{(\omega:\Omega_{0})}}}{\prod_{(\omega:\Omega_{0})}}{\prod_{(\omega:% \Omega_{0})}}{\prod_{(\omega:\Omega_{0})}}}{\mathchoice{{\textstyle\prod_{(% \omega:\Omega_{0})}}}{\prod_{(\omega:\Omega_{0})}}{\prod_{(\omega:\Omega_{0})}% }{\prod_{(\omega:\Omega_{0})}}}x^{|\omega|}\to x,\mbox{ and }$ $\displaystyle P_{1}x$ $\displaystyle:\!\!\equiv\mathchoice{\prod_{\omega:\Omega_{1}}\,}{\mathchoice{{% \textstyle\prod_{(\omega:\Omega_{1})}}}{\prod_{(\omega:\Omega_{1})}}{\prod_{(% \omega:\Omega_{1})}}{\prod_{(\omega:\Omega_{1})}}}{\mathchoice{{\textstyle% \prod_{(\omega:\Omega_{1})}}}{\prod_{(\omega:\Omega_{1})}}{\prod_{(\omega:% \Omega_{1})}}{\prod_{(\omega:\Omega_{1})}}}{\mathchoice{{\textstyle\prod_{(% \omega:\Omega_{1})}}}{\prod_{(\omega:\Omega_{1})}}{\prod_{(\omega:\Omega_{1})}% }{\prod_{(\omega:\Omega_{1})}}}x^{|\omega|}\to\mathsf{Prop}_{\mathcal{U}},$
2. 2.

For $\mathcal{U}$-small sets $x,y$ and $\alpha:P^{\omega}x,\;\beta:P^{\omega}y,\;f:x\to y$, define

 $H_{\alpha\beta}(f):\!\!\equiv H_{0,\alpha\beta}(f)\wedge H_{1,\alpha\beta}(f).$

Here

 $\displaystyle H_{0,\alpha\beta}(f)$ $\displaystyle:\!\!\equiv\forall(\omega:\Omega_{0}).\,\forall(u:x^{|\omega|}).% \,f(\alpha u)=\;\beta(f\circ u),\mbox{ and }$ $\displaystyle H_{1,\alpha\beta}(f)$ $\displaystyle:\!\!\equiv\forall(\omega:\Omega_{1}).\,\forall(u:x^{|\omega|}).% \,\alpha u\to\beta(f\circ u).$

It is now routine to check that $(P,H)$ is a standard notion of structure over $\mathcal{S}et_{\mathcal{U}}$ and hence we may use \autorefthm:sip to get that the precategory $Str_{(P,H)}(\mathcal{S}et_{\mathcal{U}})$ is a category. It only remains to observe that this is essentially the same as the precategory of $\mathcal{U}$-small $\Omega$-structures over $\mathcal{S}et_{\mathcal{U}}$.

 Title 9.8 The structure identity principle \metatable