Whitehead's principle > history in Homotopy Type Theory