On Planarity of Graphs in Homotopy Type Theory