In what sense does Homotopy type theory "model types as spaces"

Question

I've read at multiple points (e.g. here) that homotopy type theory "models" types as spaces. I can understand informally that we can "think of" types as spaces, in a vague sense. But what is formally meant by a type theory "modelling" something?

When I was taught a course on formal logic (using first order logic and a form of natural deduction) using the book "Mathematical logic by Ebbinghaus, Flum, Thomas", there was a formal semantics of logical propositions, in terms of structures and interpretations. An "interpretation of a first-order logical formula" was formally defined as a set, with mathematical functions corresponding to the symbols classified as "function symbols", similarly for mathematical relations and constants. i.e. "interpretation" has a formal definition (which can be found in that book).

Is there similarly a formal definition of "interpretation of a type theory" written down somewhere?

Answer 1

A type theory models "something" when "something" gives an interpretation of the constructions (terms and types) of the type theory. More generally, a formal theory models "something" when the constructions of the theory can be interpreted by the "objects" of "something".

• when the focus is on the (type) theory, it is said that "something" is a model of the (type) theory. Other models are possible: you can find different interpretations of the constructions of the theory.
• when the focus is on "something", it is said that the (type) theory models "something". Other formalizations are possible: you can find different sets of rules and axioms to model "something".

At the end of the day, we could also say that a theory is a "formal model" of "something": but in practice we never say "A is a formal model of B" but "A models B", or "B is a model of A".

The interpretation is not just "something that you can think of, in a vague sense". A correct interpretation is justified by a systematic study of all possible constructions of the theory: each possible construction must have its own interpretation, functions and relations must have a consistent interpretation. When "something" is also formalized, and not just an intuition, then you should be able to build an interpretation function that converts any construction of the theory into a construction of the model.

Answer 2

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:

• Essentially algebraic theories
• Generalized algebraic theories
• Quotient inductive-inductive types
• Representable map categories

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.