FIRST-ORDER HOMOTOPICAL LOGIC

Abstract

We introduce a homotopy-theoretic interpretation of intuitionistic first-order logic based on ideas from Homotopy Type Theory. We provide a categorical formulation of this interpretation using the framework of Grothendieck fibrations. We then use this formulation to prove the central property of this interpretation, namely homotopy invariance. To do this, we use the result from [8] that any Grothendieck fibration of the kind being considered can automatically be upgraded to a two-dimensional fibration, after which the invariance property is reduced to an abstract theorem concerning pseudonatural transformations of morphisms into two-dimensional fibrations.

1 Overview

The goal of this paper is to introduce a “homotopy-invariant” interpretation of first-order logic with equality, to give a description of this interpretation within the framework of categorical logic, and to give an abstract formulation and proof of the homotopy-invariance property within this framework.

The interpretation can be concisely described by the following commutative diagram.

(1.1)

On the bottom left we have intuitionistic first-order logic, on the top left we have Martin-Löf type theory, and the vertical arrow is the interpretation of IFOL into MLTT which was described in Martin-Löf’s original paper [23]. The long horizontal arrow is the homotopy-theoretic interpretation of type theory [1, 13, 32] which initiated the subject of Homotopy Type Theory (HoTT). Hence, composing these two interpretations, one obtains a homotopy-theoretic interpretation of first-order logic, which is the purpose of this paper to elaborate.

In fact, one does not need to go through these two interpretations, as the homotopical semantics for first-order logic can be described directly and very simply—it is essentially as simple as the ordinary (Tarskian) semantics for first-order logic. Hence, this interpretation gives us a simpler—but already interesting—context in which to consider the ideas involved in HoTT. A second motivation to study this interpretation is the inherent interest in first-order logic, and in particular in semantics for intuitionistic first-order logic.

Our main result is the following fundamental “homotopy invariance” theorem saying, essentially, that homotopy-equivalent structures have the same (first-order) homotopical properties. (See Sections 2.3 and 2.4 for the relevant notation and terminology.)

Theorem 1.1. Let $M,N\colon \sigma \to {\mathbf {Kan}}$ be two interpretations of an algebraic signature $\sigma $ in ${\mathbf {Kan}}$ . Let $({\varphi },\vec {x})$ be a formula-in-context over $\sigma $ , and let $\widehat M_{\vec {x}}({\varphi })\in {\mathbf {Kan}}/M(\vec {x})$ and $\widehat N_{\vec {x}}({\varphi })\in {\mathbf {Kan}}/N(\vec {x})$ be homotopical interpretations of $({\varphi },\vec {x})$ .

Then for any homotopy equivalence $\alpha \colon M\to N$ , there exists a homotopy equivalence

$$\begin{align*}\widehat M_{\vec{x}}({\varphi})\to\widehat N_{\vec{x}}({\varphi}) \end{align*}$$

lying over $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}\colon M(\vec {x})\to N(\vec {x})$ . In particular, if ${\varphi }$ is a closed formula (i.e., $\vec {x}=\emptyset $ ), then $M\vDash {\varphi }$ if and only if $N\vDash {\varphi }$ .

To prove this theorem, we first provide an “algebraic” or “functorial” version of the homotopical semantics, in the usual style of categorical logic. The above invariance theorem (which we call the “special” or “syntactic” invariance theorem) is then deduced from the following purely categorical “abstract” invariance theorem. (See Sections 3.1 and 3.2 for the relevant terminology.)

Theorem 1.2. Let be a free $h^=$ -fibration, let be a 1-discrete 2-fibration which is also an $h^=$ -fibration, and let be morphisms of $h^=$ -fibrations. Then for any pseudonatural equivalence $\alpha \colon {\varphi }\to \psi $ , there exists a pseudonatural equivalence $\Phi \to \Psi $ lying over $\alpha $ .

There is also a “second part” to the abstract invariance theorem, Theorem 3.21, which we discuss in the introduction to Section 3.

We now give some general background on homotopical and categorical semantics, in order to elucidate the significance of the above theorems.

1.1 Homotopical structures

We do not have the space here to explain the somewhat complicated and many-faceted history behind HoTT, and must assume the reader already has some familiarity with it. We will say only this much about it: the central concept of interest is that of homotopy type which roughly means “topological space up to homotopy equivalence” (though, importantly, there are other equivalent “models” for the notion of homotopy type), and the main idea is that it is homotopy types, and not sets, that are the fundamental building blocks in mathematics, with sets arising as special cases (namely the “discrete” homotopy types). Moreover, the notion of “two elements of a set being equal” is to be replaced by “two points in a space being joined by a path” (note, for instance, that in the case of discrete spaces—i.e., sets—these two notions coincide).

The fundamental role of sets in mathematics is as carriers for structures. We will be in particular concentrating on the algebraic structures, such as groups and rings. Hence, if homotopy types are to take the role of sets, there should be a notion of structures on homotopy types.

In fact, putting it this way distorts the history, as the appearance of such “homotopical structures” was one of the first developments in the history leading up to HoTT, and was, for example, studied in depth in the text [4] titled “Homotopy Invariant Algebraic Structures on Topological Spaces.” Here, the emphasis is on homotopy-invariance, meaning roughly that if some topological space X carries such a structure, so should any homotopy equivalent space Y.

For example, if one considers the structure of a (continuous) associative binary operation on X (i.e., the structure of a semigroup), we find that this indeed induces a binary operation on Y, but it is no longer associative. Rather, it is homotopy-associative, in the sense that the two resulting maps $Y\times Y\times Y\to Y$ are not equal, but homotopic. In particular, for each $x,y,z\in Y$ , we find that the elements $(x\cdot y)\cdot z$ and $ x\cdot (y\cdot z)\in Y$ are not equal but rather joined by a path; this is the first instance of “joined by a path” replacing “equal.” Such a homotopy-associative binary operation is the first instance of a homotopy-invariant algebraic structure.

Before proceeding, we would like to point out as soon as possible that the main homotopy-invariant algebraic structures of interest in topology are the so-called “higher structures”—for example “ $A_{\infty }$ ” and “ $E_{\infty }$ ” structures. These result from, for example, not just demanding that the two maps $X\times X\times X\to X$ are homotopic, but specifying such a homotopy as part of the structure, and then demanding that certain induced homotopies between maps $X\times X\times X\times X\to X$ are homotopic (and then specifying such a homotopy as part of the structure, and so on). HoTT is able (to some extent) to deal with such higher structures, whereas the First-Order Homotopical Logic considered here cannot, which is a serious limitation.

Returning to our discussion of homotopical structures, we next note that, in the subject of model theory, the way that structures satisfying certain properties are studied is via a suitable language. For example, given a set X with a binary operation “ $\cdot $ ,” demanding that the operation be associative is tantamount to requiring that the structure $(X,\cdot )$ satisfy the sentence

$$\begin{align*}\forall x,y,z\ [(x\cdot y)\cdot z=x\cdot(y\cdot z)], \end{align*}$$

formulated in first-order logic over the algebraic signature (i.e., specification of a set of sorts and of operations with given arities—see Definition 2.17) consisting of a single sort with a single binary operation “ $\cdot $ .” Of course, once one has such a definition in place, one can consider sentences of arbitrary complexity, and structures satisfying them.

Our goal here is to establish a similar framework for homotopical structures—i.e., define what it means for a given homotopical structure to satisfy an arbitrary first-order sentence. Moreover, it should be homotopy invariant in the sense that homotopy equivalent structures satisfy the same sentences. For example, a space with a binary operation should satisfy the above sentence if and only if the operation is homotopy-associative.

As another example (both of these are worked out in the examples section (Section 4.1)), the sentence

$$\begin{align*}\exists x\forall y(x=y), \end{align*}$$

over the empty signature, which would normally mean “there is a single element,” should be a satisfied by a space X if and only if X is contractible.

Before proceeding to describe how the homotopical semantics are defined, let us make two general comments.

The first is that, for reasons we will discuss below, it turns out to be difficult and unnatural to define the homotopical semantics using topological spaces. Instead, we use simplicial sets (more precisely, Kan complexes)—as indicated in (1.1)—which are another of the “models of homotopy types” mentioned above (it is possible in principle to use other categories as well—see Section 2.2). The case of topological spaces is then treated via that of Kan complexes (see Section 2.5). This is somewhat disappointing given the historical importance and intuitive appeal of topological spaces; however, it can be argued that Kan complexes are a more natural setting for homotopy theory in the context of HoTT, specifically in light of the so-called “Homotopy Hypothesis” of Grothendieck (formulated in [6]—the name seems to be due to Baez [2]).

The second is the role of intuitionistic logic, about which we have not said anything yet. An important (really, the central) feature of any interpretation of first-order logic is soundness: if a structure satisfies a sentence ${\varphi }$ , it should also satisfy any sentence $\psi $ which is a logical consequence of ${\varphi }$ . Accordingly, our homotopical semantics will satisfy this property, but only—for reasons we discuss below—for intuitionistic logic, and not all of classical logic.

1.2 Propositions-as-spaces

The key to the homotopical interpretation of first-order logic (as well as the interpretation of IFOL into MLTT—i.e., the vertical arrow in (1.1)) is the idea, inspired by the “BHK (Brouwer–Heying–Kolomogorov)” interpretation of intuitionistic first-order logic (see [31, Section 3.1]), that a formula should not be interpreted just as a truth-value, but rather a set (or, here, space), to be thought of as the “set of its proofs,” so that the proposition is interpreted as true just if this set is inhabited. The various logical connectives are then each interpreted as a certain operation on sets/spaces; the homotopy-invariance of the interpretation could then be ensured by having each of these operations on spaces be homotopy invariant.

The formalization of this—with one complication, which we return to below—can be obtained as a special case of the general “fibrational” (or “hyperdoctrinal”) interpretation of first-order logic (which we assume familiarity with—see [10, 19]).

Fix an algebraic signature $\sigma $ , a category ${\mathbf {B}}$ with finite products, and an interpretation $M\colon \sigma \to B$ of $\sigma $ in ${\mathbf {B}}$ (in the usual sense of categorical logic—see Definition 2.17). Then, given any $h^=$ -fibration ¹ (see Definition 2.2) , we can consider the interpretation of first-order formulas over $\sigma $ in (see Definition 2.19).

Thus, different choices of $h^=$ -fibrations give us different semantics for intuitionistic first-order logic, and it is now just a question of finding one which will give us the homotopical semantics.

For instance, taking an appropriate fibration in which the fiber over a set X is the power set $\mathcal {P}(X)$ , we obtain the classical, set-theoretic semantics. Next, if we take the codomain fibration whose fiber over X is the slice category ${\mathbf {Set}}/X$ (i.e., the category of X-indexed families of sets), then we obtain the “propositions-as-sets” interpretation alluded to above. We note that these examples are in fact not just h-fibrations but Boolean fibrations, i.e., the corresponding interpretations are sound for classical, and not just intuitionistic, logic. ²

The last example immediately generalizes: for any category ${\mathbf {B}}$ which is locally bicartesian closed (i.e., locally cartesian closed with finite coproducts), the fibration will be an $h^=$ -fibration, resulting in a “propositions-as-objects-in- ${\mathbf {B}}$ ” interpretation (cf. [26]). For general ${\mathbf {B}}$ , this will be a genuinely intuitionistic interpretation, i.e., will not be a Boolean fibration.

Hence, it might seem that our “propositions-as-spaces” semantics should simply result by taking ${\mathbf {B}}={\mathbf {sSet}}$ , the category of simplicial sets, which is locally bicartesian closed (as opposed to the category of topological spaces—this is one reason we cannot use the latter for the homotopical semantics). This “almost” works, except that equality is interpreted the wrong way.

To explain this, let us recall, in concrete terms, how the “propositions-as-sets,” and more generally, the “propositions-as-objects-of- ${\mathbf {B}}$ ” interpretation is defined. We have the following table, with logical connectives in the first row, and operations on (families of) sets (or more generally, objects in a locally bicartesian closed category) in the second (note that negation is omitted as it is equivalent to $(-){\Rightarrow }\bot $ ):

(1.2) $$ \begin{align}\def\arraystretch{1.5} \begin{array}{c||c||c||c||c||c||c||c} \top&\bot&\vee&\wedge&{\Rightarrow}&\forall x\in{}A_i&\exists x\in{}A_i&=\\ \hline \mathbf{1}&\emptyset&+&\times&(-)^{(-)}&\prod_{x\in{}A_i}&\sum_{x\in{}A_i}&\Delta\\ \end{array} \end{align} $$

The first two items in the bottom row (one-element set and empty set) are nullary operations, and the following three (disjoint union, product, and exponential (set of functions)) are binary operations. All of these act on families “point-wise,” e.g., ${\{X_i\}}_{i\in I}\times {\{Y_i\}}_{i\in I}:={\{{X_i\times Y_i}\}}_{i\in I}$ .

The next two, the indexed product and disjoint union, take a family of sets indexed by $A_1\times \cdots \times A_n$ and return a family of sets indexed by $A_1\times \cdots \times \widehat A_{i}\times \cdots \times A_n$ (where $\widehat A_i$ indicates that the i-th entry is omitted).

We will return to the last entry shortly.

Now, given an interpretation $M\colon \sigma \to {\mathbf {Set}}$ , the propositions-as-sets semantics should assign a set $M({\varphi })$ to each sentence (i.e., closed formula) ${\varphi }$ , and more generally, to a formula ${\varphi }$ with free variables $\vec {x}={\langle {x_1,\ldots ,x_n}\rangle }$ with sorts $\vec {A}={\langle {A_1,\ldots ,A_n}\rangle }$ , it should assign a family $M({\varphi })$ of sets indexed by the product $M(\vec {A})\underset {\mathrm {def}}=M(A_1)\times \cdots \times M(A_n)$ of the interpretations $M(A_i)$ under M of the sorts $A_i$ .

This is done, of course, by recursion on the complexity of ${\varphi }$ , and the various recursive clauses are handled according to the table (1.2). It is then straightforward to verify the desired property that the set $M({\varphi })$ is inhabited if and only if $M\vDash {\varphi }$ , i.e., the structure M satisfies ${\varphi }$ in the classical sense.

This direct description of the propositions-as-sets semantics is precisely what comes out in the case from the general notion of “interpretation in the $h^=$ -fibration .” In the case for a general locally bicartesian category ${\mathbf {B}}$ , the description is the same: we observe each of the set-theoretic operations in (1.2) is governed by a certain universal property in ${\mathbf {Set}}$ , and we take the corresponding operation in the category ${\mathbf {B}}$ (which exist by locally bicartesian closedness). In this case, “family of sets indexed by $M(\vec A)$ ” becomes “object in the slice category $B/M(\vec A)$ .”

In the general case, the reason that this interpretation is sound for intuitionistic logic is that under the Lambek–Lawvere axiomatization of intuitionistic logic (see Appendix A.2), the logical axioms governing each connective correspond precisely to the universal property defining the operations (1.2) in a locally bicartesian closed category—and more generally in an $h^=$ -fibration.

We have yet to discuss the interpretation, both for ${\mathbf {Set}}$ and for general ${\mathbf {B}}$ , of atomic formulas—where in this paper, we consider only algebraic signatures (meaning those containing no primitive relations), so that the only atomic formulas are equalities. This brings us to the last column in the table (1.2).

In the case of propositions-as-sets, we interpret equality in the obvious way: given two terms s and t of sort A which have been interpreted as some elements $M(s)$ and $M(t)$ of the set $M(A)$ , we define $M(s=t):={\{{x\in \mathbf {1}\mid M(s)=M(t)}\}}$ , i.e., (assuming classical logic):

$$\begin{align*}M(s=t)= \begin{cases} \mathbf{1},&\text{if }s=t,\\ \emptyset,&\text{otherwise}. \end{cases} \end{align*}$$

The categorical description of this is as follows. If s and t (still assumed to be of sort A) have free variables $\vec {x}$ of sorts $\vec {A}$ , then $M(s)$ and $M(t)$ are morphisms $M(\vec {A})\to M(A)\times M(A)$ , and $M(s=t)$ is the object in ${\mathbf {B}}/M(\vec {A})$ given by the pullback

of the diagonal morphism $\Delta \colon M(A)\to M(A)\times M(A)$ (hence the “ $\Delta $ ” in the table (1.2)).

In particular, this is how equality is interpreted in the $h^=$ -fibration , and amounts to strict equality of elements of a simplicial set.

However, for the homotopical semantics, this is not how we want to interpret equality! Indeed, the whole point of the homotopical semantics is that we want to interpret equality as the space of paths. This is why the homotopical semantics cannot literally be given by the $h^=$ -fibration .

In order to achieve the desired notion of equality, we need to replace the diagonal morphism with the morphism $M(A)^I\to M(A)\times M(A)$ , where I is the “simplicial interval,” making $M(A)^I$ the space of paths in $M(A)$ , and where the displayed morphism takes each path to its two endpoints (it is given by the two morphisms $M(A)^I\to M(A)^{\mathrm {pt}}\cong M(A)$ induced by the endpoint inclusions $\mathrm {pt}\to I$ ).

Thus, the definition of the homotopical semantics (stated in Section 2.3) is: given an interpretation $M\colon \sigma \to {\mathbf {Kan}}$ , ³ we interpret formulas as in the fibration —i.e., according to the rules in (1.2)—except that we interpret equality using the path-space instead of the diagonal.

A priori, this is no longer an instance of the general notion of “interpretation in an $h^=$ -fibration”; but in fact it is! Namely, for any model category ${\mathbf {C}}$ , there is a certain fibration obtained from —which we show in Section 2.2 is an $h^=$ -fibration for suitable model categories ${\mathbf {C}}$ such as ${\mathbf {sSet}}$ —such that the just-described homotopical semantics corresponds precisely to the interpretation in , at least up to homotopy equivalence (see Section 2.3). This fibration was studied in [8] (and had been previously introduced independently in [5]), where a certain 2-categorical structure on it (and in fact, on any “ ${\wedge \!\!=}$ -fibration”) is introduced, whose significance we will return to below in Section 1.3.

There are certain advantages to having our semantics be given by an $h^=$ -fibration—for example, as mentioned above, it automatically gives us the soundness of the interpretation with respect to intuitionistic logic.

But also, as we explain next, the fibrational formulation is what we use to prove the homotopy invariance property.

1.3 Functorial semantics and invariance

To prove the homotopy-invariance property of the homotopical semantics, we must bring in an important aspect of the fibrational semantics that we have yet to discuss, namely that the syntax of first-order logic over the signature $\sigma $ can itself be organized into an $h^=$ -fibration in such a way that the resulting interpretation in a general $h^=$ -fibration is then mediated by a morphism of $h^=$ -fibrations .

This is the notion of “functorial semantics” introduced by Lawvere [16] at the dawn of categorical logic. Of course, the origin of this idea is in the “algebraic semantics” for propositional logic using Boolean (or, in the intuitionistic case, Heyting) algebras.

The fibration (which is constructed in Appendix A) is given roughly as follows. The base category $\mathbf {Tm}_{\sigma }$ is the finite product category associated by Lawvere with (the empty theory over) $\sigma $ : the objects are “contexts”—i.e., finite sequences of sorts of $\sigma $ —and the morphisms are given by sequences of terms of $\sigma $ . The objects of $\mathbf {Pf}_{\sigma }$ are first-order formulas over $\sigma $ , and in particular, the fiber over a context $\vec {A}$ has as objects the formulas with free variables in the context $\vec {A}$ , and the morphisms ${\varphi }\to \psi $ are certain equivalence classes of intuitionistic deductions (proofs) of ${\varphi }{\Rightarrow }\psi $ . ⁴

The central feature of the structure (and more generally, of the algebraic structure constructed out of the syntax in the various flavours of algebraic/functorial semantics) is that it is free in an appropriate sense. The freeness precisely captures the desired property that each interpretation in an $h^=$ -fibration induces a unique (up to isomorphism) morphism of $h^=$ -fibrations. (In fact, for our purposes, we will only need the abstract existence of such a free $h^=$ -fibration, and not the particular description in terms of syntax given above.)

However, as is typical of categorical structures, the freeness has an additional element: given an $h^=$ -fibration and two interpretations $M_1,M_2\colon \sigma \to {\mathbf {B}}$ , any isomorphism of interpretations $M_1{\xrightarrow {{}_{\sim }}} M_2$ gives rise to an isomorphism between the induced morphisms . This immediately implies the isomorphism invariance of the interpretation in ; for instance, when , this says that for given an isomorphism $M_1{\xrightarrow {{}_{\sim }}} M_2$ of set-based structures $M_1,M_2\colon \sigma \to {\mathbf {Set}}$ (giving, in particular, a bijection $\alpha _{\vec {A}}\colon M_1(\vec {A})\to M_2(\vec {A})$ for each sequence of sorts $\vec {A}$ ), there is an induced bijection $M_1({\varphi })\to M_2({\varphi })$ lying over $\alpha _{\vec {A}}$ for each formula ${\varphi }$ with free variables $\vec {x}$ with sorts $\vec {A}$ . In particular, $M_1$ and $M_2$ satisfy the same sentences.

This is the recipe for our proof of the homotopy invariance; however, things are somewhat more subtle in the latter case. The point is that we are now interested in a homotopy equivalence of two structures $M_1,M_2\colon \sigma \to {\mathbf {Kan}}$ , which is no longer a purely category-theoretic notion, and therefore cannot be expected to induce an isomorphism (or rather, homotopy equivalence) of the corresponding morphisms as above.

On the other hand, a homotopy equivalence is naturally formulated as a 2-categorical notion with respect to a natural 2-categorical structure on ${\mathbf {Kan}}$ —namely, it is given by a “pseudonatural equivalence” of functors $\mathbf {Tm}_{\sigma }\to {\mathbf {Kan}}$ .

Now, in [8], we showed that for any $h^=$ -fibration (or more generally ${\wedge \!\!=}$ -fibration) , the base category ${\mathbf {B}}$ automatically inherits a 2-categorical structure—and in fact, the whole fibration becomes a “1-discrete 2-fibration”—in such a way that this recovers the usual 2-categorical structure on ${\mathbf {Kan}}$ (or more generally the category of cofibrant–fibrant objects in any model category).

With this preparation, we are able to formulate and prove the homotopy-invariance property as a purely abstract, categorical theorem (Theorem 1.2, stated in the introduction) concerning morphisms of $h^=$ -fibrations from a free $h^=$ -fibration into a 1-discrete 2-fibration.

Finally, we note that one needn’t necessarily deduce the homotopy-invariance property of the homotopical semantics from the abstract invariance theorem; there is presumably a simpler, direct proof by induction. However, the abstract invariance theorem is interesting in itself, and helps to situate the syntactic invariance theorem in a broader context.

2 Homotopical semantics

In this section, we give the definition of the homotopical semantics that was sketched in the introduction. As stated there, this is essentially (i.e., up to homotopy equivalence) obtained as a special case of interpreting logic in an $h^=$ -fibration, for a particular $h^=$ -fibration .

We first define the latter fibration in Section 2.2. Then, in Section 2.3, we introduce the general notion of interpreting first-order logic in an $h^=$ -fibration, define the homotopical semantics, and describe its relationship to the interpretation in . In Section 2.4, we provide the remaining notions needed to state the special invariance theorem, in particular that of homotopy equivalence of interpretations. Finally, in Section 2.5, we discuss how topological spaces (as opposed to simplicial sets/Kan complexes) can be handled.

2.1 Preliminaries on $h^=$ -fibrations

In this section, we recall the definition of and some basic facts concerning $h^=$ -fibrations. In [8], we discussed a part of the structure of $h^=$ -fibration, namely the notions of $\wedge $ -fibrations and ${\wedge \!\!=}$ -fibrations. After briefly recalling those and some related notions from [8], we then go on to give the “rest” of the definition of $h^=$ -fibration.

Definition 2.1.1. We briefly recall some definitions [8] to fix our terminology and notation:

• • A prefibration is simply a functor ; we call ${\mathbf {C}}$ the total category and B the base category. We denote the fiber of over $B\in {\mathbf {B}}$ by . (See [8, Section 1] for the basic notions concerning Grothendieck fibrations.)

• • A $\wedge $ -fibration is a Grothendieck fibration in which each fiber has finite products, and these are preserved by all pullback functors for $f\colon A\to B$ in ${\mathbf {B}}$ .

• • A ${\wedge \!\!=}$ -fibration is a $\wedge $ -fibration in which ${\mathbf {B}}$ has finite products, and which has equality objects for each diagonal morphism $B \xrightarrow {\Delta _{B}} B \times B$ in ${\mathbf {B}}$ , and these are required to be stable and satisfy Frobenius reciprocity (see [8, Sections 1.6 and 1.7]).

• • For a category ${\mathbf {C}}$ , the prefibration is simply the codomain functor; it is a ${\wedge \!\!=}$ fibration if ${\mathbf {C}}$ has finite limits.

• • For a model category ${\mathbf {C}}$ , the fibration (see [8, Section 11]) has as total category the homotopy category ${\mathbf {Ho}}({\mathbf {C}}^{\to })$ of a certain model structure on ${\mathbf {C}}^{\to }$ , and is induced by the codomain functor (which induces a functor out of ${\mathbf {Ho}}({\mathbf {C}}^{\to })$ since it takes weak equivalences in ${\mathbf {C}}^{\to }$ to isomorphisms in ${\mathbf {C}}$ ). The fiber over $A\in {\mathbf {C}}$ is equivalent to the homotopy category ${\mathbf {Ho}}({\mathbf {C}}/A)$ with respect to the usual slice model structure on ${\mathbf {C}}/A$ .

• • Given a model category ${\mathbf {C}}$ and $*\in {\{{{\mathrm {c}},{\mathrm {f}},{\mathrm {cf}}}\}}$ , we denote by ${\mathbf {C}}_*$ the full subcategory on cofibrant, fibrant, and cofibrant–fibrant objects, respectively. The fibrations and are obtained by restricting the codomain functor to the subcategories $({\mathbf {C}}^{\to })_*$ and ${\mathbf {Ho}}({\mathbf {C}}^{\to })_*$ , respectively (see [8, Sections 11.6–11.8]). They have fibers given by and .

• • For a full subcategory ${\mathbf {D}}\subset {\mathbf {C}}$ , the fibration is defined to be the restriction of to ${\mathbf {D}}$ (see [8, Section 13.6]).

• • A 1-discrete 2-fibration or 1D2F is a 2-functor of 2-categories whose underlying functor is a fibration and for which, given any 2-cell $\alpha \colon f\to g$ in ${\mathbf {B}}$ and any p lying over f, there is a unique 2-cell in ${\mathbf {C}}$ with domain p lying over $\alpha $ (see [8, Section 6]).

Definition 2.1. A fibration has fiberwise finite coproducts if every fiber of has finite coproducts. We have the notion of a coproduct diagram in a fiber of being stable (under pullbacks), analogous the corresponding notion for products (see [8, Section 1.5]).

We follow the conventions concerning coproducts from [8, Section 10.2], except that we use the symbols $\vee $ and $\bot $ instead of $+$ and $\mathbf {0}$ when the category under consideration is the fiber of some fibration. Also, we denote by $\operatorname {\mathrm {in}}_1$ and $\operatorname {\mathrm {in}}_2$ the coprojections into a coproduct.

Next, given objects $B,C$ in a category ${\mathbf {C}}$ , an exponential diagram based on B and C consists of an object $C^B$ (the corresponding exponential object), a product diagram $C^B\xleftarrow {\pi _1} C^B\times B \xrightarrow {\pi _{2}} B$ , and a morphism (the evaluation morphism) $\varepsilon \colon C^B\times B\to C$ satisfying the usual universal property (see, e.g., [12, p. 45]).

A category is cartesian closed if it has finite products, and there is an exponential diagram based on each pair of objects. It is bicartesian closed if it is cartesian closed and has finite coproducts. A functor between cartesian closed categories is cartesian closed if it preserves finite products and takes exponential diagrams to exponential diagrams, and a bicartesian closed functor is defined similarly.

We will generally use the above notation for exponential objects, except when the category in question is the fiber of some fibration, in which case we will write $B{\Rightarrow }{}C$ instead of $C^B$ .

A $\wedge $ -fibration has fiberwise exponentials if each fiber of is cartesian closed. We have the notion of stability (under pullbacks) of exponential diagrams in fibers, analogous to that of product and coproduct diagrams.

Definition 2.1.2. Let be a fibration. We recall the notion of indexed products and sums in .

Given a morphism $f\colon {}A\to {}B$ in ${\mathbf {B}}$ and , a $\prod _f$ -diagram based on P consists of an object (the corresponding indexed product object), a cartesian morphism ${\uparrow }\colon f^*\prod _fP\to P$ over f, and an evaluation morphism $\varepsilon \colon f^*\prod _fP\to P$ over $\operatorname {\mathrm {1}}_A$ , satisfying the appropriate universal property (see [19, p. 341]).

We refer to loc. cit. for the notion of an indexed product $\prod _fP$ (or more precisely, of the corresponding $\prod _f$ -diagram) being stable with respect to a pullback square

(this is also known as the Beck–Chevalley condition, and amounts to a certain morphism $\prod _g(h^*P)\to k^*\prod _fP$ being an isomorphism).

We say that $\prod _fP$ is stable along a morphism $k\colon D\to B$ if it is stable along each pullback square based on k as above.

By an indexed sum object $\sum _fP$ , we simply mean the codomain of a cocartesian morphism over f with domain P. As in [8], when f is a diagonal morphism and P a terminal object, we will usually write $\operatorname {\mathrm {Eq}}_A$ in place of $\sum _fP$ .

The stability or Beck–Chevalley condition for indexed sums is the same as the one for cocartesian morphisms, which was explained in [8, Section 1.6] (cf. [19, p. 342]).

Definition 2.2. A fibration is an h-fibration if it satisfies the following four conditions.

1. (i) has stable fiberwise finite products and coproducts and exponentials.

2. (ii) ${\mathbf {B}}$ has finite products.

3. (iii) For any product projection $\pi \colon {}A\times {}B\to {}B$ in ${\mathbf {B}}$ and any , there exist indexed sums and products $\sum _{\pi }P$ and $\prod _{\pi }P$ , and these (i.e., the corresponding cocartesian morphisms and $\prod _{\pi }$ -diagrams) are stable along all morphisms $k\colon D\to B$ .

is an $h^=$ -fibration if, in addition,

1. (iv) For each $B\in {\mathbf {B}}$ , there exists an equality object for $B$ (i.e., a cocartesian lift of a diagonal $\Delta _B\colon {}B\to {}B\times {}B$ with domain a terminal object ).

Definition 2.3. Given prefibrations and , a morphism of prefibrations is a pair $(\Phi ,{\varphi })$ , where ${\varphi }\colon {\mathbf {B}}\to {\mathbf {B}}'$ and $\Phi \colon {\mathbf {C}}\to {\mathbf {C}}'$ are functors such that the square

commutes (strictly). We say that $(\Phi ,{\varphi })$ is a morphism of prefibrations over ${\varphi }$ . If ${\mathbf {B}}={\mathbf {B}}'$ and ${\varphi }=\operatorname {\mathrm {1}}_{\mathbf {B}}$ , we may just write $\Phi $ instead of $(\Phi ,\operatorname {\mathrm {1}}_B)$ , and we say in this case that $\Phi $ is over ${\mathbf {B}}$ . ⁵ If and are fibrations, then $(\Phi ,{\varphi })$ is a morphism of fibrations if $\Phi $ takes cartesian morphisms to cartesian morphisms.

Note that for each $A\in {\mathbf {B}}$ , $(\Phi ,{\varphi })$ induces a functor .

If and are $*$ -fibrations (where $*$ is one of $\wedge $ , ${\wedge \!\!=}$ , h, and $h^=$ —see [8, Section 1] for the first two notions), we say that $(\Phi ,{\varphi })$ is a morphism of $*$ -fibrations if it preserves the relevant structure: (i) in all cases, the induced functors on fibers should be f.p.; (ii) if $*$ is h or $h^=$ , the induced functors on fibers should moreover be bicartesian closed, and $\Phi \colon {\mathbf {C}}\to {\mathbf {C}}'$ should preserve $\prod _{\pi }$ -diagrams and cocartesian morphisms over product projections $\pi $ ; (iii) if $*$ is ${\wedge \!\!=}$ , h, or $h^=$ , ${\varphi }\colon {\mathbf {B}}\to {\mathbf {B}}'$ should preserve finite products; and (iv) if $*$ is $h^=$ or ${\wedge \!\!=}$ , $\Phi $ should preserve cocartesian lifts of diagonal morphisms with domain a terminal object.

Next, given two morphisms of pre-fibrations, a natural transformation $(\Phi ,{\varphi })\to (\Psi ,\psi )$ is a pair $(\tilde \alpha ,\alpha )$ of natural transformations $\alpha \colon {\varphi }\to \psi $ and $\tilde \alpha \colon \Phi \to \Psi $ such that . Again, we say that $(\tilde \alpha ,\alpha )$ lies over $\alpha $ , or over ${\mathbf {B}}$ if ${\mathbf {B}}={\mathbf {B}}'$ , ${\varphi }=\operatorname {\mathrm {1}}_{\mathbf {B}}$ , and $\alpha =\operatorname {\mathrm {1}}_{\operatorname {\mathrm {1}}_B}$ . We say that $(\tilde \alpha ,\alpha )$ is an equivalence if $\alpha $ and $\tilde \alpha $ are both equivalences.

Proposition 2.4. Every $h^=$ -fibration is a ${\wedge \!\!=}$ -fibration.

Proof Referring to the definition of ${\wedge \!\!=}$ -fibration from [8, Section 1.7], we see that we are only missing the Frobenius reciprocity and stability along product projections for equality objects. These follow from certain well-known facts, which we leave to the reader, namely (i) that the existence of stable exponential objects implies Frobenius reciprocity (see, e.g., [15, p. 6], [19, p. 343], [10, p. 102]) and (ii) that, given $f\colon A\to B$ in the base category (here, we take f a product projection), if indexed products $\prod _fP$ exist for all P lying over A, then all indexed sums are stable along f (see, e.g., [19, p. 343], [10, Lemma 1.9.7]).

Definition 2.5. A category ${\mathbf {C}}$ is locally cartesian closed if each slice category ${\mathbf {C}}/X$ is cartesian closed and ${\mathbf {C}}$ has a terminal object (so in particular, ${\mathbf {C}}\cong {}{\mathbf {C}}/\mathbf {1}$ is itself cartesian closed), and it is locally bicartesian closed if it is locally cartesian closed and has finite coproducts (equivalently, the slices are bicartesian closed and ${\mathbf {C}}$ has a terminal object).

It is well-known that is an h-fibration (in fact, an $h^=$ -fibration) if and only if ${\mathbf {C}}$ is locally bicartesian closed (see, e.g., [19, p. 345], [29, Section 2.4][10, p. 81]).

Remark 2.6. It is easy to see (and well-known—see [19]) that, given a fibration and a morphism $f\colon {}A\to {}B$ in ${\mathbf {B}}$ , the existence of indexed sums or products over f is equivalent to the existence of left and right adjoints $\sum _f$ and $\prod _f$ to “the” pullback functor .

In general, this requires the axiom of choice. ⁶ One way to formulate this which does not involve any choices is to say there is always a canonical anafunctor (see [21]) , and the existence of indexed sums or products over f is equivalent to the existence of a left or right adjoint anafunctor $\sum _f$ and $\prod _f$ (which is then also canonically defined).

We also note that in the case , there is always an explicit indexed sum functor $\sum _f\colon {\mathbf {C}}/A\to {\mathbf {C}}/B$ taking $(X,x)$ to $(X,fx)$ .

2.2 The $h^=$ -fibration of spaces

We now introduce the $h^=$ -fibration ; or rather, we show that it is an $h^=$ -fibration, as it was already introduced in [8]. There, it was already shown that it is a ${\wedge \!\!=}$ -fibration. Hence, to see that it is an $h^=$ -fibration, it remains to show that this fibration has the necessary extra structure—namely, that it supports the “logical” operations $\vee ,{\Rightarrow },\forall ,\exists $ .

In fact, in op. cit., it was shown more generally that the fibration is a ${\wedge \!\!=}$ -fibration for any model category ${\mathbf {C}}$ . We recall that the first subscript “ ${\mathrm {f}}$ ” means we are restricting to fibrations, and the second that we are restricting to fibrant objects (removing the first “ ${\mathrm {f}}$ ” actually results in an equivalent fibration, in contrast to the situation with the related fibration ). We have $({\mathbf {sSet}})_{\mathrm {f}}={\mathbf {Kan}}$ , which is why we write .

It is not true that is an $h^=$ -fibration for any model category ${\mathbf {C}}$ ; we must put certain restrictions on ${\mathbf {C}}$ (satisfied, of course, by ${\mathbf {sSet}}$ ). We encapsulate the needed conditions in Definition 2.8 (“suitable model category”), similar in spirit to the notion of “type-theoretic model category” and related notions (see, e.g., [18, p. 166]). We do this just to clarify what assumptions we are using; we do not actually consider any suitable model categories besides ${\mathbf {sSet}}$ , though we suspect there are other interesting ones—we have in mind the so-called Cisinski model structures, which always satisfy conditions (ii) and (iv) of the definition.

The approach taken here is the same as in [8, Sections 12 and 13]. We first show that the fibration —from which is obtained by passing to the homotopy category in each fiber—is an h-fibration (in fact, it is an $h^=$ -fibration, but we are not interested in its equality structure), and then show that this structure is preserved upon passing to homotopy categories. Along the way, we deduce the important fact that the canonical morphism , as well as the inclusion , are morphisms of h-fibrations, which gives us an explicit description of the h-fibration structure in .

Namely, this tells us that the h-fibration operations (pullbacks, fiberwise products and coproducts, indexed products and sums, etc.) are computed in the same way as those in .

We then in fact have an explicit description of the full $h^=$ -fibration structure on , since, as was shown in [8], the equality objects are given by path spaces. That is, given $B\in {\mathbf {C}}_{\mathrm {f}}$ , we can take to be the second morphism in a factorization $B\to B^I\to B\times B$ of the diagonal $\Delta _B\colon B\to B\times B$ as a trivial cofibration followed by a fibration.

Definition 2.7. The category ${\mathbf {sSet}}$ of simplicial sets is by definition the category ${\mathbf {Set}}^{\mathbf {\Delta }^{\operatorname {op}}}$ of presheaves on the category $\Delta $ of non-empty finite ordinals and non-decreasing maps. There is a standard (“Quillen”) model structure on ${\mathbf {sSet}}$ (see [27, Chapter II, p. 3.14]). Its fibrant objects are called Kan complexes, and we set ${\mathbf {Kan}}:={\mathbf {sSet}}_{\mathrm {f}}$ for the category of Kan complexes.

Outside of the discussion in Section 2.5 and the examples in Section 4.1, we will not really use anything about this model category, except what little is needed to show that it is suitable in the sense of Definition 2.8. However, we certainly expect the reader to be familiar with it. For example, it is good to know that there is an adjunction (in fact, “Quillen equivalence”) ${\mathbf {sSet}}\leftrightarrows {\mathbf {Top}}$ (the functors being “geometric realization” and “singular simplicial set”) inducing an equivalence ${\mathbf {Ho}}({\mathbf {sSet}})\simeq {\mathbf {Ho}}({\mathbf {Top}})$ . It might also be good to know (for the sake of general cultural context) that Kan complexes can justifiably be said to provide a formal definition of the (informal) notion of “weak infinity-groupoid.”

Definition 2.8. A model category ${\mathbf {C}}$ is suitable if the following four conditions are satisfied.

1. (i) ${\mathbf {C}}$ is right-proper, i.e., weak equivalences are closed under pullbacks along fibrations. ⁷

2. (ii) ${\mathbf {C}}$ is locally cartesian closed (as a category).

3. (iii) $[f,g]\colon {}A+B\to {}C$ is a fibration whenever $f\colon {}A\to {}C$ and $g\colon {}B\to {}C$ are, and the unique morphism $0\to {}A$ is always a fibration.

4. (iv) The cofibrations of ${\mathbf {C}}$ are precisely the monomorphisms.

We note that the Quillen model structure on simplicial sets is suitable. Condition (iv) holds by definition. Condition (i) is non-trivial, but well-known, and follows from the existence of pullback and fibration preserving fibrant replacement functors (see, e.g., [24, p. 370]). As for (ii), it is well-known that any presheaf category is locally cartesian closed (see [12, p. 48]).

To see (iii), note that the “horns” $\Lambda ^n_k$ are all connected, in the sense that any two vertices are connected by a path of edges (in fact, for $n>2$ , by a single edge). It follows that any morphism $\Lambda ^n_k\to {}A+B$ to a coproduct must factor through one of the summands $A,B$ . Now, for $[f,g]\colon {}A+B\to {}C$ to be a fibration, it must lift against each horn inclusion $\Lambda ^n_k\to {}\Delta ^n$ . But if f and g are each a fibration, this follows immediately from the fact that any given morphism $\Lambda ^n_k\to {}A+B$ factors through A or B. The corresponding lifting problem for morphisms $0\to {}A$ is trivial, since there are no morphisms $\Lambda ^n_k\to 0$ .

Proposition 2.9. If ${\mathbf {C}}$ is a suitable model category, then any slice category ${\mathbf {C}}/A$ of ${\mathbf {C}}$ , with its induced model structure, is also suitable (and in fact, this is true separately for each of the conditions in Definition 2.8).

Proof It is well-known (and easy to see) that each slice of a locally cartesian closed category is locally cartesian closed; this follows from the existence of the canonical isomorphisms $({\mathbf {C}}/A)/B\cong {\mathbf {C}}/B$ . That Conditions (iii) and (iv) hold in ${\mathbf {C}}/A$ follows from the fact that a morphism $(p,\operatorname {\mathrm {1}}_A)$ in ${\mathbf {C}}/A$ is a monomorphism, cofibration, or fibration if and only if p is, and the fact that the forgetful functor ${\mathbf {C}}/A\to {\mathbf {C}}$ preserves coproducts. Similarly, Condition (i) holds since a square in a slice category ${\mathbf {C}}/A$ is a pullback square if and only if its image under the forgetful functor ${\mathbf {C}}/A\to {\mathbf {C}}$ is.

Proposition 2.10. In a suitable model category ${\mathbf {C}}$ , every object is cofibrant. Hence ${\mathbf {C}}_{\mathrm {cf}}={\mathbf {C}}_{\mathrm {f}}$ , and ${\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})=\pi ({\mathbf {C}}_{\mathrm {cf}})$ .

Proof Since the cofibrations are the monomorphisms, this amount to checking that each morphism from the initial object is a monomorphism. It is well-known that this holds in any cartesian closed category (see [25, p. 61]).

Proposition 2.11. Let ${\mathbf {C}}$ be a suitable model category, let $p\colon {}X\to {}Y$ be a fibration, and let C be a fibrant object. Then the induced map $p^C\colon {}X^C\to {}Y^C$ is a fibration.

Proof We must show that for any solid commutative diagram

in ${\mathbf {C}}$ with i a trivial cofibration, there exists a dashed morphism making the diagram commute.

Using the adjunction $(-\times {}C)\dashv (-)^C$ , this is seen to be equivalent to the existence of a dashed morphism making the corresponding diagram

commute. For this, it suffices that $i\times \operatorname {\mathrm {1}}_C$ be a trivial cofibration. Noting that it is the pullback of i along the projection $B\times {}C\to {}B$ (which is a fibration since C is fibrant), we have that $i\times \operatorname {\mathrm {1}}_{\mathbf {C}}$ is a cofibration since monomorphisms are stable under pullback, and it is a weak equivalence since ${\mathbf {C}}$ is right-proper.

2.2.1

Proposition 2.12. Let ${\mathbf {C}}$ be a suitable model category. We know from [8, Proposition 12.2] that ${\mathbf {C}}_{\mathrm {f}}$ is an f.p. category and that the inclusion ${\mathbf {C}}_{\mathrm {f}}\hookrightarrow {\mathbf {C}}$ is an f.p. functor.

We now claim that ${\mathbf {C}}_{{\mathrm {f}}}$ and the inclusion ${\mathbf {C}}_{{\mathrm {f}}}\hookrightarrow {\mathbf {C}}$ are bicartesian closed.

Proof Since ${\mathbf {C}}_{\mathrm {f}}$ is a full subcategory of ${\mathbf {C}}$ , it suffices to show that the fibrant objects in ${\mathbf {C}}$ are closed under exponentials and coproducts. Condition (iii) of “suitable” (Definition 2.8) implies that the fibrant objects are closed under coproducts. That they are closed under exponentials follows from Proposition 2.11.

Definition 2.13. In [8, Definition 13.6], for a model category ${\mathbf {C}}$ and a full subcategory ${\mathbf {D}}\subseteq {\mathbf {C}}$ , we defined to be the restriction of to ${\mathbf {D}}$ (where $*\in {\{{{\mathrm {c}},{\mathrm {f}},{\mathrm {cf}}}\}}$ ). We similarly define to be the restriction of to ${\mathbf {D}}$ .

We note that, in general, the restriction of a $*$ -fibration (with $*$ one of $\wedge $ , ${\wedge \!\!=}$ , h, and $h^=$ ) to any full subcategory having finite products is again a $*$ -fibration.

Proposition 2.14. Let ${\mathbf {C}}$ be a suitable model category. Since ${\mathbf {C}}$ is locally bicartesian closed, we know that , and hence , is an h-fibration (see Definition 2.5), and by [8, Proposition 12.3], we know that is a $\wedge $ -fibration, and that the inclusion is a morphism of $\wedge $ -fibrations.

We now claim that is an h-fibration and the inclusion is a morphism of h-fibrations.

Proof It follows from Propositions 2.9 and 2.2.1 that the fibers of , and the functors on fibers induced by the inclusion, are bicartesian closed.

Next, we need to check that, given a product projection $\pi _2\colon {}A\times {}B\to {}B$ in ${\mathbf {C}}_{{\mathrm {f}}}$ and a cocartesian morphism $(p,\pi _2)\colon (X,A\times {}B,x)\to {}(Y,B,y)$ in ${\mathbf {C}}^{\to }$ lying over $\pi _2$ , if $(X,x)$ is in , then $(Y,y)$ is in —i.e., if x is a fibration, then so is y. But the product projection $\pi _2$ is a fibration since A is fibrant, and p is an isomorphism (this being equivalent to the cocartesianness of $(p,\pi _2)$ ), hence $y=\pi _2xp^{-1}$ is a fibration as well.

Similarly, we need to check that if $(X,x)$ is a fibration, then $\prod _{\pi _2}(X,x)$ is a fibration. In the case where $B\cong \mathbf {1}_{\mathbf {C}}$ , it is well-known (e.g., [12, Lemma 1.5.2]) that $\prod _{\pi _2}(X,x)$ can be computed as a pullback along a morphism $\mathbf {1}_{\mathbf {C}}\to A^A$ of $x^A\colon X^A\to A^A$ , which is a fibration by Proposition 2.11.

We now reduce the general case to this one by using the canonical isomorphisms $({\mathbf {C}}/A\times {}B)\cong ({\mathbf {C}}/B)/(A\times {}B,\pi _2)$ and ${\mathbf {C}}/B\cong ({\mathbf {C}}/B)/(B,\operatorname {\mathrm {1}}_B)$ as follows. We wish to show that the (ana-)functor $\prod _{\pi _2}\colon {\mathbf {C}}/(A\times B)\to {\mathbf {C}}/B$ (see Remark 2.6) preserves fibrant objects, which we know in the case when B is terminal. Consider the following diagram on the left.

The bottom row preserves fibrant objects since $(B,\operatorname {\mathrm {1}}_B)$ is terminal in ${\mathbf {C}}/B$ . Hence (since the vertical isomorphisms clearly preserve fibrant objects), we will be done if we can show that the diagram commutes. But note that the diagram to the right clearly commutes (with $\Sigma _{\pi _2}$ the explicit indexed sum functor from Remark 2.6), hence the left diagram as well, since $\Pi _{\pi _2}$ is a right (ana-)adjoint to a right (ana-)adjoint $\pi _2^*$ of $\Sigma _{\pi _2}$ .

It remains to see that all the operations are “stable,” i.e., that the pullback functors are bicartesian closed, and that the cocartesian morphisms and $\prod _{\pi }$ -diagrams over product projections $\pi $ are stable. In each case, this follows immediately from the corresponding fact in .

Proposition 2.15. Let ${\mathbf {C}}$ be a suitable model category. We know from Proposition 2.2.1 that ${\mathbf {C}}_{{\mathrm {f}}}$ is bicartesian closed, and we know from [8, Proposition 12.4] that ${\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})$ is an f.p. category and that the functor $\gamma \colon {\mathbf {C}}_{\mathrm {f}}\to {\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})$ is an f.p. functor.

We now claim that the category ${\mathbf {Ho}}({\mathbf {C}}_{{\mathrm {f}}})$ and the functor $\gamma \colon {\mathbf {C}}_{\mathrm {f}}\to {\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})$ are bicartesian closed.

Proof That ${\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})$ has, and $\gamma $ preserves, finite coproducts, follows from an argument dual to the one given in [8, Proposition 12.4] (using that all objects in ${\mathbf {C}}$ are cofibrant).

We next turn to exponentials. Consider an exponential diagram

We already know that $C^B\times {}B$ is still a product in ${\mathbf {Ho}}({\mathbf {C}}_{\mathrm {f}})$ , so it remains (by Proposition 2.10) to see that for any $A\in {\mathbf {C}}_{\mathrm {f}}$ and product $A\xleftarrow {\pi _1}A\times {}B\xrightarrow {\pi _2}B$ , the composite

$$\begin{align*}\pi(A,C^B)\xrightarrow {(-)\times\operatorname{\mathrm{1}}_B}\pi(A\times{}B,C^B\times{}B)\xrightarrow {(\varepsilon\circ\text{--})}\pi(A\times{}B,C) \end{align*}$$

is a bijection. That this map is surjective is clear, since it is already surjective before passing to homotopy classes. To show injectivity, we need to show that if two morphisms $f_1,f_2\colon {}A\times {}B\to {}C$ are homotopic, then the corresponding morphisms $\tilde {f_1},\tilde {f_2}\colon {}A\to {}C^B$ are.

Let $A+A\xrightarrow {[\partial _1,\partial _2]}A\times {}I\xrightarrow {\sigma }A$ be a cylinder object for A. Because the functor $(-\times {}B)$ is a left (ana-)adjoint, it preserves coproducts, and hence the canonical morphism $[{\langle {\operatorname {\mathrm {in}}_1\pi _1,\pi _2}\rangle },{\langle {{\operatorname {\mathrm {in}}_2\pi _1,\pi _2}}\rangle }]\colon {}A\times {}B+A\times {}B\to (A+A)\times {}B$ is an isomorphism. Applying $(-\times {}B)$ to our cylinder object for A, we have a sequence of morphisms

$$\begin{align*}A\times{}B+A\times{}B\xrightarrow {\sim} (A+A)\times{}B\xrightarrow {[\partial_1,\partial_2]\times\operatorname{\mathrm{1}}_B} (A\times{}I)\times{}B\xrightarrow {\sigma\times\operatorname{\mathrm{1}}_B} A\times{}B \end{align*}$$

and we claim that this exhibits $(A\times {}I)\times {}B$ as a cylinder object for $A\times {}B$ . Indeed, the composite is clearly equal to $\nabla _{A\times {}B}$ , and $\sigma \times \operatorname {\mathrm {1}}_B$ is a weak equivalence by the right-properness of ${\mathbf {C}}$ , since it is the pullback of a weak equivalence along the projection $(A\times {}I)\times {}B\to {}A\times {}I$ , which is a fibration since B is fibrant. Moreover, the first two morphisms are cofibrations (the first being an isomorphism and the second being the pullback of a monomorphism and hence a monomorphism).

Hence, by [8, Proposition 10.5[ii]], given two homotopic maps $f_1,f_2\colon {}A\times B\to {}C$ , we obtain a left-homotopy $h\colon (A\times {}I)\times {}B\to {}C$ between them, and hence a morphism $\tilde {h}\colon {}A\times {}I\to {}C^B$ . It remains to see that this is a homotopy between $\tilde {f_1}$ and $\tilde {f_2}$ , i.e., that $\tilde {h}\partial _i=\tilde {f_i}\colon {}A\to {}C^B$ . It suffices to see that $\varepsilon \cdot ((\tilde {h}\partial _i)\times \operatorname {\mathrm {1}}_B)=f_i$ , which follows from the definition of $\tilde h$ .

Theorem 2.16. Let ${\mathbf {C}}$ be a suitable model category. By Proposition 2.14, we know that is an h-fibration, and by [8, Propositions 12.5 and 13.7], we know that is a ${\wedge \!\!=}$ -fibration and that the localization morphism is a morphism of $\wedge $ -fibrations.

We now claim that is in fact an $h^=$ -fibration, and that $\gamma $ is a morphism of h-fibrations.

Proof By Proposition 2.15, we know that the fibers of and the functors on the fibers induced by are bicartesian closed.

Next, we consider indexed sums. That is, we need to show that the image under $\gamma $ of any cocartesian morphism in over a product projection is cocartesian in . This follows from [8, Proposition 13.1] and the fact that every isomorphism is a weak equivalence.

We next consider indexed products $\prod _{\pi _2}P$ . Let $\pi _2\colon {}A\times {}B\to {}B$ be a product projection in ${\mathbf {C}}_{\mathrm {f}}$ , and let

be a $\prod _{\pi _2}$ -diagram in . We need to see that its image in is also a $\prod _{\pi _2}$ -diagram.

We know already that the image of ${\uparrow }$ is cartesian. Hence, it remains to show that for each $Q\in ({\mathbf {C}}/B)_{\mathrm {f}}$ and cartesian ${\uparrow }\colon {}f^*Q\to {}Q$ over $\pi _2$ , the composite

$$\begin{align*}\pi(Q,{\textstyle\prod}_{\pi_2}P) \xrightarrow {\pi_2^*} \pi(\pi_2^*Q,\pi_2^*{\textstyle\prod}_{\pi_2}P) \xrightarrow {(\varepsilon\circ\text{--})} \pi(\pi_2^*Q,P) \end{align*}$$

is a bijection. As in the proof of Proposition 2.2.1, it is immediate that it is surjective, and injectivity follows by a similar argument to the one there.

It remains to check the various “stability” conditions for . These are proven in the same way as the stability of products in [8, Proposition 12.5]. Namely, in each case, we reduce to showing the stability of some (rather than every) diagram of the appropriate kind, and then we choose the diagram coming from , where we already know that stability holds.

2.3 Interpreting logic in fibrations

In this section, we recall the usual notion of interpreting first-order logic in an $h^=$ -fibration, and then describe the variant of it giving the homotopical semantics. We will then prove that, up to homotopy equivalence, the homotopical semantics in a suitable model category ${\mathbf {C}}$ agrees with the (ordinary) semantics in the $h^=$ -fibration .

The homotopical semantics in ${\mathbf {C}}$ will be defined to be identical with the usual semantics in the fibration , except of course for the treatment of equality: we demand that an equality formula be interpreted not as an equality object of the fibration but as a path space; as mentioned in the introduction to Section 2.2, this is precisely how the equality objects in are given.

We note that in the case of a posetal $h^=$ -fibration (i.e., one in which the fibers are Heyting algebras), the interpretation in unambiguously assigns to each formula an object in one of the fibers of . However, in the general case, there are choices involved, and this assignment is only determined up to isomorphism.

Definition 2.17. A (multi-sorted) algebraic signature $\sigma $ is given by a set $\operatorname {\mathrm {Ob}}\sigma $ of sorts and, for each finite sequence $\vec {A}$ of sorts and each sort B, a set $\sigma (\vec {A},B)$ of function symbols (with arity $\vec {A}$ and codomain sort B). We denote the set of finite (possibly empty) sequences in a set X by $X^{<\omega }$ , and write ${\ell ({\vec {A}})}$ for the length of a finite sequence. Also, we denote concatenation of sequences (or of a sequence with a single element) by juxtaposition. Given a sequence with the name $\vec {X}$ , we will denote its entries by $X_1,\ldots ,X_{{\ell (X)}}$ .

Given a finite product category ${\mathbf {C}}$ , an interpretation M of $\sigma $ in ${\mathbf {C}}$ consists of the following data (i)–(iii):

1. (i) a function $M\colon \operatorname {\mathrm {Ob}}\sigma \to \operatorname {\mathrm {Ob}}{\mathbf {C}}$ ;

2. (ii) a choice of object $M\vec {A}$ and product diagram ${\{{\pi _i^M\colon {}M\vec {A}\to {}MA_i}\}}_{i=1}^{{\ell ({\vec {A}})}}$ on $MA_1,\ldots ,MA_{{\ell ({\vec {A}})}}$ for each sequence $\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$ (where for singleton sequences ${\langle {A}\rangle }$ with $A\in \operatorname {\mathrm {Ob}}\sigma $ , we require that $M{\langle {A}\rangle }=MA$ and $\pi _1^{M}=\operatorname {\mathrm {1}}_{MA}\colon {}M{\langle {A}\rangle }\to {}MA$ );

3. (iii) a morphism $Mf\colon {}M\vec {A}\to {}MB$ for each $f\in \sigma (\vec {A},B)$ .

We write $M\colon \sigma \to {\mathbf {C}}$ to indicate that M is an interpretation of $\sigma $ in ${\mathbf {C}}$ .

Next, given an interpretation $M\colon \sigma \to {\mathbf {C}}$ and an f.p. functor $F\colon {\mathbf {C}}\to {\mathbf {D}}$ , we obtain an interpretation $F\circ {}M\colon \sigma \to {\mathbf {D}}$ by setting $(F\circ {}M)(A)=F(MA)$ for $A\in \operatorname {\mathrm {Ob}}\sigma $ ; $(F\circ {}M)(\vec {A})=F(M\vec {A})$ and $\pi _i^{F\circ {}M}=F\pi _i^M\colon (F\circ {}M)(\vec {A})\to (F\circ {}M)A_i$ for $\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$ and $1\le {}i\le {\ell ({\vec {A}})}$ ; and $(F\circ {}M)(f)=F(Mf)$ for $f\in \sigma (\vec {A},B)$ .

For the rest of Section 2.3, fix an algebraic signature $\sigma $ .

Definition 2.18. We recall the (usual) syntax of first-order logic over $\sigma $ .

We fix, once and for all, an arbitrary infinite set $\operatorname {\mathrm {Varn}}$ of “variable names” (for definiteness, we could take $\operatorname {\mathrm {Varn}}={\mathbb {N}}$ ).

We next declare the symbols to be used in the syntax. These consist of (i) the (sorted) variable symbols, which are given by the set $\operatorname {\mathrm {Varn}}\times \operatorname {\mathrm {Ob}}\sigma $ , (ii) the functions symbols, which are just the function symbols of $\sigma $ (i.e., they are given by the disjoint union of all the sets $\sigma (\vec {A},B)$ ), and (iii) the additional symbols $\wedge $ , $\vee $ , ${\Rightarrow }$ , $\forall $ , $\exists $ , $\top $ , and $\bot $ (negation $\neg {\varphi }$ is taken as an abbreviation of ${\varphi }{\Rightarrow }\bot $ ).

Now, on the basis of these, we define the set of $\sigma $ -terms (or just terms), and then of $\sigma $ -formulas (or just formulas) as follows.

Each $\sigma $ -term t will have a sort $\operatorname {\mathrm {tp}}(t)\in \operatorname {\mathrm {Ob}}\sigma $ associated with it (the sort of t), and the set of $\sigma $ -terms is given as follows: (i) each sorted variable symbol $(v,A)$ is a term of sort A, and (ii) $ft_1\ldots t_{{\ell ({\vec {A}})}}$ is a term of sort B whenever $f\in \sigma (\vec {A},B)$ is a function symbol and $t_1,\ldots ,t_{{\ell ({\vec {A}})}}$ are terms, with $\operatorname {\mathrm {tp}} t_i=A_i$ .

Given a sequence of terms $\vec {t}={\langle {t_1,\ldots ,t_n}\rangle }$ , we will write $\operatorname {\mathrm {tp}}(\vec {t})$ for the sequence of sorts ${\langle {\operatorname {\mathrm {tp}}(A_1),\ldots ,\operatorname {\mathrm {tp}}(A_n)}\rangle }$ .

Next, the $\sigma $ -formulas are given as follows: (i) $s=t$ is a formula whenever s and t are terms of the same sort, (ii) $\top $ and $\bot $ are formulas, (iii) ${\varphi }\wedge \psi $ , ${\varphi }\vee \psi $ , and ${\varphi }{\Rightarrow }\psi $ are formulas whenever ${\varphi }$ and $\psi $ are, and (iv) $\forall v{\varphi }$ and $\exists v{\varphi }$ are formulas whenever ${\varphi }$ is a formula and v is a variable symbol.

We take for granted the notions free and bound variables in a term or formula (all variables in a term being free), as well as the notion of one formula being obtained from another by the renaming of bound variables. In fact, we will henceforth identify two formulas when they differ only by renaming of bound variables (this identification is needed, for example, in order to make the operation of capture-avoiding substitution—which we also take for granted—well defined in general).

We also take for granted the principles of structural induction and recursion. That is, to prove something about all terms or formulas, we can proceed by induction, the base cases being the atomic terms or formulas, and the induction step being to prove statement for a given formula after assuming it for its constituents. Similarly, to define a function on the set of all terms or formulas, we can likewise proceed by recursion.

Finally, we define a formula-in-context to be a pair $({\varphi },\vec {x})$ , where $\vec {x}$ is a sequence of distinct variable symbols containing all the free variables of ${\varphi }$ , and we define a term-in-context similarly.

Definition 2.19. Let ${\mathbf {B}}$ be a finite product category ${\mathbf {B}}$ , and $M\colon \sigma \to {\mathbf {B}}$ an interpretation. Given a sequence of variables $\vec {x}$ we write $M(\vec {x})$ for $M(\operatorname {\mathrm {tp}}\vec {x})$ .

We now define a function taking each term-in-context $(t,\vec {x})$ to a morphism $M_{\vec {x}}t\colon M(\vec {x})\to M(\operatorname {\mathrm {tp}} t)$ by recursion on t as follows. If t is a variable $x_i$ , we set $M_{\vec {x}}(t)=\pi _i^M\colon M(\vec {x})\to M(\operatorname {\mathrm {tp}} x_i)$ , and if $t=ft_1\ldots t_n$ with $f\in \sigma (\vec {A},B)$ (so that $\operatorname {\mathrm {tp}}(t)=B$ and $\operatorname {\mathrm {tp}}(t_i)=A_i$ ), then we take $M_{\vec {x}}(t)$ to be the composite

$$\begin{align*}M_{\vec{x}}(t)\xrightarrow {{\langle{{M_{\vec{x}}(t_1),\ldots,M_{\vec{x}}(t_n)}}\rangle}} M(\vec{A})\xrightarrow {Mf}MB \end{align*}$$

(note here that the free variables of each $t_i$ are among those in $\vec {x}$ since this is the case for t).

Next, given an $h^=$ -fibration over B, an interpretation $\widehat M$ in over M is a function assigning to each formula-in-context $({\varphi },\vec {x})$ an object , satisfying the following conditions:

1. (i) If ${\varphi }$ is $\top $ or $\bot $ , then $\widehat M_{\vec {x}}({\varphi })$ must be a terminal object $\top _{M(\vec {x})}$ or initial object $\bot _{M(\vec {x})}$ , respectively.

2. (ii) If ${\varphi }$ is $\psi \square \chi $ , where $\square $ is one of $\wedge $ , $\vee $ , or ${\Rightarrow }$ , then $\widehat M_{\vec {x}}({\varphi })$ must be, respectively, a product, coproduct, or exponential object $\widehat M_{\vec {x}}(\psi )\square \widehat M_{\vec {x}}(\chi )$ of the objects $\widehat M_{\vec {x}}(\psi )$ and $\widehat M_{\vec {x}}(\chi )$ in . ⁸

3. (iii) If ${\varphi }$ is $\forall z\psi $ or $\exists z\psi $ , then $\widehat M_{\vec {x}}({\varphi })$ (where we can assume, by our convention on bound variables, that $z\notin \vec {x}$ ) must be, respectively, an indexed product $\prod _{\pi }\widehat M_{\vec {x}z}(\psi )$ or sum $\sum _{\pi }\widehat M_{\vec {x}z}(\psi )$ of $\widehat M_{\vec {x}z}(\psi )$ , where $\pi =\langle {\pi _1^M,\ldots ,\pi _{{\ell ({\vec {x}})}}^M}\rangle $ .

4. (iv) If ${\varphi }$ is $s=t$ , with s and t terms of sort B, then $\widehat M_{\vec {x}}({\varphi })$ must be a pullback ${\langle {{M_{\vec {x}}(s),M_{\vec {s}}(t)}}\rangle }^*\operatorname {\mathrm {Eq}}_{MB}$ along ${\langle {{M_{\vec {x}}(s),M_{\vec {s}}(t)}}\rangle }\colon M(\vec {x})\to MB\times MB$ of an equality object $\operatorname {\mathrm {Eq}}_{MB}$ over $MB\times MB$ .

We also say that the pair $(\widehat M,M)$ is an interpretation of $\sigma $ in and write .

If ${\varphi }$ is a closed formula (i.e., has no free variables), we say that M satisfies ${\varphi }$ , and write $M\vDash {\varphi }$ , if there exists a morphism $\mathbf {1}\to \widehat M_{\emptyset }({\varphi })$ in (this notion really depends on and not just on M, but by Proposition 2.20 it does not depend on $\widehat M$ ).

Given an interpretation $\widehat M$ in over M and a morphism of $h^=$ -fibrations , we obtain an interpretation in over ${\varphi }\circ M$ , denoted $\Phi \circ \widehat M$ , given by $(\Phi \circ \widehat M)_{\vec x}(\psi ):=\Phi (\widehat M_{\vec x}(\psi ))$ .

Proposition 2.20. Given an $h^=$ -fibration and an interpretation $\sigma \colon M\to {\mathbf {B}}$ in ${\mathbf {B}}$ , any two interpretations in over M are isomorphic—i.e., if $\widehat M$ and $\widehat M'$ are two interpretations in over M, then $\widehat M_{\vec {x}}{\varphi }$ and $\widehat M^{\prime }_{\vec {x}}{\varphi }$ are isomorphic objects in for every $({\varphi },\vec {x})$ . Moreover (using the axiom of choice), there always exists an interpretation in over M.

Proof The first claim follows by induction on ${\varphi }$ since for each possible ${\varphi }$ , one of the clauses in the definition of interpretation over M determines $\widehat M_{\vec {x}}({\varphi })$ up to isomorphism based on the constituent formulas of ${\varphi }$ .

For the second claim, we just choose fiberwise product, fiberwise coproducts, etc., in and then recursively define an interpretation over M.

Remark 2.3.1. We now consider some examples of interpretations in $h^=$ -fibrations, all of which were mentioned in Section 1.2 in the introduction.

If ${\mathbf {C}}={\mathbf {Set}}$ , then an interpretation $M\colon \sigma \to {\mathbf {Set}}$ is just a $\sigma $ -structure in the usual, set-theoretic sense. ⁹ Then, if we consider the sub- $h^=$ -fibration of consisting of morphisms which are inclusions of subsets—then there is exactly one interpretation in over M, and this recovers the classical semantics of first-order logic. Namely, $M_{\vec {x}}({\varphi })$ is then given by ${\{{\vec {a}\in M(\vec {x}) \mid M\underset {\vec {x}\mapsto \vec {a}}{\vDash }{\varphi }}\}}$ .

Next, if we instead take the fibration , then an interpretation in over M recovers the “propositions as sets” semantics.

Similarly, taking for any locally cartesian closed category with finite coproducts ${\mathbf {C}}$ with, we recover the “propositions as objects of ${\mathbf {C}}$ ” semantics.

Finally, if we take ${\mathbf {C}}={\mathbf {sSet}}$ , we get the “propositions as objects of ${\mathbf {sSet}}$ ” semantics which, as explained in Section 1.2, is not our desired homotopical semantics.

We now want to convince ourselves that taking the fibration does give us the homotopical semantics). But let us first define what the latter is.

Definition 2.21. Given an interpretation $M\colon \sigma \to {\mathbf {C}}$ , with ${\mathbf {C}}$ any suitable model category (in fact, any model category which is locally bicartesian closed), we define a homotopical interpretation $\widehat M$ over M to be a function taking each $\sigma $ -formula-in-context $({\varphi },\vec {x})$ to an object , satisfying the same conditions as in Definition 2.19, except that in (iv) the equality object $\operatorname {\mathrm {Eq}}_{MB}$ over $MB$ is replaced by a path object over $MB$ —i.e., the second factor in a factorization of $\Delta _{MB}\colon MB\to MB\times MB$ as a weak equivalence followed by a fibration.

Below, we will be concerned only with interpretations $M\colon \sigma \to {\mathbf {C}}_{\mathrm {f}}$ landing in the subcategory ${\mathbf {C}}_{\mathrm {f}}$ . In this case, each object $\widehat M_{\vec {x}}({\varphi })$ lies in the subfibration of (this follows by induction using Proposition 2.14 and the fact that $\widehat M_{\vec {x}}(s=t)$ is by definition a fibration).

Again, for a closed formula ${\varphi }$ , we write $M\vDash {\varphi }$ to mean that there exists a morphism $\mathbf {1}_{{\mathbf {C}}}\to \widehat M_{\emptyset }\varphi $ in ${\mathbf {C}}/M(\emptyset )\cong {\mathbf {C}}$ and again (now by Proposition 2.23), we note that this is independent of $\widehat M$ .

We again have, as in Proposition 2.20, that a homotopical interpretation over M always exists. However, we no longer have the uniqueness up to isomorphism, the reason being that there exist non-isomorphic path spaces over a given space. Still (for suitable ${\mathbf {C}}$ ), it is unique up to homotopy equivalence as we will see presently.

Definition 2.22. Let ${\mathbf {C}}$ be a model category and let $A,B\in {\mathbf {C}}_{\mathrm {cf}}$ be cofibrant-fibrant objects. Recall that in this case, a morphism $f\colon A\to B$ is a weak equivalence if and only if there exists $g\colon B\to A$ such that $gf$ and $fg$ are homotopic to the identity (where we recall that for objects in ${\mathbf {C}}_{\mathrm {cf}}$ , “left-homotopic” and “right-homotopic” are equivalent)—see, e.g., [8, Proposition 10.7]. For emphasis, we call such an f a homotopy equivalence and g a homotopy inverse.

Note that f is homotopy equivalence if and only if it is an equivalence (see Definition 3.1) with respect to the Quillen 2-categorical structure on ${\mathbf {C}}_{\mathrm {cf}}$ [8, Definition 15.7].

If such an f exists, we say that A and B are homotopy equivalent.

We note that in practice, we will deploy this notion for suitable model categories ${\mathbf {C}}$ , in which every object is cofibrant, so it is only necessary to restrict to fibrant objects.

Proposition 2.23. Let $M\colon \sigma \to {\mathbf {C}}_{\mathrm {f}}$ be an interpretation with ${\mathbf {C}}$ a suitable model category.

Now suppose $\widehat M$ is an arbitrary function assigning to each $\sigma $ -formula-in-context $({\varphi },\vec {x})$ an object $\widehat M_{\vec {x}}({\varphi })\in {\mathbf {C}}/M(\vec x)_{\mathrm {f}}$ . Recall the localization morphism , and define the function $\gamma \circ \widehat M$ (taking values in the fibers of ) as in the end of Definition 2.19.

Then $\gamma \circ \widehat M$ is an interpretation in over M if and only if $\widehat M$ is homotopy equivalent to a homotopical interpretation over M, in the sense that there is some homotopical interpretation $\widehat M'$ over M such that $\widehat M_{\vec x}{\varphi }$ and $\widehat M^{\prime }_{\vec {x}}{\varphi }$ are homotopy equivalent for each $({\varphi },\vec {x})$ .

Moreover, any two homotopical interpretations over M are homotopy equivalent.

Proof Suppose $\widehat M$ is homotopy equivalent to a homotopical interpretation $\widehat M'$ . Then $\gamma \circ \widehat M$ and $\gamma \circ \widehat M'$ are isomorphic, and hence it suffices to check that the latter is an interpretation in over M.

We need to check each of the conditions in Definition 2.19. Conditions (i)–(iii) follow from the fact that they are satisfied by $\widehat M$ and the fact that is a morphism of h-fibrations. Condition (iv) follows from [8, Proposition 13.1] and the definition of homotopical interpretation.

Conversely, suppose $\gamma \circ \widehat M$ is an interpretation in over M, and let $\widehat M'$ be any homotopical interpretation. Then by what we just showed, $\gamma \circ \widehat M'$ is also an interpretation in over M, and hence isomorphic to $\gamma \circ \widehat M$ by Proposition 2.20. But this means precisely that $\widehat M$ and $\widehat M'$ are homotopy equivalent (since, by the suitability of ${\mathbf {C}}$ , all the objects $\widehat M_{\vec {x}}({\varphi })$ and $\widehat M^{\prime }_{\vec {x}}({\varphi })$ are cofibrant-fibrant).

The last claim follows for the same reason.

2.4 Homotopy equivalence

We now introduce the remaining notions that are present in the statement of the special invariance theorem, Theorem 3.24 (which was also stated in the introduction).

The first is the definition of homotopy equivalence of $\sigma $ interpretations. We also include the definition of (ordinary) homomorphism of $\sigma $ -interpretations, for the sake of motivation, and since we will use it later (in the definition of free finite product category).

The second is, given two fibrations $X\to A$ and $Y\to B$ in a model category, the notion of a homotopy between morphisms $X\to Y$ lying over a given homotopy between morphisms $A\to B$ . In the case of topological spaces, this is a familiar notion, and we verify that it is well-behaved in general.

Definition 2.24. Given two interpretations $M,N\colon \sigma \to {\mathbf {C}}$ , a homomorphism $\alpha \colon {}M\to {}N$ consists of morphisms $\alpha _A\colon {}MA\to {}NA$ for each sort $A\in \operatorname {\mathrm {Ob}}\sigma $ , such that for each $f\in \sigma (\vec {A},B)$ , the following diagram commutes, where we write $\alpha _{\vec {A}}$ for $\alpha _{A_1}\times \cdots \times \alpha _{A_{{\ell ({\vec {A}})}}}$ .

Given a suitable model structure on ${\mathbf {C}}$ and two interpretations $M,N\colon \sigma \to {\mathbf {C}}_{\mathrm {f}}={\mathbf {C}}_{{\mathrm {cf}}}$ , a homotopy homomorphism $\alpha \colon {}M\to {}N$ consists of a morphism $\alpha _A\colon {}MA\to {}NA$ for each $A\in \operatorname {\mathrm {Ob}}\sigma $ , such that, for each function symbol $f\in \sigma (\vec {A},B)$ , the morphisms $\alpha _B\circ {}Mf$ and $Nf\circ \alpha _{\vec {A}}$ are homotopic (note that $M\vec {A}$ is still in ${\mathbf {C}}_{\mathrm {f}}={\mathbf {C}}_{{\mathrm {cf}}}$ as the latter is close under products).

A homotopy homomorphism $\alpha \colon {}M\to {}N$ is a homotopy equivalence if $\alpha _A$ is a homotopy equivalence for each $A\in \operatorname {\mathrm {Ob}}\sigma $ . If such an $\alpha $ exists, we say that M and N are homotopy equivalent.

Definition 2.25. Let ${\mathbf {C}}$ be a model category, let $(X,A,x),(Y,B,y)\in {\mathbf {C}}^{\to }$ be fibrations, and let $(p,f),(q,g)\colon {}(X,A,x)\to (Y,B,y)$ be morphisms. A right homotopy from $(p,f)$ to $(q,g)$ consists of right-homotopies $k\colon {}A\to B^I$ from f to g and $\hat {k}\colon {}X\to Y^I$ from p to q, together with a morphism $y^I\colon Y^I\to B^I$ making the following two diagrams on the right commute. ¹⁰

(2.1)

We also call $\hat k$ a right homotopy from p to q over k. If such a homotopy exists, we say that $(p,f)$ and $(q,g)$ are right homotopic and that p and q are right homotopic over k.

There is a dual notion of a left homotopy $\hat h$ from p to q over a left homotopy h from f to g, corresponding to the two diagrams above to the left.

Note that if $f=g$ and h is the trivial homotopy $A\times I\xrightarrow {\sigma }A\xrightarrow {f=g}B$ , then p and q are left-homotopic over h if and only if $(p,f)$ to $(q,g)$ are left-homotopic in the model structure of [8, Definition 11.1] by [8, Proposition 11.3].

Proposition 2.26. With $(p,f)$ and $(q,g)$ as in Definition 2.25, if X and A are cofibrant and Y and B are fibrant, then the notions of $(p,f)$ and $(q,g)$ being left or right homotopic are equivalent, and are both equivalence relations.

Moreover, being homotopic over some fixed (left or right) homotopy h from f to g depends only on the homotopy class of h (in the sense of [8, Section 14]), and if p and q are homotopic over h, and q and r are homotopic over $h'$ , then p and r are homotopic over the composite of h and $h'$ .

Proof The first claim follows from the existence of a model structure on ${\mathbf {C}}^{\to }$ in which the notions of left and right homotopic are the ones given above, and in which an object of ${\mathbf {C}}^{\to }$ is cofibrant iff both domain and codomain are, and is fibrant iff it is a fibration with fibrant codomain (and hence domain).

The model structure in question is characterized by the property that its cofibrations and weak equivalences are the object-wise cofibrations and weak equivalences; see, e.g., [9, Theorem 5.1.3] (this is also known as the “injective model structure,” and is also a “Reedy model structure”).

By inspecting the definitions, one finds that a left-homotopy is indeed precisely the notion given above. However, for right-homotopies, there is the additional condition that the induced morphism $Y^I\to B^I\times _{B\times B}(Y\times Y)$ must be a fibration in order for (2.1) to be a path object for $(Y,B,y)$ . But this can always be arranged by factoring it as a trivial cofibration followed by a fibration $Y^I\to Y^{I'}\to B^I\times _{B\times B}(Y\times Y)$ and then replacing $Y^I$ by $Y^{I'}$ .

The last statement follows from the fact that the codomain functor ${\mathbf {C}}^{\to }\to {\mathbf {C}}$ preserves “all” of the model structure—fibrations, cofibrations, weak equivalences, and finite limits and colimits—and hence takes composites of homotopies to composites of homotopies.

For the second to last claim, we need to show that, given a homotopy $\hat h\colon X\times I\to Y$ from p to q over a homotopy $h\colon A\times I\to B$ (where we denote the auxiliary morphism $X\times I\to A\times I$ by $x\times I$ as above), and a homotopic homotopy $h'\colon A\times I'\to B$ , there is a homotopic homotopy $\hat h'\colon X\times I'\to Y$ over $h'$ .

So suppose we are given a left-homotopy $H\colon A\times J\to B$ from h to $h'$ , so that we have a factorization of $[\sigma ,\sigma ]\colon (A\times I)+_{A+A}(A\times I')\to A$ as a cofibration $(A\times I)+_{A+A}(A\times I')\xrightarrow {[\partial _1,\partial _2]}A\times J$ and a weak equivalence $\sigma \colon A\times J\to A$ (which we may assume is a trivial fibration since B is fibrant). ¹¹

Now let $X\times I'$ be a cylinder object on X with $[\partial _1,\partial _2]\colon X+X\to X\times I'$ a cofibration, and let $x\times I'\colon X\times I'\to A\times I'$ be a morphism as in (2.1) (this can be obtained as a diagonal filler assuming $\sigma \colon A\times I'\to A$ is a trivial fibration, which we may by [8, Proposition 14.4]), and factor $[\sigma ,\sigma ]\colon (X\times I)+_{X+X}(X\times I')\to X$ as a cofibration and trivial fibration $(X\times I)+_{X+X}(X\times I')\xrightarrow {[\partial _1,\partial _2]}X\times J\xrightarrow {\sigma }X$ . Now choose a diagonal filler $x\times J$ in

Finally, choose a diagonal filler $\hat H$ in the following square (where the morphism on the left is a trivial cofibration).

The composite $\hat H\partial _2\colon X\times I'\to Y$ is then the desired homotopy.

Definition 2.27. Let ${\mathbf {C}}$ be a model category and $(p,f)\colon (X,A)\to (Y,B)$ a morphism in $({\mathbf {C}}_{\mathrm {cf}})^{\to }$ , and suppose f is a homotopy equivalence. We say that p is a homotopy equivalence over f if p is a homotopy equivalence, and moreover, there exist homotopy inverses $g\colon B\to A$ and $q\colon Y\to X$ such that the homotopies from $qp$ to $\operatorname {\mathrm {1}}_X$ and from $pq$ to $\operatorname {\mathrm {1}}_Y$ lie over homotopies from $gf$ to $ \operatorname {\mathrm {1}}_A$ and from $fg$ to $\operatorname {\mathrm {1}}_B$ .

Remark 2.4.1. With these definition in place, we can now formulate the special invariance theorem, Theorem 3.24, which was already restated in the introduction, and so we won’t repeat it here.

2.5 Topological spaces

In Section 2.2, we showed that is an $h^=$ -fibration and that is a morphism of h-fibrations.

As mentioned in the introduction, we cannot hope to prove this with ${\mathbf {Top}}$ ( $={\mathbf {Top}}_{\mathrm {f}}$ ) in place of ${\mathbf {Kan}}$ , since ${\mathbf {Top}}$ is not locally cartesian closed.

However, it would also be nice to be able to define homotopical semantics valued in topological spaces. We now briefly discuss some possible solutions to this issue.

2.5.1 Composing with $\operatorname {\mathrm {Sing}}\colon {\mathbf {Top}}\to {\mathbf {sSet}}$ .

The simplest way to define ${\mathbf {Top}}$ -valued homotopical semantics is to simply do so via simplicial sets (which is the approach we take in Section 4.1): we have the singular simplicial set functor $\operatorname {\mathrm {Sing}}\colon {\mathbf {Top}}\to {\mathbf {sSet}}$ , which preserves products, being a right adjoint.

Hence, given an interpretation $M\colon \sigma \to {\mathbf {Top}}$ , we can compose it with $\operatorname {\mathrm {Sing}}$ to obtain a $\sigma $ -interpretation $\operatorname {\mathrm {Sing}}\circ M$ in ${\mathbf {sSet}}$ and we then define a homotopical interpretation over $\sigma $ to be one over $\operatorname {\mathrm {Sing}}\circ M$ .

The reason why this is a sensible thing to do is that—at least when M is valued in spaces homotopy equivalent to a CW-complex—the properties which can be described using the homotopical semantics (namely, the “homotopical” ones) can all be recovered from the associated singular simplicial set—see Section 4.1 for examples.

2.5.2 The fibration .

An important observation in this connection is that, although cannot be an h-fibration, it turns out that (or the equivalent fibration ) is, after all, an h- (and even an $h^=$ -)fibration, by virtue of its close relationship to .

The reason for this is that, when ${\mathbf {Top}}$ is endowed with its standard (“Quillen”) model structure (or better, with its “mixed” model structure—see [24, p. 356]), the adjunction (the left adjoint being “geometric realization”) becomes a Quillen equivalence, from which it follows that, for fibrant $X\in {\mathbf {Top}}$ , the induced functor ${\mathbf {Top}}/X\to {\mathbf {sSet}}/\operatorname {\mathrm {Sing}}(X)$ is also a Quillen equivalence (with respect to the induced model structures), which therefore induces equivalences ${\mathbf {Ho}}({\mathbf {Top}}/X)\to {\mathbf {Ho}}({\mathbf {sSet}}/\operatorname {\mathrm {Sing}}(X))$ .

It follows that we have a morphism of fibrations which is a “fiberwise equivalence” (Definition 3.9), from which it follows that is an $h^=$ -fibration (since is and $\operatorname {\mathrm {Sing}}(X)\in {\mathbf {Kan}}$ for all $X\in {\mathbf {Top}}$ ).

Thus, since homotopical interpretations in a model category ${\mathbf {C}}$ correspond to ordinary interpretations in , we can, in a sense, define homotopical semantics directly in ${\mathbf {Top}}$ , by simply defining this to be the fibrational semantics in .

The main problem with this is that, unlike in the case of suitable ${\mathbf {C}}$ , the $h^=$ -fibration structure on is given very inexplicitly, and hence we cannot say, for any particular formula, what its interpretation in ${\mathbf {Top}}$ actually is.

However, it is worth noting that we can get a handle on some formulas, namely those not involving implication and universal quantification, as is a “ $\exists \vee \!{\wedge \!\!=}$ -fibration” (and a morphism of such).

2.5.3 Convenient categories of spaces.

One might hope to circumvent the failure of ${\mathbf {Top}}$ to be locally cartesian by passing to a modified category of spaces; the well-established solution to ${\mathbf {Top}}$ not being cartesian closed is to pass to a “convenient” subcategory of ${\mathbf {Top}}$ (such as the compactly generated spaces) that is cartesian closed. Unfortunately, the various categories used for this purpose are not (or at least not known to be) locally cartesian closed.

However, there are well-known “enlargements” of subcategories of ${\mathbf {Top}}$ which are locally cartesian closed, i.e., a (reasonably large) full subcategory ${\mathbf {C}}\subset {\mathbf {Top}}$ with a full and faithful functor $i\colon {\mathbf {C}}\to {\mathbf {D}}$ . An example is the category ${\mathbf {D}}$ of subsequential spaces [11] (with ${\mathbf {C}}$ the category of sequential topological spaces).

Hence, one might hope to use such a category ${\mathbf {D}}$ for the homotopical semantics instead, by extending to it the usual model structure(s) on ${\mathbf {Top}}$ . One can indeed produce such model structures, at least in the case of subsequential spaces. However, the result still fails to be suitable, and as a result suffers from the same problem mentioned in the previous section: it becomes difficult to actually compute the interpretation of any given formula (in particular, it requires taking cofibrant replacements ¹² ).

3 The invariance theorem

We now formulate and prove the homotopy-invariance property of the homotopical semantics; we first prove the “abstract” version, which is purely categorical, and then deduce from it the “special” version of the theorem, concerning the homotopical semantics.

The formulation and proof of the abstract invariance theorem is actually independent of the results of the previous section; these were presented first only in order to give some motivation for the abstract invariance theorem. The latter involves an arbitrary $h^=$ -fibration , which for the special invariance theorem we will want to take to be the $h^=$ -fibration introduced above.

Moreover, is assumed to have the structure of a 1-discrete 2-fibration (1D2F), which is a 2-categorical structure on ${\mathbf {C}}'$ and ${\mathbf {B}}'$ compatible with the fibration in which the fibers are, however, still 1-categories (this is the “1-discreteness”)—see [8, Section 6] for the definition and some motivation. However, the presence of a 1D2F structure on is not really an extra requirement: in op. cit., it is proven that every ${\wedge \!\!=}$ -fibration admits a “universal” 1D2F structure, and that, in the case of (for any model category ${\mathbf {C}}$ ), this recovers the familiar 2-category structure on ${\mathbf {C}}_{\mathrm {cf}}$ given in terms of homotopies (and we will show in Section 3.4 that the 2-categorical structure on the total category of also has a natural interpretation in terms of homotopies).

The abstract invariance theorem also involves a second fibration which is free on a signature $\sigma $ in the sense discussed in the introduction, so that the morphisms correspond precisely to interpretations of $\sigma $ in ${\mathbf {C}}'$ (the morphism ${\mathbf {C}}\to {\mathbf {C}}'$ then capturing the unique-up-to-isomorphism interpretation of $\sigma $ in over ${\mathbf {B}}'$ ); moreover, the natural isomorphisms between such morphisms, correspond to isomorphisms of $\sigma $ -interpretations $\sigma \to {\mathbf {B}}$ . As discussed in the introduction, this immediately leads to the isomorphism invariance property for interpretations in . Note that the 1D2F structure on plays no role in this.

Now, when the f.p. category ${\mathbf {B}}$ has a 2-categorical structure, there is a notion of pseudonatural equivalence of interpretations $\sigma \to {\mathbf {B}}'$ , which correspond to homotopy equivalences of interpretations in the case of ${\mathbf {Kan}}$ . On the other hand, we have a notion of pseudonatural equivalence of morphisms , and the existence of one of these between the morphisms induced by two interpretations $\sigma \to {\mathbf {B}}'$ recovers, in the case of , the homotopy invariance property asserted in the special invariance theorem.

The import of the invariance theorem, then, is that the free fibration satisfies with respect to pseudonatural equivalence the same universal property that it satisfies with respect to isomorphisms, i.e., that a pseudonatural equivalence between two interpretations $\sigma \to {\mathbf {B}}'$ induces a pseudonatural equivalence of the induced morphisms . This comprises two parts.

In the first part, we have ${\mathbf {B}}$ being an arbitrary f.p. category, and a free $h^=$ -fibration over ${\mathbf {B}}$ , so that an f.p. morphism ${\mathbf {B}}\to {\mathbf {B}}'$ induces a morphism . The statement is then that a pseudonatural equivalence between two morphisms ${\mathbf {B}}\to {\mathbf {B}}'$ induces a pseudonatural equivalence between the resulting morphisms .

The second part only involves f.p. (2-)categories and makes no reference to fibrations. Namely, here we take ${\mathbf {B}}$ to be free on $\sigma $ , so that each interpretation $\sigma \to {\mathbf {B}}'$ induces an f.p. morphism ${\mathbf {B}}\to {\mathbf {B}}'$ , and the statement is then that a pseudonatural equivalence between interpretations $\sigma \to {\mathbf {B}}'$ induces a pseudonatural equivalence between the induced morphisms ${\mathbf {B}}\to {\mathbf {B}}'$ .

With the abstract invariance theorem in place, we then, in Section 3.4, prove the “special” or “syntactic” invariance theorem which, unlike the abstract invariance theorem, involves the interpretation of terms and formulas in an $h^=$ -fibration, as introduced in Section 2.3. This is deduced easily from the abstract invariance theorem by using the equivalence between the 2-categorical notions present in the abstract invariance theorem and the corresponding “homotopical” notions in the particular 1D2F . Most of this equivalence was proven in or is deduced easily from the work in [8]; however, there is one essential part (namely, the homotopical interpretation of 2-cells in the total category of ) that is missing in op. cit., and which is proven in Section 3.4.

The special invariance theorem is also proven in two “stages” (though these do not correspond to the two parts of the abstract invariance theorem): the first is to draw a general “homotopy-invariance” (or better, “pseudonatural-equivalence-invariance”) conclusion about the interpretation of first-order logic in an arbitrary $h^=$ -fibration , and the second is to specialize this to the case of .

We begin with some preliminaries on 2-categories, and we prove some facts about 1D2Fs that were not considered in [8] (but otherwise, we refer to the latter for general background on 1D2Fs).

3.1 Preliminaries on 2-categories and 1D2Fs

We begin with some generalities on 2-categories and 1D2Fs.

First, we will recall the notion of pseudonatural transformation and equivalence, and some related notions. We note that this is a small part of a larger structure; the totality of 2-categories forms a three-dimensional structure, which is more or less elaborate depending on the weakness or strictness of the concepts being considered. Our approach here is to strive for the minimal possible generality that suffices for our purposes.

We then prove some basic facts that we will need about 1D2Fs. Each of them is a generalization of a basic property of fibrations, in which equality of morphisms is replaced by existence of a 2-cell.

Finally, we give the notion of pseudonatural equivalence of morphisms of fibrations, which will be essential for the formulation of the abstract invariance theorem.

Definition 3.1. Given a category ${\mathbf {C}}$ , a 2-category ${\mathbf {D}}$ , and functors $F,G\colon {\mathbf {C}}\to {\mathbf {D}}$ , a pseudonatural transformation $\alpha \colon {}F\to {}G$ consists of the following data (i)–(ii), subject to the conditions (iii) and (iv):

1. (i) A 1-cell $\alpha _A\colon {}FA\to {}GA$ for each $A\in {\mathbf {C}}$ .

2. (ii) An isomorphism 2-cell

   
   for each morphism $f\colon {}A\to {}B$ in ${\mathbf {C}}$ .

3. (iii) For each pair $A\xrightarrow {f}B\xrightarrow {g}C$ of composable morphisms in ${\mathbf {C}}$ , we have $(\operatorname {\mathrm {1}}_{Gg}\circ \alpha _f)(\alpha _g\circ \operatorname {\mathrm {1}}_{Ff})=\alpha _{gf}$ .

4. (iv) For each $A\in {\mathbf {C}}$ , we have $\alpha _{\operatorname {\mathrm {1}}_A}=\operatorname {\mathrm {1}}_{\alpha _A}$ .

Note that a pseudonatural transformation $\alpha $ with $\alpha _f=\operatorname {\mathrm {1}}$ for all f is just a natural transformation.

Given pseudonatural transformations $F\xrightarrow {\alpha }G\xrightarrow {\beta }H$ , their composite $\beta \circ \alpha $ is defined by the prescriptions $(\beta \circ \alpha )_A=\beta _A\circ \alpha _A$ and $(\beta \circ \alpha )_f=(\beta _f\circ \alpha _A) (\beta _A\circ \alpha _f)$ . We leave it to the reader to verify that this is again a pseudonatural transformation.

A 1-cell $f\colon {}A\to {}B$ in a 2-category is an equivalence if there exists a 1-cell $g\colon {}B\to {}A$ and isomorphism 2-cells $g\circ {}f\cong {}\operatorname {\mathrm {1}}_A$ and $f\circ {}g\cong {}\operatorname {\mathrm {1}}_B$ —such a g is called a quasi-inverse to f. The pseudonatural transformation $\alpha \colon {}F\to {}G$ is a pseudonatural equivalence if $\alpha _A$ is an equivalence in ${\mathbf {D}}$ for each $A\in {\mathbf {C}}$ .

Definition 3.2. Given categories ${\mathbf {B}}$ and ${\mathbf {C}}$ , 2-categories ${\mathbf {D}}$ and $\mathbf {E}$ , functors $F\colon {\mathbf {B}}\to {\mathbf {C}}$ and $G,H\colon {\mathbf {C}}\to {\mathbf {D}}$ , a 2-functor $K\colon {\mathbf {D}}\to \mathbf {E}$ , and a pseudonatural transformation $\alpha \colon {}G\to {}H$ , as in

we define (i) the whiskering of $\alpha $ by K, which we denote by $K\circ \alpha $ , to be the pseudonatural transformation $KG\to {}KH$ defined by $(K\circ \alpha )_A=K(\alpha _A)$ and $(K\circ \alpha )_f=K(\alpha _f)$ for $A\in \operatorname {\mathrm {Ob}}{\mathbf {C}}$ and $f\in \operatorname {\mathrm {Ar}}{\mathbf {C}}$ ; and (ii) the whiskering of $\alpha $ by F, denoted by $\alpha \circ {}F$ , to be the pseudonatural transformation $GF\to {}HF$ defined by $(\alpha \circ {}F)_A=\alpha _{FA}$ and $(\alpha \circ {}F)_f=\alpha _{Ff}$ .

We leave to the reader the easy proof that these are in fact pseudonatural transformations as claimed.

We note that the whiskering of a pseudonatural equivalence (on either side) is again a pseudonatural equivalence.

Proposition 3.3. In a 1D2F, we have the following generalization of the universal property for cartesian morphisms.

Let be a 1D2F, and suppose we have a solid diagram

with q cartesian over g, r lying over h, and $\alpha $ a 2-cell $h\to {}gf$ .

Then there exists a unique 1-cell $p\colon {}P\to {}Q$ over f for which there exists a (necessarily unique) 2-cell $r\to {}qp$ over $\alpha $ .

Proof We know that there is a unique 2-cell $\sigma \colon {}r\to {}r'$ over $\alpha $ with domain r, and we can (and must) then take p to be unique morphism $P\to {}Q$ over f such that $qp=r'$ :

Proposition 3.4. Next, we have a generalization in 1D2Fs of the uniqueness up to isomorphism of cartesian morphisms in fibrations.

Given a 1D2F and a diagram

in which r, p, q, $\sigma $ lie over $\operatorname {\mathrm {1}}_A$ , f, g, $\alpha $ , respectively, and p and q are cartesian: if $\alpha $ (and hence $\sigma $ ) is an isomorphism 2-cell, then r is an isomorphism 1-cell.

Proof By Proposition 3.3, there is a unique morphism $r'\colon {}Q\to {}P$ over A for which there exists a (necessarily unique) 2-cell $\sigma '\colon {}q\to {}pr'$ over $\alpha ^{-1}$ :

Then $r'r$ and $\operatorname {\mathrm {1}}_P$ are both the unique morphism $t\colon {}P\to {}P$ over $\operatorname {\mathrm {1}}_A$ for which there exists a 2-cell $p\to {}pt$ ; hence $r'r=\operatorname {\mathrm {1}}_P$ . Similarly, $rr'=\operatorname {\mathrm {1}}_Q$ .

Proposition 3.5. We also have a generalization in 1D2Fs of the “2-of-3” property of cartesian morphisms in fibrations.

Given a 1D2F and a diagram

with p, q, r, $\sigma $ lying over f, g, h, $\alpha $ , respectively, if $\alpha $ (and hence $\sigma $ ) is invertible, and q and r are cartesian, then so is p.

Proof Choosing a cartesian lift ${\uparrow }\colon {}f^*Q\to {}Q$ of f, we obtain a factorization $p=\ {\uparrow }\overline {p}$ as in

It then follows from Proposition 3.4 that $\overline {p}$ is an isomorphism, and hence that p is cartesian.

Definition 3.6. Let be a fibration, be a 1D2F, ${\varphi },\psi \colon {\mathbf {B}}\to {}{\mathbf {B}}'$ functors, and $\Phi ,\Psi \colon {\mathbf {C}}\to {}{\mathbf {C}}'$ functors lying over ${\varphi }$ and $\psi $ . We say that a pseudonatural transformation $\beta \colon \Phi \to \Psi $ lies over a pseudonatural transformation $\alpha \colon {\varphi }\to \psi $ if (here we are using the “whiskering” operations from Definition 3.2).

3.2 The abstract invariance theorem: first part

We now come to the proof of the (first part of the) abstract version of the homotopy-invariance property. In this generality, the theorem states that a free $h^=$ -fibration satisfies with respect to pseudonatural transformations the same property which it satisfies with respect to natural transformations.

We make a small digression to discuss freeness. In classical (“0-categorical”) algebra, a free object (group, ring, etc.) is required to satisfy a certain universal property, which then determines it up to isomorphism. In the case of categorical structures, it is often more natural to impose conditions that determine the object under consideration up to equivalence. However, there are usually different conditions which do this.

In the case at hand, namely that of being a free $h^=$ -fibration over ${\mathbf {B}}$ , the weakest such condition one could impose is that, for any other $h^=$ -fibration over ${\mathbf {B}}$ , there exists a morphism of fibrations over ${\mathbf {B}}$ , and that, any two such morphisms are isomorphic; and this is in fact the definition we use.

A slightly stronger condition one could demand is that, given any $h^=$ -fibration , any f.p. functor ${\varphi }\colon {\mathbf {B}}\to {}{\mathbf {B}}'$ can be extended to a morphism of $h^=$ -fibrations, and for any natural isomorphism ${\varphi }\to {}\psi $ to another f.p. functor, there is a natural isomorphism $\Phi \to \Psi $ lying over it; let us call this the global universal property, and the previous one the local universal property.

One can see that a free $h^=$ -fibration (in the above sense—i.e., satisfying the local universal property) automatically satisfies the global universal property. The invariance theorem then says that, when is a 1D2F, satisfies the global universal property with respect to pseudonatural equivalences and not just natural isomorphisms.

The proof of the global universal property from the local one is more or less the same for natural isomorphisms and for pseudonatural equivalences—indeed, we will prove both of them simultaneously—and proceeds (roughly) by pulling back the fibration along the given functors ${\varphi },\psi \colon {\mathbf {B}}\to {}{\mathbf {B}}'$ and then appealing to the universal property of with respect to $h^=$ -fibrations over ${\mathbf {B}}$ .

An essential step here is showing that the natural isomorphism or pseudonatural equivalence ${\varphi }\to \psi $ induces an equivalence of fibrations over ${\mathbf {B}}$ between the pullbacks. It is easy to see why this should work for pseudonatural transformations and not just natural transformations, if we look at the situation from the “pseudo-functor to ${\mathbf {Cat}}$ ” perspective on fibrations (see, e.g., [8, Section 6]). Namely, from this perspective, the pullback of a fibration along a morphism ${\varphi }\colon {\mathbf {B}}\to {\mathbf {B}}'$ is just given by composing ${\varphi }^{\operatorname {op}}\colon {\mathbf {B}}^{\operatorname {op}}\to {\mathbf {B}}^{\prime \operatorname {op}}$ with the pseudo-functor . On the other hand, a morphism of fibrations over ${\mathbf {B}}$ corresponds to a pseudonatural transformation of pseudo-functors from ${\mathbf {B}}^{\operatorname {op}}$ to ${\mathbf {Cat}}$ . Hence, given a natural isomorphism $\alpha \colon {\varphi }\to \psi $ , the induced equivalence between the pullbacks along ${\varphi }$ and $\psi $ is obtained as the whiskering

The point is now that this whiskering can be carried out just as well if $\alpha $ is a pseudo-natural transformation.

Definition 3.7. Given a prefibration and a functor $F\colon {\mathbf {B}}\to {\mathbf {B}}'$ , we define the pullback of along F to be the usual pullback

in the (1-)category of categories, where we write ${{F}^{\uparrow }{{\mathbf {C}}'}}$ , as indicated, for the associated functor $F^*{\mathbf {C}}'\to {\mathbf {C}}'$ . Explicitly, the objects of $F^*{\mathbf {C}}'$ are pairs $(A,P)$ with $A\in {\mathbf {B}}$ and , and the morphisms are pairs $(f,p)$ with $f\in \operatorname {\mathrm {Ar}}{\mathbf {B}}$ and $p\in \operatorname {\mathrm {Ar}}{\mathbf {C}}'$ lying over $Ff$ .

The prefibration is a fibration if is, and inherits many properties from —in particular, if ${\mathbf {B}}$ is an f.p. category and F is an f.p. functor, then if is an $h^=$ -fibration, is as well. The reason is that ${{F}^{\uparrow }{{\mathbf {C}}'}}$ induces isomorphisms on fibers for each $A\in {\mathbf {B}}$ , and—if is a fibration—a morphism in $F^*{\mathbf {C}}'$ is cartesian or cocartesian if and only if its image under ${F^{\uparrow }{\mathbf {C}}}'$ is, and similarly the $\prod $ -diagrams in $F^*{\mathbf {C}}'$ are exactly those whose images under ${{F}^{\uparrow } C'}$ are $\prod $ -diagrams. In particular, $({{F}^{\uparrow }{\mathbf {C}}}',F)$ is a morphism of $(h^=)$ -fibrations.

By the universal property of the pullback, given any other prefibration over ${\mathbf {B}}$ and any morphism of prefibrations, we have a unique morphism of prefibrations over ${\mathbf {B}}$ such that ${{F}^{\uparrow }{\mathbf {C}}}'\cdot \overline {\Phi }=\Phi $ . It follows from the above observations that $\overline {\Phi }$ is a morphism of ( $h^=$ -)fibrations whenever and are ( $h^=$ -)fibrations and $(\Phi ,{\varphi })$ is a morphism thereof.

If is a 1D2F, then we define to be the pullback of the underlying fibration of (thus is a fibration of 1-categories).

Construction 3.8. Let ${\mathbf {B}}$ be a category, let be a cloven 1D2F (i.e., the underlying fibration is cloven [8, Section 1.3]), let $F,G\colon {\mathbf {B}}\to {}{\mathbf {B}}'$ be functors, and let $\alpha \colon {}F\to {}G$ be a pseudonatural transformation. We will construct from this a morphism of fibrations over ${\mathbf {B}}$ between the associated pullback fibrations, as well as a pseudonatural transformation ${\check {\alpha }}\colon {{F}^{\uparrow }{\mathbf {C}}}'\circ {\tilde {\alpha }}\to {{G}^{\uparrow }{\mathbf {C}}}'$ over $\alpha $ , as shown below. We will define these simultaneously.

Given $A\in {\mathbf {B}}$ and (i.e., ), we set , and we set ${\check {\alpha }}_{(A,P)}$ to be the morphism ${{(\alpha _A)}^{\uparrow }P}\colon \alpha _A^*P\to {}P$ .

Next, let $(f,p)\colon (A,P)\to (B,Q)$ be a morphism in $G^*{\mathbf {C}}'$ . Since we want ${\tilde {\alpha }}(f,p)$ to be a morphism over $f\colon {}A\to {}B$ in ${\mathbf {B}}$ , it must be of the form $(f,p')$ for some $p'\colon (\alpha _A)^*P\to {}(\alpha _A)^*Q$ over $Ff$ . Seeing as we want there to be a 2-cell

$$\begin{align*}{\check{\alpha}}_{(f,p)}\colon {\check{\alpha}}_{(B,Q)}\cdot({{F}^{\uparrow}{\mathbf{C}}}')({\tilde{\alpha}}(f,p)) ={{(\alpha_B)}^{\uparrow}Q}\cdot{}p' \longrightarrow p\cdot{{(\alpha_A)}^{\uparrow}P} =({{G}^{\uparrow}{\mathbf{C}}}')(f,p)\cdot{\check{\alpha}}_{(A,P)} \end{align*}$$

lying over $\alpha _f$ , we see that we are forced to define $p'$ to be the unique morphism over $Ff$ for which there exists a 2-cell

lying over $\alpha _f$ (such a $p'$ exists by Proposition 3.3 since $\alpha _{f}$ is invertible), and we must take ${\check {\alpha }}_f$ to be this 2-cell lying over $\alpha _f$ .

We now prove simultaneously that ${\tilde {\alpha }}$ is a functor and that ${\check {\alpha }}$ is a pseudonatural transformation.

Let $(A,P)\xrightarrow {(f,p)}(B,Q)\xrightarrow {(g,q)}(C,R)$ be morphisms in $G^*{\mathbf {C}}'$ . Let us write $(f,p')$ and $(g,q')$ for ${\tilde {\alpha }}(f,p)$ and ${\tilde {\alpha }}(g,q)$ , as well as $(gf,(qp)')$ for ${\tilde {\alpha }}(gf,qp)$ . We must show that the 2-cells

are equal—i.e., that $(\operatorname {\mathrm {1}}_q\circ {}{\check {\alpha }}_{(f,p)})({\check {\alpha }}_{(g,q)}\circ {}\operatorname {\mathrm {1}}_{p'})={\check {\alpha }}_{(gf,qp)}$ —and also that $q'p'=(qp)'$ . The first claim follows at once from the second by 1-discreteness. The second claim is true since $(qp)'$ is by definition the unique morphism $\alpha _A^*P\to \alpha _C^*R$ over $F(gf)$ for which there exists a 2-cell as above on the right, and $q'p'$ also has this property.

The proof of the remaining (unitality) property of ${\tilde {\alpha }}$ and ${\check {\alpha }}$ is similar.

Finally, we must see that ${\tilde {\alpha }}$ preserves cartesian morphisms. This follows from the definition of ${\tilde {\alpha }}$ , Proposition 3.5, and the fact that a morphism $(f,p)$ in $F^*{\mathbf {C}}'$ is cartesian if and only if p is.

Definition 3.9. A morphism is a fiberwise equivalence if the induced functor is an equivalence for each $A\in {\mathbf {B}}$ .

Proposition 3.10. With , F, G, and $\alpha $ as in Construction 3.8, if $\alpha $ is a pseudonatural equivalence, then ${\tilde {\alpha }}$ is a fiberwise equivalence and ${\check {\alpha }}$ is a pseudonatural equivalence.

Also, if $\alpha $ is natural transformation or natural isomorphism, then so is ${\check {\alpha }}$ .

Proof To see that ${\tilde {\alpha }}$ is a fiberwise equivalence, note that the induced functor is (with respect to the identifications and ) just the pullback functor . This is an equivalence, since, given a quasi-inverse $\beta _A$ for $\alpha _A$ , we obtain a quasi-inverse $(\beta _A)^*$ for $(\alpha _A)^*$ .

We now prove that ${\check {\alpha }}$ is a pseudonatural equivalence. Since each $\alpha _A$ is an equivalence in ${\mathbf {B}}'$ and each ${\check {\alpha }}_A$ is a cartesian lift of $\alpha _A$ , it suffices to prove that any cartesian lift of an equivalence in a 1D2F is again an equivalence.

Let $f\colon {}A\to {}B$ be an equivalence with quasi-inverse $g\colon {}B\to {}A$ , so that there exist isomorphism 2-cells $\alpha \colon \operatorname {\mathrm {1}}_A{\xrightarrow {{}_{\sim }}}{}gf$ and $\beta \colon \operatorname {\mathrm {1}}_B{\xrightarrow {{}_{\sim }}}{}fg$ , and let $p\colon {}P\to {}Q$ be a cartesian lift of f. By Proposition 3.3, there exists a unique morphism $q\colon {}Q\to {}P$ over g for which there exists a (necessarily invertible) 2-cell $\operatorname {\mathrm {1}}_Q{\xrightarrow {{}_{\sim }}}{}pq$ over $\beta $ . It remains to see that $qp\cong \operatorname {\mathrm {1}}_P$ . By Proposition 3.5, q is cartesian, and hence, by the argument we just gave, there exists $p'\colon {}P\to {}Q$ with $qp'\cong \operatorname {\mathrm {1}}_P$ . We then have $p\cong {}pqp'\cong {}p'$ and hence $qp\cong {}qp'\cong \operatorname {\mathrm {1}}_P$ .

The last statement follows immediately from the construction of ${\check {\alpha }}$ and the fact that any cartesian lift of an isomorphism is an isomorphism.

Definition 3.11. An $h^=$ -fibration is free over ${\mathbf {B}}$ if, for any $h^=$ -fibration over ${\mathbf {B}}$ , there is up to isomorphism a unique morphism of $h^=$ -fibrations over ${\mathbf {B}}$ ; i.e., there exists such a morphism, and for any two such, there exists a natural isomorphism over ${\mathbf {B}}$ between them. ¹³

In Appendix A, it is shown that there exists a free $h^=$ -fibration over any f.p. category ${\mathbf {B}}$ .

We see from the definition that any two free $h^=$ -fibrations over ${\mathbf {B}}$ are equivalent over ${\mathbf {B}}$ .

We will now show that any such also satisfies a universal property with respect to any $h^=$ -fibration (with possibly different base ${\mathbf {B}}'$ ).

Proposition 3.12. If is a free $h^=$ -fibration over ${\mathbf {B}}$ and is any $h^=$ -fibration, then for any f.p. functor ${\varphi }\colon {\mathbf {B}}\to {\mathbf {B}}'$ , there exists a morphism of $h^=$ -fibrations over ${\varphi }$ . Moreover (though we will not need this), $\Phi $ is determined uniquely up to natural isomorphism over ${\varphi }$ .

Proof Taking the pullback of along ${\varphi }$ , we have by the discussion in Definition 3.7 that is an $h^=$ -fibration. Hence, by the freeness of , we then have a morphism of $h^=$ -fibrations over ${\mathbf {B}}$ . Since the composite of morphism of $h^=$ -fibrations is again one, $({{{\varphi }}^{\uparrow }{{\mathbf {C}}'}}\circ \Psi ,{\varphi })$ is as desired.

For uniqueness: given morphisms of $h^=$ -fibrations, by the universal property of , we have morphisms over ${\mathbf {B}}$ with $\Phi ={{{\varphi }}^{\uparrow }{{\mathbf {C}}'}}\circ \Psi '$ and $\Phi '={{{\varphi }}^{\uparrow }{{\mathbf {C}}'}} \circ \Psi '$ . By the freeness of , we have a natural isomorphism $\Psi {\xrightarrow {{}_{\sim }}}\Psi '$ over ${\mathbf {B}}$ , and whiskering with ${{{\varphi }}^{\uparrow }{{\mathbf {C}}'}}$ gives a natural isomorphism $\Phi {\xrightarrow {{}_{\sim }}}\Phi '$ over ${\varphi }$ as desired.

Theorem 3.13. Suppose is a free $h^=$ -fibration, is a 1D2F which is also an $h^=$ -fibration, are morphisms of $h^=$ -fibrations, and $\alpha \colon {\varphi }\to \psi $ is a pseudonatural equivalence.

Then there exists a pseudonatural equivalence $\Phi \to \Psi $ lying over $\alpha $ (which, if $\alpha $ is a natural isomorphism, can be taken to be a natural isomorphism).

In particular, for each $P\in {\mathbf {C}}$ over some $A\in {\mathbf {B}}$ , there is an equivalence $p\colon \Phi {}P\to \Psi {}P$ lying over the equivalence $\alpha _A\colon {\varphi }{}A\to \psi {}A$ (note that the natural additional condition that p have a quasi-inverse q lying over a quasi-inverse of $\alpha _A$ , so that the associated 2-cells $\operatorname {\mathrm {1}}_{\Phi {}P}{\xrightarrow {{}_{\sim }}}{}qp$ and $\operatorname {\mathrm {1}}_{\Psi {}P}{\xrightarrow {{}_{\sim }}}{}pq$ in ${\mathbf {C}}$ lie over the corresponding ones in ${\mathbf {B}}$ —cf. Definition 2.25—is satisfied automatically)—and if $\alpha $ (and hence each $\alpha _A$ ) is an isomorphism, then p can be taken to be one as well.

Proof To begin, we choose a cleavage of (which we can do by the axiom of choice—otherwise, we must assume explicitly that admits a cleavage). Consider the pullbacks of along ${\varphi }$ and $\psi $ . We then have the situation depicted in Construction 3.8, with $F={\varphi }$ and $G=\psi $ . By Proposition 3.10 the morphism of fibrations is a fiberwise equivalence and hence, by Lemma 3.14, a morphism of $h^=$ -fibrations.

By the definition of the pullback, we have morphisms of fibrations and over ${\mathbf {B}}$ such that ${{{\varphi }}^{\uparrow }{\mathbf {C}}}'\circ \overline \Phi =\Phi $ and ${{\psi }^{\uparrow }{\mathbf {C}}}'\circ \overline \Psi =\Psi $ —and by the discussion in Definition 3.8, these are morphisms of $h^=$ -fibrations. Hence, since the composite of morphisms of $h^=$ -fibrations over ${\mathbf {B}}$ is again one, we have that is a morphism of $h^=$ -fibrations. Hence, by the freeness of , we have a natural isomorphism $\eta \colon \overline {\Phi }\to {\tilde {\alpha }}\overline {\Psi }$ of morphisms of $h^=$ -fibrations over ${\mathbf {B}}$ :

Hence, the “pasting” of $\eta $ and ${\check {{\alpha }}}$ —i.e., the composite pseudonatural transformation $({\check {\alpha }}\circ \operatorname {\mathrm {1}}_{\overline {\Psi }})\circ (\operatorname {\mathrm {1}}_{{{{\varphi }}^{\uparrow }{{\mathbf {C}}'}}}\circ \eta )$ —is as desired (since it is an equivalence and lies over $\alpha $ ).

In case $\alpha $ is a natural isomorphism, then Proposition 3.10 says that ${\check {\alpha }}$ is a natural isomorphism, and hence so is the pasting of $\eta $ and ${\check {\alpha }}$ .

Lemma 3.14. Suppose and are $h^=$ -fibrations, and is a morphism of fibrations which is a fiberwise equivalence with ${\varphi }$ an f.p. functor. Then $(\Phi ,{\varphi })$ is a morphism of $h^=$ -fibrations.

Proof ${\varphi }$ is product-preserving by assumption, and the induced functors are clearly bi-cartesian closed since they are equivalences. Hence, it only remains to see that the relevant co-cartesian morphisms and $\prod $ -diagrams are preserved.

In fact, all co-cartesian morphisms and $\prod $ -diagrams are preserved. This follows easily from the fact that, in the present situation, given a morphism $f\colon {}A\to {B}$ in ${\mathbf {B}}$ and objects P and Q in and , $\Phi $ induces a bijection between morphisms $P\to {Q}$ lying over f and morphisms $\Phi {P}\to \Phi {Q}$ lying over ${\varphi }{f}$ , and moreover that $p\colon {}P\to {Q}$ is cartesian if and only if $\Phi {}p$ is.

3.3 The abstract invariance theorem: second part

The theorem proven in the previous section was stated with respect to an arbitrary free $h^=$ -fibration over an f.p. category ${\mathbf {B}}$ . However, in practice, we are interested in the particular case of ${\mathbf {B}}$ being a free f.p. category on a given signature $\sigma $ .

As mentioned above, the definition of the latter is arranged so that the f.p. functors ${\mathbf {B}}\to {\mathbf {B}}'$ correspond precisely to the interpretations $\sigma \to {\mathbf {B}}'$ , and so that the natural isomorphisms between functors ${\mathbf {B}}\to {\mathbf {B}}'$ correspond to isomorphisms of interpretations $\sigma \to {\mathbf {B}}'$ .

However, for the purpose of the homotopy invariance for the homotopical semantics, we will want to start with a homotopy equivalence of interpretations $\sigma \to {\mathbf {B}}'$ —which, in the context of a general 2-category ${\mathbf {B}}'$ , corresponds to a pseudonatural equivalence of interpretations $\sigma \to {\mathbf {B}}'$ (Definition 3.18).

Hence, the second part of the abstract invariance theorem will show that a pseudonatural equivalence of interpretations $\sigma \to {\mathbf {B}}'$ induces a pseudonatural equivalence between the induced functors ${\mathbf {B}}\to {\mathbf {B}}'$ . Note that this is analogous to the first part: in both cases, we have a universal property with respect to natural isomorphisms, and want to show that it still holds for pseudonatural equivalences.

The proof proceeds by considering a modified arrow category ${{({\mathbf {B}}')}^{\overset {\sim }{\rightsquigarrow }}}$ , such that the f.p. functors into ${{({\mathbf {B}}')}^{\overset {\sim }{\rightsquigarrow }}}$ are pseudonatural equivalences of f.p. functors into ${\mathbf {B}}'$ , and the $\sigma $ -interpretations in ${{({\mathbf {B}}')}^{\overset {\sim }{\rightsquigarrow }}}$ are homotopy-equivalences of $\sigma $ -interpretations into ${\mathbf {B}}'$ ; this reduces the claim to the original freeness property of ${\mathbf {B}}$ .

Definition 3.15. Given a 2-category ${\mathbf {C}}$ , we define ${{\mathbf {C}}}^{\rightsquigarrow }$ , the pseudo-arrow category of ${\mathbf {C}}$ , to have as objects functors $\mathbf {2}\to {\mathbf {C}}$ —i.e., 1-cells in ${\mathbf {C}}$ —and to have as morphisms pseudonatural transformations, with composition being given by composition of pseudonatural transformations which, as we leave to the reader to verify, is associative and has identities

In other words a morphism $\alpha $ from $f_1\colon {}A_1\to {}B_1$ to $f_2\colon {}A_2\to {}B_2$ in ${\mathbf {C}}^{\rightsquigarrow }$ is a triple $(\alpha _A,\alpha _B,\alpha _f)$ with $\alpha _A\colon {}A_1\to {}A_2$ , $\alpha _B\colon {}B_1\to {}B_2$ , and $\alpha _f\colon \alpha _B\circ {}f_1\xrightarrow {\sim }f_2\circ {}\alpha _A$ .

There are obvious domain and codomain functors $\operatorname {\mathrm {dom}},\operatorname {\mathrm {cod}}\colon {\mathbf {C}}^{\rightsquigarrow }\to {\mathbf {C}}$ .

We define ${{\mathbf {C}}^{\overset {\sim }{\rightsquigarrow }}}$ to be the full subcategory of ${\mathbf {C}}^{\rightsquigarrow }$ with objects the equivalences in ${\mathbf {C}}$ .

Proposition 3.16. Given a 2-category ${\mathbf {C}}$ , if ${\mathbf {C}}$ has finite 2-categorical products (see [8, Definition 7.1]), then the categories ${\mathbf {C}}^{\rightsquigarrow }$ and ${{\mathbf {C}}^{\overset {\sim }{\rightsquigarrow }}}$ have finite products. Moreover, the inclusion functor ${{\mathbf {C}}^{\overset {\sim }{\rightsquigarrow }}}\hookrightarrow {\mathbf {C}}^{\rightsquigarrow }$ , as well as the functors $\operatorname {\mathrm {dom}},\operatorname {\mathrm {cod}}\colon {\mathbf {C}}^{\rightsquigarrow }\to {\mathbf {C}}$ , are f.p. functors.

Proof Given 1-cells $g\colon {}A\to {}C$ and $h\colon {}B\to {}D$ and products $A\times {}B$ and $C\times {}D$ in ${\mathbf {C}}$ , we will show that the morphisms $g\times {}h\to {}g$ and $g\times {}h\to {}h$ in ${\mathbf {C}}^{\rightsquigarrow }$ given by $(\pi _1,\pi _1,\operatorname {\mathrm {1}}_{g\pi _1})$ and $(\pi _2,\pi _2,\operatorname {\mathrm {1}}_{h\pi _2})$ exhibit $g\times {}h$ as a product of g and h. It follows that $\operatorname {\mathrm {dom}}$ and $\operatorname {\mathrm {cod}}$ are f.p.

Given a 1-cell $f\colon {}X\to {}Y$ in ${\mathbf {C}}$ and morphisms $(s,t,\alpha )\colon {}f\to {}g$ and $(u,v,\beta )\colon {}f\to {}h$ in ${\mathbf {C}}^{\rightsquigarrow }$ , we must show that there is a unique morphism $(w,x,\gamma )\colon {}f\to {}g\times {}h$ such that $\pi _1w=s$ , $\pi _2w=u$ , $\pi _1x=t$ , $\pi _2x=v$ , $\operatorname {\mathrm {1}}_{\pi _1}\circ \gamma =\alpha $ , and $\operatorname {\mathrm {1}}_{\pi _2}\circ \gamma =\beta $ . Clearly, we must take $w={\langle {{s,u}}\rangle }$ and $x={\langle {{t,v}}\rangle }$ . Then, since $C\times {}D$ is a 2-categorical product, there is a unique 2-cell $\gamma \colon {\langle {{gs,hu}}\rangle }\to {\langle {{tf,vf}}\rangle }$ such that $\operatorname {\mathrm {1}}_{\pi _1}\circ \gamma =\alpha $ and $\operatorname {\mathrm {1}}_{\pi _2}\circ \gamma =\beta $ .

Finally, we must see that if f and g are equivalences in ${\mathbf {C}}$ , then $f\times {}g$ is one as well. In fact, if $f^{-1}$ and $g^{-1}$ are quasi-inverses to f and g, then $f^{-1}\times {}g^{-1}$ is easily seen to be a quasi-inverse to $f\times {}g$ .

Proposition 3.17. Given a category ${\mathbf {C}}$ , a 2-category ${\mathbf {D}}$ , and functors $F,G\colon {\mathbf {C}}\to {\mathbf {D}}$ , the functors F and G are pseudonaturally equivalent if and only if there exists a functor $H\colon {\mathbf {C}}\to {{\mathbf {D}}^{\overset {\sim }{\rightsquigarrow }}}$ such that $\operatorname {\mathrm {dom}}\circ {}H=F$ and $\operatorname {\mathrm {cod}}\circ {}H=G$ .

Proof The proof is by inspection, the point being that the data of a functor $H\colon {\mathbf {C}}\to {{\mathbf {D}}^{\overset {\sim }{\rightsquigarrow }}}$ are precisely the data of a pseudonatural equivalence $\operatorname {\mathrm {dom}}\circ {}H\to \operatorname {\mathrm {cod}}\circ {}H$ , and the condition that H be a functor is equivalent to the given data defining a pseudonatural transformation.

Definition 3.18. Given a signature $\sigma $ and a 2-category ${\mathbf {C}}$ with finite 2-categorical products, the underlying category of ${\mathbf {C}}$ also has finite products, and we can consider interpretations $\sigma \to {\mathbf {C}}$ . Given two such interpretations $M,N\colon \sigma \to {\mathbf {C}}$ , a pseudohomomorphism $\alpha \colon {}M\to {}N$ consists of a 1-cell $\alpha _A\colon {}M\to {}N$ for each $A\in \operatorname {\mathrm {Ob}}\sigma $ , such that there exists an invertible 2-cell $\alpha _B\circ {}Mf\to {}Nf\circ \alpha _{\vec {A}}$ for each $f\in \sigma (\vec {A},B)$ (where $\alpha _{\vec {A}}$ is defined as in Definition 2.24).

A pseudonatural homomorphism $\alpha \colon {}M\to {}N$ is a pseudoequivalence ¹⁴ if $\alpha _A$ is an equivalence in ${\mathbf {C}}$ for each $A\in \operatorname {\mathrm {Ob}}\sigma $ . If such an $\alpha $ exists, we say that M and N are pseudoequivalent.

Note that when ${\mathbf {C}}$ is the category of cofibrant-fibrant objects in a model category, endowed with the Quillen 2-categorical structure [8, Definition 15.7], then the notions of pseudohomomorphism and pseudoequivalence specialize to those of homotopy homomorphism and homotopy equivalence (Definition 2.24).

Proposition 3.19. Two interpretations $M,N\colon \sigma \to {\mathbf {C}}$ are pseudoequivalent if and only if there exists an interpretation $H\colon \sigma \to {{\mathbf {C}}^{\overset {\sim }{\rightsquigarrow }}}$ such that $\operatorname {\mathrm {dom}}\circ {}H=M$ and $\operatorname {\mathrm {cod}}\circ {}H=N$ .

Proof Given a pseudoequivalence $\alpha \colon {}M\to {}N$ , we define the interpretation $H\colon \sigma \to {{\mathbf {C}}^{\overset {\sim }{\rightsquigarrow }}}$ by setting $HA=\alpha _A\colon {}MA\to {}NA$ for $A\in \operatorname {\mathrm {Ob}}\sigma $ ; $H\vec {A}=\alpha _{\vec {A}}\colon {}M\vec {A}\to {}N\vec {A}$ and $\pi _i^H=(\pi _i^M,\pi _i^N,\operatorname {\mathrm {1}})$ for $\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$ ; and for $f\in \sigma (\vec {A},B)$ , we take $Hf$ to be $(Mf,Nf,\beta )$ , where $\beta \colon \alpha _B\circ {}Mf\to {}Nf\circ \alpha _{\vec {A}}$ is any invertible 2-cell (which exists since $\alpha _A$ is a pseudohomomorphism).

The proof of the converse (which we will not need) is similar; given H, we define $\alpha _A=HA$ for $A\in \operatorname {\mathrm {Ob}}\sigma $ . The fact that $\alpha $ satisfies the required property then follows from the existence of the morphisms $Hf\in \operatorname {\mathrm {Ar}}{\mathbf {C}}^{\rightsquigarrow }$ for $f\in \sigma (\vec {A},B)$ , and the fact that $H\vec {A}$ and $\alpha _{\vec {A}}$ are isomorphic (but not necessarily equal!) for each $\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$ .

Definition 3.20. Given a signature $\sigma $ and an f.p. category ${\mathbf {C}}$ , the interpretations $\sigma \to {\mathbf {C}}$ and homomorphisms form a category in an obvious manner, which we denote by $\operatorname {Int}(\sigma ,{\mathbf {C}})$ .

Given two f.p. functors $F,G\colon {\mathbf {C}}\to {\mathbf {D}}$ and a natural transformation $\alpha \colon {}F\to {}G$ , we have the interpretations $F\circ M,G\circ M\colon \sigma \to {\mathbf {D}}$ , and we obtain a homomorphism $\alpha \circ {}M\colon {}F\circ {}M\to {}G\circ {}M$ by setting $(\alpha \circ {}M)_A=\alpha _{MA}$ .

This defines, for each $M\colon \sigma \to {\mathbf {C}}$ , a functor $(\text {--}\circ M)\colon \operatorname {\mathrm {FPFun}}({\mathbf {C}},{\mathbf {D}})\to \operatorname {Int}(\sigma ,{\mathbf {D}})$ .

Given an interpretation $i\colon \sigma \to {\mathbf {C}}$ , we say that the f.p. category ${\mathbf {C}}$ is free on $\sigma $ (via i) if $(\text {--}\circ i)\colon \operatorname {\mathrm {FPFun}}({\mathbf {C}},{\mathbf {D}})\to \operatorname {Int}(\sigma ,{\mathbf {D}})$ is an isomorphism of categories for each f.p. category ${\mathbf {D}}$ . ¹⁵ Note that this property determines ${\mathbf {C}}$ up to isomorphism.

It is well-known that there exists a free f.p. category on any signature $\sigma $ (see Proposition A.6 in Appendix A).

Theorem 3.21. Let ${\mathbf {C}}$ be a free f.p. category on the algebraic signature $\sigma $ via $i\colon \sigma \to {\mathbf {C}}$ , and let $M,N\colon \sigma \to {\mathbf {D}}$ be two interpretations into an f.p. 2-category ${\mathbf {D}}$ . Then M and N are pseudoequivalent if and only if the induced f.p. functors $\widetilde {M},\widetilde {N}\colon {\mathbf {C}}\to {\mathbf {D}}$ are pseudonaturally equivalent.

Moreover, for any pseudoequivalence $\alpha \colon M\to N$ , there is a pseudonatural equivalence $\tilde \alpha \colon \widetilde {M}\to \widetilde {N}$ with $\tilde \alpha _{iA}=\alpha _{A}$ for all $A\in \operatorname {\mathrm {Ob}}\sigma $ (and vice versa).

Proof We have, by definition, that $\widetilde {M}\circ {}i=M$ and $\widetilde {N}\circ {}i=N$ .

Given a pseudonatural equivalence $\tilde \alpha \colon \widetilde {M}\to \widetilde {N}$ , we thus have a pseudoequivalence

$$\begin{align*}M=\widetilde{M}\circ{}i\xrightarrow {\tilde\alpha\circ{}i}\widetilde{N}\circ{}i=N, \end{align*}$$

where $\tilde \alpha \circ {}i$ is the pseudoequivalence given by $(\tilde \alpha \circ {}i)_A=\tilde \alpha _{iA}$ for each $A\in \operatorname {\mathrm {Ob}}\sigma $ . To see that $(\tilde \alpha \circ i)_B\circ Mf\cong Nf\circ (\tilde \alpha \circ i)_{\vec {A}}$ for $f\in \sigma (\vec {A},B)$ , first note that $(\tilde \alpha \circ i)_B\circ Mf=\tilde \alpha _{iB}\circ \widetilde {M}(if)\cong \widetilde {N}(if)\circ \tilde \alpha _{i\vec {A}}= Nf\circ \tilde \alpha _{i\vec {A}}$ by pseudonaturality of $\tilde \alpha $ . But one can also see that $\tilde \alpha _{i\vec {A}}\cong (\tilde \alpha \circ i)_{\vec {A}}$ using the pseudonaturality of $\tilde \alpha $ , the product-preservation of N, and the 2-categorical universal property of the product $N\vec {A}$ , and hence $Nf\circ \alpha _{i\vec {A}}\cong Nf\circ (\alpha \circ i)_{\vec {A}}$ .

Conversely, given a pseudoequivalence $\alpha \colon {}M\to {}N$ , we have by Proposition 3.19 an interpretation $H\colon \sigma \to {}{{\mathbf {D}}^{\overset {\sim }{\rightsquigarrow }}}$ with $\operatorname {\mathrm {dom}}\circ {}H=M$ and $\operatorname {\mathrm {cod}}\circ {}H=N$ . Hence, we have an induced f.p. functor $\widetilde {H}\colon {\mathbf {C}}\to {{\mathbf {D}}^{\overset {\sim }{\rightsquigarrow }}}$ with $\widetilde {H}\circ {}i=H$ and hence

$$\begin{align*}(\operatorname{\mathrm{dom}}\circ\widetilde{H})\circ{}i=M\quad\text{and}\quad (\operatorname{\mathrm{cod}}\circ\widetilde{H})\circ{}i=N \end{align*}$$

(here, we are using that composition of f.p. functors is associative with composition of an interpretation and an f.p. functor). Hence, using the freeness of ${\mathbf {C}}$ again, we have $\operatorname {\mathrm {dom}}\circ \widetilde {H}=\widetilde {M}$ and $\operatorname {\mathrm {cod}}\circ \widetilde {H}=\widetilde {N}$ . By Proposition 3.17, we have a pseudonatural equivalence $\tilde {\alpha }\colon \operatorname {\mathrm {dom}}\circ \widetilde {H}\to \operatorname {\mathrm {cod}}\circ \widetilde {H}$ , and hence we obtain the desired pseudonatural equivalence

$$\begin{align*}\widetilde{M}= \operatorname{\mathrm{dom}}\circ\widetilde{H}\xrightarrow {\tilde\alpha} \operatorname{\mathrm{cod}}\circ\widetilde{H}= \widetilde{N}. \end{align*}$$

The “moreover” statement is clear from the two constructions just given.

3.4 The special invariance theorem

We now show how to derive syntactic conclusions from the abstract invariance theorem. This follows the general pattern in abstract/categorical logic (described, for example, in [22]) of a theorem about syntax and a purely algebraic theorem being related by an appropriate “translation” theorem, describing the relationship between the algebraic structures and the syntax being considered.

In the present case, if we were to follow the usual procedure, this would involve showing that the free f.p. category ${\mathbf {B}}$ on a signature $\sigma $ and the free $h^=$ -fibration over ${\mathbf {B}}$ can be constructed “out of the syntax” of first-order logic over $\sigma $ —specifically, in such a way that the morphisms of ${\mathbf {B}}$ are given by the $\sigma $ -terms, and the objects of ${\mathbf {C}}$ by the formulas (the morphisms then being certain equivalence classes of formal deductions).

In Appendix A, we will (mostly) show that indeed admits such a description. However, for the purposes of deriving the special invariance theorem from the abstract one, this description is actually not needed; we only need the existence of the free f.p. category ${\mathbf {B}}$ and $h^=$ -fibration . That is, the only thing we use about these objects is their defining universal property, and nothing else. We would only need the full syntactic description of if we wanted to go in the other direction and deduce the abstract invariance theorem from the syntactic one (this would also require “packing more” into the syntactic invariance theorem than is really natural from the syntactic point of view).

The reason that we don’t need the syntactic description of is that, even without it, we can still interpret logic over $\sigma $ into , and transport this interpretation along any morphism of $h^=$ -fibrations . Knowing that two such morphisms are pseudonaturally equivalent is then enough to deduce the desired invariance property for the resulting interpretations in .

We first work in the context of a general $h^=$ -fibration (which automatically inherits a 1D2F structure from the results of [8]), showing that the abstract invariance theorem implies a syntactic invariance theorem for interpretations in , involving the 2-categorical structure. We then deduce the invariance theorem for the homotopical semantics by specializing to the case .

This involves translating between the 2-categorical structure on and the model structure on ${\mathbf {Kan}}$ (or rather ${\mathbf {sSet}}$ ). The main point is that the resulting 2-categorical structure on ${\mathbf {Kan}}$ is the same as the Quillen 2-categorical structure, as was proven in [8, Part IV]. However, we also need to know that the 2-cells in the total category of are given by homotopies lying over homotopies in the base, as defined in Section 2.4. This result really “should” have been included in op. cit., but it was not, so we prove it here.

Theorem 3.22. Let $\sigma $ be a signature, let be an $h^=$ -fibration, and let $(\widehat M,M),(\widehat N,N)\colon \sigma \to {\mathbf {C}}'$ be interpretations in .

Now suppose that has a 1D2F structure such that ${\mathbf {B}}$ has 2-categorical products (for example, it could be the “universal” 1D2F structure from [8]).

Then given any pseudoequivalence $\alpha \colon M\to N$ , there exists, for each formula-in-context $({\varphi },\vec {x})$ over $\sigma $ , an equivalence $\widehat {M}_{\vec {x}}({\varphi })\to \widehat {N}_{\vec {x}}({\varphi })$ in ${\mathbf {C}}'$ lying over the equivalence $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}\colon M(\vec {x})\to N(\vec {x})$ in ${\mathbf {B}}'$ .

Proof Let ${\mathbf {B}}$ be a free f.p. category on $\sigma $ (via $i\colon \sigma \to {\mathbf {B}}$ ) and let be a free $h^=$ -fibration over ${\mathbf {B}}$ .

By the universal properties of each of these (and Proposition 3.12), we have f.p. functors ${\varphi },\psi \colon {\mathbf {B}}\to {\mathbf {B}}'$ with ${\varphi }\circ i=M$ and $\psi f\circ i=N$ , and morphisms of $h^=$ -fibrations over ${\varphi }$ and $\psi $ .

Now let $\alpha \colon M\to N$ be a pseudoequivalence. By Theorem 3.21, we have a pseudonatural equivalence $\tilde \alpha \colon {\varphi }\to \psi $ with $\tilde \alpha _{iA}=\alpha _A$ for $A\in \operatorname {\mathrm {Ob}}\sigma $ , from which it follows that $\tilde \alpha _{i\vec {A}}\cong \alpha _{\vec {A}}$ for $\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$ , as explained in the proof of that theorem.

Next, by Theorem 3.13, we have for each $A\in {\mathbf {B}}$ and $P\in {\mathbf {C}}$ an equivalence $\beta _P\colon \Phi P\to \Psi P$ in ${\mathbf {C}}'$ lying over the equivalence $\alpha _A\colon MA\to NA$ in ${\mathbf {B}}'$ .

Now let $\hat \imath $ be an interpretation in over i. Then $\Phi \circ \hat \imath $ and $\Psi \circ \hat \imath $ are interpretations in over M and N, and hence are isomorphic to $\widehat M$ and $\widehat N$ , respectively.

Given a formula-in-context $(\chi ,\vec {x})$ , we have the object $\hat \imath _{\vec {x}}(\chi )$ in ${\mathbf {C}}$ , and hence an equivalence $\beta _{\hat \imath _{\vec {x}}(\chi )}\colon \Phi (\hat \imath _{\vec {x}}(\chi ))\to \Psi (\hat \imath _{\vec {x}}(\chi ))$ over the equivalence $\tilde \alpha _{i(\vec {x})}\colon M(\vec {x})\to N(\vec {x})$ . Using the isomorphisms $\Phi (\hat \imath _{\vec {x}}(\chi ))\cong \widehat M_{\vec {x}}(\chi )$ and $\Psi (\hat \imath _{\vec {x}}(\chi ))\cong \widehat N_{\vec {x}}(\chi )$ over $M(\vec {x})$ and $N(\vec {x})$ , and the isomorphism $\tilde \alpha _{i(\vec {x})}\cong \alpha _{\operatorname {\mathrm {tp}}\vec {x}}$ , it follows that there is also an equivalence $\widehat M_{\vec {x}}(\chi )\to \widehat N_{\vec {x}}(\chi )$ over the equivalence $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}$ , as desired.

Theorem 3.23. Let ${\mathbf {C}}$ be a model category, and consider the $h^=$ -fibration with its 1D2F structure from [8, Theorem 6.11]. Let be a 2-cell in ${\mathbf {C}}_{\mathrm {f}}$ with A cofibrant. According to [8, Section 15], such a 2-cell is given by a homotopy class of homotopies $f\to {}g$ .

Next, let $(p,f),(q,g)\colon {}(X,A,x)\to {}(Y,B,y)$ be morphisms in $({\mathbf {C}}^{\to })_{\mathrm {f}}$ (i.e., morphisms in ${\mathbf {C}}^{\to }$ with x and y fibrant—note that we are using, as usual, the model structure on ${\mathbf {C}}^{\to }$ from [8, Definition 11.1], not the one referenced in the proof of Proposition 2.26) and assume X is cofibrant.

Recall from [8, Definition 11.7] that we write $\gamma (p,f),\gamma (q,g)\colon {}(X,A,x)\to (Y,B,y)$ for the images of $(p,f)$ and $(g,q)$ in ${\mathbf {Ho}}({\mathbf {C}}^{\to })_{\mathrm {f}}$ .

We now claim that there exists a 2-cell $\gamma (p,f)\to {}\gamma (q,g)$ over $\alpha $ if and only if there is a homotopy from p to q over $\alpha $ , regarded as a homotopy (class of homotopies) from f to g (this only depends on the homotopy class $\alpha $ by Proposition 2.26).

Proof Let $k\colon {}A\to {}B^I$ be a representative of $\alpha $ .

We first unwind the definition of the 2-cells in the total category of . Let us write P and Q for $(X,x)$ and $(Y,y)$ , respectively. By definition (see [8, Theorem 6.11 and Definition 6.4]), there exists a 2-cell $\gamma (p,f)\to \gamma (q,g)$ if and only if the diagram

commutes. Now, inserting the definitions of P and Q, and of the pullback functors $\pi _1^*$ and $\pi _2^*$ and the equality object $\operatorname {\mathrm {Eq}}_B$ in the ${\wedge \!\!=}$ -cloven ${\wedge \!\!=}$ -fibration (see [8, Section 15.1]), this is the same as diagram on the left below (where, for conciseness, we are identifying objects and morphisms in ${\mathbf {C}}^{\to }$ with their domains), where the fiber product $Y\times _B{}B^I$ is taken with respect to $d_1\colon {}B^I\to {}B$ .

(3.1)

We would now like to reformulate the commutativity of this diagram in simpler terms.

Note that the morphism ${\langle {{y,sy}}\rangle }\colon Y\to Y\times _BB^I$ is a weak equivalence, since composing it with the trivial fibration $\pi _1\colon Y\times _BB^I\to Y$ (which is pulled back from the trivial fibration $d_1\colon B^I\to B$ ) yields $\operatorname {\mathrm {1}}_Y$ . Hence, we may factor it as a trivial cofibration followed by a trivial fibration $Y\xrightarrow {i}Z\xrightarrow {\pi }Y\times _BB^I$ ; we consider Z an object over $B\times B$ via $(\operatorname {\mathrm {1}}_B\times y)\pi $ . Next, suppose we have a morphism $\nu \colon Z\to B\times Y$ over $B\times B$ such that $\gamma (\nu )\gamma (\pi )^{-1}=\operatorname {\mathrm {sub}}_B^Q$ (we will find such a $\nu $ below).

Now choose a lift $z\colon X\to Z$ of ${\langle {{p,kx}}\rangle }$ along $\pi $ . Since $(X,A,x)$ is cofibrant and $(B\times Y,B\times B,\operatorname {\mathrm {1}}\times y)$ fibrant, the commutativity of the diagram on the left above is then equivalent to the commutativity of the diagram on the right up to homotopy in ${\mathbf {C}}^{\to }$ . As remarked at the end of Definition 2.25, this is equivalent to $\nu z$ and ${\langle {{fx,q}}\rangle }$ being homotopic over the trivial homotopy from ${\langle {{f,g}}\rangle }$ to itself. Since we must have $\pi _1\nu z=fx$ , this is in turn equivalent to $\pi _2\nu z$ and q being homotopic over the trivial homotopy from g to itself.

We conclude that the left side of the equivalence in the theorem statement is equivalent to $\pi _2\nu z$ and q being homotopic over the trivial homotopy from g to itself.

We still need to define $\nu $ . To do so, first consider a pullback $(Y\times Y)\times _{B\times B}B^I$ with respect to $y\times y$ and ${\langle {{d_1,d_2}}\rangle }$ , and factor ${\langle {{\Delta _Y,sy}}\rangle }\colon Y\to (Y\times Y)\times _{B\times B}B^I$ as a trivial cofibration and fibration $Y\xrightarrow {s}Y^I\xrightarrow {{\langle {{{\langle {{d_1,d_2}}\rangle },y^I}}\rangle }}(Y\times Y)\times _{B\times B}B^I$ (thus producing the situation in the last diagram of (2.1) in Definition 2.25) and choose a diagonal filler j in the following square.

Now define $\nu ={\langle {{yd_1,d_2}}\rangle } j\colon Z\to B\times Y$ (note that this is indeed a morphism over $B\times B$ ). Let us verify that it satisfies the required condition $\gamma (\nu )\gamma (\pi )^{-1}=\operatorname {\mathrm {sub}}_B^Q$ . By the definition of $\operatorname {\mathrm {sub}}_B^Q$ , this means that the triangle below on the left should commute in ${\mathbf {Ho}}({\mathbf {C}}^{\to })_{\mathrm {f}}$ , or equivalently, that the isomorphic diagram in the center should commute. But in fact, the diagram on the right in ${\mathbf {C}}^{\to }$ already commutes before applying $\gamma $ .

Now, since (by definition) $\pi z={\langle {{p,kx}}\rangle }\colon X\to Y\times _BB^I$ , the composite $jz\colon X\to Y^I$ gives a homotopy from p to $d_2jz=\pi _2\nu z$ over k. Hence, by Proposition 2.26, we conclude that p and q are homotopic over k if and only if q and $\pi _2\nu z$ are homotopic over the trivial homotopy on g, as desired.

Theorem 3.24. Let ${\mathbf {C}}$ be a suitable model category and let $M,N\colon {}\sigma \to {\mathbf {C}}_{\mathrm {f}}$ be $\sigma $ -interpretations, and suppose we have a homotopy equivalence $\alpha \colon M\to N$ .

Then, given homotopical $\sigma $ -interpretations $\widehat M$ and $\widehat N$ over M and N, there exists, for each formula-in-context $({\varphi },\vec {x})$ over $\sigma $ , a homotopy equivalence $\widehat M_{\vec {x}}({\varphi })\to \widehat N_{\vec {x}}({\varphi })$ over the homotopy equivalence $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}\colon M(\vec {x})\to N(\vec {x})$ .

Proof As remarked in Definition 3.18, a homotopy equivalence of $\sigma $ -interpretations in ${\mathbf {C}}_{\mathrm {f}}={\mathbf {C}}_{\mathrm {cf}}$ is the same thing as a pseudoequivalence with respect to the Quillen 2-category structure. Moreover, it follows from Theorem 3.23 that there is a homotopy equivalence $\widehat M_{\vec {x}}({\varphi })\to \widehat N_{\vec {x}}({\varphi })$ over the homotopy equivalence $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}$ if and only if there is an equivalence $\widehat M_{\vec {x}}({\varphi })\to \widehat N_{\vec {x}}({\varphi })$ over the equivalence $\alpha _{\operatorname {\mathrm {tp}}\vec {x}}$ in the 1D2F .

Since, by Proposition 2.23, $\gamma \circ \widehat M$ and $\gamma \circ \widehat N$ are $\sigma $ -interpretations in over M and N, the claim now follows from Theorem 3.22.

4 Examples and further questions

We now give some examples of sentences and their interpretation under the homotopical semantics. In each case, we fix some algebraic signature $\sigma $ and a $\sigma $ -interpretation M in ${\mathbf {Kan}}$ (or in ${\mathbf {Top}}_{\mathrm {c}}$ —the category of topological spaces which are homotopy equivalent to a CW complex—and then consider the interpretation $\operatorname {\mathrm {Sing}}\circ M$ , as discussed in Section 2.5). We then take some first-order sentence over this signature and see what it means for it to be satisfied in M (or in the case of ${\mathbf {Top}}_{\mathrm {c}}$ , in $\operatorname {\mathrm {Sing}}\circ M$ )—i.e., for its interpretation to be a non-empty space with respect to any homotopical interpretation $\widehat M$ over M (or $\operatorname {\mathrm {Sing}}\circ M$ ).

Though the notion of satisfaction in M is independent of the choice of homotopical interpretation $\widehat M$ , it will be convenient to use this freedom to choose a particular such $\widehat M$ , where we recall that (up to isomorphism) our only freedom is in the choice of equality objects; we take these to be the “standard” path-spaces $X^I\to X\times X$ in ${\mathbf {sSet}}$ , where I is the simplicial interval $\Delta ^1$ .

After the examples, we consider some further questions regarding the material of this paper.

4.1 Examples of interpretations of sentences

4.1.1 Contractibility.

First, we consider the signature $\sigma $ consisting of a single sort A and having no operation symbols, and the sentence in this language

$$\begin{align*}\exists x\ \forall y\ (x=y). \end{align*}$$

We claim that this is interpreted under the semantics as “A is contractible.”

Fix a $\sigma $ -interpretation in ${\mathbf {Kan}}$ , i.e., a Kan complex X.

Now, the formula $x=y$ in the context ${\langle {x,y}\rangle }$ is interpreted as the path-space fibration $X^I\xrightarrow {{\langle {{d_1,d_2}}\rangle }}X\times {}X$ . Next, the formula $\forall {}y\,(x=y)$ is interpreted as an indexed product $\prod _{\pi _1}(X^I,{\langle {{d_2,d_2}}\rangle })$ . Finally, $\exists {}x\,\forall {}y{}\,(x=y)$ is interpreted (as always, up to isomorphism) as the domain of $\prod _{\pi _1}(X^I,{\langle {{d_2,d_2}}\rangle })$ .

Hence, we are interested in when the domain of $\prod _{\pi _1}(X^I,{\langle {{d_1,d_2}}\rangle })$ is non-empty. This will hold if and only if there is a morphism $(\mathbf {1}_{\mathbf {sSet}},x)\to {}\prod _{\pi _1}(X^I,{\langle {{d_1,d_2}}\rangle })$ in ${\mathbf {sSet}}/X$ for some $x\colon \mathbf {1}_{\mathbf {sSet}}\to {}X$ . By the adjunction (Remark 2.6), this is equivalent to having a morphism from $\pi _1^*(\mathbf {1}_{\mathbf {sSet}},x)\cong (X,{\langle {{x!,\operatorname {\mathrm {1}}_X}}\rangle })$ to $(X^I,{\langle {{d_1,d_2}}\rangle })$ in ${\mathbf {C}}/X\times {}X$ :

But this is by definition a (right-)homotopy between X and the constant map $x!$ , i.e., a contraction of X onto x.

If we start with a topological space $X\in {\mathbf {Top}}_{\mathrm {c}}$ instead of a Kan complex, then the above shows that X satisfies the sentence in question if and only if the singular simplicial set of X is contractible. But as is well-known, this holds if and only if X itself is contractible.

4.1.2 Homotopies.

Now let $\sigma $ be the signature consisting of two sorts $A,B$ and two function symbols $f,g\colon {}A\to {B}$ . We consider the sentence

$$\begin{align*}\forall{x\in{A}}\ (f(x)=g(x)). \end{align*}$$

We claim that this is interpreted as “f is homotopic to g.”

Suppose we have a $\sigma $ -interpretation in ${\mathbf {Kan}}$ ; that is, two Kan complexes $X,Y$ , and two morphisms $f,g\colon {}X\to {Y}$ . The formula $y_1=y_2$ (in the context ${\langle {{y_1,y_2}}\rangle }$ ) will (again) be interpreted as the path-space fibration $Y^I\xrightarrow {{\langle {{d_1,d_2}}\rangle }}Y\times {}Y$ . Now, we have the morphism ${\langle {{f,g}}\rangle }\colon {}X\to {Y\times {Y}}$ , and $f(x)=g(x)$ (in the context ${\langle {x}\rangle }$ ) will be interpreted as ${\langle {{f,g}}\rangle }^*(Y^I,{\langle {{d_1,d_2}}\rangle })$ . Finally, the above sentence will be interpreted as $\prod _!{\langle {{f,g}}\rangle }^*(Y^I,{\langle {{d_1,d_2}}\rangle })$ , the points of which are (by the adjunction) in bijection with the sections of ${\langle {{f,g}}\rangle }^*(Y^I,{\langle {{d_1,d_2}}\rangle })$ , which are in turn in bijection with the lifts

which are, of course, by definition (right-)homotopies $f\sim {g}$ .

For a $\sigma $ -interpretation in ${\mathbf {Top}}_{\mathrm {c}}$ , i.e., a pair of maps $f,g\colon {}X\to {}Y$ , we thus see that the above sentence is satisfied if and only if $\operatorname {\mathrm {Sing}}(f)$ and $\operatorname {\mathrm {Sing}}(g)$ are homotopic and, again, this is the case if and only if f and g are homotopic.

Now considering a signature with two sorts $A,B$ and two function symbols $f\colon {}A\to {B}$ and $g\colon {}B\to {A}$ , we have by the same reasoning as above that

$$\begin{align*}\forall{x\in{A}}\ (g(f(x))=x)\,\wedge\, \forall{y\in{B}}\ (f(g(y))=y) \end{align*}$$

is interpreted (in both ${\mathbf {Top}}_{\mathrm {c}}$ and ${\mathbf {Kan}}$ ) as “f and g constitute a homotopy equivalence” (i.e., both composites are homotopic to the identity).

Similarly, for the signature consisting of a single sort A and binary function symbol $f\colon {}A\times {A}\to {A}$ ,

$$\begin{align*}\forall{}x,y,z\in{}A\ [f(f(x,y),z)=f(x,f(y,z))] \end{align*}$$

is interpreted as “f is homotopy-associative.”

4.1.3 Classical logic.

We now give an example showing that the homotopical semantics are not sound with respect to classical logic. By this we mean that there is a formula of the form $\neg \neg {P}{\Rightarrow }{P}$ over some signature $\sigma $ and a $\sigma $ -interpretation (in ${\mathbf {Top}}_{\mathrm {c}}$ and ${\mathbf {Kan}}$ ) under which the interpretation of this formula is empty.

First, we note that it is important that P is not a closed formula. Indeed, a closed formula is interpreted as a Kan complex X, and its negation is interpreted as an empty Kan complex or one-point Kan complex according to whether X is non-empty or empty. From this it follows that the interpretation of $\neg \neg {P}{\Rightarrow }{P}$ (and similarly $P\vee \neg {P}$ ) is always non-empty. This circumstance is familiar, for example, from Kleene’s realizability semantics for intuitionistic arithmetic.

Now, for our example, we consider, in the signature $\sigma $ consisting of a single sort A and no function symbols, the sentence

(4.1) $$ \begin{align} (\exists x \ \forall y \ (\neg\neg{x=y})) {\Rightarrow} (\exists x \ \forall y \ (x=y)). \end{align} $$

Given a structure X (in ${\mathbf {Kan}}$ or ${\mathbf {Top}}_{\mathrm {c}}$ ) for $\sigma $ we have already seen that the interpretation of the right side of this implication is inhabited if and only if X is contractible. Let us consider the left side. We first consider the case of X in ${\mathbf {Kan}}$ . We will show that this sentence is satisfied if and only if X is non-empty and path-connected (i.e., for any vertices $x,y\in {X}_0$ there is an edge $e\in {X}_1$ from x to y).

We have, again, that $x=y$ is interpreted as the path space $(X^I,{\langle {{d_1,d_2}}\rangle })$ . We recall that $\neg \neg x=y$ is an abbreviation of $(x=y{\Rightarrow }\bot ){\Rightarrow }\bot $ . Here, $\bot $ is interpreted as the initial Kan fibration $(\emptyset ,\text {!`},X)$ .

Now, it easy to see that in any category (such as ${\mathbf {Kan}}/X$ ) with a strong initial object $0$ (i.e., every morphism with codomain $0$ is an isomorphism), any exponential object $A{\Rightarrow }0$ is a subsingleton (i.e., the morphism $!_{A{\Rightarrow }0}$ to the terminal object is a monomorphism). Since there exists a morphism $A\to ((A{\Rightarrow }0){\Rightarrow }0)$ , it follows that the unique morphism $A\to 1$ factors through $(A{\Rightarrow }0){\Rightarrow }0$ .

In the case of a Kan fibration $(E,e)$ in ${\mathbf {Kan}}/X$ , this tells us that $\neg \neg ({E},e)$ is a monomorphism into X whose image contains the image of e. In particular, if E is surjective onto X, then $\neg \neg {(E,e)}$ is an isomorphism.

Now, if X is path-connected, then the path space $X^I$ is clearly surjective on vertices. But as an easy inductive argument shows, any Kan fibration which is surjective on vertices is surjective. Hence, for X path-connected, $\neg \neg {x=y}$ is interpreted as an isomorphism, whence it follows that, for X non-empty and path-connected, the following sentence is satisfied.

(4.2) $$ \begin{align} \exists x \ \forall y \ (\neg\neg{x=y}). \end{align} $$

For the other direction, it suffices to see that if a Kan fibration $(E,e)$ in ${\mathbf {Kan}}/X$ is not surjective, then neither is $\neg \neg (E,e)$ , since if $\neg \neg {}x=y$ is interpreted as a non-surjective morphism, the interpretation of (4.2) must be empty. Suppose e is not surjective and let $p\in {X_0}$ be a vertex not in the image of e. Then the minimal sub-simplicial set ${\langle {{p}}\rangle }$ of X containing p is disjoint from the image of e. Hence $({\langle {p}\rangle },i)\wedge (E,e)\cong \mathbf {0}$ , where $i\colon {\langle {p}\rangle }\to {}E$ is the inclusion, so we have a morphism $({\langle {p}\rangle },i)\to \neg ({E},e)$ . In particular, $({\langle {p}\rangle },i)\wedge \neg ({E},e)$ is non-empty, so there cannot be a morphism $({\langle {p}\rangle },i)\to \neg \neg ({E},e)$ .

Note that by the same kind of argument as in the previous examples, we also have that the interpretation of the sentence (4.2) in ${\mathbf {Top}}_{\mathrm {c}}$ is “A is non-empty path-connected.”

Now suppose X is a Kan complex or a topological space in ${\mathbf {Top}}_{\mathrm {c}}$ which is path-connected but not contractible (for instance, the circle). Then the sentence (4.1) is interpreted as a non-empty Kan complex, whereas the conclusion is interpreted as the empty Kan complex. Hence the implication is empty.

Finally, we note that this implies that (the universal closure of)

$$\begin{align*}\neg\neg{x=y}{\Rightarrow}{x=y} \end{align*}$$

cannot be satisfied for such an X since this would imply (by the soundness of the interpretation with respect to intuitionistic logic) that (4.1) would also be satisfied.

4.1.4 Homotopy-equivalence.

We saw above that we can easily express that two morphisms constitute a homotopy equivalence, in the same way as we would classically express that they constitute a bijection. We can also classically express that a single function $f\colon {}A\to {B}$ is a bijection by

$$\begin{align*}\forall{b\in{B}}\ \exists{a\in{A}}\ ( fa=b\wedge \forall{a'\in{A}}\ (fa'=b{\Rightarrow}{a'=a}) ). \end{align*}$$

Let us see that the interpretation of this sentence (in ${\mathbf {Kan}}$ , and hence in ${\mathbf {Top}}_{\mathrm {c}}$ ) is non-empty if and only if the interpretation of f is a homotopy equivalence.

First of all, the sentence is equivalent to the conjunction of

$$\begin{align*}\forall{b\in{B}}\ \exists{a\in{A}}\ ( fa=b) \quad\text{and}\quad \forall{b\in{B}}\ \exists{a\in{A}} \ \forall{a'\in{A}}\ (fa'=b{\Rightarrow}{a'=a} ). \end{align*}$$

The same reasoning as in Section 4.1.2 shows that the first part is satisfied by a map $f\colon {}X\to {}Y$ if and only if there exists a map $g\colon {}Y\to {}X$ such that $f\circ {}g$ is homotopic to $\operatorname {\mathrm {1}}_Y$ .

The second part, with the quantifiers removed, is interpreted as a certain fibration over $Y\times {}X\times {}X$ . By making use of the relevant adjunctions, we can see that the space which is the interpretation of the quantified sentence is inhabited if and only if there exist a map $g\colon {}Y\to {}X$ and a dotted lift in the following diagram.

Here, in $X\times _YY^I$ , X is mapping to Y via f and $Y^I$ is mapping to Y via $d_1$ ; and in the object on the bottom-left of the diagram, $Y\times {}X$ is mapping to $Y\times {}X\times {}X$ via ${\langle {{\pi _1,g\pi _1,\pi _2}}\rangle }$ , and $X\times (X\times _YY^I)$ is mapping to $Y\times {}X\times {}X$ via ${\langle {{d_2\pi _2\pi _2,\pi _1,\pi _1\pi _2}}\rangle }$ .

We claim that such a lift exists if and only if $g\circ {}f$ is homotopic to $\operatorname {\mathrm {1}}_X$ .

In one direction, we have a map $q\colon {}X\to {}(Y\times {}X)\times _{Y\times {}X\times {}X}(X\times (X\times _Y{Y^I}))$ which is given by ${\langle {{{\langle {{f,\operatorname {\mathrm {1}}_X}}\rangle },{\langle {{gf,{\langle {\operatorname {\mathrm {1}}_X,sf}\rangle }}}\rangle }}}\rangle }$ (where s is, as usual, the canonical map $Y\to {}Y^I$ ). Hence, given a lift k as above, the composite $\pi _2kq$ gives a homotopy $X\to {}X^I$ from $\operatorname {\mathrm {1}}_X$ to $gf$ .

In the other direction, suppose we have a homotopy $h\colon {}X\to {}X^I$ from $\operatorname {\mathrm {1}}_X$ to $gf$ . We then define k as ${\langle {{\pi _1\pi _1,h'}}\rangle }$ , where $h'$ is the composite

$$\begin{align*}(Y\times{}X)\times_{Y\times{}X\times{}X}(X\times(X\times_Y{Y^I})) \xrightarrow {{\langle{{h\pi_2\pi_1,g^I\pi_2\pi_2\pi_2}}\rangle}} X^I\times_XX^I\to{}X^I \end{align*}$$

in which the second map is composition of paths.

4.2 Further problems and questions

We mention some possible further directions.

4.2.1 Completeness.

This is probably the most natural question to ask about the homotopical semantics: are they a complete semantics for intuitionistic logic? I.e., is it the case that, if a sentence ${\varphi }$ over a signature $\sigma $ is satisfied by every $\sigma $ -structure in ${\mathbf {Kan}}$ , then ${\varphi }$ is intuitionistically provable?

And if it is not complete for intuitionistic logic, then (as was pointed out to me by Thomas Icard) we can still try to characterize the “intermediate” logic between intuitionistic and classical for which it is complete.

4.2.2 Limited expressivity.

We mentioned at the end of Section 1.1 that first-order homotopical logic is much less expressive than homotopy type theory. However, we have not proven that any particular property is inexpressible, and it would be interesting to do so—for example, to prove that over the trivial signature with a single sort A and no function symbols, there is no sentence ${\varphi }$ satisfied by exactly those spaces X which are simply connected. Or to give another example, there should be no sentence over the signature consisting of one sort and a single binary operation which is satisfied exactly by those operations satisfying the “ $A_4$ ” (or “Stasheff pentagon”) condition.

4.2.3 Higher-dimensional generalizations.

Given this lack of expressiveness, it is natural to seek extensions of first-order logic which increase the expressiveness. For example, one could add some, but not all, of what is present in type theory—say, an additional sort $s=_At$ for any two terms s and t of sort A, so that one could express that “two homotopies are homotopic”: $e=_{s=_At}e'$ .

One would hope to have a nice categorical formulation of the corresponding semantics, as we have for first-order homotopical logic. Indeed, it is also natural to seek “higher-dimensional” generalizations of the fibrational semantics. For example, the fact that we can only express “one level” of homotopies in the language seems to correspond to the fact that the fibrations we are considering are (“only”) two-dimensional. On the “semantic” side, there are natural higher-dimensional categories close at hand—for example, instead of having the fibers of be the homotopy categories of the slices ${\mathbf {C}}/A$ , one could try to take the corresponding $\infty $ -categories (or some truncation thereof). We might then seek a higher-dimensional analogue of the syntactic fibration, morphisms out of which would give the semantics for such “higher-dimensional” extensions of first-order logic.

4.2.4 Relationship to univalence.

Steve Awodey and Ulrik Buchholtz (independently) suggested an interesting alternative approach to proving the homotopy invariance of the homotopical semantics for first-order logic by working within HoTT.

Namely, in that context, we could understand the homotopical semantics to simply assign a type $M({\varphi })$ to each sentence ${\varphi }$ , given a structure M defined within type theory. The homotopy invariance should then say that given an isomorphic structure $M'\cong M$ , we should have $M({\varphi })\cong M'({\varphi })$ .

But using an appropriate version of univalence (or rather, a “structure-identity principle” [30, Section 9.8]), one would then conclude that $M=_{\mathcal {U}}M'$ ( $\mathcal {U}$ being an appropriate type with $M,M':\mathcal {U}$ ), from which we immediately conclude $M({\varphi })=M'({\varphi })$ .