9.8 The structure identity principle

The structure identity principle is an informal principle that expresses that isomorphic structures are identical. We aim to prove a general abstract result which can be applied to a wide family of notions of structure, where structures may be many-sorted or even dependently-sorted, infinitary, or even higher order.

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.

A type family $P:X_{0}\to\mathcal{U}$ . For each $x:X_{0}$ the elements of $P x$ are called $(P,H)$ -structures on $x$ .
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)$ -homomorphism from $\alpha$ to $\beta$ .
3.

For $x:X_{0}$ and $\alpha:Px$ , we have $H_{\alpha\alpha}(1_{x})$ .
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 $P x$ 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 $P x$ 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.

$f(\omega^{a}x)=\omega^{b}(f\circ x)$ if $\omega:\Omega_{0}$ , and
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.

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.

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

	$\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}},$

	$\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).$