9.8 The structure identity principle

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

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

We start with a precategory $X$ . In our application tosingle-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)$ -structureson $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)$ -homomorphismfrom $\\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 structureif 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}}$ .