Homotopy type theory is an extension of Martin-L\"of type theory, based
on a correspondence with homotopy theory and higher category theory.
The propositional equality type becomes proof-relevant, and acts like
paths in a space.  Higher inductive types are a new class of datatypes
which are specified by constructors not only for points but also for
paths.  In this paper, we show how patch theory in the style of the
Darcs version control system can be developed in homotopy type theory.
We reformulate patch theory using the tools of homotopy type theory, and
clearly separate formal theories of patches from their interpretation in
terms of basic revision control mechanisms.  A patch theory is presented
by a higher inductive type. Models of a patch theory are functions from
that type, which, because function are functors, automatically preserve
the structure of patches. Several standard tools of homotopy theory come
into play, demonstrating the use of these methods in a practical
programming context.