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.
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 [Reference Martin-Löf23]. The long horizontal arrow is the homotopy-theoretic interpretation of type theory [Reference Awodey and Warren1, Reference Kapulkin and Lumsdaine13, Reference Warren32] 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 [Reference Boardman and Vogt4] 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 [Reference Grothendieck6]—the name seems to be due to Baez [Reference Baez2]).
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 [Reference Troelstra and van Dalen31, 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 [Reference Jacobs10, Reference Makkai19]).
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
Footnote
1
(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.Footnote
2
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. [Reference Palmgren26]). 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 $
):
$$ \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}}$
,Footnote
3
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 [Reference Helfer8] (and had been previously introduced independently in [Reference Cagne5]), 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 [Reference Lawvere16] 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 $
.Footnote
4
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 [Reference Helfer8], 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 [Reference Helfer8], 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 [Reference Helfer8], we then go on to give the “rest” of the definition of
$h^=$
-fibration.
Definition 2.1.1. We briefly recall some definitions [Reference Helfer8] 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, Section 6]).
; we call 
over 
. (See [
in which each fiber 
has finite products, and these are preserved by all pullback functors 
for 
for each diagonal morphism 
is simply the codomain functor; it is a 
(see [
over 
and 
are obtained by restricting the codomain functor to the subcategories 
and 
.
is defined to be the restriction of 
to 
is a 2-functor of 2-categories whose underlying functor is a fibration and for which, given any 2-cell 
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 [Reference Helfer8, Section 1.5]).
We follow the conventions concerning coproducts from [Reference Helfer8, 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., [Reference Johnstone12, 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 [Reference Makkai19, 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 [Reference Helfer8], 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 [Reference Helfer8, Section 1.6] (cf. [Reference Makkai19, p. 342]).
Definition 2.2. A fibration 
is an h-fibration if it satisfies the following four conditions.
-
(i)
has stable fiberwise finite products and coproducts and exponentials. -
(ii)
${\mathbf {B}}$
has finite products. -
(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$
.
has stable fiberwise finite products and coproducts and exponentials.
, there exist indexed sums and products 
is an
$h^=$
-fibration if, in addition,
-
(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 ).
for 
).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}}$
.Footnote
5
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 [Reference Helfer8, 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 [Reference Helfer8, 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., [Reference Lawvere15, p. 6], [Reference Makkai19, p. 343], [Reference Jacobs10, 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., [Reference Makkai19, p. 343], [Reference Jacobs10, 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., [Reference Makkai19, p. 345], [Reference Seely29, Section 2.4][Reference Jacobs10, p. 81]).
Remark 2.6. It is easy to see (and well-known—see [Reference Makkai19]) 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.Footnote
6
One way to formulate this which does not involve any choices is to say there is always a canonical anafunctor (see [Reference Makkai21]) 
, 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 [Reference Helfer8]. 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., [Reference Lumsdaine and Shulman18, 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 [Reference Helfer8, 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 [Reference Helfer8], 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 [Reference Quillen27, 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.
-
(i)
${\mathbf {C}}$
is right-proper, i.e., weak equivalences are closed under pullbacks along fibrations.Footnote
7
-
(ii)
${\mathbf {C}}$
is locally cartesian closed (as a category). -
(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. -
(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., [Reference May and Ponto24, p. 370]). As for (ii), it is well-known that any presheaf category is locally cartesian closed (see [Reference Johnstone12, 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 [Reference McLarty25, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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., [Reference Johnstone12, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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):
-
(i) a function
$M\colon \operatorname {\mathrm {Ob}}\sigma \to \operatorname {\mathrm {Ob}}{\mathbf {C}}$
; -
(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$
); -
(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:
-
(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. -
(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 .Footnote
8
-
(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 $
. -
(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.Footnote
9
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., [Reference Helfer8, 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}}$
[Reference Helfer8, 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 [Reference Helfer8, 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.Footnote
10
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 [Reference Helfer8, Definition 11.1] by [Reference Helfer8, 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 [Reference Helfer8, 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., [Reference Hovey9, 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).Footnote
11
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 [Reference Helfer8, 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 [Reference May and Ponto24, 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 [Reference Johnstone11] (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 Footnote
12
).
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 [Reference Helfer8, 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 [Reference Helfer8]; 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 [Reference Helfer8] (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):
-
(i) A 1-cell
$\alpha _A\colon {}FA\to {}GA$
for each
$A\in {\mathbf {C}}$
. -
(ii) An isomorphism 2-cell
for each morphism
$f\colon {}A\to {}B$
in
${\mathbf {C}}$
.
-
(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}$
. -
(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., [Reference Helfer8, 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 [Reference Helfer8, 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.Footnote
13
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 [Reference Helfer8, 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
Footnote
14
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 [Reference Helfer8, 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}}$
.Footnote
15
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 [Reference Makkai22]) 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 [Reference Helfer8]), 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 [Reference Helfer8, 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 [Reference Helfer8]).
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 [Reference Helfer8, Theorem 6.11]. Let 
be a 2-cell in
${\mathbf {C}}_{\mathrm {f}}$
with A cofibrant. According to [Reference Helfer8, 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 [Reference Helfer8, Definition 11.1], not the one referenced in the proof of Proposition 2.26) and assume X is cofibrant.
Recall from [Reference Helfer8, 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 [Reference Helfer8, 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 [Reference Helfer8, 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$
.
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
$$ \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.
$$ \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 })$
.
Appendix A The syntactic fibration
The main purpose of this appendix is to construct a free
$h^=$
-fibration 
over any f.p. category
${\mathbf {B}}$
. When
${\mathbf {B}}$
is itself a free f.p. category on some signature
$\sigma $
, this is the “syntactic” fibration associated with
$\sigma $
, such that the morphisms out of it into some fibration 
correspond to interpretations of
$\sigma $
in 
.
The construction of 
closely parallels the analogous construction for propositional logic from [Reference Harnik and Makkai7], to which we refer for a thorough discussion of and motivation behind the construction.
In op. cit., the construction (which is of a category and not a fibration) is directly “syntactic”; the objects of the category are propositional formulas, and the morphisms are equivalence classes of logical deductions.Footnote
16
In an earlier version of this paper, we similarly provided a “syntactic” construction of 
(which in particular could only be carried out in the case that
${\mathbf {B}}$
is free), but in the present version, we provide a more direct construction, in line with the usual construction of free structures.
We note that in op. cit, the “direct” construction and the “syntactic” construction are one and the same. This is because of the observation due to Lambek that the inference rules of intuitionistic propositional logic precisely correspond to the universal properties of the operations in a bicartesian closed category.
In the case of intuitionistic first-order logic, there is an analogous situation (this being an observation of Lawvere), but with
$h^=$
-fibrations instead of bicartesian closed categories. The reason that the two constructions of the free
$h^=$
-fibration are no longer identical is that there is a slight discrepancy between the syntax of first-order logic (as it is usually construed) and the operations in a fibration; in the latter, “substitution” (i.e., pullbacks) is a “primitive” operation, whereas in the syntax it is not, and also, the fibrational and syntactic treatments of equalities and quantifiers differs slightly as well.
This complicates considerably the task of showing that the “syntactically” constructed fibration is in fact an
$h^=$
-fibration, and that it is free. This—in addition to the advantage of it working over arbitrary
${\mathbf {B}}$
—is why we opt here for the direct construction.
On the other hand, the advantage of the syntactic construction is that it makes it clear that the morphisms are precisely equivalence classes of deductions, and this fact is obscured in the present construction. It is still “almost” obvious from the construction (the only problem being the discrepancies mentioned above between the syntax and the
$h^=$
-fibration operations), but to actually prove it is non-trivial, and we do not attempt to do so, though we discuss the matter in Section A.3.
We will, however, show the weaker result that, for two objects P and Q in the free
$h^=$
-fibration corresponding to given formulas
${\varphi }$
and
$\psi $
, there exists a morphism
$P\to Q$
if and only if
${\varphi }{\Rightarrow }\psi $
is intuitionistically provable.
A.1 The free
$h^=$
-fibration over an f.p. category
${\mathbf {B}}$
We now construct the free
$h^=$
-fibration over an arbitrary finite product category
${\mathbf {B}}$
. As we have mentioned, this notion of freeness is given by a certain universal property which determines the fibration up to equivalence over
${\mathbf {B}}$
.
However, the construction will proceed by producing (in the standard way) a structure which is free in the stricter (“0-categorical”) sense (thus determining it up to isomorphism—though we will not make use of this fact).
To perform the latter construction, we will have to specify what kind of free structure we want to construct, and for this we will deploy the notion of multi-sorted algebraic signature in a different way than in the rest of the paper (but in the same way as in [Reference Harnik and Makkai7]); in particular, in this case, we will be concerned with ordinary set-based structures for the signature, rather than ones valued in simplicial sets or in other categories.
Definition A.1.1. We recall the standard construction of an initial structure (or free structure with no generators) on a multi-sorted algebraic signature
$\sigma $
, which we will use twice in what follows.Footnote
17
Recall from Definition 2.18 that the set of terms over
$\sigma $
was defined relative to a fixed infinite set
$\operatorname {\mathrm {Varn}}$
of variable names. In fact, the set thus constructed—or better, the
$\operatorname {\mathrm {Ob}}\sigma $
-indexed family of sets—is precisely the free
$\sigma $
-structure on the (
$\operatorname {\mathrm {Ob}}\sigma $
-indexed) set
$\operatorname {\mathrm {Var}}_{\sigma }=\operatorname {\mathrm {Ob}}\sigma \times \operatorname {\mathrm {Varn}}$
. If we instead take
$\operatorname {\mathrm {Varn}}=\emptyset $
—or, what amounts to the same thing—if we take only the closed
$\sigma $
-terms (those not having any free variables)—we obtain the definition of the initial
$\sigma $
-structure. This structure is characterized up to isomorphism by an obvious universal property—this is precisely the “principal of structural recursion” mentioned in Definition 2.18. As was said there, we will freely make use of this—as well as the corresponding principle of structural induction—when dealing with the initial
$\sigma $
-structure.
We will also need to make use of the initial model of an algebraic theory—i.e., of an algebraic signature
$\sigma $
together with a set of identities, each identity being given by a pair of
$\sigma $
-terms of the same sort. Concretely, this initial model is obtained as the quotient of the initial
$\sigma $
-structure by a certain equivalence relation: to begin with, we have a relation R consisting of all pairs of closed terms obtained by substituting arbitrary closed terms for the variables in each of the given identities. We then take the least congruence relation containing R, i.e., the least equivalence relation
$\sim $
satisfying
$ft_1\ldots t_n\sim ft_1'\ldots t_n'$
whenever
$t_1\sim t_1',\ldots ,t_n\sim t_n'$
for any function symbol f of
$\sigma $
.
Again, this structure has a universal property, now with respect to all
$\sigma $
-structures satisfying the given identities.
Construction A.1. Let
${\mathbf {B}}$
be a finite product category. We will define the free
$h^{=}$
-fibration over
${\mathbf {B}}$
in terms of initial structures on certain signatures associated with
${\mathbf {B}}$
.
To begin with, we describe a certain multi-sorted algebraic signature
$\sigma _{\mathbf {B}}$
associated with
${\mathbf {B}}$
. For the set of sorts, we set
$\operatorname {\mathrm {Ob}}\sigma _{\mathbf {B}}:=\operatorname {\mathrm {Ob}}{\mathbf {B}}$
, and it has function symbols:
-
(i)
$\top _A,\bot _A\in \sigma _{\mathbf {B}}(\emptyset ,A)$
for each
$A\in {\mathbf {B}}$
and
$\operatorname {\mathrm {Eq}}_{\Delta }\in \sigma _{\mathbf {B}}(\emptyset ,B)$
of sort B for each diagonal morphism
$\Delta \colon A\to B$
in
${\mathbf {B}}$
, -
(ii)
$\wedge _A,\vee _A,{\Rightarrow }_A\in \sigma _{\mathbf {B}}({\langle {A,A}\rangle },A)$
for each
$A\in {\mathbf {B}}$
, -
(iii)
$\prod _{\pi },\sum _{\pi }\in \sigma _{\mathbf {B}}(A,B)$
for each product projection
$\pi \colon A\to B$
in
${\mathbf {B}}$
and
$f^*\in \sigma _{\mathbf {B}}(B,A)$
for each morphism
$f\colon A\to B$
in
${\mathbf {B}}$
.
Let
$\operatorname {\mathrm {Ob}}{\mathbf {C}}$
be the initial structure on the above signature, as described in Definition A.1.1 and, for
$A\in {\mathbf {B}}$
, denote by 
its set of elements of sort A (the notation will be justified soon).
Next, we describe a second algebraic signature
$\sigma _{\mathbf {B}}'$
whose set
$\operatorname {\mathrm {Ob}}\sigma _{B}'$
of sorts is the set of triples
$(P,Q,f)$
, with 
and 
for some
$A,B\in {\mathbf {B}}$
, and with
$f\colon A\to B$
a morphism in
${\mathbf {B}}$
.
The function symbols of this signature are given schematically below (compare [Reference Harnik and Makkai7, p. 210]). Each figure indicates a set of operations, one for each of the possible values of the relevant parameters
$A,B,C,f,g,P,Q,R,S,T,\Delta ,A',B',\pi ,\pi ',h,k$
. The range of these parameters is given as follows:
$A,B,C\in \operatorname {\mathrm {Ob}}{\mathbf {B}}$
;
$f\colon A\to B$
and
$g\colon B\to C$
are morphisms in B; 
, 
, and 
;
$\Delta \colon A\to B$
is a diagonal morphism; and finally,
$A',B',\pi ,\pi ',h,k$
are objects and morphisms in
${\mathbf {B}}$
forming a pullback square
with
$\pi $
(and hence
$\pi '$
) a product projection.
Each figure below displays, above the horizontal line, the arity of the operation, and below, the codomain sort, and also introduces a notation for the function symbol (i.e., recalling that normally, for a function symbol f and terms
$t_1,\ldots ,t_k$
of the appropriate sorts, we write
$ft_1\ldots t_k$
for the resulting term, we introduce an alternative notation for
$ft_1\ldots t_k$
). To indicate that a term p is of sort
$(P,Q,f)$
, we write
$p\colon P\xrightarrow [f]{}Q$
. If the subscript f is omitted, it is assumed to be
$\operatorname {\mathrm {1}}_A$
.
Category and fibration structure:
$$\begin{align*}\frac{{\vphantom{P}}}{1_P\colon{}P\xrightarrow {}P}\hspace{18pt} \frac{p\colon{}P\xrightarrow [f]{}S\quad{}q\colon{}S\xrightarrow [g]{}T}{q\circ{}p\colon{}P\xrightarrow [gf]{}T}\hspace{18pt} \frac{{\vphantom{P}}}{{{f}^{\uparrow}{S}}\colon f^*S\xrightarrow [f]{} S}\hspace{18pt} \frac{p\colon{}P\xrightarrow [gf]{}T}{\overline{p}^{f,g}\colon{}P\xrightarrow [f]{}g^*T} \end{align*}$$
Finite products and coproducts:
$$\begin{align*}\frac{}{!_P\colon{}P\to{}\top_{A}}{\hspace{40pt}} \frac{{\vphantom{P}}}{{\text{!`}}_P\colon\bot_{A}\to{}P} \end{align*}$$
$$\begin{align*}\frac{{\vphantom{P}}}{\pi_{PQ}\colon{}P\wedge{}Q\to{}P}\hspace{20pt} \frac{{\vphantom{P}}}{\pi^{\prime}_{PQ}\colon{}P\wedge{}Q\to{}Q}\hspace{20pt} \frac{p\colon{}P\to{Q}\quad{}q\colon{}P\to{R}}{{\langle{{p,q}}\rangle}\colon{}P\to{Q\wedge{R}}} \end{align*}$$
$$\begin{align*}\frac{{\vphantom{P}}}{\kappa_{PQ}\colon{}P\to{}P\vee{}Q}\hspace{20pt} \frac{{\vphantom{P}}}{\kappa^{\prime}_{PQ}\colon{}Q\to{}P\vee{}Q}\hspace{20pt} \frac{p\colon{}P\to{R}\quad{}q\colon{}Q\to{R}} {{\left[p,q\right]}\colon P\vee{}Q\to{R}} \end{align*}$$
Exponentials:
$$\begin{align*}\frac{{\vphantom{P}}}{\varepsilon_{PQ}\colon(P{\Rightarrow}{}Q)\wedge{}P\to{}Q}\hspace{20pt} \frac{p\colon{}P\wedge{}Q\to{R}}{p^{\sim}\colon{}P\to{}Q{\Rightarrow}{R}} \end{align*}$$
Indexed products and sums:
$$\begin{align*}\frac{} {\varepsilon^{\Pi}_{\pi,P}\colon\pi^*\prod_{\pi} P\xrightarrow [\operatorname{\mathrm{1}}_A]{}P}\hspace{12pt} \frac{p\colon\pi^*S\xrightarrow [\operatorname{\mathrm{1}}_A]{}P}{\lambda{}p\colon{}S\xrightarrow [\operatorname{\mathrm{1}}_B]{}\prod_{\pi} P} {\hspace{24pt}} \frac{} {{P^{\uparrow}\pi}\colon{}P\xrightarrow [\pi]{}\sum_{\pi}{}P}\hspace{12pt} \frac{p\colon{}P\xrightarrow [\pi]{}S}{\underline p\colon\sum_{\pi} P\xrightarrow [\operatorname{\mathrm{1}}_B]{}S} \end{align*}$$
Equality objects:
$$\begin{align*}\frac{{\vphantom{P}}}{\rho_{\Delta}\colon\top_{A}\xrightarrow [\Delta]{}\operatorname{\mathrm{Eq}}_{\Delta}}\hspace{20pt} \frac{f\colon\top_A\xrightarrow [\Delta]{}S} {\xi{}f\colon\operatorname{\mathrm{Eq}}_{\Delta}\xrightarrow [\operatorname{\mathrm{1}}_B]{}S} \end{align*}$$
Stability of the operations under pullbacks
$$\begin{align*}\frac{{\vphantom{P}}}{{\mathrm{inv}}^{\top}_A\colon \top_{A'}\xrightarrow [\operatorname{\mathrm{1}}_{A'}]{}h^*\top_A}{\hspace{40pt}} \frac{{\vphantom{P}}}{{\mathrm{inv}}^{\bot}_A\colon h^*\bot_A\xrightarrow [\operatorname{\mathrm{1}}_{A'}]{}\bot_{A'}} \end{align*}$$
$$\begin{align*}\frac{{\vphantom{P}}}{{\mathrm{inv}}^{\wedge}_{PQ}\colon h^*P\wedge h^*Q\xrightarrow [\operatorname{\mathrm{1}}_{A'}]{}h^*(P\wedge Q)}{\hspace{40pt}} \frac{{\vphantom{P}}}{{\mathrm{inv}}^{\vee}_{PQ}\colon h^*(P\vee Q)\xrightarrow [\operatorname{\mathrm{1}}_{A'}]{}h^*P\vee h^* Q} \end{align*}$$
$$\begin{align*}\frac{{\vphantom{P}}}{{\mathrm{inv}}^{\Rightarrow}_{PQ}\colon h^*P{\Rightarrow} h^*Q\xrightarrow [\operatorname{\mathrm{1}}_{A'}]{}h^*(P{\Rightarrow} Q)} \end{align*}$$
$$\begin{align*}\frac{{\vphantom{P}}}{{\mathrm{inv}}^{\Sigma}_{\pi\pi'hk}\colon k^*\sum_{\pi} P\to\sum_{\pi'}h^*P}{\hspace{40pt}} \frac{{\vphantom{P}}}{{\mathrm{inv}}^{\Pi}_{\pi\pi'hk}\colon\prod_{\pi'}h^*P\to k^*\prod_{\pi} P} \end{align*}$$
Next, we will define certain identities defined over
$\sigma _{\mathbf {B}}'$
.
Each figure below represents a set of identities, one (or more) for each possible value of the relevant parameters
$A,B,C,f,g,P,Q,R,S,T,\Delta ,A',B',\pi ,\pi ',h,k,D, g',T'$
. The range of these parameters is as above, and in addition,
$D\in \operatorname {\mathrm {Ob}}{\mathbf {B}}$
,
$g'$
is a morphism
$C\to D$
, and 
.
We introduce certain abbreviations: under “Exponentials,” we write
$x\wedge y$
for
${\langle {{x\circ \pi _{PQ},y\circ \pi ^{\prime }_{PQ}}}\rangle }$
; under “Stability of the operations under pullbacks,” for an expression
$x\colon X\xrightarrow [\operatorname {\mathrm {1}}_A]{}Y$
, we write
$h^*x$
for
$\overline {x\circ {{h}^{\uparrow }Y}}^{\operatorname {\mathrm {1}}_{A'},h}$
, and similarly with
$\pi ^*x$
under “Indexed products and sums”; finally, under “Stability of the operations under pullbacks,” we write “
$X=Y^{-1}$
” as a shorthand for the two identities
$Y\circ X=\operatorname {\mathrm {1}}_W$
and
$X\circ Y=\operatorname {\mathrm {1}}_Z$
with appropriate W and Z.
Category:
$$\begin{align*}\frac{p\colon{}P\xrightarrow [f]{}S\hspace{20pt}{}q\colon{}S\xrightarrow [g]{}T\hspace{20pt}{}r\colon{}T\xrightarrow [h]{}T'} {p\circ{1_P}=p\hspace{20pt}{}1_S\circ{}p=p\hspace{20pt} {(r\circ{}q)\circ{}p=r\circ(q\circ{}p)}} \end{align*}$$
Fibration:
$$\begin{align*}\frac{p\colon{}P\xrightarrow [gf]{}T} {{{g}^{\uparrow}T}\circ \overline{p}^{f,g}=p}{\hspace{40pt}} \frac{p\colon{}P\xrightarrow [f]{}g^*T} {\overline{{{g}^{\uparrow}T}\circ p}^{f,g}=p} \end{align*}$$
Finite products and coproducts:
$$\begin{align*}\frac{p\colon{}P\to\top_{A}} {p=!_P}{\hspace{40pt}} \frac{p\colon\bot_{A}\to{}P} {p={\text{!`}}_P} \end{align*}$$
$$\begin{align*}\frac{p\colon{}P\to{}Q\hspace{20pt}{}q\colon{}P\to{}R} {\pi_{QR}\circ{\langle{{p,q}}\rangle}=p\hspace{20pt} \pi^{\prime}_{QR}\circ{\langle{{p,q}}\rangle}=q}\hspace{20pt} \frac{p\colon{}P\to{}Q\wedge{}R} {{\langle{{{\pi_{QR}\circ{}p,\pi^{\prime}_{QR}\circ{}p}}}\rangle}=p} \end{align*}$$
$$\begin{align*}\frac{p\colon{}P\to{}R\hspace{20pt}{}q\colon{}Q\to{}R} {[p,q]\circ\kappa_{PQ}=p\hspace{20pt} [p,q]\circ\kappa^{\prime}_{PQ}=q}\hspace{20pt} \frac{p\colon{}P\vee{}Q\to{}R} {[p\circ\kappa_{PQ},p\circ\kappa^{\prime}_{PQ}]=p} \end{align*}$$
Exponentials:
$$\begin{align*}\frac{p\colon{}P\wedge{}Q\to{}R} {\varepsilon_{QR}\circ{}(p^{\sim}\wedge{}1_Q)=p}{\hspace{40pt}} \frac{p\colon{}P\to{}(Q\Rightarrow{}R)} {(\varepsilon_{QR}\circ(p\wedge1_Q))^{\sim}=p} \end{align*}$$
Indexed products and sums:
$$\begin{align*}\frac{p\colon\pi^*S\xrightarrow [\operatorname{\mathrm{1}}_A]{}P} {\varepsilon^{\Pi}_{\pi,P}\circ\pi^*\lambda{}p=p}\hspace{20pt} \frac{p\colon{}S\xrightarrow [\operatorname{\mathrm{1}}_B]{}\prod_{\pi}{}P} {\lambda(\varepsilon^{\Pi}_{\pi,P}\circ\pi^*p)=p} {\hspace{40pt}} \frac{p\colon{}P\xrightarrow [\pi]{}S} {\underline{p}\circ{P^{\uparrow}\pi}=p}\hspace{20pt} \frac{p\colon\sum_{\pi} P\xrightarrow [\operatorname{\mathrm{1}}_B]{}S} {\underline{p\circ{P^{\uparrow}\pi}}=p} \end{align*}$$
Equality objects:
$$\begin{align*}\frac{p\colon\top_{A}\xrightarrow [\Delta]{}S} {\rho_{\Delta}\circ(\xi p)=p}{\hspace{40pt}} \frac{p\colon\operatorname{\mathrm{Eq}}_B\xrightarrow [\operatorname{\mathrm{1}}_B]{}S} {\xi(p\circ{}\rho_{\Delta})=p} \end{align*}$$
Stability of the operations under pullbacks
$$\begin{align*}{\mathrm{inv}}^{\top}_A\circ!_{h^*\top_A}=\operatorname{\mathrm{1}}_{h^*\top_A}\hspace{20pt} {\text{!`}}_{h^*\bot_A}\circ{\mathrm{inv}}^{\bot}_A=\operatorname{\mathrm{1}}_{h^*\bot_A} \end{align*}$$
$$\begin{align*}{\langle{{h^*\pi_{PQ},h^*\pi^{\prime}_{PQ}}}\rangle} =({\mathrm{inv}}^{\wedge}_{PQ})^{-1}\hspace{20pt} [h^*\kappa_{PQ},h^*\kappa^{\prime}_{PQ}]=({\mathrm{inv}}^{\vee}_{PQ})^{-1} \end{align*}$$
$$\begin{align*}h^*\varepsilon_{QR}\circ {\mathrm{inv}}^{\wedge}_{(Q\to R)Q}=({\mathrm{inv}}^{\Rightarrow}_{QR})^{-1} \end{align*}$$
$$\begin{align*}\underline{\overline{({{\pi}^{\uparrow}{P}})\circ({{h}^{\uparrow}P})}^{\pi',k}}=({\mathrm{inv}}^{\Sigma}_{\pi\pi'hk})^{-1}\quad \lambda\Big( h^*\varepsilon^{\Pi}_{\pi,P}\circ \overline{\overline{({{k}^{\uparrow}{{\textstyle\prod}_{\pi} P}})\circ({{\pi'}^{\uparrow}{(k^*{\textstyle\prod}_{\pi} P)}})}^{h,\pi}}^{\operatorname{\mathrm{1}}_{A'},h} \Big) =({\mathrm{inv}}^{\Pi}_{\pi\pi'hk})^{-1} \end{align*}$$
We now consider the initial model of the algebraic theory given by the above signature and identities, and we define a fibration 
by taking the set of objects of
${\mathbf {C}}$
to be
$\operatorname {\mathrm {Ob}}{\mathbf {C}}$
(as defined above)—and in particular taking the objects in the fiber over
$A\in {\mathbf {B}}$
to be 
(as defined above). Next, for a morphism
$f\colon A\to B$
in
${\mathbf {B}}$
and objects 
and 
, we take the set of morphisms
$P\to Q$
lying over f to be the set of elements of this initial model of sort
$(P,Q,f)$
(i.e.,
$P\xrightarrow [f]{}Q$
in the above notation).
For composition of morphisms in
${\mathbf {C}}$
, we take the operation
$\circ $
. It follows from the “Category” identities that this makes
${\mathbf {C}}$
into a category, and by the definition of the operation
$\circ $
, we have that this makes 
a prefibration (i.e., a functor).
The remaining operations and equations were chosen in precisely such a way so as to ensure that 
is an
$h^=$
-fibration.
Proposition A.2. The
$h^=$
-fibration 
defined above is free over
${\mathbf {B}}$
.
Proof Let 
be a second
$h^=$
-fibration over
${\mathbf {B}}$
. We must show that there is up to isomorphism a unique functor 
of
$h^=$
-fibrations over
${\mathbf {B}}$
(for general 
, this will require the axiom of choice).
By “specifying all the operations” in 
—i.e., choosing cartesian lifts (a cleavage), fiberwise products, coproducts, and exponentials, indexed products and sums along product projections, and equality objects—we obtain a
$\sigma _{\mathbf {B}}$
-structure with underlying (
$\operatorname {\mathrm {Ob}}\sigma _{\mathbf {B}}=\operatorname {\mathrm {Ob}}{\mathbf {B}}$
-indexed-)set
$\operatorname {\mathrm {Ob}}{\mathbf {C}}'$
.
By the initiality of the
$\sigma _{\mathbf {B}}$
-structure
$\operatorname {\mathrm {Ob}}{\mathbf {C}}$
, this gives us a function
$\Phi \colon \operatorname {\mathrm {Ob}}{\mathbf {C}}\to \operatorname {\mathrm {Ob}}{\mathbf {C}}'$
over
${\mathbf {B}}$
and preserving the specified operations.
We now consider a structure over
$\sigma _{\mathbf {B}}'$
, where the set of elements of sort
$(P,Q,f)$
is the set 
of morphisms
$\Phi P\to \Phi Q$
in 
lying over f. The operations are given in the obvious way. For instance, given
$f\colon A\to B$
in
${\mathbf {B}}$
and 
, the element
${{f}^{\uparrow }P}$
of sort
$(f^*P,P,f)$
should be a morphism
$\Phi (f^*P)\to \Phi P$
lying over f. But by the definition of
$\Phi $
, we know that
$\Phi (f^*P)$
is equal to the specified pullback
$f^*(\Phi P)$
, and hence we can take the morphism in question to be the specified cartesian lift
${{f}^{\uparrow }{(\Phi P)}}\colon f^*(\Phi P)\to \Phi P$
.
It follows from the fact that 
is an
$h^=$
-fibration that this structure satisfies all the identities listed above. Hence, by the initiality (with respect to the structures satisfying those identities) of the
$\sigma _{\mathbf {B}}'$
-structure given by the morphisms of
${\mathbf {C}}$
, we obtain a function 
preserving all of the operations. In particular, preservation of
$\circ $
and
$\operatorname {\mathrm {1}}$
implies that this is a functor, and it is then by definition a morphism of prefibrations.
The preservation of the remaining operations prove that this morphism of prefibrations preserve the specified
$h^=$
-fibration structure (the specified fiberwise product and coproducts, etc.), from which it follows that all instances of such operations (arbitrary fiberwise products and coproducts, etc.) are preserved.
This gives us the existence in the freeness statement.
Now suppose that we have two morphisms of
$h^=$
-fibrations 
over
${\mathbf {B}}$
. We would like to show that they are isomorphic over
${\mathbf {B}}$
.
We define isomorphisms
$\alpha _P\colon \Phi P{\xrightarrow {{}_{\sim }}} \Phi 'P$
by structural recursion on P. In each case, the isomorphism is determined by the universal properties of
$\Phi P$
and
$\Phi ' P$
using the isomorphisms already established. For example, suppose P is of the form
$Q\wedge R$
, and we have already isomorphisms
$\Phi Q{\xrightarrow {{}_{\sim }}} \Phi 'Q$
and
$\Phi R{\xrightarrow {{}_{\sim }}} \Phi 'R$
. We know that
$\Phi P$
is a product of
$\Phi Q$
and
$\Phi R$
and that
$\Phi 'P$
is a product of
$\Phi 'Q$
and
$\Phi 'R$
, and so we have an induced isomorphism
$\Phi P{\xrightarrow {{}_{\sim }}}\Phi 'P$
.
It remains to see that
$\alpha $
is a natural isomorphism over
${\mathbf {B}}$
. Note first of all that the isomorphisms all lie over identity morphisms in
${\mathbf {B}}$
, as required.
We check the naturality condition for morphisms p in
${\mathbf {C}}$
by structural induction on p (that is, recalling that the morphisms of
${\mathbf {C}}$
are equivalence classes of closed
$\sigma _{\mathbf {B}}'$
-terms, we do an induction on the
$\sigma _{\mathbf {B}}'$
-terms themselves). The base cases of this induction correspond to the 0-ary operations in
$\sigma _{\mathbf {B}}'$
. In each case, the naturality condition follows from the definition of
$\alpha $
. For instance, the isomorphism
$\alpha _{P\wedge Q}$
is defined precisely in such a way that the naturality squares for
$\pi _{PQ}$
and
$\pi ^{\prime }_{PQ}$
commute. (The base cases also include the various “
$\mathrm {inv}$
” morphisms under “Stability of the operations under pullbacks”; in this case, naturality follows from the fact that the naturality condition for a morphism implies the naturality condition for its inverse.)
The various induction steps all amount to showing that the naturality condition for a morphism induced by a certain universal property follows from the naturality conditions for the morphisms it is induced from. This can be checked straightforwardly in each case.
Remark A.1.2. We now explain a possible second, more conceptual (though not necessarily simpler) approach to proving the existence of a free
$h^=$
-fibration over an f.p. category
${\mathbf {B}}$
, using the “two-dimensional monad theory” of [Reference Blackwell, Kelly and Power3].
We first observe that the
$h^=$
-fibrations over
${\mathbf {B}}$
in which all of the operations (cartesian lifts fiberwise products and coproducts, etc.) have been specified—let us call these “
$h^=$
-cloven”
$h^=$
-fibrations—form a category, in which the morphisms are morphisms of
$h^=$
-fibrations over
${\mathbf {B}}$
that preserve all of the specified operations; and in fact, this category has a natural 2-categorical structure, in which we take as 2-cells all natural transformations over
${\mathbf {B}}$
. It also comes with a forgetful 2-functor to the 2-category
${\mathbf {Cat}}/{\mathbf {B}}$
of categories over
${\mathbf {B}}$
.
We now would like to say that this forgetful functor is monadic; i.e., that the
$h^=$
-cloven
$h^=$
-fibrations are precisely the T-algebras for a (in fact finitary) 2-monad T on
${\mathbf {Cat}}/{\mathbf {B}}$
. One can imagine constructing this monad by hand; for instance, the total category of 
should have as objects terms over the multi-sorted signature
$\sigma _{\mathbf {B}}$
introduced in Construction A.1, with
$\operatorname {\mathrm {Ob}}{\mathbf {C}}$
as the set of (sorted) variables, and as morphisms (equivalence classes of) terms over the signature
$\sigma _{\mathbf {B}}'$
with
$\operatorname {\mathrm {Ar}}{\mathbf {C}}$
as the set of sorted variables. Alternatively, one might hope to appeal to a
${\mathbf {Cat}}$
-enriched version of the Beck monadicity theorem.
In any case, if this monadicity is established—and assuming, as one would expect, that the morphisms of T-algebras (and 2-cells between them) in the sense of [Reference Blackwell, Kelly and Power3, p. 3] are precisely the morphisms of
$h^=$
-fibrations (and natural transformations)—then the existence of the free
$h^=$
-fibration over
${\mathbf {B}}$
follows easily from the results of op. cit.
Namely, we have (as usual) that the free
$h^=$
-cloven
$h^=$
-fibration 
produced in Construction A.1 is the free T-algebra on the empty category
$\emptyset \to {\mathbf {B}}$
over
${\mathbf {B}}$
(i.e., the value at
$\emptyset \to {\mathbf {B}}$
of the left adjoint to the forgetful functor from
$h^=$
-cloven
$h^=$
-fibrations). The desired universal property is then established as follows. According to [Reference Blackwell, Kelly and Power3, Corollary 5.6], 
(and more generally any free T-algebra) is “flexible,” which implies by [Reference Blackwell, Kelly and Power3, Theorem 4.7] that every morphism out of 
is isomorphic to a strict one. Since, for each
$h^=$
-fibration 
over
${\mathbf {B}}$
(once we make 
into a T-algebra by arbitrarily specifying operations on it), there is a unique strict morphism 
, it follows that any two morphisms 
are isomorphic, as desired.
A.2 Deductions
We will now formally introduce the notion of “intuitionistic validity” of first-order formulas; i.e., we introduce the (or rather a) deductive system for intuitionistic first-order logic.
The axiomatization we present is the one due to Lambek (for the propositional part) and Lawvere, in which the rules of inference corresponding to each logical connective correspond to the universal property of the corresponding categorical operation. As a result, we do not even need to state most of the rules, but rather just refer to the corresponding
$h^=$
-fibration operations as listed in Construction A.1.
As we mentioned in the introduction to Appendix A, this makes it “almost” obvious that the morphisms in the free
$h^=$
-fibration are given by equivalence classes of deductions. But, as we also mentioned there, there are exceptions: namely, the rules for quantification, equality, and substitution take on a different form.
For quantification, the difference is that in the syntax, we only quantify over a single variable at a time, whereas in the fibration, we take indexed sums and products along arbitrary product projections (corresponding to quantifying over several variables at once).
For equality, there is a similar circumstance, that we consider cocartesian lifts of arbitrary diagonal morphisms (corresponding to equating several pairs of terms at once). In addition, these cocartesian lifts correspond to equalities between variables, whereas in the syntax, we have equalities between arbitrary terms.
Finally, the substitution rule below corresponds to the pullback operation
$p\mapsto f^*p$
, which is not primitive among the operations listed in Construction A.1, but rather is derived from the cartesian lifts and their universal property.
Our definition of “deduction” will be given in terms of an initial structure for a certain algebraic signature, just as were the morphisms for the free
$h^=$
-fibration in Construction A.1. Hence, the deductions are given by closed terms over this signature (“proof terms” as they are often called in the context of dependent type theory) rather than the traditional “trees”; but of course, the tree corresponding to a certain deduction is recovered as the “syntax tree” of the corresponding term.
After introducing the notion of deduction, we prove the fundamental soundness property: that provable formulas are satisfied by all interpretations into a fibration; and for that purpose, we need another fundamental fact about fibrations which we have not mentioned explicitly, and which we state in Lemma A.4, namely the one relating pullbacks in a fibration to the syntactic operation of substitution.
Definition A.3. Let
$\sigma $
be a signature. We now define the set of deductions of first-order formulas over
$\sigma $
. Associated with each premise is a context
$\vec {x}$
, which is (as usual) a tuple of sorted variables, as well as a premise and conclusion, which are
$\sigma $
-formulas whose free variables are among those in
$\vec {x}$
. To indicate that p is a deduction with the context, premise, and conclusion
$\vec {x}$
,
${\varphi }$
, and
$\psi $
, we write
$p\colon {\varphi }\le _{\vec {x}}\psi $
.
Now, the set of deductions is defined inductively, and is in fact the initial structure for a certain multi-sorted algebraic signature, whose sorts are the triples
${\varphi }\le _{\vec {x}}\psi $
as above, which we call sequents. We must now describe the function symbols—which we will call “rules of inference”—and their arities and output sorts. For the most part, these are given as a subset of those listed in the first table in Construction A.1 (on page 39)—namely, those under “Finite products and coproducts” and “Exponentials” and the first two under “Category and fibration structure”—with certain modifications. The modifications are: (i) we now allow
$P,Q,R$
to be arbitrary formulas (so that for each figure in the table, we get one rule of inference for each choice of such formulas), (ii) we ignore the subscripts
$_{f}$
,
$_g$
,
$_{gf}$
, and
$_A$
in the figures for
$q\circ p$
,
$!_P$
and
${\text {!`}}_P$
, and (iii) we replace each arrow
$\to $
with
$\le _{\vec {x}}$
, where
$\vec {x}$
is an arbitrary context containing all the free variables of the formulas
$P,Q,R$
involved (so that, again, we get one rule of inference for each possible value of
$\vec {x}$
). The arities and output sorts of the function symbols are to be understood in the same way as in Construction A.1 (e.g., the arity of the rule of inference corresponding to the function symbol “
$\circ $
” is
${\langle {{P\le _{\vec {x}}Q,Q\le _{\vec {x}}R}}\rangle }$
and its output sort is
$P\le _{\vec {x}}R$
).
Finally, we have the following rules of inference (corresponding to the rest of the operations in the table on page 39, except for the “stability” ones), where again the arities and output sorts are to be understood in the same way as above. Note that unlike in the table on page 39, we are not introducing any notation for these function symbols (i.e., rules of inference).
Again, each figure below presents a set of inference rules, one for each value of the relevant parameters. Here,
$\vec {x}$
,
$\vec {y}$
are arbitrary sequences of variables, and
$y,z$
are arbitrary variables, with z and y of the same sort in the final rule;
$P,Q,R$
are arbitrary formulas, with certain restrictions on the free variables; namely, they should be among those in
$\vec {y}$
in the “Substitution rule,” among those in
$\vec {x}z$
in the “Quantifiers” rules, and among those in
$\vec {x}yz$
in the “Equality rule,” and moreover z should not be free in P and Q, respectively, in the first and third quantifier rules; and
$\vec {t}$
is an arbitrary tuple of terms with free variables among those in
$\vec {x}$
and with
$\operatorname {\mathrm {tp}}\vec {t}=\operatorname {\mathrm {tp}}\vec {y}$
.
We denote by
$X[\vec {a}:=\vec {b}]$
the result of (simultaneously) substituting the terms
$\vec {b}$
for the variables
$\vec {a}$
in a term or formula X (where we may assume that the none of the variables in
$\vec {a}$
are bound in X—see Definition 2.18).
Substitution:
$$\begin{align*}\frac{P\le_{\vec{y}}Q}{P[\vec{y}:=\vec{t}]\le_{\vec{x}}Q[\vec{y}:=\vec{t}]} \end{align*}$$
Quantifiers:
$$\begin{align*}\frac{P\le_{\vec{x}z}Q}{P\le_{\vec{x}}\forall z Q}\hspace{20pt} \frac{{\vphantom{P}}}{\forall z P\le_{\vec{x}z} P}{\hspace{40pt}} \frac{P\le_{\vec{x}z}Q}{\exists z P\le_{\vec{x}}Q}\hspace{20pt} \frac{{\vphantom{P}}}{P\le_{\vec{x}z}\exists z P} \end{align*}$$
Equality:
$$\begin{align*}\frac{{\vphantom{P}}}{\top\le_{\vec{x}z}z=z}{\hspace{40pt}} \frac{\top\le_{\vec{x}y}P[z:=y]}{y=z\le_{\vec{x}yz}P} \end{align*}$$
We say that a sequent
${\varphi }\le _{\vec {x}}\psi $
is provable if it is the sort of some deduction, and that a formula
${\varphi }$
is provable if
$\top \le _{\vec {x}}{\varphi }$
is provable for some (and hence, by the substitution rule, every) context
$\vec {x}$
containing the free variables of
${\varphi }$
.
Generalizing Definition 2.19, given an
$h^=$
-fibration 
and an interpretation 
, we say that M satisfies the sequent
${\varphi }\le _{\vec {x}}\psi $
if there exists a morphism
$\widehat M_{\vec {x}}({\varphi })\to \widehat M_{\vec {x}}(\psi )$
over
$M(\vec {x})$
.
Lemma A.4. Let
${\mathbf {B}}$
be an f.p. category, and let
$M\colon \sigma \to {\mathbf {B}}$
be an interpretation. Then for any tuples-of-terms-in-context
$(\vec {t},\vec {y})$
and
$(\vec {s},\vec {x})$
with
$\operatorname {\mathrm {tp}}(\vec {s})=\vec {y}$
, we have
$M_{\vec {y}}\vec {t}\cdot M_{\vec {x}}\vec {s}=M_{\vec {x}}(\vec {t}[\vec {y}:=\vec {s}])$
.
Next, given an
$h^=$
-fibration 
over
${\mathbf {B}}$
and an interpretation
$\widehat M$
in 
over M, then for any tuple-of-terms-in-context
$(\vec {t},\vec {x})$
and any formula-in-context
$({\varphi },\vec {y})$
with
$\operatorname {\mathrm {tp}}(\vec {t})=\operatorname {\mathrm {tp}}(\vec {y})$
, we have
$(M_{\vec x}\vec {t})^*(\widehat M_{\vec y}{\varphi })\cong \widehat M_{\vec {x}}({\varphi }[\vec {x}:=\vec {t}])$
.
Proof This is well-known (and as we mentioned, is fundamental to the role of fibrations in logic). Both claims are proven by induction. The second claim uses the first claim for the base case of equality, and the remaining induction steps all make use of the various stability conditions in an
$h^=$
-fibration. We leave the details to the reader.
Proposition A.5. Given any interpretation 
of a signature
$\sigma $
, M satisfies every provable sequent
${\varphi }\le _{\vec {x}}\psi $
over
$\sigma $
.
Proof We need to show that for every deduction
$p\colon {\varphi }\le _{\vec {x}}\psi $
, there exists a morphism
$\widehat M_{\vec {x}}({\varphi })\to \widehat M_{\vec {x}}(\psi )$
over
$M(\vec {x})$
and of course, we prove this by induction on p.
But in each induction step, it follows immediately from the definition of
$\widehat M$
that such a morphism exists, where for the “Substitution,” “Quantifier,” and “Equality” rules, we must use Lemma A.4 concerning pullbacks and substitution (and the special case of it that says that if z is not free in
${\varphi }$
, then
$M_{\vec {x}z}({\varphi })=\pi ^*M_{\vec {x}}({\varphi })$
, with
$\pi ={\langle {{\pi ^M_1,\ldots ,\pi ^M_{{\ell ({\vec {x}})}}}}\rangle }$
).
For the “Equality” rule, we also need to use the stability of equality morphisms (i.e., cocartesian lifts of generalized diagonal morphisms—see [Reference Helfer8, Sections 1.6 and 1.7]), which holds in
$h^=$
-fibrations by Proposition 2.4.
A.3 The free
$h^=$
-fibration over a free f.p. category
We now specialize to the case of a free
$h^=$
-fibration over the free f.p. category on some signature
$\sigma $
, and draw certain “syntactic” conclusions. Namely, in this case, as we have said, the free
$h^=$
-fibration can be given a direct, syntactic construction, in which the objects of the total category are formulas and the morphisms are equivalence classes of deductions, and we would like to recover this description from our construction.
Here, we will recover only part of this description: we will show that the objects of the total category “are” the formulas (more precisely, that each object is isomorphic to the interpretation of some formula), and that a morphism exists between two of these if and only if the corresponding implication is provable (as we explain in the proof, this amounts to a completeness theorem for the fibrational semantics).
We note that the “posetal” version of the syntactic construction of the free
$h^=$
-fibration is much simpler, and in fact, we will make use of it in the proof of said completeness theorem.
We would like to mention a second way to recover the morphisms-as-deductions description of the free
$h^=$
-fibration. Namely, rather than adapting the construction of the fibration to conform to the syntax, we can observe that the “syntax of first-order logic” is not absolute; one could also just use a different syntax and deductive system so as to be adapted to the above construction of the free
$h^=$
-fibration. This would involve slightly modifying the implementation of equality and quantification in the syntax, as well as introducing “explicit substitutions,” i.e., substitution as a primitive operation.
To begin with, we recall the well-known construction, due to Lawvere, of a free f.p. category associated with an algebraic signature
$\sigma $
(cf. [Reference Makkai20, p. 473]).
Proposition A.6. Given an algebraic signature
$\sigma $
, there exists a free f.p. category
${\mathbf {B}}$
over
$\sigma $
via an interpretation
$i\colon \sigma \to {\mathbf {B}}$
. Moreover any such
${\mathbf {B}}$
and i have the following property: every object in
${\mathbf {B}}$
is of the form
$i(\vec {A})$
for a unique
$\vec {A}\in (\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$
, and every morphism
$i(\vec {A})\to i(\vec {B})$
is of the form
$i_{\vec {x}}(\vec {t})$
for a tuple-of-terms-in-context
$(\vec {t},\vec {x})$
, unique up to substituting
$\vec {x}$
for a different sequence
$\vec {y}$
of variables with
$\operatorname {\mathrm {tp}}(\vec {y})=\vec {A}$
(i.e., replacing
$(\vec {t},\vec {x})$
with
$(\vec {t}[\vec {x}:=\vec {y}],\vec {y})$
.
Proof The stated property together with the first part of Lemma A.4 determines
${\mathbf {B}}$
and
$i\colon \sigma \to {\mathbf {B}}$
up to isomorphism, and it is straightforward to verify that this indeed produces an f.p. category and has the required universal property.
Definition A.7. Proposition A.6 gives an explicit description of a free f.p. category on an algebraic signature
$\sigma $
: the set of objects is
$(\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$
, the morphisms are equivalence classes of tuples-of-terms-in-context up to renaming of variables, and composition is given by substitution as in Lemma A.4.
We denote the resulting category by
$\mathbf {Tm}_{\sigma }$
and the associated
$\sigma $
-interpretation (which is the identity on
$(\operatorname {\mathrm {Ob}}\sigma )^{<\omega }$
and takes each tuple-of-terms-in-context to its equivalence class) by
$i\colon \sigma \to \mathbf {Tm}_{\sigma }$
.
Proposition A.8. Given a free
$h^=$
-fibration 
over
$\mathbf {Tm}_{\sigma }$
and an interpretation
$\hat \imath $
in 
over i, each object in
${\mathbf {C}}$
is isomorphic to
$\hat \imath _{\vec {x}}{\varphi }$
for some
$(\vec {x},{\varphi })$
.
Proof Let
$\mathcal {A}\subset \operatorname {\mathrm {Ob}}{\mathbf {C}}$
be the set of objects which are isomorphic to some
$\hat \imath _{\vec {x}}{\varphi }$
. It suffices to see that
$\mathcal {A}$
is closed under all of the operations which inductively define the set
$\operatorname {\mathrm {Ob}}{\mathbf {C}}$
.
It is obvious from the definition of
$\hat \imath _{\vec {x}}{\varphi }$
that
$\mathcal {A}$
is closed under fiberwise products, coproducts, and exponentials and since every object of
$\mathbf {Tm}_{\sigma }$
is of the form
$i(\vec {A})$
, it follows that
$\mathcal {A}$
includes initial and terminal objects in each fiber. By Lemma A.4 and since every morphism in
$\mathbf {Tm}_{\sigma }$
is of the form
$i_{\vec {x}}(\vec {t})$
,
$\mathcal {A}$
is also closed under pullbacks.
Next, we have that
$\mathcal {A}$
is closed under certain indexed products and sums, namely the ones along projections of the form
${\langle {{\pi _1^i,\ldots ,\pi _{{\ell ({\vec {A}})}}^i}}\rangle }\colon i(\vec {A}B)\to i(\vec {A})$
. We also know that
$\mathcal {A}$
is closed under indexed product and sums along isomorphisms, as these are the same as pullbacks. Also, if
$\mathcal {A}$
is closed under indexed products and sums of any two composable morphisms, then the same is true of the composite (this is because
$\prod _{gf}P\cong \prod _g\prod _fP$
and similarly with
$\sum _{gf}$
, since a composite of (ana-)adjoints is an (ana-)adjoint of the composite).
But now it is easy to see that every product projection in
$\mathbf {Tm}_{\sigma }$
is a composite of the above particular product projections and isomorphisms.
Finally, we need to see that
$\mathcal {A}$
contains an equality object
$\operatorname {\mathrm {Eq}}_A$
for every diagonal morphisms
$\Delta \colon A\to A\times A$
. Firstly, it suffices to do this for some diagonal morphism for each object A (since, for example,
$\mathcal {A}$
is closed under isomorphisms, as every isomorphism is cartesian). Next, for a product
$A\times B$
, we have that
$\operatorname {\mathrm {Eq}}_{A\times B}$
is a fiberwise product of pullbacks of
$\operatorname {\mathrm {Eq}}_A$
and
$\operatorname {\mathrm {Eq}}_B$
(see [Reference Lawvere15, p. 10] or [Reference Helfer8, Theorem 7.2]), so the claim for
$A\times B$
follows from that of A and B. Hence, by induction, it suffices to show the claim for each
$i({\langle {{A}}\rangle })$
, for which we have
$\operatorname {\mathrm {Eq}}_{{\langle {{A}}\rangle }}\cong \hat \imath _{{\langle {{x,y}}\rangle }}(x=y)$
(with
$\operatorname {\mathrm {tp}}(x)=\operatorname {\mathrm {tp}}(y)=A$
), and for the terminal object
$\mathbf {1}=i(\emptyset )$
, for which 
.
Theorem A.9. Let 
be a free
$h^=$
-fibration over
$\mathbf {Tm}_{\sigma }$
, and fix an interpretation
$\hat \imath $
in 
over i. Then a sequent
${\varphi }\le _{\vec {x}}\psi $
is satisfied by i if and only if it is provable.
Proof The
$(\Longleftarrow )$
implication follows from soundness (Proposition A.5). We now consider the other implication.
Fix a sequent
${\varphi }\le _{\vec {x}}\psi $
, and suppose it is satisfied by i, i.e., there exists a morphism
$\hat \imath _{\vec {x}}({\varphi })\to \hat \imath _{\vec {x}}(\psi )$
over
$i(\vec {x})$
. Note that it is then satisfied by any interpretation in any
$h^=$
-fibration 
. Indeed, given an interpretation 
, we have, by the freeness of 
, a morphism 
with
$\xi \circ i=M$
. Then
$\Xi \circ \hat \imath $
and
$\widehat M$
will be isomorphic interpretations over M, and the morphism
$\hat \imath _{\vec {x}}({\varphi })\to \hat \imath _{\vec {x}}(\psi )$
then gives a morphism
$$\begin{align*}\widehat M_{\vec{x}}({\varphi}) \cong (\Xi\circ\hat\imath)_{\vec{x}}({\varphi})\to (\Xi\circ\hat\imath)_{\vec{x}}(\psi) \cong \widehat M_{\vec{x}}(\psi) \end{align*}$$
over
$M(\vec {x})$
.
Hence, it suffices to show the completeness of the fibrational semantics—i.e., that if a sequent is satisfied by every interpretation in an
$h^=$
-fibration, then it is provable.
A heavy-handed way to do this is to appeal, for example, to Kripke’s completeness theorem for intuitionistic logic. Kripke models are precisely interpretations in the
$h^=$
-fibrations 
with P an arbitrary poset. Kripke’s completeness theorem then says that if a sequent is satisfied by every interpretation in such an
$h^=$
-fibration, then it is provable.
Besides being overkill, this proof has the following disadvantage: we might like to deduce Kripke’s completeness theorem from its categorical formulation in [Reference Makkai19, Reference Makkai20], and this proof would make such a deduction circular. Hence, we now give a more direct proof.
Namely, we will produce a single fibration 
over
${\mathbf {B}}$
such that any sequent satisfied by i (with respect to 
) is provable.
will be a posetal fibration (i.e., the fibers are posets), where each fiber is a “Lindenbaum–Tarski (Heyting) algebra.” Namely, to define the fiber over
$\vec {A}$
, consider the preorder whose objects are formulas-in-context
$({\varphi },\vec {x})$
with
$\operatorname {\mathrm {tp}}(\vec {x})=\vec {A}$
, with the ordering given by provability (i.e.,
$({\varphi },\vec {x})\le (\psi ,\vec {y})$
if
${\varphi }\le _{\vec {x}}\psi [\vec {y}:=\vec {x}]$
is provable), and take its “posetal collapse (or reflection)” (i.e., identify objects that are equal in the ordering).
Organizing these fibers into a fibration amounts to defining a functor
$\mathbf {Tm}_{\sigma }^{\operatorname {op}}\to \mathbf {Poset}$
to the category of posets with the given action on objects, and we do this by sending
$[\vec {t},\vec {x}]$
(square brackets denotes the equivalence class) to the function 
taking
$[{\varphi },\vec {y}]$
to
$[{\varphi }[\vec {y}:=\vec {t}],\vec {x}]$
. That this is well-defined and a morphism of posets follows from the substitution rule, and it follows from the fact that
${\varphi }[\vec {y}:=\vec {t}][\vec {x}:=\vec {s}]={\varphi }[\vec {y}:=(\vec {t}[\vec {x}:=\vec {s}])]$
that this defines a functor.
That the resulting fibration is fiberwise bicartesian-closed (i.e., has Heyting algebra fibers) follows immediately from the rules of inference for the propositional connectives. The rules of inference for equality and quantifiers give the existence of equality objects and indexed products and sums over certain (generalized) diagonal and projection morphisms, but as in the proof of Proposition A.8, these morphisms generate all of the diagonal morphisms and projections. We leave the details to the reader.
The resulting fibration is in fact the posetal reflection of the free fibration 
, and is the free posetal
$h^=$
-fibration over 
(see [Reference Makkai19, p. 349]), though we will need neither of these facts.
In fact, we are done, as it is immediate from the definition that, under the obvious interpretation
$\hat \imath $
in 
over i, that a sequent is provable if and only if it is satisfied by i.
Corollary A.10. For any signature
$\sigma $
, there exists a free
$h^=$
-fibration 
and an interpretation
$\hat \imath $
in 
over i such that
-
• The objects in
are equivalence classes
$[{\varphi },\vec {x}]$
of formulas-in-context with
$\operatorname {\mathrm {tp}}\vec {x}=\vec {A}$
(the equivalence relation being renaming of variables—i.e.,
$({\varphi },\vec {x})$
and
$(\psi ,\vec {y})$
are equivalent iff
$\psi ={\varphi }[\vec {x}:=\vec {y}]$
). -
• We have
$\hat \imath _{\vec {x}}{\varphi }=[{\varphi },\vec {x}]$
for all
$({\varphi },\vec {x})$
. -
• There is a morphism
$[{\varphi },\vec {x}]\to [\psi ,\vec {x}]$
in if and only if
${\varphi }\le _{\vec {x}}\psi $
is provable.
are equivalence classes 
if and only if 
Acknowledgments
I am grateful to McGill’s Logic, Category Theory, and Computation seminar and Carnegie Mellon’s Homotopy Type Theory seminar for allowing me to speak about this project at a very early stage, and to Steve Awodey for encouraging me to write it up, and also for pointing out an interesting connection between our invariance theorem and the Univalence Axiom (which was also independently observed by Ulrik Buchholtz).
I would also like to acknowledge the various contributors to ncatlab.org, which is an invaluable resource in general, and has been no less for this project.
Finally, I am grateful to the referee for suggesting several changes which improved the paper.
which are themselves “posetal” in this sense, but this is not the case for the fibration 
of interest.
, in which we can uniformly specify all the required operations.
), so that, for instance, 
should be an h-fibration.
there is a unique isomorphism between them, as our Construction 
