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? 


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