Syllepsis in Homotopy Type Theory