Type theories are algebraic theories. This means that for every type theory (there are multiple variants of type theory, with different type formers and constructions), a model of the theory is a particular collection of sets and operations, satisfying some equations. The initial (freely generated) model of a type theory is called the syntax of the type theory. Initiality entails that for any model, there is a morphism (a family of structure-preserving interpretation functions) from the syntax to the model.
The situation is exactly the same as with other algebraic structures; the difference is that models of type theories are significantly larger and more complicated gadgets than well-known algebraic structures.
For example, let's compare groups and models of a type theory.
- A group is a set together with an identity element and an associative, unital and invertible binary function.
- A model of the type theory is a category with a terminal object (objects represent typing contexts, the terminal object the empty context and morphisms parallel substitutions), together with "family" structure representing types and terms, and data for specific type formers. There are multiple equivalent ways to specify all of this, for example categories with families, comprehension categories or natural models. All of these are multi-sorted, since already in a category there are multiple sets (for objects and arrows).
- The initial group is the trivial group. There is a unique group homomorphism from the trivial group to any group. A homomorphism is a function between underlying sets which preserves all structure, e.g. it maps the identity element to the identity element.
- The initial model of the type theory is the syntax. There is a unique model morphism from the syntax to any model, which consists of interpretation functions, mapping syntactic contexts to contexts in the model, syntactic types to types in the model and so on, and these functions preserve all structure. For example, the interpretation function maps the syntactic empty context to the semantic empty context, and syntactic type/term formers to corresponding semantic type/term formers.
There are different formal classes of algebraic theories, based on how flexible/general the specification is. For example, we may talk about single-sorted or multi-sorted algebraic structures. Type theories require a fairly general notion of algebraic signatures to describe. There are again multiple ways to specify such signatures. All of the following systems are sufficient to specify type theories:
I remark that the notion of model that falls out from specifying theories in the algebraic fashion, is much more general than the conventional notion of model in the study of first-order logical theories. In logic, only the extra-logical structure can vary over models (interpretations of sorts, operations and axioms), the interpretation of logical structure (variables, quantifiers, logical connectives, sometimes the equality symbol as well) is fixed. In contrast, the algebraic specification allows every syntactic construction to be interpreted differently in different models.
It is possible to use algebraic model theory for first-order logic as well. Hyperdoctrines are one way to do this. It's also possible to specify the algebraic syntax of first-order logic in a more direct type-theoretic flavor, by reusing formal notions of binding, variables and substitutions to specify logical syntax, and adding connectives and quantifiers as certain proposition formers.
In what sense does Homotopy type theory “model types as spaces”?
To model types as spaces, we have to define a model of HoTT, such that closed types in the model are mathematical structures which can be viewed as spaces. There's again some wiggle room here, because there are multiple notions of spaces in mathematics.
For example, cubical sets is one way to define spaces. In the cubical set model of HoTT, we define a particular model, such that typing contexts and closed types are cubical sets, parallel substitutions are natural transformations, types are a certain kind of "dependent" cubical sets, and every type and term former has an interpretation, satisfying $\beta\eta$ equations.