Unit: a type checker for dependent type theory

Abstract

We present Unit, a type checker for dependent type theory with a module system in the tradition of Automath and a uniform treatment of definitions. There is no unification, no instance search, no tactics and no unfolding heuristic, so the work of checking can be observed and compared with the informal proof. With Unit we have checked a model of univalent type theory, synthetic algebraic geometry up to Chatelet's theorem, and synthetic Stone duality with its cohomology, and results on finite free resolustions. These developments show that a small, uniform system supports substantial mathematics, and give concrete reasons to reconsider the complexity routinely accepted in proof assistants.