Voevodsky and type theory