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?

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

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

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?

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?

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