It is. I wonder what this will mean for Homotopy Type Theory.
One of Voevodsky's views was that all the foundation for a dependently typed formalization of maths is already there, and that it mainly needs to be organized in a better way (cf his unimath project).