Both Russell 1919 and Russell 1959 stress the importance of the notion of structure.  For instance, in Chapter VI of Russell 1919, it is noticed that two similar relations essentially have the same properties, and hence have the same “structure”.  (The notion of “similarity” of relations was introduced in Russell 1901.)  We can also use this framework to refine Russell’s discussions on the notion of structure. For instance, let Monoid be the type of pairs \(A,p\) where \(p\) is an element of \(M A\). Two such pairs \(A,p\) and \(B,q\) are isomorphic if there exists a bijection \(f\) from \(A\) to \(B\) such that \(q\) is equal to the transport of structure of \(p\) along \(f\). A consequence of the Axiom of Univalence is that two isomorphic elements of the type Monoid are equal, and hence shares the same properties. Notice that such a general transport of properties is not possible when structures are formulated in a set theoretic framework. Indeed, in a set theoretic framework, it is possible to formulate properties using the membership relations, for instance the property that the carrier set of the structure contains the natural number \(0\), property that is not preserved in general by isomorphisms. Intuitively, the set theoretical description of a structure is not abstract enough since we can talk about the way this structure is built up. This difference between set theory and type theory is yet another illustration of the characterization by J.Reynolds 1983 of a type structure as a “syntactical discipline for enforcing level of abstraction”. 