  In this paper, we present a constructive and proof-relevant development of
graph theory, including the notion of maps, their faces, and maps of graphs
embedded in the sphere, in homotopy type theory. This allows us to provide an
elementary characterisation of planarity for locally directed finite and
connected multigraphs that takes inspiration from topological graph theory,
particularly from combinatorial embeddings of graphs into surfaces. A graph is
planar if it has a map and an outer face with which any walk in the embedded
graph is walk-homotopic to another. A result is that this type of planar maps
forms a homotopy set for a graph. As a way to construct examples of planar
graphs inductively, extensions of planar maps are introduced. We formalise the
essential parts of this work in the proof-assistant Agda with support for
homotopy type theory.
