Peter LeFanu Lumsdaine in Homotopy Type Theory