Elementary Equivalence =?  Homotopy Equivalence 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
 A: The dream behind this question is that perhaps one could think of an elementary substructure as a homotopical retract of the ambient structure
I have tried and failed to do something similar for models of a sufficiently nice theory, say a first order categorical theory such as ACF; here is what my thoughts were. My desired weak equivalences were: add a finite tuple to a model M and get a model Ma prime(primary) and minimal over $M\cup a$ (acyclic cofibration); represent a model $N$ as the union $\cup M_i$ of an increasing chain of elementary submodels of strictly smaller cardinality (acyclic fibration). 
The first one is an elementary equivalence between a model and its substructure, and thus fits your suggested definition. However, the second one requires one to extend your category of models and consider the category of families of models; from the categorical point of view, you formally add new limits ignoring those limits you already have in your category. 
It is then easy to define a model "pre"structure that satisfies some of the axioms of a model category; Lowenheim-Skolem theorem then means that every morphism can be decomposed as a cofibration and an acyclic fibration, and existence of prime and minimal models (that holds for sufficiently nice theories) means that every morphism decomposes as an anyclic cofibration and a fibration (axiom M2 of Quillen). But that's all: I was not able to construct a model category for an interesting theory, say non-locally modular or even ACF itself. 
We were only able to construct a model category for a trivial theory T with the empty language; then this all becomes set theory and is described in here and here
