The Simplicial Model of Univalent Foundations (after Voevodsky)