Mathematical logic entered the modern era through the work of Kurt Gödel, who established his famous
Completeness and Incompleteness Theorems at the University of Vienna in the 1930`s. The Completeness Theorem
gave birth to model theory, an extremely active and important area of mathematical logic, with deep connections to
other areas of mathematics. This proposal focuses on one of the central aspects of model theory - classification
theory that is concerned with the notion of a categorical theory; roughly, a categorical theory is such that its
expressive power is enough to describe the model completely, something that was - before Gödel - presumed to
hold for many theories. We aim to find examples of (non-first-order) categorical theories describing notions
coming from homotopy theory, and hope for some applications.