Equality and sameness from Frege to Martin-Löf to Voevodsky

C. Ortiz Hill's book Word and Object in Frege, Husserl and Russell contains an interesting discussion on equality and identity in Frege and Husserl.

This question is exactly what Martin-Löf type theory and the contemporary developments in homotopy type theory and Voevodsky's univalent foundations of mathematics are all about.

Gödel once referred to Husserl as 'the true Kant'. I sometimes think of Per Martin-Löf as 'the true Frege' due to his very similar role as founder of a radical new system of mathematical logic and foundations of mathematics. In Martin-Löf type theory we have two notions of equality. One is extrinsic and corresponds to sameness and satisfies Leibniz's law. The other is internal, and corresponds to equality, sameness according to some aspect. To use a geometric analogy, one notion corresponds to two segments completely coinciding, being in fact, the 'same' segment, whilst the other corresponds to two segments having the same length (and hence having the possibility of one being moved in the plane so as to coincide with the other). To be able to have Leibniz's law for internal equality is not something that is just given, it needs to be proven for special conditions. ML type theory also allows us to work with reification in a controlled way, specially regarding how internal equality between higher types is treated.

Voevodsky's univalent foundations was conceived specifically for mathematics, thus it postulates extra axioms on top of ML type theory for the purposes of doing mathematics. These extra axioms evidently can be questioned in different contexts or as candidates for a universal logic.
Voevodsky views a certain property involving extensional equality of functions - a third kind of equality, weaker than internal equality, called equivalence - in a geometric light. He does not postulate internal (let alone extrinsic) equality for equivalent functions. Thus he is not a Fregean. Thus while internally equal functions are equivalent, equivalent functions are not necessarily internally equal. How then is mathematics possible ? Voevodsky's univalence axiom reads:

Internal equality itself is equivalent to equivalence.

So Husserl criticized Frege for conflating sameness and equality (and thus questioned the extensionality principle, Law V). Sameness is a much stronger notion than equality.

Martin-Löf and Voevodsky say: let us keep sameness outside and distinct and instead work with a strong and weak kind of equality. Let us take versions of Law V, and an analogue of that useful but fatally flawed identification of sameness and equality, and transpose them instead to strong and weak equality. In this way we can do mathematics.