  We define Quillen model structures on a family of presheaf toposes arising
from tree unravellings of Kripke models, leading to a homotopy theory for modal
logic. Modal preservation theorems and the Hennessy-Milner property are
revisited from a homotopical perspective.
