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?
NOTE: Andreas Blass has (rightly) asked why I mention elementary embedding in my question, whereas the title talks about homotopy equivalences. Point well taken: I should reformulate the question in a broader form, as: can you choose some maps in the category as weak equivalences, so that we can have a homotopy category, possibly with a good amount of homotopy limits and colimits to do some real computations?
PS: The dream behind this question is that perhaps one could think of an elementary substructure as a homotopical retract of the ambient structure , and more generally one could come up with a notion of "continuous deformation" of structures, just like in the topological category
