Álvaro Pelayo, Michael A. Warren, homotopy type theory and Voevodsky's univalent foundations?, arXiv:1210.5658