Controlled theories, categorification, and homotopification

In this paper, we introduce the notion of a controlled theory, originally developed in the author's thesis, as a structural tool for the study of higher categorical algebra. We define a notion of deformation for pros and controlled theories in a cartesian closed category. Furthermore, we show that deformations of controlled theories naturally produce Lawvere theories enriched over the same base category. We construct functorial one-dimensional categorifications and homotopifications of controlled theories, yielding Lawvere $2$-theories and Lawvere theories enriched in simplicial sets, respectively. As an application, we obtain a new model for $\infty$-groups and construct a model of coherent group-like $E_\infty$-spaces, which we will show in future work models infinite loop spaces.