  We present a novel mechanism for controlling the unfolding of definitions in
dependent type theory. Traditionally, proof assistants let users specify
whether each definition can or cannot be unfolded in the remainder of a
development; unfolding definitions is often necessary in order to reason about
them, but an excess of unfolding can result in brittle proofs and intractably
large proof goals. In our system, definitions are by default not unfolded, but
users can selectively unfold them in a local manner. We justify our mechanism
by means of elaboration to a core type theory with extension types, a
connective first introduced in the context of homotopy type theory. We prove a
normalization theorem for our core calculus and have implemented our system in
the cooltt proof assistant, providing both theoretical and practical evidence
for it.
