Floris van Doorn in Homotopy Type Theory