  In this article we propose a definition of a procdh topos. We show that it
encodes procdh excision, has bounded homotopy dimension and therefore is
hypercomplete and admits a conservative family of fibre functors. We also
describe the local rings.
  As an application, we show that nonconnective $K$-theory is the procdh
sheafification of connective $K$-theory, and that the motivic cohomology
recently proposed by Elmanto and Morrow is the procdh sheafification of
Voevodsky's motivic cohomology.
