Not the op, but basically Voevodsky realized that the notion of equality in type theories as implemented in Coq or Agda is fundamentally more fine grained than

Not the op, but basically Voevodsky realized that the notion of equality in type theories as implemented in Coq or Agda is fundamentally more fine grained than what mathematicians are used to thinking of. This mismatch causes problems when formalizing mathematics in type theory. Voevodsky proposed the univalence axiom which can be used to obtain more equalities and gave rise to the field of homotopy type theory (HoTT). An intuition about the univalence axiom is that it allows to regard isomorphic types as equal. (This isn't entirely correct but gives a good intuition). The consequences of the axiom are severe (probably in a good way) but a lot more research is needed. The hopes are that the work on HoTT will make it easier to formalize mathematics and in turn make it easier to verify software.