One of the most interesting novelties in recent foundational studies is Voevodsky's Homotopical Type Theory project (see [here][1]). 

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][2], 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


  [1]: http://homotopytypetheory.org/
  [2]: http://en.wikipedia.org/wiki/Weak_equivalence_(homotopy_theory)