  This paper introduces Isabelle/HoTT, the first development of homotopy type
theory in the Isabelle proof assistant. Building on earlier work by Paulson, I
use Isabelle's existing logical framework infrastructure to implement essential
automation, such as type checking and term elaboration, that is usually handled
on the source code level of dependently typed systems. I also integrate the
propositions-as-types paradigm with the declarative Isar proof language,
providing an alternative to the tactic-based proofs of Coq and the proof terms
of Agda. The infrastructure developed is then used to formalize foundational
results from the Homotopy Type Theory book.
