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)(AB) 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 Px are called (P,H)-structures on x.

  2. 2.

    For x,y:X0 and α:Px, β:Py, to each f:homX(x,y) a mere proposition

    Hαβ(f).

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

  3. 3.

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

  4. 4.

    For x,y,z:X0 and α:Px, β:Py, γ:Pz, if f:homX(x,y), we have

    Hαβ(f)Hβγ(g)Hαγ(gf).

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

(αxβ):Hαβ(1x).

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=𝖲𝗍𝗋(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

    homA((x,α),(y,β)):\setoff:xy|Hαβ(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 Str(P,H)(X) is a category.

Proof.

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:xy 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)(xy) is an equivalence. Thus, it will suffice to show that for any p:x=y and for any (α:Px), (β:Py), 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 yx 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 A0B0, and whose set of morphisms from F0:A0B0 to G0:A0B0 is (a:A0)homB(F0a,G0a). 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 (F0G0)(a:A0)(F0aG0a). Moreover, the map idtoiso:(F0=G0)(F0G0) of BA0 is equal to the composite

(F0=G0)a:A0(F0a=G0a)a:A0(F0aG0a)(F0G0)

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(F0a,F0a) 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 Ff=Ff1F0a=1F0aFf=Ff. 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 ωax to each x:|a||ω|, to each relation symbol. And given Ω-structures a,b, a function f:|a||b| is a homomorphism ab if it preserves the structure; i.e. if for each symbol ω of the signature and each x:|a||ω|,

  1. 1.

    f(ωax)=ωb(fx) if ω:Ω0, and

  2. 2.

    ωaxωb(fx) if ω:Ω1.

Note that each x:|a||ω| is a function x:|ω||a| so that fx: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 𝒮et𝒰 of 𝒰-small sets. We want to define the precategory of 𝒰-small Ω-structures over 𝒮et𝒰 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 𝒮et𝒰.

Definition 9.8.4.

  1. 1.

    For each 𝒰-small set x define

    Px:P0x×P1x.

    Here

    P0x :ω:Ω0x|ω|x, and
    P1x :ω:Ω1x|ω|𝖯𝗋𝗈𝗉𝒰,
  2. 2.

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

    Hαβ(f):H0,αβ(f)H1,αβ(f).

    Here

    H0,αβ(f) :(ω:Ω0).(u:x|ω|).f(αu)=β(fu), and
    H1,αβ(f) :(ω:Ω1).(u:x|ω|).αuβ(fu).

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

Title 9.8 The structure identity principle
\metatable