9.8 The structure identity principle

The structureMathworldPlanetmath identityPlanetmathPlanetmathPlanetmathPlanetmath principle is an informal principle that expresses that isomorphicPlanetmathPlanetmathPlanetmath 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)→(A≃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 𝒰-small sets, where 𝒰 is a univalent type universePlanetmathPlanetmath.

Definition 9.8.1.

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

  1. 1.

    A type family P:X0→𝒰. For each x:X0 the elements of P⁢x are called (P,H)-structures on x.

  2. 2.

    For x,y:X0 and α:P⁢x, β:P⁢y, to each f:homX⁡(x,y) a mere proposition


    If Hα⁢β⁢(f) is true, we say that f is a (P,H)-homomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath from α to β.

  3. 3.

    For x:X0 and α:P⁢x, we have Hα⁢α⁢(1x).

  4. 4.

    For x,y,z:X0 and α:P⁢x, β:P⁢y, γ:P⁢z, if f:homX⁡(x,y), we have


When (P,H) is a notion of structure, for α,β:P⁢x we define


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=𝖲𝗍𝗋(P,H)⁢(X).

  • •

    The type of objects of A is the type A0:≡∑(x:X)Px. If a≡(x,α):A0, we may write |a|:≡x.

  • •

    For (x,α):A0 and (y,β):A0, we define


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 Str(P,H)⁢(X) is a category.


By the definition of equality in dependent pair types, to give an equality (x,α)=(y,β) consists of

  • •

    An equality p:x=y, and

  • •

    An equality p*(α)=β.

Since P is set-valued, the latter is a mere proposition. On the other hand, it is easy to see that an isomorphism (x,α)≅(y,β) in 𝖲𝗍𝗋(P,H)⁢(X) consists of

  • •

    An isomorphism f:x≅y in X, such that

  • •

    Hα⁢β⁢(f) and Hβ⁢α⁢(f-1).

Of course, the second of these is also a mere proposition. And since X is a category, the function (x=y)→(x≅y) is an equivalence. Thus, it will suffice to show that for any p:x=y and for any (α:P⁢x), (β:P⁢y), we have p*(α)=β if and only if both Hα⁢β⁢(𝗂𝖽𝗍𝗈𝗂𝗌𝗈⁢(p)) and Hβ⁢α⁢(𝗂𝖽𝗍𝗈𝗂𝗌𝗈⁢(p)-1).

The “only if” direction is just the existence of the function 𝗂𝖽𝗍𝗈𝗂𝗌𝗈 for the category 𝖲𝗍𝗋(P,H)⁢(X). For the “if” direction, by inductionMathworldPlanetmath on p we may assume that y≡x and p≡𝗋𝖾𝖿𝗅x. However, in this case 𝗂𝖽𝗍𝗈𝗂𝗌𝗈⁢(p)≡1x and therefore 𝗂𝖽𝗍𝗈𝗂𝗌𝗈⁢(p)-1=1x. Thus, α≤xβ and β≤xα, which implies α=β 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 BA0 whose objects are functions A0→B0, and whose set of morphisms from F0:A0→B0 to G0:A0→B0 is ∏(a:A0)homB⁡(F0⁢a,G0⁢a). Composition and identities are inherited directly from those in B. It is easy to show that γ:homBA0⁡(F0,G0) is an isomorphism exactly when each componentMathworldPlanetmathPlanetmath γa is an isomorphism, so that we have (F0≅G0)≃∏(a:A0)(F0a≅G0a). Moreover, the map idtoiso:(F0=G0)→(F0≅G0) of BA0 is equal to the composite


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, BA0 is a category.

Now we define a notion of structure on BA0 for which P⁢(F0) is the type of operationsMathworldPlanetmath F:∏(a,a′:A0)homA⁡(a,a′)→homB⁡(F0⁢a,F0⁢a′) which extend F0 to a functorMathworldPlanetmath (i.e. preserve composition and identities). This is a set since each homB⁡(–,–) is so. Given such F and G, we define γ:homBA0⁡(F0,G0) 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′ are both structures on F0 and the identity is a natural transformation from F to F′, then for any f:homA⁡(a,a′) we have F′⁢f=F′⁢f∘1F0⁢a=1F0⁢a∘F⁢f=F⁢f. Applying function extensionality, we conclude F=F′. Thus, we have a standard notion of structure, and so by \autorefthm:sip, the precategory BA is a category.

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

  1. 1.

    f⁢(ωa⁢x)=ωb⁢(f∘x) if ω:Ω0, and

  2. 2.

    ωa⁢x→ωb⁢(f∘x) if ω:Ω1.

Note that each x:|a||ω| is a function x:|ω|→|a| so that f∘x:bω.

Now we assume given a (univalent) universe 𝒰 and a 𝒰-small signature Ω; i.e. |Ω| is a 𝒰-small set and, for each ω:|Ω|, the set |ω| is 𝒰-small. Then we have the category 𝒮⁢e⁢t𝒰 of 𝒰-small sets. We want to define the precategory of 𝒰-small Ω-structures over 𝒮⁢e⁢t𝒰 and use \autorefthm:sip to show that it is a category.

We use the first order signature Ω to give us a standard notion of structure (P,H) over 𝒮⁢e⁢t𝒰.

Definition 9.8.4.

  1. 1.

    For each 𝒰-small set x define



    P0⁢x :≡∏ω:Ω0x|ω|→x, and
    P1⁢x :≡∏ω:Ω1x|ω|→𝖯𝗋𝗈𝗉𝒰,
  2. 2.

    For 𝒰-small sets x,y and α:Pω⁢x,β:Pω⁢y,f:x→y, define



    H0,α⁢β⁢(f) :≡∀(ω:Ω0).∀(u:x|ω|).f(αu)=β(f∘u), and
    H1,α⁢β⁢(f) :≡∀(ω:Ω1).∀(u:x|ω|).αu→β(f∘u).

It is now routine to check that (P,H) is a standard notion of structure over 𝒮⁢e⁢t𝒰 and hence we may use \autorefthm:sip to get that the precategory S⁢t⁢r(P,H)⁢(𝒮⁢e⁢t𝒰) is a category. It only remains to observe that this is essentially the same as the precategory of 𝒰-small Ω-structures over 𝒮⁢e⁢t𝒰.

Title 9.8 The structure identity principle