One of the most interesting novelties in recent foundational studies is Voevodsky's Homotopical Type Theory project (see here).
Finally homotopy theory ideas have entered in a royal fashion the foundational arena!
I wonder if other areas of logic and foundational studies can be tackled from an homotopical standpoint. For instance, in model theory, one encounters the central notion of elementary equivalence:
two structures M and N of the same signature $\sigma$ are called elementarily equivalent if they satisfy the same first-order σ-sentences.σ-sentences.
The question:
take elementary embedding as a notion of weak equivalence, what kind of structure has the associated homotopy category? Perhaps dreaming a little, can one even manage to identify a Quillen model structure on the category of $\sigma$ -structures?