 The connections between type theory, set theory and category theory gets a new light through the work on Univalent Foundations (Voevodsky 2015) and the Axiom of Univalence. This involves in an essential way the extension of type theory described in the previous section, in particular dependent types, the view of propositions as types, and the notion of universe of types. These development are also relevant for discussing the notion of structure, the importance of which was for instance emphasized in Russell 1959.