This can be used to give a formulation of the notion of transport of structures (Bourbaki 1957) along equivalences. For instance, let \(M A\) be the type of monoid structures on the set \(A\): this is the type of tuples \(m, e, p\) where \(m\) is a binary operation on \(A\) and \(e\) an element of \(A\) and \(p\) a proof that these elements satisfy the usual monoid laws. The rule of substitution of equal by equal takes the form