While type theory certainly has traditionally been used for different purposes than model theory, as noted in this Philosophy SE post, I wonder to what extent type theory could model model theory itself.
My motivation for this question is based on an observation that we can view the typing relation in type theory as analagous to the "is a model of" relation in model theory. For example, one might regard the Sigma type $Magma(A) :\equiv\Sigma_{a:A} A \rightarrow A \rightarrow A$ as the theory of magmas over a type A, and components of said type models of the theory.
Now certainly, model theory has more structure to it than a simple "x is a model of y" relation between theories and models of those theories, but I think the idea of interpreting types and terms as a theory/model relation begs the question: Can we develop a richer language in type theory to deal with this types as theories, terms as models interpretation in order to interpret traditional (i.e. ZFC-based) model theory within a type theoretic framework? And, if full interpretation with classical model theory is not possible, is there still some meaningful type-based model theory that we could develop?
Denoting $\mathcal{U}$ as a type universe, one usualy one writes $\mathsf{MagmaStr} : \mathcal{U} \to \mathcal{U}$ for the magma structure over some type. As allready noted the magma structure of $A$ is just a map $A \times A \to A$ so it should be $\mathsf{MagmaStr}(A) = A \times A \to A$.
For a type theoretical definition of $\mathsf{Magma} : \mathcal{U_1}$ itself I would write $\mathsf{Magma} = \sum_{A : \mathcal{U}} A \times A \to A$ note that this type, the magmas in a the universe $\mathcal{U}$, lives in a higher universe level. Then a member of $\mathsf{Magma}$ is a pair of of a type $A$ and a binary operator on $A$ living in $\mathcal{U}$. In that way the type $\mathsf{Magma}$ can be seen as a theory and the members of this type as its models.
Ofcourse the $\mathsf{Magma}$ answer is somewhat simplistic but the above readily generalizes to for example a $\mathsf{SemiGroup} = \sum_{G : \mathcal{U}} \sum_{* : G \times G \to G} \prod_{a b c : M} (a * b) * c = a * (b * c)$. Which is a bit more involved as you can see.
It think that within this framework a lot model theory can be done, at least if the type theory is rich enough.