Homology, Homotopy and Applications, vol.5(2), 2003, pp.137–209

ON THE GEOMETRY OF INTUITIONISTIC S4 PROOFS

JEAN GOUBAULT-LARRECQ and ÉRIC GOUBAULT

(communicated by Gunnar Carlsson)

Abstract

The Curry-Howard correspondence between formulas and types, proofs and programs, proof simplification and program execution, also holds for intuitionistic modal logic S4. It turns out that the S4 modalities translate as a monoidal comonad on the space of proofs, giving rise to a canonical augmented simplicial structure. We study the geometry of these augmented simplicial sets, showing that each type gives rise to an augmented simplicial set which is a disjoint sum of nerves of finite lattices of points, plus isolated (−1)-dimensional subcomplexes. As an application, we give semantics of modal proofs (a.k.a., programs) in categories of augmented simplicial sets and of topological spaces, and prove a completeness result in the style of Friedman: if any two proofs have the same denotations in each augmented simplicial model, then they are convertible. This result rests both on the fine geometric structure of the constructed spaces of proofs and on properties of subscone categories—the categorical generalization of the notion of logical relations used in lambda-calculus.

1. Introduction

One of the most successful paradigms in modern theoretical computer science is the so-called Curry-Howard isomorphism [29], an easy but surprising connection between proofs in intuitionistic logics and functional programs, which has far-reaching consequences. One cardinal principle here is that logics help design well-crafted programming constructs, with good semantical properties. In intuitionistic logic, implications denote function spaces, conjunctions give rise to cartesian products, disjunctions are disjoint sums, false is the empty type, true is the unit type, universal quantifications are polymorphic types, existential quantifications are abstract

The first author acknowledges GIE Dyade, a common venture between Bull S.A. and INRIA, where part of this work was accomplished. Received October 15, 2001, revised July 24, 2002; published on April 22, 2003. 2000 Mathematics Subject Classification: 03B45, 03B70, 18A25, 18C15, 18C50, 18D15, 18F20, 18G10, 18G30, 55U10, 68N18, 68Q55 Key words and phrases: comonads, completeness, Curry-Howard correspondence, distributivity laws (for comonads), intuitionistic logic, lambda-calculus, logical relations, modal logic, presheaves, resolution functors, S4, simplicial sets, subscones. \begin{matrix}c \\ ◯ \end{matrix} 2003, Jean Goubault-Larrecq and Éric Goubault. Permission to copy for private use granted.

data types. Classical logic in addition introduces the rich concept of continuation [26, 42], while the modal logic S4 introduces a form of staged computation [44, 11].

Our aim in this paper is to show that S4 proofs are also geometric objects. To be precise, S4 formulas correspond to augmented simplicial sets, and S4 proofs correspond to maps between these spaces. In particular, this extends the Curry-Howard picture to:

Logic  Programming  Geometry
Formulae  =  Types  = Augmented Simplical Sets
Proofs  =  Programs  = Augmented Simplicial Maps
Equality of Proofs = Convertibility =  Equality of Maps

The = signs are exact, except possibly for the Programs=Augmented Simplicial Maps one (we only get definable augmented simplicial maps). In particular, it is well-known that equality of proofs, as defined by the symmetric closure of detour, or cut-elimination [47], is exactly convertibility of terms (programs). We shall in addition show that two (definable) augmented simplicial maps are equal if and only if their defining terms are convertible, i.e., equal as proofs (bottom right = sign). This will be Theorem 72 and Corollary 73, an S4 variant of Friedman’s Theorem [16], which will constitute the main goal of this paper.

While Friedman’s Theorem in the ordinary, non-modal, intuitionistic case can be proved in a relatively straightforward way using logical relations [40], the S4 case is more complex, and seems to require one to establish the existence of a certain strong retraction of one augmented simplicial set HomΔ̂(S4 [F], S4 [G]) onto another S4 [F ⊃ G] (Corollary 48). By the way, we invite the reader to check that the existence of the corresponding strong retraction in the category of sets (as would be needed to map our techniques to the non-modal case) is trivial. The existence of the announced retraction in the category Δ̂ of augmented simplicial sets is more involved, and prompts us to study the geometry of S4 proofs themselves.

The plan of the paper is as follows. After we review related work in Section 2, we deal with all logical preliminaries in Section 3. We start by recalling some basic concepts in logics in Section 3.1, and go on to the Curry-Howard correspondence between types and formulae, proofs and programs, equality of proofs and convertibility in Section 3.2. We also introduce the logic we shall use, namely minimal intuitionistic S4, giving its Kripke semantics (Section 3.4) as well as a natural deduction system and a proof term language λ_{S4}, essentially due to [7], for it. This is in Section 4.1, where we also prove basic properties about λ_{S4}—confluence, strong normalization of typed terms—and study the structure of normal and so-called η-long normal forms.

We come to the meat of this paper in Section 4, where we observe that each type F induces an augmented simplicial set whose q-simplices are terms of type □^{q+1}F modulo ≈. We characterize exactly the computation of faces and degeneracies on terms written in η-long normal form in Section 4.1, where they take a particularly simple form. This allows us to study the geometry of these terms in a precise way in Section 4.2. The crucial notion here is oriented contiguity, which is an oriented form of path-connectedness. It turns out that this allows us to characterize the simplicial part of these augmented simplicial sets as the nerve of its points ordered by contiguity—this is an oriented simplicial complex. In dimension −1, we get all connected components of these simplicial complexes, as we show in Section 4.3. We also show that each non-empty connected component is a finite lattice of points (0-simplices). In Section 4.4 we turn to another important construction in these augmented simplicial sets, that of planes. Using the lattice structure, we are able to show that there are augmented simplicial maps projecting the whole space onto planes, under mild conditions. This is the essential ingredient in showing that HomΔ̂(S4 [F], S4 [G]) strongly retracts onto S4 [F ⊃ G], as announced above.

Section 5 reverses the picture and shows that we may always interpret proofs as augmented simplicial maps. In general, we may always interpret proofs in any cartesian closed category (CCC) with a (strict) monoidal comonad—so-called strict CS4 categories—, as shown in Section 5.1 and Section 5.2. We give examples of strict CS4 categories in Section 5.1. In Section 5.2, we show additionally that the typed λ_{S4} calculus is a way of describing the free strict CS4 category on a given set of base types. In particular, strict CS4 categories offer a sound and complete way of describing λ_{S4} terms and equalities between them. However, these categories are general constructions that need to be made more concrete. We would like to be able to compare proofs in S4 by looking at them not in any strict CS4 category, but in more concrete ones, in particular in the category Δ̂ of augmented simplicial sets. We show that λ_{S4} terms still get interpreted faithfully in Δ̂ in Section 5.7—this is Friedman’s Theorem for S4, which we prove using a variant of Kripke logical relations indexed over the category Δ, and using in an essential way the strong retraction of HomΔ̂(S4 [F], S4 [G]) onto S4 [F ⊃ G] that we constructed in Section 4.4. We review logical relations in Section 5.3, explain how they work and why they should be generalized to some form of Kripke logical relation in our case. This is complex, and better viewed from an abstract, categorical viewpoint: this is why we use subscones (presented in Section 5.4), establish the Basic Lemma in Section 5.5 and the Bounding Lemma in Section 5.6, the main two ingredients in the equational completeness theorem of Section 5.7.

The proof of some minor theorems of this paper have been elided. Please refer to the full report for fuller proofs [23].

2. Related Work

First, let us dispel a possible misunderstanding. The part of this paper concerned with logic is about the proof theory of S4, that is, the study of proof terms as a programming language, not about validity or provability. The reader interested in categorical models of validity in the modal case is referred to [52] and the references therein. In this line, a well-known topological interpretation of the □ modality of S4, due to Kuratowski, is as follows: interpret each formula F as a subset of some topological space, and □F as the interior of F. (In general, any coclosure operator works here.) Note that this interpretation collapses □F with □□F, while our interpretations of □ will not. In fact no □^{p}F can be compared with any □^{q}F in our interpretations unless p = q.

It is easier to reason on proof terms than directly on proofs. In particular, it is more convenient to reason on Church’s λ-calculus than on natural deduction proofs. This is why we use Bierman and de Paiva’s λ_{S4} language [7] of proof terms for S4. There would have been many other suitable proposals, e.g., [44, 11, 38]. In particular, [21] dispenses with boxes around terms to represent □-introduction rules, by using operators with non-negative indices corresponding to dimensions. The augmented simplicial structure of the language is apparent in the syntax of this language; however λ_{S4} turned out to be more convenient technically.

S4 proof terms have been used for partial evaluation [50], run-time program generation [11], in higher-order abstract syntax [34], etc. The idea is that whereas F is a type of values, □F is a type of delayed computations of values of type F, or of terms denoting values of type F; d evaluates these computations or these terms to return their values, and s lifts any delayed computation M to a doubly delayed computation whose value is M itself. This is similar to eval/quote in Lisp [35], or to processes evolving through time, say, starting at t = 0 and homing in on their values at t = 1, as argued in the (unpublished) paper [22]. This is also similar to the viewpoint of Brookes and Geva [9], where comonads (□, d, s) are enriched into so-called computational comonads, by adding a natural transformation γ from the identity functor to □ allowing to lift any value, not just any computation, to a computation; γ must be such that d ∘ γ_{F} = id_{F} and s ∘ γ_{F} = γ_{□F} ∘ γ_{F}. In Δ̂, such a γ induces a contracting homotopy s_{q}^{−1} : K_{q} → K_{q+1} for every q ⩾ −1, by s_{q}^{−1} ˆ=□^{q+1}(γ_{K_{−1}}); these are often used to build resolutions of chain complexes. While our comonads need not be computational in this sense, the role of contracting homotopies should become clearer by pondering over Proposition 67 and the construction of Lemma 46.

It is tempting to compare the computational comonads to E. Moggi’s computational λ-calculus, i.e. CCCs with a strong monad. [6] is a nice introduction to the latter, and to their relation with Fairtlough and Mendler’s propositional lax logic. According to Brookes and Geva, there is no special connection between computational comonads and strong monads. However, in a sense they do express similar concerns in programming language theory. Moreover, as shown in [6], strong monads are best understood as the existential dual ♢ (“in some future”) to □ (“in all futures”). Kobayashi [32] deals with a calculus containing both □ and ♢. Pfenning and Davies [43] give an improved framework for combining both □ and ♢, and show how lax logic is naturally embedded in it. While classical negation provides a natural link between both modalities, in intuitionistic logic the link is more tenuous. Following R. Goré, there is a more cogent, intuitionistically valid connection between an existential and a universal modality, provided the existential modality is defined as a monad that is left-adjoint to □. In this sense, Moggi’s strong monad should be written as the tense logic modality ♦ (“in some past”), so that ♦F ⊃ G is provable if and only if F ⊃ □G is. This duality is reflected in programming-language semantics, where □F is the type of computations whose values are in F, while ♦G is the type of values produced by computations in G. Geometrically, ♦F builds a space of cones over the space F (at least as soon as F is connected), and this may be defined in categories of topological spaces or of augmented simplicial sets [46]; it turns out that the cone modality is indeed a strong monad. However existentials, and therefore also ♦, are hard to deal with in establishing equational completeness results, and this is why we won’t consider them in this paper. (The notion of logical relation for strong monads developed in [24] may be of some help here.)

We hope that studies of the kind presented here will help understand connections between computation, logic and geometry. The relation to other geometric ways of viewing computation, such as [27] on distributed computation, is yet to be clarified. Another interesting piece of work at the intersection of logic (here, linear logic) and simplicial geometry is [3, 4], which provides sophisticated models for the multiplicative-exponential fragment of linear logic [17] based on affine simplicial spaces with an extra homological constraint. Note that there are strong links between S4 and linear logic, see e.g., [37].

3. Logics, the Curry-Howard Correspondence, and S4

3.1. Logics

Consider any logic, specified as a set of deduction rules. So we have got a notion of formula, plus a notion of deduction, or proof. Those formulas that we can deduce are called theorems. For example, in minimal propositional logic, one of the smallest non-trivial logics, the formulas are given by the grammar:

F, G ::= A|F ⊃ G

where A ranges over propositional variables in some fixed set Σ, and ⊃ is implication. (This logic is called minimal because removing the only operator, ⊃, would leave us with something too skinny to be called a logic at all.) The deductions in the standard Hilbert system for intuitionistic minimal logic are given by the following axioms:

F ⊃ G ⊃ F  (1)
(F ⊃ G ⊃ H) ⊃ (F ⊃ G) ⊃ F ⊃ H  (2)

where F, G, H range over all formulas, and ⊃ associates to the right, that is, e.g., F ⊃ G ⊃ H abbreviates F ⊃ (G ⊃ H); and the modus ponens rule:

F ⊃ G F ; (MP) ; G

which allows one to deduce G from two proofs, one of F ⊃ G, the other of F. Now there is a third level, apart from formulas and proofs, namely proof simplifications. Consider for example the following proof:

\begin{aligned}\begin{aligned}& (1) \\ F ⊃ G ⊃ F \end{aligned} & \begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} π_{1} \\ F \end{matrix} \\ & (MP) \\ G ⊃ F \end{aligned} \begin{matrix}\begin{matrix}· \\ · \\ · \end{matrix} π_{2} \\ G \end{matrix}
(MP)
F

This may be simplified to just the proof π_{1}. The idea that proofs may be simplified until no simplification can be made any longer, obtaining equivalent normal proofs, was pioneered by Gerhard Gentzen [48] to give the first finitist proof (in the sense of Hilbert) of the consistency of first-order Peano arithmetic. If the logical system is presented in a proper way, as with Gentzen’s sequent calculus, it is easy to see that false has no normal proof (no rule can lead to a proof of false). So false has no proof, otherwise any proof π of false could be simplified to a normal proof of false, which does not exist. Hilbert systems as the one above are not really suited to the task, and we shall instead use natural deduction systems [47] in Section 3.3.

3.2. The Curry-Howard Correspondence

Note that there is another reading of the logic. Consider any formula as being a set: F ⊃ G will denote the set of all total functions from the set F to the set G. Then proofs are inhabitants of these sets: interpret the one-step proof (1) as the function taking x ∈ F and returning the function that takes y ∈ G and returns x, interpret (2) as the more complex functional that takes x ∈ F ⊃ G ⊃ H, y ∈ F ⊃ G, and z ∈ F, and returns x(z)(y(z)); finally, if π_{1} is a proof of F ⊃ G—a function from F to G—and π_{2} is in F, then (MP) builds π_{1}(π_{2}), an element of G. Syntactically, we build a programming language by defining terms:

M, N, P ::= K|S|MN

where K and S are constants and MN denotes the application of M to N. (This language is called combinatory logic.) We may restrict to well-typed terms, where the typing rules are: K has any type F ⊃ G ⊃ F, S has any type (F ⊃ G ⊃ H) ⊃ (F ⊃ G) ⊃ F ⊃ H, and if M has type F ⊃ G and N has type F, then MN has type G. This may be written using typing judgments M : F, which assign each term M a type F, using typing rules:

K : F ⊃ G ⊃ F  (3)
S : (F ⊃ G ⊃ H) ⊃ (F ⊃ G) ⊃ F ⊃ H  (4)
M : F ⊃ G N : F
(MP)
MN : G

Note the formal similarity with the proof rules (1), (2), and (MP). Any typing rule can be converted to a proof, by forgetting terms. Conversely, any proof can be converted to a typing derivation by labeling judgments with suitable terms. Furthermore, given a typable term M, there is a unique so-called principal typing from which all other typings can be recovered (Hindley’s Theorem). This constitutes half of the so-called Curry-Howard correspondence between programs (terms) and proofs. Subscripting K and S with the types they are meant to have at each occurrence in a term even makes this an isomorphism between typable terms and proofs.

Let us introduce the second half of the Curry-Howard correspondence: the proof simplification steps give rise to program reduction rules; here, the natural choice is KMN → M, SMNP → MP (NP). It turns out that these reduction rules give rise to a notion of computation, where a term (a program) is reduced until a normal term is reached. This reduction process is then exactly the proof simplification process described above.

3.3. Natural Deduction and the Lambda-Calculus

The language of Hilbert systems and combinatory logic is not easy to work with, although this can be done [28]. A more comfortable choice is given by Church’s λ-calculus [2], the programming language associated with minimal logic in natural deduction format [47]. Its terms are given by the grammar:

M, N, P ::= x|λx · M|MN

where x ranges over variables, λx · M is λ-abstraction (“the function that maps x to M”, where M typically depends on x). For convenience, we write MN_{1}N_{2} … N_{k} instead of (… ((MN)N_{1})N_{2} …)N_{k} (application associates to the left), and λx_{1}, x_{2}, …, x_{k} · M instead of λx_{1} · λx_{2} · . . . λx_{k} · M.

Typing, i.e., proofs, are described using sequents instead of mere formulae. A sequent is an expression of the form x_{1} : F_{1}, …, x_{n} : F_{n} ⊢ M : F, meaning that M has type F under the assumptions that x_{1} has type F_{1}, …, x_{n} has type F_{n}. This is needed to type λ-abstractions. In this paper, the context x_{1} : F_{1}, …, x_{n} : F_{n} will be a list of bindings x_{i} : F_{i}, where the x_{i}’s are distinct. We shall usually write Γ, Θ for contexts. The notation Γ, x : F then denotes x_{1} : F_{1}, …, x_{n} : F_{n}, x : F, provided x is not one of x_{1}, …, x_{n}. The typing rules are:

\begin{aligned}& (Ax) (1 ⩽ i ⩽ n) \\ x_{1} : F_{1}, …, x_{n} : F_{n} ⊢ x_{i} : F_{i} \end{aligned} ; Γ, x : F ⊢ M : G ; (⊃ I) ; Γ ⊢ λx · M : F ⊃ G Γ ⊢ M : F ⊃ G Γ ⊢ N : F ; (⊃ E) ; Γ ⊢ MN : G

Finally, computation, i.e., proof simplification, is described by the β-reduction rule (λx · M)N → M[x := N], where M[x := N] denotes the (capture-avoiding) substitution of N for x in M. We may also add the η-reduction rule λx · Mx → M, provided x is not free in M. Although this is not necessary for proof normalization, η-reduction allows one to get an extensional notion of function, where two functions are equal provided they return equal results on equal arguments. (This also corresponds to reducing proofs of axiom sequents to proofs consisting of just the (Ax) rule, proof-theoretically.)

3.4. Minimal Intuitionistic S4

The topic of this paper is the intuitionistic modal logic S4. For simplicity, we consider minimal intuitionistic S4, which captures the core of the logic: formulae, a.k.a. types, are defined by: F ::= A | F ⊃ F | □F where A ranges over a fixed set Σ of base types. (While adding conjunctions ∧, and truth ⊤ do not pose any new problems, it should be noted that adding disjunctions ∨, falsehood ⊥ or ♦ would not be as innocuous for some of the theorems of this paper.)

The usual semantics of (classical) S4 is its Kripke semantics. For any Kripke frame (W, ⊵) (a preorder), and a valuation ρ mapping base types A ∈ Σ to sets of worlds (those intended to make A true), define when a formula F holds at a world w ∈ W in ρ, abbreviated w, ρ ⊧ F: w, ρ ⊧ A if and only if w ∈ ρ(A); w, ρ ⊧ F ⊃ G if and only if, if w, ρ ⊧ F then w, ρ ⊧ G; and w, ρ ⊧ □F if and only for every w′ ⊵ w, w′, ρ ⊧ F. Think of □F as meaning “from now on, in every future F holds”.

The idea that the truth value of a formula F may depend on time is natural, e.g. in physics, where “the electron has gone through the left slit” may hold at time t but not at t′.

In intuitionistic S4 we may refine the semantics of formulae to include another preordering ⩾ on worlds, accounting for intuitionistic forcing. Intuitively, ⩾ may be some ordering on states of mind of a mathematician, typically the ⊇ ordering on sets of basic facts that the mathematician knows (the analogy is due to Brouwer). Then if the mathematician knows F ⊃ G when he is in some state of mind w (abbreviated w ⊧ F ⊃ G), and if he knows F, he should also know G. Further, knowing F ⊃ G in state of mind w also means that, once the mathematician has extended his state of mind to a larger w′, if this w′ allows him to deduce F, then he should be able to deduce G in the w′ state of mind. The intuitionistic meaning of F ⊃ G is therefore that w ⊧ F ⊃ G if and only if, for every w′ ⩾ w, if w′ ⊧ F then w′ ⊧ G. Knowing the negation of F in state of mind w not only means knowing that F does not hold in w, but also that it cannot hold in any state of mind w′ ⩾ w, i.e., any w′ extending w. One distinguishing feature of intuitionistic logic is that it may be the case that there are formulae F such that neither F nor its negation hold in some state of mind w—think of F as an unsolved conjecture—, so the classical tautology F ∨ ¬F does not hold in general.

The Kripke semantics of intuitionistic S4 is as follows.

Definition 1 (Kripke Semantics). An intuitionistic Kripke frame is a triple (W, ⊵, ⩾), where ⊵ and ⩾ are preorderings on W such that ⩾ ⊆ ⊵.

A valuation ρ on W is a map from base types in Σ to upper sets of worlds in W; an upper set is any subset of W such that whenever w ∈ W and w′ ⩾ w, w′ ∈ W.

The semantics of S4 formulas is given by:

w, ρ ⊧ A iff w ∈ ρ(A)
w, ρ ⊧ F ⊃ G iff for every w′ ⩾ w, if w′, ρ ⊧ F then w′, ρ ⊧ G
w, ρ ⊧ □F iff for every w′ ⊵ w, w′, ρ ⊧ F

An S4 formula F is valid, written ⊧ F, if and only if w, ρ ⊧ F in every frame (W, ⊵, ⩾), for every w ∈ W, for every valuation ρ.

The resulting logic is called IntS4 in [51], and the condition relating ⩾ and ⊵ there is (⩾ ∘ ⊵ ∘ ⩾) =⊵. In the S4 case where ⊵ is a preorder, this is equivalent to our ⩾ ⊆ ⊵.

For all our analogy with states of mind of a mathematician is worth, the condition ⩾ ⊆ ⊵ intuitively states that you can only learn new basic facts (increase w.r.t. ⩾) while time passes (⊵), but time may pass without you learning any new facts.

We have mentioned the ♦ modality in Section 2. This would have the expected semantics: w, ρ ⊧ ♦F if and only if for some w′ with w ⊵ w′, w′, ρ ⊧ F. The other two modalities ■ (“in all pasts”) and ♢ (“in some future”) are naturally defined in intuitionistic modal logic by introducing a new binary relation ⊴ on W, which needs not be the converse of ⊵, letting w, ρ ⊧ ■F if and only if for every w′ ⊴ w, w′, ρ ⊧ F, and w, ρ ⊧ ♢F if and only if for every w′ with w ⊴ w′, w′, ρ ⊧ F [51]. The only constraints on ⩾, ⊵ and ⊴ are that, in addition to ⩾ ⊆ ⊵, we should have ⩾ ⊆ ⊴, ⊴ ⊆ (⊴ ∩ ⊵^{o})∘ ⩾, and ⊵ ⊆ (⊵ ∩ ⊴^{o})∘ ⩾, where R^{o} denotes the converse of relation R.

3.5. Natural Deduction for Intuitionistic S4

In this paper, we shall not be so much interested in validity of S4 formulas as in actual proofs of S4 formulas. So let us talk about proofs.

We use λ_{S4} as a language of proof terms for S4 [7]. The raw terms are:

M, N, P ::= x | MN | λx · M | dM | M · θ

where θ is an explicit substitution, that is, a substitution that appears as an explicit component of terms. A substitution θ is any finite mapping from variables x_{i} to terms M_{i}, 1 ⩽ i ⩽ n, and is written {x_{1} := M_{1}, …, x_{n} := M_{n}}; its domain dom θ is the set {x_{1}, …, x_{n}}. (We omit the type subscript of variables whenever convenient.) The yield yld θ is defined as ⋃_{x∈dom θ} fv(θ(x)), mutually recursively with the set of free variables fv(M) of the term M: fv(x) ˆ={x}, fv(MN) ˆ= fv(M) ∪ fv(N), fv(λx · M) ˆ= fv(M) \ {x}, fv(dM) ˆ= fv(M), fv( M · θ) ˆ= yld θ. (We use ˆ= for equality by definition.) Moreover, we assume that, in any term M · θ, fv(M) ⊆ dom θ; we also assume Barendregt’s naming convention: no variable occurs both free and bound, or bound at two different places—bound variables are x in λx · M and all variables

in dom θ in M · θ.

Our notations differ from [7]. There M · {x_{1} := N_{1}, …, x_{n} := N_{n}} is written box M with N_{1}, …, N_{n} for x_{1}, …, x_{n}. The new notation allows one, first, to materialize the explicit substitution more naturally, and second the frame notation will be put to good use to explain what simplices look like. Also, dM is written unbox M in [7]; we use dM because it is more concise and hints that some face operator is at work.

Substitution application Mθ is defined by: xθ ˆ=θ(x) if x ∈ dom θ, xθ ˆ=x otherwise; (MN)θ ˆ=(Mθ)(Nθ); (λx·M)θ ˆ=λx·(Mθ) provided x ∉ dom θ∪yld θ; (dM)θ ˆ=d(Mθ); ( M · θ′)θ ˆ= M · (θ′ · θ), where substitution concatenation θ′ · θ is defined as {x_{1} := M_{1}, …, x_{n} := M_{n}} · θ ˆ={x_{1} := M_{1}θ, …, x_{n} := M_{n}θ}.

Terms are equated modulo α-conversion, the smallest congruence ≡ such that:

λx · M ≡ λy · (M{x := y})

M · {x_{1} := N_{1}, …, x_{n} := N_{n}} ≡

M{x_{1} := y_{1}, …, x_{n} := y_{n}} · {y_{1} := N_{1}, …, y_{n} := N_{n}}

provided y is not free in M in the first case, and y_{1}, …, y_{n} are not free in M and are pairwise distinct in the second case, with identical type subscripts as x_{1}, …, x_{n} respectively.

The d operator is a kind of “eval”, or also of “comma” operator in the language Lisp [35]. The M, θ ↦ M · θ operator is more complex. Let’s first look at a special case: for any term M such that fv(M) = {x_{1}, …, x_{n}}, let M be

M · {x_{1} := x_{1}, …, x_{n} := x_{n}}—or, more formally, M{x_{1} := x′_{1}, …, x_{n} := x′_{n}} ·

{x′_{1} := x_{1}, …, x′_{n} := x_{n}}. Then M behaves like “quote” M in Lisp, or more exactly, “backquote” M; and provided dom θ = fv(M), M ·θ is exactly ( M ) θ: this is a syntactic closure in the sense of [5], namely a quoted term M together with an environment θ mapping free variables of M to their values.

\begin{aligned}& (Ax) \\ Γ, x : F, Θ ⊢ x : F \end{aligned}

Γ ⊢ M : F ⊃ G Γ ⊢ N : F ; (⊃ E) ; Γ ⊢ MN : G Γ, x : F ⊢ M : G ; (⊃ I) ; Γ ⊢ λx · M : F ⊃ G

Γ ⊢ M : □F ; (□E) ; Γ ⊢ dM : F \overbrace{Γ ⊢ N_{i} : □F_{i}}^{1⩽i⩽n} x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢ M : G ; (□I) ; Γ ⊢ M · \{x_{1} := N_{1}, …, x_{n} := N_{n}\} : □G

Figure 1: Typing λ_{S4} terms

The typing rules [7], defining a natural deduction system for minimal S4, are as in Figure 1, where Γ, Θ, …, are typing contexts, i.e. lists of bindings x : F, where x is a variable, F is a type, and no two bindings contain the same variable in any given context. The exchange rule:

{Γ, x : F, y : G, Θ ⊢ M : H \atop Γ, y : G, x : F, Θ ⊢ M : H}

is easily seen to be admissible, so we can consider typing contexts as multisets instead of lists. In particular, there is no choice to be made as to the order of the variables x_{1}, …, x_{n} in the right premise of rule (□I).

(β) (λx · M)N → M{x := N}  (d) d( M · θ) → Mθ
(gc) M · (θ, {x := N}) → M · θ  provided x ∉ fv(M)
(ctr) M · (θ, {x := N, y := N}) → M{y := x} · (θ, {x := N})
( □ ) M · (θ, {x := N · θ′}) → M{x := N } · (θ, θ′)
(η) λx · Mx → M provided x ∉ fv(M)  (η□) dx · {x := N} → N

Figure 2: The reduction relation of λ_{S4}

Define the reduction relation → on λ_{S4}-terms as the smallest relation compatible with term structure (i.e., if M → N then C[M] → C[N], where C[P] denotes any term with a distinguished occurrence of P) defined in Figure 2 [7, 20]. Terms that match the left-hand side of rules are called redexes (for reduction expression). The convertibility relation ≈ is the smallest congruence extending →; in other words, ≈ is the reflexive symmetric transitive closure of →. In addition, we write →^{+} the transitive closure of →, and →^{∗} its reflexive transitive closure.

Rule (d) is like Lisp’s rule for evaluating quoted expressions: evaluating M , by d M , reduces to M. Rule ( □ ) can be seen either as an inlining rule, allowing one to inline the definition of x as N inside the body M of the box M , or logically as a box-under-box commutation rule. (gc) is a garbage collection rule, while (ctr) is a contraction rule. We use a new notation in these rules: if θ and θ′ are two substitutions with disjoint domains, then θ, θ′ denotes the obvious union.

The last two rules are so-called extensional equalities. Together with (gc), (η□) allows us to deduce dx · θ ≈ xθ, but not dM · θ ≈ Mθ for any term M: M has to be a variable. For a discussion of this, see [21].

3.6. Standard Properties: Subject Reduction, Confluence, Strong Nor-

malization We now prove standard properties of proof simplification calculi. The following lemma is by a series of easy but tedious computations; it says that

reduction preserves typings, alternatively that it rewrites proofs to proofs of the same sequents.

Lemma 2 (Subject Reduction). If the typing judgment Γ ⊢ M : F is derivable and M → N then Γ ⊢ N : F is derivable.

Proposition 3 (Strong Normalization). If M is typable, then it is strongly normalizing, i.e., every reduction sequence starting from M is finite.

Proof. By the reducibility method [18]. Let SN be the set of strongly normalizing terms, and define an interpretation of types as sets of terms as follows:

• for every base type A, ||A|| ˆ=SN;

• ||F ⊃ G|| ˆ={M ∈ SN|whenever M →^{∗} λx · M_{1} then for every N ∈ ||F ||, M_{1}{x := N} ∈ ||G||};

• ||□F || ˆ={M ∈ SN|whenever M →^{∗} M_{1} · θ then M_{1}θ ∈ ||F ||}

Observe that: (CR1) ||F || ⊆ SN for every type F; (CR2) For every M ∈ ||F ||, if M → M′ then M′ ∈ ||F ||. This is by structural

induction on F. This is clear when F is a base type. For implications, assume M ∈ ||F ⊃ G|| and M → M′; then M′ ∈ SN, and if M′ →^{∗} λx · M_{1}, then M →^{∗} λx · M_{1}, so by definition of ||F ⊃ G||, M_{1}{x := N} ∈ ||G|| for every N ∈ ||F ||; therefore M′ ∈ ||F ⊃ G||. The case of box types is proved similarly.

(CR3) For every neutral term M, if M′ ∈ ||F || for every M′ with M → M′, then M ∈ ||F ||. (Call a term neutral if and only if it is not of the form λx · M or M · θ.) This is again by structural induction on F. This is clear when F is a base type. For implications, assume that every M′ such that M → M′ is in ||F ⊃ G||, and show that M ∈ ||F ⊃ G||. Clearly M ∈ SN, since every reduction starting from M must be empty or go through some M′ ∈ ||F ⊃ G|| ⊆ SN by (CR1). So assume that M →^{∗} λx · M_{1}. Since M is neutral, the given reduction is non-empty, so there is an M′ such that M → M′ →^{∗} λx · M_{1}. By assumption M′ ∈ ||F ⊃ G||, so for every N ∈ ||F ||, M_{1}{x := N} ∈ ||G||. It follows that M ∈ ||F ⊃ G||. The case of box types is similar.

Next we show that:

1. If M ∈ ||F ⊃ G|| and N ∈ ||F ||, then MN ∈ ||G||. By (CR1), M and N are in SN, so we prove this by induction on the pair (M, N) ordered by →, lexicographically. Note that MN is neutral, and may only rewrite in one step to M′N where M → M′, or to MN′ where N → N′, or to M_{1}{x := N} by (β) (if M = λx · M_{1}). In the first two cases, M′ ∈ ||F ⊃ G||, resp. N′ ∈ ||F || by (CR2), so we may apply the induction hypothesis. In the third case, this is by definition of ||F ⊃ G||. In each case we get a term in ||G||, so by (CR3) MN ∈ ||G||.

2. If M{x := N} ∈ ||G|| for every N ∈ ||F ||, then λx · M ∈ ||F ⊃ G||. To show this, we show the converse of 1: if for every N ∈ ||F ||, MN ∈ ||G||, then M ∈ ||F ⊃ G||. Indeed, first M ∈ SN: take any variable x; x is in ||F || by (CR3), so Mx ∈ ||G|| by assumption, so Mx ∈ SN by (CR1), hence M ∈ SN. Second, assume that M →^{∗} λx · M_{1}, then for every N ∈ ||F ||, MN →^{∗} M_{1}{x := N} ∈ ||G|| by (CR2). So M ∈ ||F ⊃ G||. Using this, assume that M{x := N} ∈ ||G|| for every N ∈ ||F ||, and show that λx · M ∈ ||F ⊃ G||. It is enough to show that (λx · M)N ∈ ||G|| for every N ∈ ||F ||. We do this by induction on (M, N) ordered by →, which is well-founded: indeed, N ∈ ||F || ⊆ SN by (CR1), and M = M{x := x} ∈ ||G|| ⊆ SN by (CR1), since x ∈ ||F || by (CR3). Since (λx · M)N is neutral, apply (CR3): (λx · M)N may rewrite to (λx · M′)N with M → M′ (this is in ||G|| by (CR2) and the induction hypothesis), or to (λx · M)N′ with N → N′ (similar), or to M{x := N} by (β) (in ||G|| by assumption), or to M′N by (η) where M = M′x, x not free in M′ (then M′N = M{x := N}, which is in ||G|| by assumption).

3. If M ∈ ||□F ||, then dM ∈ ||F ||. This is by induction on M ordered by →, which is well-founded since by (CR1) M ∈ SN. Now dM may rewrite either to dM′ with M → M′ (then apply the induction hypothesis, noting that

M′ ∈ ||□F || by (CR2), so dM′ ∈ ||F ||), or to M_{1}θ, provided M = M_{1} · θ

(then M_{1}θ ∈ ||F || by definition). Since dM is neutral, by (CR3) dM ∈ ||F ||.

4. If Mθ ∈ ||F || and θ maps each variable x ∈ dom θ to some strongly normalizing term, then M · θ ∈ ||□F ||. First we show the converse of 3: if dM ∈ ||F || then M ∈ ||□F ||. First since dM ∈ ||F || ⊆ SN by (CR1), M ∈ SN. It remains to show that whenever M →^{∗} M_{1} · θ then M_{1}θ ∈ ||F ||. However then dM →^{∗} M_{1}θ must be in ||F || by (CR2). Knowing this, let Mθ be in ||F || and θ map each variable x ∈ dom θ to some strongly normalizing term. Let us show that M · θ ∈ ||□F ||. By the converse of 3 shown above, it is enough to show that d M · θ ∈ ||F ||. We shall prove this using (CR3), since d M · θ is neutral. Letting θ be {x_{1} := N_{1}, …, x_{n} := N_{n}}, we show this by induction on, first, N_{1}, …, N_{n} ordered by the multiset extension [12] of → ∪▷, where ▷ is the immediate superterm relation (it is well-known that as soon as N_{i} is in the well-founded part of →, it is also in the well-founded part of → ∪▷; the multiset extension allows one to replace any element N_{i} of the multiset by any finite number of smaller elements, and is well-founded on all multisets of elements taken from the well-founded part of the underlying ordering); and second on Mθ, lexicographically. Now d M ·θ may rewrite in one step to:

• Mθ by (d); this is in ||F || by assumption.

• dN_{1} by (η□), where M = dx_{1} and n = 1. Then dN_{1} = Mθ is in ||F || by assumption.

• d M′ · θ where M → M′. By (CR2) M′θ ∈ ||F ||, so we may apply the induction hypothesis.

• d M ·θ′ where θ′ = {x_{1} := N_{1}, …, x_{i} := N′_{i}, …, x_{n} := N_{n}} and N_{i} → N′_{i}.

Since N′_{i} ∈ SN, we may apply the induction hypothesis.

• d M · θ′ where θ = θ′, {x := N} and x is not free in M by (gc). This is by the induction hypothesis. The same argument applies for (ctr).

• d M{x := N } ·(θ_{1}, θ′) where θ = θ_{1}, {x := N ·θ′} by ( □ ). We wish to

apply the induction hypothesis. For this, we have to check that M{x :=

N }(θ_{1}, θ′) is in ||F ||. But Mθ is in ||F || and equals M(θ_{1}, {x := N ·θ′}.

The latter is equal or rewrites by (gc) to M(θ_{1}, {x := ( N )θ′}) = M{x := N }(θ_{1}, θ′), so the latter is in ||F || by (CR2).

We now check that, given any typing derivation π of x_{1} : F_{1}, …, x_{n} : F_{n} ⊢ M : F, for every N_{1} ∈ ||F_{1}||, …, N_{n} ∈ ||F_{n}||, M{x_{1} := N_{1}, …, x_{n} := N_{n}} ∈ ||F ||. This is by structural induction on π. The (Ax) cas is obvious, while the other cases are dealt with by using items 1–4 above. Since x_{i} ∈ ||F_{i}|| by (CR3), it follows that M ∈ ||F ||. By (CR1), M ∈ SN.

Proposition 4 (Confluence). If M is typable, and if M →^{∗} N_{1} and M →^{∗} N_{2}, then there is P such that N_{1} →^{∗} P and N_{2} →^{∗} P.

Proof. A long and uninteresting series of computations shows that all critical pairs are joinable, hence λ_{S4} is locally confluent [13]. This holds also on typable terms because of Lemma 2. By Newman’s Lemma (every locally confluent and strongly normalizing rewrite system is confluent) and Proposition 3, λ_{S4} is confluent on typed λ_{S4}-terms.

Corollary 5. Every typable λ_{S4}-term has a unique normal form.

3.7. The Shape of Normal Forms, η-Long Normal Forms

One way of describing normal forms for typed terms is by the typing system BN of Figure 3.

Lemma 6. Call a term beta-normal if and only if it contains no (β), (d), (gc), ( □ ) redex (i.e., no redex except possibly (ctr), (η) or (η□) redexes).

\begin{aligned}& (Ax_{E}) \\ Γ, x : F, Θ ⊢_{E} x : F \end{aligned}  Γ ⊢_{E} M : F ⊃ G Γ ⊢_{I} N : F ; (⊃ E_{E}) ; Γ ⊢_{E} MN : G

Γ ⊢_{E} M : F ; (F lip) ; Γ ⊢_{I} M : F  Γ ⊢_{E} M : □F ; (□E_{E}) ; Γ ⊢_{E} dM : F

Γ, x : F ⊢_{I} M : G ; (⊃ I_{I}) ; Γ ⊢_{I} λx · M : F ⊃ G \begin{aligned}\overbrace{Γ ⊢_{E} N_{i} : □F_{i}}^{1⩽i⩽n} & \begin{matrix}x_{1} : □F_{1}, …, x_{n} : □F_{n} \\ ⊢_{I} M : G \end{matrix} \\ & (□I_{I}) \\ Γ ⊢_{I} M · \{x_{1} := N_{1}, …, x_{n} := N_{n}\} : □G \end{aligned}
(fv(M) = {x_{1}, …, x_{n}})

Figure 3: Typing beta-normal forms: System BN

If Γ ⊢ M : F and M is beta-normal, then Γ ⊢_{I} M : F. Moreover, if M is neutral, i.e., not starting with a λ or a box, then Γ ⊢_{E} M.

Conversely, if Γ ⊢_{I} M : F or Γ ⊢_{E} M : F, then Γ ⊢ M : F and M is beta-normal.

Proof. By structural induction on the given derivation of Γ ⊢ M : F. The cases M a variable, and M of the form λx · M_{1} are trivial. If M = M_{1}M_{2}, with Γ ⊢ M_{1} : G ⊃ H and Γ ⊢ M_{2} : G, then M_{1} must be neutral, otherwise by typing M_{1} would start with a λ, and then M would be a (β)-redex. So by induction hypothesis Γ ⊢_{E} M_{1} : G ⊃ H. Since by induction hypothesis Γ ⊢_{I} M_{2} : G, it follows by rule (⊃ E_{E}) that Γ ⊢_{E} M : H. The case where M = dM_{1} is similar. Finally, when M is

of the form M_{1} · θ, with θ = {x_{1} : N_{1}, …, x_{n} : N_{n}}, Γ ⊢ N_{i} : □F_{i} (1 ⩽ i ⩽ n), and

x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢ M_{1} : F, then by induction hypothesis x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢_{I} M_{1} : F. Moreover, since M is not a (gc) redex, fv(M) = {x_{1}, …, x_{n}}. Also, every N_{i} must be neutral, otherwise by typing they would start with a box, which is forbidden because M is not a ( □ ) redex, so by induction hypothesis Γ ⊢_{E} N_{i} : □F_{i}. It follows that rule (□I_{I}) applies, therefore Γ ⊢_{I} M : □F.

Conversely: if Γ ⊢_{I} M : F or Γ ⊢_{E} M : F, then it is obvious that Γ ⊢ M : F: erase all E and I subscripts, and remove all instances of (F lip). It remains to show that M is beta-normal. Consider any subterm of M. If it is of the form M_{1}M_{2}, then its type must have been derived using the (⊃ E_{E}) rule, which implies that M_{1} is typed as in Γ ⊢_{E} M_{1} : F ⊃ G; but no rule in BN (Figure 3) would allow one to derive such a judgment if M_{1} began with λ; so M_{1}M_{2} is not a (β)-redex. Similarly, no subterm of M can be a (d) redex. The side-conditions on rule (□I_{I}) entail that no subterm of M is a (gc) redex, while the fact that N_{i} : □F_{i} must have been derived using a ⊢_{E} judgment entails that no N_{i} starts with a box, hence that no subterm of M is a ( □ ) redex. So M is beta-normal.

A more convenient form than normal forms is the η-long normal form, imitating that of [30] in the non-modal case. In the S4 case, η-long normal forms are slightly more complex, but can be described as follows, including an additional linearity constraint on boxes.

Definition 7 (η-long normal form). Call a term M linear if and only if every free variable of M occurs exactly once in M. Formally, define the notion of being linear in W, where W is a finite set of variables, as follows. Every variable is linear in W, λx · M is linear in W provided M is linear in W \ {x}, MN is linear in W provided M and N are and fv(M) ∩ fv(N) ∩ W = ∅, ∂M is linear in W provided M is, M · {x_{1} := N_{1}, …, x_{n} := N_{n}} is linear in W provided each N_{i}, 1 ⩽ i ⩽ n, is linear in W, and fv(N_{i}) ∩ fv(N_{j}) ∩ W = ∅ for every 1 ⩽ i ≠ j ⩽ n. A term M is linear provided it is linear in fv(M).

Call (F lip_{0}) the rule (F lip) restricted to the case where F is in the set Σ of base types, and (□I_{0}) the rule (□I_{I}) restricted to the case where M is linear. Call BN_{0} the typing system BN where all instances of (F lip) are instances of (F lip_{0}), and all instances of (□I_{I}) are instances of (□I_{0}).

A term M is said to be η-long normal of type F in Γ if and only if we can derive Γ ⊢_{I} M : F in system BN_{0}.

Lemma 8 (Weakening). For every BN derivation of Γ ⊢_{∗} M : F (∗ ∈ {I, E}), for every context Θ, there is a BN derivation of Γ, Θ ⊢_{∗} M : F.

Proof. By structural induction on the given derivation. This is mostly obvious, provided we assume all bound variables have been renamed so as to be distinct from the ones in Θ.

Lemma 9. For every M such that Γ ⊢ M : F, M has an η-long normal form η[M]. That is, there is a term η[M] such that M ≈ η[M] and Γ ⊢ η[M] : F.

Proof. First by Proposition 3 and Lemma 6, we may assume that Γ ⊢_{I} M : F. The idea is then, first, to rewrite every instance of (F lip) on non-base types F using only instances of (F lip) on smaller types F, until all we get is instances of (F lip_{0}). This is done using the following two rules:

Γ ⊢_{E} M : F ⊃ G ; (F lip) ; Γ ⊢_{I} M : F ⊃ G ⟶ Γ, x : F ⊢_{E} M : F ⊃ G \begin{aligned}& (Ax_{E}) \\ Γ, x : F ⊢_{E} x : F \end{aligned} ; (F lip) ; Γ, x : F ⊢_{I} x : F ; (⊃ E_{E}) ; Γ, x : F ⊢_{E} Mx : G ; (F lip) ; Γ, x : F ⊢_{I} Mx : G ; (⊃ I_{I}) ; Γ ⊢_{I} λx · Mx : F ⊃ G(5)

Γ ⊢_{E} M : □F ; (F lip) ; Γ ⊢_{I} M : □F ⟶ Γ ⊢_{E} M : □F \begin{aligned}& (Ax_{E}) \\ x : □F ⊢_{E} x : □F \end{aligned} ; (□E_{E}) ; x : □F ⊢_{E} dx : F ; (F lip) ; x : □F ⊢_{I} dx : F ; (□I_{I}) ; Γ ⊢_{I} dx · \{x := M\} : □F  (6)

where in the right-hand side of the first rule, the derivation of Γ, x : F ⊢_{E} M : F ⊃ G is obtained from the one of Γ ⊢_{E} M : F ⊃ G by weakening (Lemma 8).

This terminates, because the sum of the sizes of formulae on the right-hand sides of judgments in (F lip) decreases (define the size |F | of a formula F by |A| ˆ=1, |F ⊃ G| ˆ=|F | + |G| + 1, |□F | ˆ=|F | + 1).

On the other hand, we make every instance of (□I_{I}) one of (□I_{0}) by linearizing the term M. That is, for each free variable x_{i} in M, 1 ⩽ i ⩽ n, with k_{i} ⩾ 1 distinct occurrences in M, create k_{i} fresh variables x_{i1}, …, x_{ik_{i}}, let M′ be M where the jth occurrence of x_{i} is replaced by x_{ij}, for every 1 ⩽ i ⩽ n, 1 ⩽ j ⩽ k_{i}, and rewrite the derivation:

\overbrace{Γ ⊢_{E} N_{i} : □F_{i}}^{1⩽i⩽n} x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢ M : F ; (□I_{I}) ; Γ ⊢ M · \{x_{1} := N_{1}, …, x_{n} : N_{n}\} : □F  (7)

into:

\overbrace{Γ ⊢_{E} N_{i} : □F_{i}}^{1⩽i⩽n,1⩽j⩽k_{i}} (x_{ij} : □F_{i})_{1⩽i⩽n,1⩽j⩽k_{i}} ⊢ M′ : F ; (□I_{0}) ; Γ ⊢ M′ · \{(x_{ij} := N_{i})_{1⩽i⩽n,1⩽j⩽k_{i}}\} : □F  (8)

Lemma 10. Let Γ ⊢ M : F. Then M has at most one η-long normal form of type F in Γ.

Proof. Let M′ be an η-long normal form of M. M′ is beta-normal by construction. Let R_{η} be the rewrite system consisting of rules (η) and (η□). It is clear that R_{η} terminates and rewrites beta-normal terms to beta-normal terms. Similarly the rewrite system R_{ctr} consisting of the sole rule (ctr) terminates and rewrites R_{η}- normal beta-normal terms to R_{η}-normal beta-normal terms. Let M′′ be any R_{η}- normal form of M′, and M′′′ be any R_{ctr}-normal form of M′′. Then M′′′ is R_{ctr}- normal, R_{η}-normal and beta-normal, hence normal.

Since M′ is an η-long normal form of M, M ≈ M′, so M ≈ M′′′. By Proposition 4 and since M′′′ is normal, M →^{∗} M′′′. Summing up, M →^{∗} M′′′_{R_{ctr}}^{∗} ← M′′_{R_{η}}^{∗} ← M′, where →_{R} denotes rewriting by R.

Observe now that the rewrite system R_{ctr}^{−1} on derivations defined by the transformation M_{1}{y := x} · (θ, {x := N}) → M_{1} · (θ, {x := N, y := N}) (where both x and y are free in M_{1}) is locally confluent. Moreover, whenever M_{1} is well-typed and beta-normal, and rewrites to M_{2} by R_{ctr}, then M_{2} rewrites to M_{1} by R_{ctr}^{−1}. Finally, R_{ctr}^{−1} terminates: for any term M_{1}, let μ(M_{1}) be ∑_{x∈fv(M_{1})}(n(x, M_{1}) − 1) where n(x, M_{1}) is the number of occurrences of x in M_{1}; by induction on μ(M_{1}) followed lexicographically by the multiset of the terms xθ, x ∈ dom θ ordered by →_{R_{ctr}^{−1}}, M_{1} · θ is R_{ctr}^{−1}-terminating as soon as each xθ is, x ∈ dom θ; it follows by structural induction on terms that every term is R_{ctr}^{−1}-terminating.

Similarly, the rewrite system R_{η}^{−1} on derivations defined by (5) and (6) is terminating (as already noticed in Lemma 9), locally confluent, and whenever M_{1} is well-typed and beta-normal, and rewrites to M_{2} by R_{η}, then M_{2} rewrites to M_{1} by R_{η}^{−1} So if M′ is any η-long normal form of M, then M →^{∗} M′′′ →_{R_{ctr}^{−1}}^{∗} M′′ →_{R_{η}^{−1}}^{∗} M′. In general, if M′_{1} and M′_{2} are two η-long normal forms of M, we get M →^{∗}

M′′′ →_{R_{ctr}^{−1}}^{∗} M′′_{1} →_{R_{η}^{−1}}^{∗} M′_{1} and M →^{∗} M′′′ →_{R_{ctr}^{−1}}^{∗} M′′_{2} →_{R_{η}^{−1}}^{∗} M′_{2}. Since R_{ctr}^{−1} is

confluent and M′′_{1} and M′′_{2} are R_{ctr}^{−1}-normal, M′′_{1} = M′′_{2}. Since R_{η}^{−1} is confluent and M′_{1} and M′_{2} are η-long normal, hence R_{η}^{−1}-normal, M′_{1} = M′_{2}.

Lemmas 9 and 10 entail:

Proposition 11 (η-long normalization). For every term M such that Γ ⊢ M : F is derivable, M has a unique η-long normal form of type F in Γ, which we write η[M]. In particular, whenever Γ ⊢ M : F and Γ ⊢ M′ : F, M ≈ M′ if and only if η[M] = η[M′].

The value of η-long normal forms is that substituting terms N_{i} of a certain form for variables in any η-long normal form yields an η-long normal form again:

Lemma 12. If x_{1} : F_{1}, …, x_{n} : F_{n}, Θ ⊢_{∗} M : F (∗ ∈ {I, E}) and Γ ⊢_{E} N_{i} : F_{i} in system BN_{0} for every i, 1 ⩽ i ⩽ n, then Γ, Θ ⊢_{∗} M{x_{1} := N_{1}, …, x_{n} := N_{n}} : F in system BN_{0}.

Proof. By structural induction on the given derivation of x_{1} : F_{1}, …, x_{n} : F_{n}, Θ ⊢_{∗} M : F in BN_{0}. If this was derived by (Ax_{E}), then ∗ = E; if M = x_{i} for some i, then F = F_{i}, M{x_{1} := N_{1}, …, x_{n} := N_{n}} = N_{i} and we may indeed deduce Γ, Θ ⊢_{E} N_{i} : F, by weakening from Γ ⊢_{E} N_{i} : F (Lemma 8); otherwise let M be variable x, then M{x_{1} := N_{1}, …, x_{n} := N_{n}} = x, and we get Γ, Θ ⊢_{E} x : F by (Ax_{E}). If the last rule is (⊃ E_{E}), (□E_{E}) or (F lip_{0}), this is by the induction hypothesis, straightforwardly. If the last rule is (⊃ I_{I}), then ∗ = I, M is of the form λx · M_{1}, F is of the form G ⊃ H, and by induction hypothesis we have been able to derive Γ, Θ, x : G ⊢_{I} M_{1}{x_{1} := N_{1}, …, x_{n} := N_{n}} : H, from which we get Γ, Θ ⊢_{I} M{x_{1} := N_{1}, …, x_{n} := N_{n}} : G ⊃ H by (⊃ I_{I}). Finally, if the last rule is (□I_{0}), then ∗ = I, F is of the form □G, M is of the form M_{1} · {y_{1} := P_{1}, …, y_{k} := P_{k}}, fv(M_{1}) = {y_{1}, …, y_{k}}, M_{1} is linear, and the typing derivation ends in:

\overbrace{x_{1} : F_{1}, …, x_{n} : F_{n}, Θ ⊢_{E} P_{j} : □G_{j}}^{1⩽j⩽k} y_{1} : □G_{1}, …, y_{k} : □G_{k} ⊢_{I} M_{1} : G

(□I_{0})

x_{1} : F_{1}, …, x_{n} : F_{n}, Θ ⊢_{I} M_{1} · {y_{1} := P_{1}, …, y_{k} := P_{k}} : □G

By induction hypothesis, we have got a derivation in BN_{0} of Γ, Θ ⊢_{E} P_{j}{x_{1} := N_{1}, …, x_{n} := N_{n}} : □G_{j}. Together with the derivation above of y_{1} : □G_{1}, …, y_{k} : □G_{k} ⊢_{I} M_{1} : G, and since fv(M_{1}) = {y_{1}, …, y_{k}}, M_{1} is linear, we may apply (□I_{0}) and derive

Γ, Θ ⊢_{I} M_{1} · { y_{1} := P_{1}{x_{1} := N_{1}, …, x_{n} := N_{n}},
…,
y_{n} := P_{n}{x_{1} := N_{1}, …, x_{n} := N_{n}}} : □G

But this is precisely Γ, Θ ⊢_{I} M{x_{1} := N_{1}, …, x_{n} := N_{n}} : □G.

Lemma 13. If M is η-long normal of type □F in Γ, then M is of the form M_{1} ·θ. Moreover, η[dM] = M_{1}θ.

Proof. The first part is obvious: Γ ⊢_{I} M : □F in system BN_{0}, but only rule (□I_{0}) can lead to this. Also, letting θ be {x_{1} := N_{1}, …, x_{n} := N_{n}}, we have x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢_{I} M_{1} : F in BN_{0}, and Γ ⊢_{E} N_{i} : □F_{i} in BN_{0} for each i, 1 ⩽ i ⩽ n. By Lemma 12, Γ ⊢_{I} M_{1}θ : F in BN_{0}. Since dM ≈ M_{1}θ, by Proposition 11 η[dM] = M_{1}θ.

The crucial thing in Lemma 13 is not so much that dM ≈ M_{1}θ, which is obvious. Rather, it is the fact that once we have reduced d( M_{1} · θ) to M_{1}θ by (d), we have already reached its η-long normal form.

Similarly, we obtain:

Lemma 14. Let sM ˆ= x · {x := M}. If M ˆ= M_{1} · θ is η-long normal of type □F

in Γ, then η[sM] = M_{1} · θ.

Proof. First sM = x · {x := M_{1} · θ} ≈ M_{1} · θ. Then since M is η-long normal,

letting θ be {x_{1} := N_{1}, …, x_{n} := N_{n}}, we have x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢_{I} M_{1} : F in BN_{0}, and Γ ⊢_{E} N_{i} : □F_{i} in BN_{0} for each i, 1 ⩽ i ⩽ n. So we can produce the following BN_{0} derivation:

\overbrace{\begin{matrix}· \\ · \\ · \end{matrix} ; Γ ⊢_{E} N_{i} : □F_{i}}^{1⩽i⩽n} \begin{aligned}\overbrace{(Ax_{E}) ; \begin{matrix}x_{1} : □F_{1}, …, x_{n} : □F_{n} \\ ⊢_{E} x_{i} : □F_{i} \end{matrix}}^{1⩽i⩽n} & \begin{matrix}· \\ · \\ · \end{matrix} ; \begin{matrix}x_{1} : □F_{1}, …, x_{n} : □F_{n} \\ ⊢_{I} M_{1} : F \end{matrix} \\ & (□I_{0}) \\ x_{1} : □F_{1}, …, x_{n} : □F_{n} ⊢_{I} M_{1} : □F \end{aligned}
(□I_{0})

Γ ⊢_{I} M_{1} · θ : □□F

so M_{1} · θ is η-long normal of type □□F in Γ. The claim then follows by Propo-

sition 11.

4. The Augmented Simplicial Structure of λ_{S4}

We define an augmented simplicial set consisting of typed λ_{S4}-terms. Recall that:

Definition 15 (A.s. set, a.s. map). An augmented simplicial set K is a family of sets K_{q}, q ⩾ −1, of q-simplices, a.k.a. simplices of dimension q, with face maps ∂_{q}^{i} : K_{q} → K_{q−1} and degeneracy maps s_{q}^{i} : K_{q} → K_{q+1}, 0 ⩽ i ⩽ q, such that:

\begin{matrix}(i) ∂_{q−1}^{i} ∘ ∂_{q}^{j} = ∂_{q−1}^{j−1} ∘ ∂_{q}^{i} & (ii) s_{q+1}^{i} ∘ s_{q}^{j−1} = s_{q+1}^{j} ∘ s_{q}^{i} & (iii) ∂_{q+1}^{i} ∘ s_{q}^{j} = s_{q−1}^{j−1} ∘ ∂_{q}^{i} \\ (iv) ∂_{q+1}^{i} ∘ s_{q}^{i} = id & (v) ∂_{q+1}^{i+1} ∘ s_{q}^{i} = id & (vi) s_{q−1}^{i} ∘ ∂_{q}^{j} = ∂_{q+1}^{j+1} ∘ s_{q}^{i} \end{matrix}

where 0 ⩽ i ⩽ q in (iv), (v), and 0 ⩽ i < j ⩽ q in the others.

An augmented simplicial map f : K → L is a family of maps f_{q} : K_{q} → L_{q}, q ⩾ −1, such that ∂_{q}^{i} ∘ f_{q} = f_{q−1} ∘ ∂_{q}^{i} and s_{q}^{i} ∘ f_{q} = f_{q+1} ∘ s_{q}^{i}, 0 ⩽ i ⩽ q.

Subscripts start at −1, which is standard and allows one to have q match the geometric dimension. We sometimes abbreviate “augmented simplicial” as “a.s.” in the sequel. Also, when we run a risk of confusion, we write ∂_{K_{q}}^{i} for ∂_{q}^{i}, and s_{K_{q}}^{i} for s_{q}^{i}.

The category Δ̂ of augmented simplicial sets as objects, and augmented simplicial maps as morphisms (see [36], VII.5), can also be presented as follows. Let Δ be the category whose objects are finite ordinals [q] ˆ={0, 1, …, q}, q ⩾ −1, and whose morphisms are monotonic (i.e., non-decreasing) maps. This category is generated

by morphisms [q − 1]⟶^{δ_{q}^{i}}[q] (mapping j < i to j and j ⩾ i to j + 1) and [q + 1]⟶^{σ_{q}^{i}}[q] (mapping j ⩽ i to j and j > i to j − 1), and relations that are most succinctly described as (i)–(vi) where ∂ is replaced by δ, s by σ, and composition order is reversed. Then Δ̂ is the category of functors from the opposite category Δ^{o} to the category Set of sets.

In general, Ĉ denotes the category of functors from C^{o} to Set, a.k.a. presheaves over C. Ĉ is always an elementary topos [33], hence is a cartesian-closed category (CCC ). The terminal object 1 of Δ̂ is such that 1_{q} is a singleton {∗} for every q ⩾ −1. The product K ×L is such that (K × L)_{q} ˆ=K_{q} ×L_{q}, ∂_{(K×L)_{q}}^{i}(u, v) ˆ=(∂_{K_{q}}^{i}u, ∂_{L_{q}}^{i}v)

and s_{(K×L)_{q}}^{i}(u, v) ˆ=(s_{K_{q}}^{i}u, s_{L_{q}}^{i}v): i.e., product is component-wise.

The structure of exponentials, i.e., internal homs HomΔ̂(K, L) is given by general constructions [33], which will be largely irrelevant here. For now, let us just say that we have got a.s. application maps App : HomΔ̂(K, L) × K → L, and an abstraction operator Λ on a.s. maps f : K × L → M, so that Λf is an a.s. map from K to HomΔ̂(L, M), satisfying certain equations to be specified below. Furthermore, (−1)-simplices of HomΔ̂(K, L) are just simplicial maps from K to L, while 0-simplices are homotopies between maps, and q-simplices for q ⩾ 0 are higher-dimensional homotopies.

In general, in any CCC C—not just Δ̂—, let ! denote the unique morphism

X⟶^{!}1. For cartesian products, we have a pair X ⟶^{⟨f,g⟩}Y × Z for every X⟶^{f}Y and X⟶^{g}Z, and projections X_{1} × X_{2}⟶^{π_{i}}X_{i}, i ∈ {1, 2}. We also have internal hom objects (exponentials) Hom_{C}(X, Y), application Hom_{C}(X, Y) × X⟶^{App}Y, and abstraction X⟶^{Λf}Hom_{C}(Y, Z) for every X × Y ⟶^{f}Z. These obey the following categorical combinator equations [10], where we omit types (objects) for the sake of conciseness:

(a) id ∘ f = f  (b) f ∘ id = f  (c) f ∘ (g ∘ h) = (f ∘ g) ∘ h
(!) ∀f : X → 1 · f =!  (e) π_{1} ∘ ⟨f, g⟩ = f (f) π_{2} ∘ ⟨f, g⟩ = f
(g) ⟨π_{1}, π_{2}⟩ = id  (h) ⟨f, g⟩ ∘ h = ⟨f ∘ h, g ∘ h⟩
(k) Λf ∘ h = Λ(f ∘ ⟨h ∘ π_{1}, π_{2}⟩) (l) App ∘ ⟨Λf, g⟩ (m) Λ(App ∘ ⟨f ∘ π_{1}, π_{2}⟩) = f
= f ∘ ⟨id, g⟩

For reasons of convenience, we shall abbreviate ⟨f ∘ π_{1}, g ∘ π_{2}⟩ as f × g. Then, the following are derived equations:

(g′) id × id = id  (h′) (f × g) ∘ (f′ × g′) = (f ∘ f′) × (g ∘ g′)

(k′) Λf ∘ h = Λ(f ∘ (h × id))

(l′) App ∘ ⟨Λf ∘ h, g⟩ = f ∘ ⟨h, g⟩ (l′′) App ∘ (Λf × id) = f (m′) Λ(App ∘ (f × id)) = f

4.1. The Augmented Simplicial Sets S4 [Γ ⊢ F]

We observe that the S4 modality allows us to exhibit an augmented simplicial structure. We shall see later on (Section 5.2) that this arises from a comonad through the use of certain resolution functors. However, for now we prefer to remain syntactic and therefore relatively concrete.

Definition 16 (S4 [Γ ⊢ F]). For every context Γ, for every type F, let [Γ ⊢ F] be the set of all equivalence classes of λ_{S4}-terms M such that Γ ⊢ M : F is derivable, modulo ≈.

For every q ⩾ −1, let S4 [Γ ⊢ F]_{q} be [Γ ⊢ □^{q+1}F], and let S4 [Γ ⊢ F] be the family (S4 [Γ ⊢ F]_{q})_{q⩾−1}.

For every function f from [Γ ⊢ F_{1}] × … × [Γ ⊢ F_{n}] to [Γ ⊢ G], define □f as the function from [Γ ⊢ □F_{1}] × … × [Γ ⊢ □F_{n}] to [Γ ⊢ □G] that maps the tuple

(M_{1}, …, M_{k}) to f(dx_{1}, …, dx_{k}) · {x_{1} := M_{1}, …, x_{k} := M_{k}}.

Say that f is substitutive whenever f(M_{1}, …, M_{k})θ ≈ f(M_{1}θ, …, M_{k}θ).

Finally, let ∂_{q}^{i} be the function from S4 [Γ ⊢ F]_{q} to S4 [Γ ⊢ F]_{q−1}, 0 ⩽ i ⩽ q, defined by ∂_{q}^{i}M ˆ=(□^{i}d)M; and let s_{q}^{i} be the function from S4 [Γ ⊢ F]_{q} to S4 [Γ ⊢ F]_{q+1}, 0 ⩽ i ⩽ q, defined by s_{q}^{i}M ˆ=(□^{i}s)M, where sM ˆ= x · {x := M}.

Lemma 17. The following hold: 1. □id = id. 2. if f is substitutive, then □f ∘□g = □(f ∘ g). 3. for every f, □f is substitutive. 4. ∂_{q}^{i} and s_{q}^{i} are substitutive.

Proof. 1. □id(M) = dx · {x := M} ≈ M (by (η□)), so □id = id.

2. For every functions f and g, provided f is substitutive, then

□f(□g(M)) = f(dx) · {x := g(dy) · {y := M}}
≈ f(dx){x := g(dy) } · {y := M} (by ( □ ))
≈ f(d g(dy) ) · {y := M} (since f is substitutive)
≈ f(g(dy)) · {y := M} (by (d))

So □f ∘ □g = □(f ∘ g). 3. is obvious, and 4. follows from 3.

Proposition 18. For every Γ and F, the triple (S4 [Γ ⊢ F], (∂_{q}^{i})_{0⩽i⩽q}, (s_{q}^{i})_{0⩽i⩽q}) is an augmented simplicial set.

Proof. Because of Lemma 17, it is enough to check (i)–(vi) in the case i = 0, as the general case then follows immediately by induction on i:

(i) ∂_{q−1}^{0}(∂_{q}^{j}M) = d(□∂_{q−1}^{j−1}M) = d ∂_{q−1}^{j−1}(dx) · {x := M} ≈ ∂_{q−1}^{j−1}(dM) (by (d))

= ∂_{q−1}^{j−1}(∂_{q}^{0}M).

(ii) s_{q+1}^{0}(s_{q}^{j−1}M) = y · {y := s_{q}^{j−1}M}, while s_{q+1}^{j}(s_{q}^{0}M) = □s_{q}^{j−1}(s_{q}^{0}M)

= s_{q}^{j−1}(dy) · {y := s_{q}^{0}M} = s_{q}^{j−1}(dy) · {y := x · {x := M}}

≈ s_{q}^{j−1}(d x ) · {x := M} (by ( □ )) ≈ s_{q}^{j−1}x · {x := M} (by (d)).

If j = 1, then s_{q+1}^{0}(s_{q}^{j−1}M) = y · {y := x · {x := M}} ≈ x · {x := M}

(by ( □ )) = s_{q}^{0}x · {x := M}, and this is precisely s_{q+1}^{j}(s_{q}^{0}M).

If j > 1, then it obtains s_{q+1}^{0}(s_{q}^{j−1}M) = y · {y := s_{q}^{j−1}M}

= y · {y := □s_{q−1}^{j−2}M} = y · {y := s_{q−1}^{j−2}(dx) · {x := M}}

≈ s_{q−1}^{j−2}(dx) · {x := M} (by ( □ )) = □s_{q−1}^{j−2}x · {x := M}

= s_{q}^{j−1}x · {x := M}, which is exactly s_{q+1}^{j}(s_{q}^{0}M).

(iii) ∂_{q+1}^{0}(s_{q}^{j}M) = d(□s_{q−1}^{j−1}M) = d s_{q−1}^{j−1}(dx) · {x := M} ≈ s_{q−1}^{j−1}(dM) (by (d))

= s_{q−1}^{j−1}(∂_{q}^{0}M).

(iv) ∂_{q+1}^{0}(s_{q}^{0}M) = d( x · {x := M}) ≈ M by (d).

(v) ∂_{q+1}^{1}(s_{q}^{0}M) = □∂_{q}^{0}(s_{q}^{0}M) = d(dx) ·{x := y · {y := M}} ≈ d(d y ) ·{y := M}

(by ( □ )) ≈ dy · {y := M} (by (d)) ≈ M (by (η□)).

(vi) s_{q−1}^{0}(∂_{q}^{j}M) = s_{q−1}^{0}(□∂_{q−1}^{j−1}M) = x · {x := ∂_{q−1}^{j−1}(dy) · {y := M}}

≈ ∂_{q−1}^{j−1}(dy) · {y := M} (by ( □ )) = ∂_{q}^{j}y · {y := M}, while on the other

hand ∂_{q+1}^{j+1}(s_{q}^{0}M) = □∂_{q}^{j}( y · {y := M}) = ∂_{q}^{j}(dx) · {x := y · {y := M}}

≈ ∂_{q}^{j}(d y ) · {y := M} (by ( □ )) ≈ ∂_{q}^{j}y · {y := M} (by (d)).

By Lemma 13, the η-long normal form of any term of type □^{q+1}F in Γ can

be written in a unique way … M_{0} · θ_{q} · θ_{q−1} . . . · θ_{0}. Fix a variable x_{0}, and let

θ_{q+1} be {x_{0} ↦ M_{0}}. Then this is also … x_{0}θ_{q+1} · θ_{q} · θ_{q−1} . . . · θ_{0}. Therefore q-

simplices in S4 [Γ ⊢ F] are basically sequences of q +2 substitutions, with additional typing and linearity conditions and conditions on the domains of substitutions. Let us compute faces and degeneracies as they act on η-long normal forms. For short, call the η-long normal form of a q-simplex M in S4 [Γ ⊢ F] the unique η-long normal form of type □^{q+1}F in Γ of M.

First the following lemma will help us compute η-long normal forms of □f applied to arguments in η-long normal form themselves.

Lemma 19. Let f be any function from [Γ ⊢ F_{1}] × … × [Γ ⊢ F_{n}] to [Γ ⊢ G]. We say that f is linearity-preserving if and only if for every η-long normal form M_{1} of type F_{1} in Γ, …, for every η-long normal form M_{n} of type F_{n} in Γ, if M_{1}, …, M_{n} are linear, then the η-long normal form of f(M_{1}, …, M_{n}) of type G in Γ is linear, too. By abuse, write f(M_{1}, …, M_{n}) this η-long normal form again.

Say that f is non-collapsing if and only if, for every η-long normal forms M_{1} of type F_{1} in Γ, …, M_{n} of type F_{n} in Γ, then fv(f(M_{1}, …, M_{n})) = fv(M_{1}) ∪ … ∪ fv(M_{n}).

Let M_{1} · θ_{1}, …, M_{n} · θ_{n} be η-long normal forms of respective types □F_{1}, …, □F_{n} in Γ. Assume without loss of generality that θ_{1}, …, θ_{n} have pairwise disjoint domains. If f is substitutive, linearity-preserving and non-collapsing, then the η-long normal form of type G in Γ of □f( M_{1} · θ_{1}, …, M_{n} · θ_{n}) is exactly

f(M_{1}, …, M_{n}) · (θ_{1}, …, θ_{n}).

Proof. □f( M_{1} · θ_{1}, …, M_{n} · θ_{n})

= f(dx_{1}, …, dx_{n}) · {x_{1} := M_{1} · θ_{1}, …, x_{n} := M_{n} · θ_{n}}

≈ f(dx_{1}, …, dx_{n}){x_{1} := M_{1} , …, x_{n} := M_{n} } · (θ_{1}, …, θ_{n}) (by ( □ ))

≈ f(d M_{1} , …, d M_{n} ) · (θ_{1}, …, θ_{n}) (since f is substitutive) ≈ f(M_{1}, …, M_{n}) ·

(θ_{1}, …, θ_{n}) (by (d)). It remains to show that the latter is η-long normal of type □G in Γ, which will allow us to use Proposition 11. We only have to check that fv(f(M_{1}, …, M_{n})) = dom θ_{1} ∪ … ∪ dom θ_{n} and that f(M_{1}, …, M_{n}) is linear. The former is because f is non-collapsing, and fv(M_{i}) = dom θ_{i}, 1 ⩽ i ⩽ n. The latter is because f is linearity-preserving, and each M_{i} is linear. Indeed, fv(M_{i}) = dom θ_{i} and M_{i} is linear because M_{i} · θ_{i} is η-long normal.

Proposition 20. Let M ∈ S4 [Γ ⊢ F]_{q}, of η-long form … x_{0}θ_{q+1} · θ_{q} · θ_{q−1} . . . ·

θ_{0}. Then the η-long form of ∂_{q}^{i}M is:

. . . . . . x_{0}θ_{q+1} · θ_{q} · θ_{q−1} . . . · θ_{i+2} · (θ_{i+1} · θ_{i}) · θ_{i−1} . . . · θ_{0}  (9)

and the η-long form of s_{q}^{i}M is:

. . . . . . x_{0}θ_{q+1} · θ_{q} · θ_{q−1} . . . · θ_{i+1} · id · θ_{i} . . . · θ_{0}  (10)

where id is the identity substitution on dom θ_{i}.

Proof. By induction on i, simultaneously with the fact that ∂_{q}^{i} and s_{q}^{i} are substitutive, linearity-preserving and non-collapsing. The inductive case is by Lemma 19. In the base case, if i = 0, then (9) is by Lemma 13, and (10) is by Lemma 14.

The geometry of S4 [Γ ⊢ F] is therefore very close to that of the nerve of a category whose objects are contexts Γ, and whose morphisms Γ⟶^{θ}Θ are substitutions θ such that, letting Θ be y_{1} : G_{1}, …, y_{m} : G_{m}, θ is of the form {y_{1} := M_{1}, …, y_{m} := M_{m}} where Γ ⊢ M_{i} : G_{i} is derivable for each i, 1 ⩽ i ⩽ m. Identities are the identity substitutions, composition is substitution concatenation. (It is not quite a nerve, because of the added conditions on substitutions.) The connection with nerves will be made precise in Theorem 30 below.

4.2. The Geometry of S4 [Γ ⊢ F]

In Proposition 20, note that substitutions are taken as is, in particular not modulo ≈. This hints at the fact that S4 [Γ ⊢ F] will in general not be a Kan complex: recall that a nerve of a small category C is Kan if and only if C is a groupoid, i.e., if and only if all morphisms in C are isomorphisms. In the category of substitutions above, the only isomorphisms are renamings {x_{1} := y_{1}, …, x_{n} := y_{n}}, where y_{1}, …, y_{n} are pairwise distinct variables.

Proposition 21. S4 [Γ ⊢ F] is not Kan in general.

Proof. Being Kan would imply in particular that given any two 1-simplices M_{0} and M_{1} with ∂_{1}^{0}M_{0} = ∂_{1}^{0}M_{1}, there should be a 2-simplex M such that ∂_{2}^{0}M = M_{0}

and ∂_{2}^{1}M = M_{1}. Write the η-long normal forms of M_{0} as x_{0}θ_{2} · θ_{1} · θ_{0}, of M_{1}

as x_{0}θ′_{2} · θ′_{1} · θ′_{0}. The condition ∂_{1}^{0}M_{0} = ∂_{1}^{0}M_{1} means that x_{0}θ_{2} · (θ_{1} · θ_{0}) =

x_{0}θ′_{2} · (θ′_{1} · θ′_{0}). In particular, up to a renaming of the variables free in x_{0}θ′_{2}:

θ_{2} = θ′_{2}, θ_{1} · θ_{0} = θ′_{1} · θ′_{0}  (11)

If M exists, then M is of the form x_{0}ϑ_{3} · ϑ_{2} · ϑ_{1} · ϑ_{0}, and up to renamings

of bound variables, ∂_{2}^{0}M = M_{0} entails:

ϑ_{3} = θ_{2}, ϑ_{2} = θ_{1}, ϑ_{1} · ϑ_{0} = θ_{0}  (12)

and ∂_{2}^{1}M = M_{1} entails:

ϑ_{3} = θ′_{2}, ϑ_{2} · ϑ_{1} = θ′_{1}, ϑ_{0} = θ′_{0}  (13)

It follows that θ′_{1} must be an instance of θ_{1}, in particular. (An instance of a substitution θ is a substitution of the form θ · θ′.) But (11) does not guarantee this. For example, take θ_{2} ˆ=θ′_{2} ˆ={x_{0} := dx_{0}}, θ′_{1} ˆ={x_{0} := x_{1}}, θ_{1} ˆ={x_{0} := dx_{1}}, θ_{0} ˆ={x_{1} := x_{1}}, θ′_{0} ˆ={x_{1} := dx_{1}}. It is easily checked that M_{0} and M_{1} are in S4 [Γ ⊢ F]_{1}, i.e., they are of type □^{2}F in Γ, for any formula F, where Γ ˆ=x_{1} : □^{2}F.

This settles the case, at least when Γ contains at least one formula of the form □^{2}F. When Γ is empty, it is easy to see that S4 [Γ ⊢ F] is empty except possibly in dimension −1, so this is trivially Kan—but the geometry of such simplicial sets is uninteresting.

The following notion will be useful in studying the geometry of S4 [Γ ⊢ F]:

Definition 22 (Contiguity). Let K be an augmented simplicial set. The q-simp-lex x is one-step contiguous to the q-simplex y, in short x ⇾ y, if and only if there is a (q + 1)-simplex z in K, and two indices i, j with 0 ⩽ i < j ⩽ q + 1 such that ∂_{q+1}^{j}z = x and ∂_{q+1}^{i}z = y, and x ≠ y.

The q-simplex x is contiguous to y if and only if x ⇾^{∗} y, and strictly contiguous if and only if x ⇾^{+} y. We say that x and y are contiguous if and only if x ⇿ y, where ⇿ is the reflexive symmetric transitive closure of ⇾.

Contiguity is usually presented a bit differently. In particular, it is usually not required that j > i in one-step contiguity. Then ⇾^{∗} is an equivalence relation. However we shall need the finer notion of ⇾ in the sequel.

The following lemma, for example, is unusual:

Lemma 23. The relation ⇾ is well-founded on S4 [Γ ⊢ F].

Proof. Define the following measure μ(M) for q-simplices M in S4 [Γ ⊢ F]_{q}. When-

ever M has η-long normal form … x_{0}θ_{q+1} · θ_{q} . . . ·θ_{0}, let μ(M) be the (q+2)-tuple

(|θ_{q+1}|, |θ_{q}|, …, |θ_{0}|), ordered lexicographically from left to right, where |θ| is the size of θ, defined in any obvious way.

Let M and M′ be two q-simplices in S4 [Γ ⊢ F], and assume that M ⇾ M′. Then there is a (q + 1)-simplex N, say:

… x_{0}θ_{q+2} · θ_{q+1} . . . · θ_{1} · θ_{0}

and i < j such that ∂_{q+1}^{j}N = M, ∂_{q+1}^{i}N = M′. That is:

M = . . . . . . . . . x_{0}θ_{q+2} · θ_{q+1} . . . · (θ_{j+1} · θ_{j}) · θ_{j−1} . . . · θ_{i+1} · θ_{i} . . . · θ_{0}

M′ = . . . . . . . . . x_{0}θ_{q+2} · θ_{q+1} . . . · θ_{j+1} · θ_{j} . . . · θ_{i+2} · (θ_{i+1} · θ_{i}) . . . · θ_{0}

Clearly μ(M) ⩾ μ(M′). We claim that μ(M) > μ(M′). Since the lexicographic ordering on sizes is well-founded, this will establish the result.

Assume on the contrary that μ(M) = μ(M′). Then, |θ_{j+1} · θ_{j}| = |θ_{j+1}|, so up to a renaming of bound variables, θ_{j+1} · θ_{j} = θ_{j+1}, so θ_{j} = id. Then |θ_{j}| = |θ_{j−1}|, …, |θ_{i+2}| = |θ_{i+1}|, which imply that θ_{j−1}, …, θ_{i+1} must map variables to variables. By the linearity constraints on η-long normal forms, they must be one-to-one. So up to renaming of bound variables, θ_{j−1} = … = θ_{i+1} = id. But then M = M′, contradicting M ⇾ M′.

Corollary 24. The relation ⇾^{+} on S4 [Γ ⊢ F] is a strict ordering.

Proof. If it were reflexive, then we would have M ⇾^{+} M for some M, hence an infinite decreasing chain M ⇾^{+} M ⇾^{+} M ⇾^{+} …

Definition 25 (Vertices, Component). Let K be any augmented simplicial set. Given any q-simplex x of K, q ⩾ 0, the vertices of x are those 0-simplices that are iterated faces of x. The ith vertex of x, 0 ⩽ i ⩽ q, is ð_{q}^{i}x ˆ=∂_{1}^{0} … ∂_{i}^{i−1}∂_{i+1}^{i+1} … ∂_{q}^{q}x.

The component π_{0}x is ∂_{0}^{0} … ∂_{i}^{i} … ∂_{q}^{q}x.

It is well-known that each q-simplex has exactly q + 1 vertices (possibly equal), and these are ð_{q}^{0}x, …, ð_{q}^{q}x. Moreover, these vertices are contiguous:

Lemma 26. Let K be any augmented simplicial set. Given any q-simplex x of K, q ⩾ 0,

ð_{q}^{0}x ⇾^{∗} ð_{q}^{1}x ⇾^{∗} … ⇾^{∗} ð_{q}^{q}x

Proof. To show that ð_{q}^{i}x ⇾^{∗} ð_{q}^{i+1}x, let y be the 1-simplex ∂_{2}^{0} … ∂_{i+1}^{i−1}∂_{i+2}^{i+2} … ∂_{q}^{q}x. Then ∂_{1}^{0}y = ð_{q}^{i+1}x and ∂_{1}^{1}y = ð_{q}^{i}x, so ð_{q}^{i}x ⇾^{=} ð_{q}^{i+1}x, where ⇾^{=} is ⇾ ∪ =.

Observe that there is no need to take ⇾^{+} instead of ⇾ in the case of 0-simplices in λ_{S4}:

Lemma 27. The relation ⇾ is transitive on 0-simplices of S4 [Γ ⊢ F].

Proof. Note that, if M and M′ are two 0-simplices, then M ⇾ M′ means that for some 1-simplex M_{1}, ∂_{1}^{1}M_{1} = M and ∂_{1}^{0}M_{1} = M′.

So assume that M ⇾ M′ ⇾ M′′. There is a 1-simplex N · θ_{1} · θ_{2} such that

M = Nθ_{1} · θ_{2} and M′ = N · (θ_{1} · θ_{2}). There is also a 1-simplex N′ · θ′_{1} · θ′_{2}

such that M′ = N′θ′_{1} · θ′_{2} and M′′ = N′ · (θ′_{1} · θ′_{2}). Comparing both forms for M′, we must have, up to renaming of bound variables, N = N′θ′_{1} and θ′_{2} = θ_{1} · θ_{2}. So

M_{2} ˆ= N′ · θ′_{1} · θ_{1} · θ_{2} is a valid 2-simplex. Take M_{1} ˆ=∂_{2}^{1}M_{2} = N′ · (θ′_{1} · θ_{1}) · θ_{2}.

Then ∂_{1}^{1}M_{1} = M and ∂_{1}^{0}M_{1} = M′′, so M ⇾^{=} M′′. By Corollary 24, M ⇾ M′′.

The following lemma shows that, basically, if two λ_{S4}-simplices are contiguous, then they are so in a unique way:

Lemma 28 (Two-face Lemma). Let M, M′ be two q-simplices of S4 [Γ ⊢ F], q ⩾ 0. Then for any 0 ⩽ i < j ⩽ q + 1, there is at most one (q + 1)-simplex N of S4 [Γ ⊢ F] such that ∂_{q}^{j}N = M and ∂_{q}^{i}N = M′.

Proof. Assume N exists, and write it as:

… x_{0}ϑ_{q+2} · ϑ_{q+1} . . . · ϑ_{1} · ϑ_{0}

Also, write:

M = … x_{0}θ_{q+1} · θ_{q} . . . · θ_{1} · θ_{0}

M′ = … x_{0}θ′_{q+1} · θ′_{q} . . . · θ′_{1} · θ′_{0}

Since ∂_{q}^{j}N = M, up to renaming of bound variables, θ_{0} = ϑ_{0}, …, θ_{j−1} = ϑ_{j−1}, θ_{j} = ϑ_{j+1} · ϑ_{j}, θ_{j+1} = ϑ_{j+2}, …, θ_{q+1} = ϑ_{q+2}. And since ∂_{q}^{i}N = M′, up to renaming of bound variables, θ′_{0} = ϑ_{0}, …, θ′_{i−1} = ϑ_{i−1}, θ′_{i} = ϑ_{i+1} · ϑ_{i}, θ′_{i+1} = ϑ_{i+2}, …, θ′_{q+1} = ϑ_{q+2}.

In particular, ϑ_{0} = θ_{0}, …, ϑ_{j−1} = θ_{j−1}, ϑ_{i+2} = θ′_{i+1}, …, ϑ_{q+2} = θ′_{q+1}. So ϑ is determined uniquely as soon as j > i + 1. If j = i + 1, this determines ϑ uniquely, except possibly for ϑ_{j}. Now we use the additional equations θ_{j} = ϑ_{j+1} · ϑ_{j} and θ′_{i+1} = ϑ_{i+2}. The latter means that θ′_{j} = ϑ_{j+1}. Since every variable of dom ϑ_{j} is free in some term in the range of ϑ_{j+1}, this determines ϑ_{j} uniquely.

In the case of S4 [Γ ⊢ F], Lemma 26 is the only condition on vertices that needs to be satisfied for them to be vertices of a q-simplex:

Proposition 29. Let M_{0}, M_{1}, …, M_{q} be q +1 0-simplices of S4 [Γ ⊢ F]. If M_{0} ⇾^{∗} M_{1} ⇾^{∗} … ⇾^{∗} M_{q}, then there is a unique q-simplex M such that ð_{q}^{i}M = M_{i}, 0 ⩽ i ⩽ q.

Proof. By Lemma 27, M_{0} ⇾^{=} M_{1} ⇾^{=} … ⇾^{=} M_{q}.

We now show uniqueness by induction on q ⩾ 0. If q = 0, this is obvious. Otherwise, by induction there is at most one (q − 1)-simplex M^{0} with vertices M_{1} ⇾^{=} … ⇾^{=} M_{q}, and at most one (q − 1)-simplex M^{q} with vertices M_{0} ⇾^{=} … ⇾^{=} M_{q−1}. If there is any q-simplex M with vertices M_{0}, M_{1}, …, M_{q}, then ∂_{q}^{0}M = M^{0} and ∂_{q}^{q}M = M^{q}, so there is at most one such M by Lemma 28.

Existence: write M_{i} as N_{i} · θ_{i} for each i, 0 ⩽ i ⩽ q. Since for each i < q,

M_{i} ⇾^{=} M_{i+1}, there are (unique) 1-simplices N′_{i} · ϑ_{1}^{i} ·ϑ_{0}^{i} such that, up to renaming

of bound variables, N_{i} = N′_{i}ϑ_{1}^{i}, θ_{i} = ϑ_{0}^{i}, N_{i+1} = N′_{i}, θ_{i+1} = ϑ_{1}^{i} · ϑ_{0}^{i}. Note that N_{i} = N_{i+1}ϑ_{1}^{i}, and ϑ_{0}^{i+1} = ϑ_{1}^{i} · ϑ_{0}^{i}. So define:

M ˆ= . . . . . . N_{q} · ϑ_{1}^{q−1} . . . · ϑ_{1}^{i−1} . . . · ϑ_{1}^{0} · ϑ_{0}^{0}

In particular, ð_{q}^{0}M = N_{q}ϑ_{1}^{q−1} … ϑ_{1}^{i−1} … ϑ_{1}^{0} · ϑ_{0}^{0} = N_{q−1}ϑ_{1}^{q−2} … ϑ_{1}^{0} · ϑ_{0}^{0} = … =

N_{0} · ϑ_{0}^{0} = M_{0}. And for every i > 0, ð_{q}^{i}M = N_{q}ϑ_{1}^{q−1} … ϑ_{1}^{i} · (ϑ_{1}^{i−1} · . . . · ϑ_{1}^{0} · ϑ_{0}^{0})

= N_{i} · (ϑ_{1}^{i−1} · . . . · ϑ_{1}^{1} · ϑ_{1}^{0} · ϑ_{0}^{0}) = N_{i} · (ϑ_{1}^{i−1} · . . . · ϑ_{1}^{1} · ϑ_{0}^{1}) = … = N_{i} · ϑ_{0}^{i} =

M_{i}.

To sum up, the non-augmented part of S4 [Γ ⊢ F] can be characterized as a particularly simple nerve:

Theorem 30 (Nerve Theorem). Let C[Γ ⊢ F] be the partial order consisting of the 0-simplices of S4 [Γ ⊢ F], ordered by contiguity ⇾^{∗}. Then the (non-augmented) simplicial set (S4 [Γ ⊢ F]_{q})_{q∈ℕ} is (isomorphic to) the nerve N(C[Γ ⊢ F]).

Proof. Recall that the nerve of a category C has diagrams:

A_{0}  \overline{f_{1} ≻} A_{1}  \overline{f_{2} ≻} … \overline{\begin{matrix}f_{q−1} \\ ≻ \end{matrix}} A_{q−1}  \overline{f_{q} ≻} A_{q}

as q-simplices, where f_{1}, f_{2}, …, f_{q} are morphisms in C, and q ⩾ 0. The ith face is obtained by removing A_{i} from the sequence, composing the neighboring arrows if 0 < i < q, and dropping them if i = 0 or i = q. The ith degeneracy is obtained by duplicating A_{i}, adding an identity morphism.

By Lemma 26 and Proposition 29, q-simplices M are in bijection with ordered sequences of 0-simplices M_{0} ⇾^{∗} M_{1} ⇾^{∗} … ⇾^{∗} M_{q}. Moreover, for every j, 0 ⩽ j ⩽ q − 1, the jth vertex of ∂_{q}^{i}M is:

ð_{q}^{j}∂_{q}^{i}M = ∂_{1}^{0} … ∂_{j}^{j−1}∂_{j+1}^{j+1} … ∂_{q−1}^{q−1}∂_{q}^{i}M = \{ \begin{matrix}ð_{q}^{j}M & if j < i \\ ð_{q}^{j+1}M & if j ⩾ i \end{matrix}

That is, the vertices of ∂_{q}^{i}M are those of M except ð_{q}^{i}M. Similarly, for every j, 0 ⩽ j ⩽ q + 1, the jth vertex of s_{q}^{i}M is:

ð_{q}^{j}s_{q}^{i}M = ∂_{1}^{0} … ∂_{j}^{j−1}∂_{j+1}^{j+1} … ∂_{q+1}^{q+1}s_{q}^{i}M = \{ \begin{matrix}ð_{q}^{j}M & if j ⩽ i \\ ð_{q}^{i}M & if j = i + 1 \\ ð_{q}^{j−1}M & if j > i + 1 \end{matrix}

That is, the vertices of s_{q}^{i}M are those of M in sequence, with ð_{q}^{i}M occurring twice.

In other words, (S4 [Γ ⊢ F]_{q})_{q∈ℕ} is an oriented simplicial complex. Recall that an oriented simplicial complex is a family of linearly ordered sequences of so-called points, containing all one-element sequences, and such that any subsequence of an element of the family is still in the family. In fact, it is the full oriented simplicial complex, containing all linearly ordered sequences of points.

It is futile to study the classical notions of loop homotopy in such an oriented simplicial complex. Indeed, all loops are trivial: if the 1-simplex M is a loop, i.e., ∂_{1}^{0}M = ∂_{1}^{1}M is some point N, then its sequence of vertices is N ⇾^{∗} N, so M is a degenerate 1-simplex. Homotopies of loops, and in fact the natural extension of homotopies between 1-simplices, is trivial, too: let M, M′ be two 1-simplices with ∂_{1}^{0}M = ∂_{1}^{0}M′ = M_{0} and ∂_{1}^{1}M = ∂_{1}^{1}M′ = M_{1}; if there is a homotopy 2-simplex P connecting them, then its faces are M, M′ plus some degenerate 1-simplex, so the sequence of vertices of P must be M_{1} ⇾^{∗} M_{0} ⇾^{∗} M_{0} or M_{1} ⇾^{∗} M_{1} ⇾^{∗} M_{0}, from which it follows that the homotopy is one of the two degeneracies of M = M′.

In short, two 1-simplices are homotopic in the classical sense if and only if they are equal, and all homotopies are degenerate. However, studying homotopies of paths (not just loops) certainly remains interesting. In particular, the geometry of preorders and lattices viewed through their order complexes is a rich domain [8].

4.3. Components

The last section closes the case for non-negative dimensions. In dimension −1, recall that there are two extremal ways to build an augmentation of a simplicial set (see e.g., [14]). One, exemplified by the nerve construction for augmented simplicial sets, builds the augmentation of the simplicial set K, K_{−1}, as a one-element set (an empty set if K is empty), and ∂_{0}^{0} is the unique function K_{0} → K_{−1}. The other builds K_{−1} as the set of connected components of K_{0}, that is, as the set of ⇿-equivalence classes of points. It turns out that the latter is how the augmentation is built in S4 [Γ ⊢ F], except that there might also be (−1)-simplices that are the component of no q-simplex for any q ⩾ 0. In other words, the components are exactly the path connected components, plus isolated (−1)-dimensional simplices. This is shown in Proposition 32 below. First, we observe:

Proposition 31 (Lattice of points). Let M_{0} be a (−1)-simplex of S4 [Γ ⊢ F].

The set C(M_{0}) of 0-simplices M such that ∂_{0}^{0}M = M_{0}, equipped with the ordering ⇾^{∗}, is empty or is a finite lattice.

Proof. Every such M can be written in a unique way N · θ, with Nθ = M_{0}. But, up to the names of free variables in N, there are only finitely many such N’s and θ’s. So C(M_{0}) is finite.

In the rest of the proof, fix a typing of M_{0}. This way, each subterm of M_{0} gets a unique type. This will allow us to reason by induction on M_{0}—in general, on terms—instead on a BN_{0} derivation of Γ ⊢_{I} M_{0} : F.

Note that N · θ ⇾^{∗} N′ · θ′ if and only if N · θ ⇾^{=} N′ · θ′ (by Lemma 27) if

and only if for some N_{0} · ϑ_{1} · ϑ_{0}, N = N_{0}ϑ_{1}, θ = ϑ_{0}, N′ = N_{0}, θ′ = ϑ_{1} · ϑ_{0} (up

to renaming of bound variables), if and only if N = N′ϑ_{1} for some substitution ϑ_{1}. In other words, if and only if N is an instance of N′.

Then every pair of points M_{1}, M_{2} of C(M_{0}) has a supremum M. That is, M ⇾^{∗} M_{1}, M ⇾^{∗} M_{2} and for every M′ such that M′ ⇾^{∗} M_{1} and M′ ⇾^{∗} M_{2}, M ⇾^{∗} M′. Write M_{1} as N_{1} · θ_{1}, M_{2} as N_{2} · θ_{2}, with N_{1}θ_{1} = N_{2}θ_{2}. Then, if M exists, M is a common instance of N_{1} and N_{2}. It is easy to see that there is a least common instance N_{1}∧N_{2} of N_{1} and N_{2}, i.e., one such that every other instance of N_{1} and N_{2} is an instance of N_{1} ∧ N_{2}. More generally, given any finite set W of variables (used to collect λ-bound variables), call an instance of N away from W any term Nθ such that dom θ∩W = ∅. Then if there is a common instance of N_{1} and N_{2} away from W, then there is a least one N_{1} ∧_{W} N_{2}, where N_{1} and N_{2} are linear, and it is computed as in Figure 4. Then define N_{1} ∧ N_{2} as N_{1} ∧_{∅} N_{2}. Since N_{1}θ = N_{2}θ_{2} = M_{0}, there is a unique substitution θ with dom θ = fv(N_{1} ∧ N_{2}), and the free variables of N_{1} ∧ N_{2} being free variables of N_{1} or N_{2}, have boxed types. Therefore M ˆ= N_{1} ∧ N_{2} · θ is a well-typed term, and M ⇾^{∗} M_{1} and M ⇾^{∗} M_{2}, since N_{1} ∧ N_{2} is both an instance

x_{1} ∧_{W} N_{2} ˆ= N_{2}  (x_{1} ∉ W)
N_{1} ∧_{W} x_{2} ˆ= N_{1}  (x_{2} ∉ W)
(N_{1}N′_{1}) ∧_{W} (N_{2}N′_{2}) ˆ= (N_{1} ∧_{W} N_{2})(N′_{1} ∧_{W} N′_{2})
(λx · N_{1}) ∧_{W} (λx · N_{2}) ˆ= λx · (N_{1} ∧_{W ∪{x}} N_{2})
dN_{1} ∧_{W} dN_{2} ˆ= d(N_{1} ∧_{W} N_{2})
N · {x_{1} := N_{11}, …, x_{n} := N_{n1}} ∧_{W} N · {x_{1} := N_{12}, …, x_{n} := N_{n2}}
ˆ= N · {x_{1} := N_{11} ∧_{W} N_{12}, …,
x_{n} := N_{n1} ∧_{W} N_{n2}}

Figure 4: Least common instances

of N_{1} and an instance of N_{2}. Moreover, by construction this is the least one, so M is the supremum of M_{1} and M_{2}. (This is unification [31]. The key here is that we basically only need unification modulo an empty theory, instead of the theory of the relation ≈.) We write M as M_{1} ⊔ M_{2}.

Symmetrically, every pair of points M_{1}, M_{2} of C(M_{0}) has an infimum M. That is, M_{1} ⇾^{∗} M, M_{2} ⇾^{∗} M and for every M′ such that M_{1} ⇾^{∗} M′ and M_{2} ⇾^{∗} M′,

M′ ⇾^{∗} M. Write again M_{1} as N_{1} · θ_{1}, M_{2} as N_{2} · θ_{2}, with N_{1}θ_{1} = N_{2}θ_{2}.

Calling a generalization of a term N (away from W) any term having N as instance (away from W), we may compute a greatest common generalization N_{1} ∨_{W} N_{2} away from W of N_{1} and N_{2} as in Figure 5, where N_{1}θ_{1} = N_{2}θ_{2}. As above, letting

x_{1} ∨_{W} N_{2} ˆ= x_{1}  (x_{1} ∉ W)
N_{1} ∨_{W} x_{2} ˆ= x_{2}  (x_{2} ∉ W)
(N_{1}N′_{1}) ∨_{W} (N_{2}N′_{2}) ˆ= (N_{1} ∨_{W} N_{2})(N′_{1} ∨_{W} N′_{2})
(λx · N_{1}) ∨_{W} (λx · N_{2}) ˆ= λx · (N_{1} ∨_{W ∪{x}} N_{2})
dN_{1} ∨_{W} dN_{2} ˆ= d(N_{1} ∨_{W} N_{2})
N · {x_{1} := N_{11}, …, x_{n} := N_{n1}} ∨_{W} N · {x_{1} := N_{12}, …, x_{n} := N_{n2}}
ˆ= N · {x_{1} := N_{11} ∨_{W} N_{12}, …,
x_{n} := N_{n1} ∨_{W} N_{n2}}

Figure 5: Greatest common generalizations

N_{1} ∨ N_{2} ˆ=N_{1} ∨_{∅} N_{2}, there is a unique substitution θ such that fv(N_{1} ∨ N_{2}) = dom θ and (N_{1} ∨ N_{2})θ = M_{0}, and M ˆ= N_{1} ∨ N_{2} · θ is a well-typed term, from which we conclude that M is indeed the infimum of M_{1} and M_{2}. Write M as M_{1} ⊓ M_{2}.

It remains to show that, if C(M_{0}) is not empty, then it has a least element ⊥ and a greatest element ⊤. This is obvious, as ⊥ can be defined as the (finite) infimum of all elements of C(M_{0}), and ⊤ as the (finite) supremum of all elements of C(M_{0}).

Proposition 32. Given any two 0-simplices M_{1} and M_{2} of S4 [Γ ⊢ F], M_{1} ⇿ M_{2} if and only if ∂_{0}^{0}M_{1} = ∂_{0}^{0}M_{2}.

Proof. Clearly, if M_{1} ⇾^{=} M_{2}, i.e. if ∂_{1}^{1}N = M_{1} and ∂_{1}^{0}N = M_{2} for some 1-simplex N, then ∂_{0}^{0}M_{1} = ∂_{0}^{0}∂_{1}^{1}N = ∂_{0}^{0}∂_{1}^{0}N = ∂_{0}^{0}M_{2}. So if M_{1} ⇿ M_{2}, then ∂_{0}^{0}M_{1} = ∂_{0}^{0}M_{2}.

Conversely, assume ∂_{0}^{0}M_{1} = ∂_{0}^{0}M_{2}, and name M_{0} this (−1)-simplex. By Proposition 31, there is an element M_{1} ⊔ M_{2} in C(M_{0}), such that M_{1} ⊔ M_{2} ⇾^{∗} M_{1} and M_{1} ⊔ M_{2} ⇾^{∗} M_{2}. In particular M_{1} ⇿ M_{2}.

In other words, non-empty components C(M_{0}) coincide with path-connected components.

This generalizes to higher dimensions:

Proposition 33. For any two q-simplices M_{1} and M_{2} of S4 [Γ ⊢ F], M_{1} ⇿ M_{2} if and only if π_{0}M_{1} = π_{0}M_{2}.

Proof. Recall that π_{0}M denotes the component of M (Definition 25).

If M_{1} ⇾^{=} M_{2}, then there is a (q+1)-simplex N and j > i such that M_{1} = ∂_{q+1}^{j}N, M_{2} = ∂_{q+1}^{i}N. So π_{0}M_{1} = π_{0}N = π_{0}M_{2}.

Conversely, assume π_{0}M_{1} = π_{0}M_{2} = M_{0}. So every vertex of M_{1} and M_{2} is in C(M_{0}). Using the Nerve Theorem 30, we equate q-simplices with ordered sequences of q + 1 vertices. Then notice that the sequence N_{0} ⇾^{=} N_{1} ⇾^{=} … ⇾^{=} N_{i} ⇾^{=} … ⇾^{=} N_{q} is contiguous to N_{0} ⇾^{=} N_{1} ⇾^{=} … ⇾^{=} N′_{i} ⇾^{=} … ⇾^{=} N_{q} as soon as N_{i} ⇾^{=} N′_{i}. Indeed the former is the (i + 1)st face, and the latter is the ith face of the sequence N_{0} ⇾^{=} N_{1} ⇾^{=} … ⇾^{=} N_{i} ⇾^{=} N′_{i} ⇾^{=} … ⇾^{=} N_{q}. Iterating, we obtain that the sequence N_{0} ⇾^{=} N_{1} ⇾^{=} … ⇾^{=} N_{q} is contiguous to N′_{0} ⇾^{=} N′_{1} ⇾^{=} … ⇾^{=} N′_{q} as soon as N_{i} ⇾^{∗} N′_{i} for every i, 0 ⩽ i ⩽ q. Recall that every vertex of M_{1} and M_{2} is in C(M_{0}). Using Proposition 31, M_{1}, viewed as the sequence ð_{q}^{0}M_{1} ⇾^{∗} ð_{q}^{1}M_{1} ⇾^{∗} … ⇾^{∗} ð_{q}^{q}M_{1}, is contiguous to (ð_{q}^{0}M_{1} ⊓ ð_{q}^{0}M_{2}) ⇾^{∗} (ð_{q}^{1}M_{1} ⊓ ð_{q}^{1}M_{2}) ⇾^{∗} … ⇾^{∗} (ð_{q}^{q}M_{1} ⊓ ð_{q}^{q}M_{2}). Similarly for M_{2}. Since M_{1} and M_{2} are contiguous to the same q-simplex, M_{1} ⇿ M_{2}.

4.4. Planes and Retractions

Next, we show that certains subspaces of S4 [Γ ⊢ F] are retracts of the whole space, under some mild conditions.

Definition 34 (Planes). Call a type boxed if and only if it is of the form □F. Call Γ boxed if and only if it maps variables to boxed types.

Let Γ be a context, and Θ ˆ=y_{1} : □G_{1}, …, y_{p} : □G_{p} be a boxed subcontext of Γ. The plane Θ^{⊥} of S4 [Γ ⊢ F] is the set of 0-simplices of S4 [Γ ⊢ F] having an η-long normal form of the form N · θ such that

for every y ∈ dom θ · if y_{i} ∈ fv(yθ) then yθ = y_{i}  (14)

for every i, 1 ⩽ i ⩽ p.

(Note that the types of variables y_{j}, 1 ⩽ j ⩽ p, have to start with □ for this definition to make sense. To be fully formal, we should mention Γ and F in the notation for Θ^{⊥}. However, Γ and F will be clear from context.) From the point of view of Gentzen-style sequents, a term in the given plane corresponds to a proof that ends in a □-introduction rule followed by series of cuts on formulae occurring on the left of the □-introduction rule, none of which being any of the □G_{i}s in Θ.

By extension, using Theorem 30 and Proposition 32, we define q-simplices of Θ^{⊥} as contiguous sequences of points M_{0} ⇾^{∗} M_{1} ⇾^{∗} … ⇾^{∗} M_{q} of Θ^{⊥} for q ⩾ 0, and as components of points of Θ^{⊥} if q = −1.

It is not hard to see that Θ^{⊥} = S4 [Γ ⊢ F] if Θ is empty. On the other hand, if Γ = Θ, then the points of Θ^{⊥} are of the form N , with component N. In this case, any component N of the plane Θ^{⊥} contains exactly one point, namely N . It follows that in this case Θ^{⊥} is a discrete collection of points.

Lemma 35. For any boxed subcontext Θ of Γ, Θ^{⊥} is a sub-a.s. set of S4 [Γ ⊢ F].

Proof. Clearly every q-simplex of Θ^{⊥} is a q-simplex of S4 [Γ ⊢ F]. That faces and degeneracies of q-simplices of Θ^{⊥} are still in Θ^{⊥} is by construction.

Lemma 36. Let Θ be any boxed subcontext of Γ, and M_{0} ∈ S4 [Γ ⊢ F]_{−1}. For any two 0-simplices M_{1} and M_{2} of C(M_{0}):

1. if M_{1} ⇾^{∗} M_{2} and M_{2} ∈ Θ^{⊥} then M_{1} ∈ Θ^{⊥}.

2. if M_{1} and M_{2} are in Θ^{⊥} then so are M_{1} ⊓ M_{2} and M_{1} ⊔ M_{2}.

Proof. 1. Let M_{1} ˆ= N_{1} · θ_{1} be in C(M_{0}), and M_{2} ˆ= N_{2} · θ_{2} be in C(M_{0}) and in Θ^{⊥}. So for every z ∈ dom θ_{2} such that y_{i}, 1 ⩽ i ⩽ p, is free in zθ_{2}, zθ_{2} = y_{i}. Since M_{1} ⇾^{∗} M_{2}, not only is N_{1} an instance of N_{2}, but there is also a substitution ϑ such that θ_{2} = ϑ·θ_{1}, dom ϑ = dom θ_{2} = fv(N_{2}) and fv(N_{2}ϑ) = dom θ_{1}. Assume that y_{i} is free in yθ_{1} for some y ∈ dom θ_{1} = fv(N_{2}ϑ). So y occurs free in some zϑ, z ∈ fv(N_{2}). In particular, y_{i} is free in zϑθ_{1} = zθ_{2}. Therefore zθ_{2} = y_{i}, recalling that M_{2} ∈ Θ^{⊥}. In other words, zϑθ_{1} = y_{i}. It follows by standard size considerations that zϑ is a variable. Since y occurs free in zϑ, it obtains zϑ = y. So yθ_{1} = y_{i}.

2. Let M_{1} ˆ= N_{1} · θ_{1} and M_{2} ˆ= N_{2} · θ_{2} in Θ^{⊥}. For simplicity, assume that Θ contains exactly one variable y_{1}. This entails no loss of generality, as in general Θ^{⊥} is the intersection of all (y_{i} : F_{i})^{⊥}, y_{i} ∈ dom Θ. That M_{1} ⊔ M_{2} is in Θ^{⊥} follows from 1, since M_{1} ⊔ M_{2} ⇾^{∗} M_{1}. On the other hand M_{1} ⊓ M_{2} is of the form N_{1} ∨ N_{2} · θ where θ is the unique substitution with domain fv(N_{1} ∨ N_{2}) such that (N_{1} ∨ N_{2})θ = M_{0}. In general, we may compute θ as θ_{∅,M_{0}}(N_{1}, N_{2}), where θ_{W,M_{0}}(N_{1}, N_{2}) is the unique substitution with domain fv(N_{1} ∨_{W} N_{2}) \ W such that (N_{1} ∨_{W} N_{2})θ_{W,M_{0}}(N_{1}, N_{2}) = M_{0}, provided N_{1} ∨_{W} N_{2} exists and N_{1} and N_{2} are linear and have M_{0} as common instance. This parallels the computation of N_{1} ∨_{W} N_{2}:

θ_{W,M_{0}}(x_{1}, N_{2}) ˆ={x_{1} := M_{0}} (x_{1} ∉ W)
θ_{W,M_{0}}(N_{1}, x_{2}) ˆ={x_{2} := M_{0}} (x_{2} ∉ W)
θ_{W,M_{0}M′_{0}}(N_{1}N′_{1}, N_{2}N′_{2}) ˆ=θ_{W,M_{0}}(N_{1}, N_{2}) ∪ θ_{W,M′_{0}}(N′_{1}, N′_{2})
θ_{W,λx·M_{0}}(λx · N_{1}, λx · N_{2}) ˆ=θ_{W ∪{x},M_{0}}(N_{1}, N_{2})
θ_{W,dM_{0}}(dN_{1}, dN_{2}) ˆ=θ_{W,M_{0}}(N_{1}, N_{2})
θ_{W, N ·{x_{1}:=M_{1},...,x_{n}:=M_{n}}} ( N · {x_{1} := N_{11}, …, x_{n} := N_{n1}},

…

N · {x_{1} := N_{12}, …, x_{n} := N_{n2}})

ˆ= ⋃_{j=1}^{n} θ_{W,M_{j}}(N_{j1}, N_{j2})

Notice that unions of substitutions are well-defined because we assume N_{1} and N_{2} are linear terms away from W (i.e., no two distinct subterms share any free variable except possibly for variables in W). Now, generalize the claim as follows. Assume that the common instance M_{0} of N_{1} and N_{2} away from W is M_{0} = N_{1}θ_{1} = N_{2}θ_{2} with dom θ_{1} = fv(N_{1}), dom θ_{2} = fv(N_{2}). Assume also that for every variable z ∈ dom θ_{i} such that y_{1} is free in zθ_{i} then y_{1} = zθ_{i}, for every i ∈ {1, 2}. Then an easy induction on terms shows that for every variable y ∈ fv(N_{1}∨_{W} N_{2})\W such that y_{1} is free in yθ_{W,M_{0}}(N_{1}, N_{2}), then yθ_{W,M_{0}}(N_{1}, N_{2}) = y_{1}. The crucial cases are the first two of the definition, which are symmetric. In particular in the first case, assume N_{1} = x_{1} ∉ W. By assumption x_{1}θ_{1} = N_{2}θ_{2} = M_{0}; then θ_{W,M_{0}}(x_{1}, N_{2}) = {x_{1} := M_{0}} is θ_{1} restricted to x_{1}, therefore indeed yθ_{W,M_{0}}(N_{1}, N_{2}) = y_{1}, whatever y may be. The claim follows by taking W = ∅.

Proposition 37 (Projection). If Γ is boxed, then for any Θ ⊆ Γ, there is an augmented simplicial map π_{Θ^{⊥}}, projection onto Θ^{⊥}, from S4 [Γ ⊢ F] to its sub-a.s. set Θ^{⊥}, which coincides with the identity on Θ^{⊥}.

Proof. Let us first define π_{Θ^{⊥}} on 0-simplices. Using Proposition 31, define π_{Θ^{⊥}} ( N · θ) as the infimum ⨅ S of the set S of elements M ∈ Θ^{⊥} such that

M ⇾^{∗} N · θ. Observe that, since Γ is boxed, Nθ is well-typed, hence is a valid 0-simplex. Moreover, it is clear that Nθ ∈ Θ^{⊥}, and Nθ ⇾^{∗} N · θ. So S is not empty, therefore ⨅ S exists and is a 0-simplex of S4 [Γ ⊢ F]. By Lemma 36 any finite non-empty infimum of elements of Θ^{⊥} is in Θ^{⊥}. By Proposition 31 S4 [Γ ⊢ F] is finite, so S is a finite non-empty infimum of elements of Θ^{⊥}. So π_{Θ^{⊥}}( N · θ) = ⨅ S is in Θ^{⊥}.

If N ·θ is already in Θ^{⊥}, then it is in S. Since M ⇾^{∗} N ·θ for every M in S by construction, N ·θ is the minimal element of S, hence N ·θ = ⨅ S = π_{Θ^{⊥}}( N ·θ). So π_{Θ^{⊥}} indeed coincides with the identity on Θ^{⊥}.

To show that π_{Θ^{⊥}} extends to an a.s. map from S4 [Γ ⊢ F] to Θ^{⊥}, it remains to show that π_{Θ^{⊥}} preserves components (obvious) and contiguity (for dimensions ⩾ 1). As far as the latter is concerned, let M_{1} ⇾^{∗} M_{2} be 0-simplices in S4 [Γ ⊢ F]. Since M_{1} ⇾^{∗} M_{2}, {M ∈ Θ^{⊥}|M ⇾^{∗} M_{1}} ⊆ {M ∈ Θ^{⊥}|M ⇾^{∗} M_{2}}, so ⨅{M ∈ Θ^{⊥}|M ⇾^{∗} M_{1}} ⇾^{∗} ⨅{M ∈ Θ^{⊥}|M ⇾^{∗} M_{2}}. That is, π_{Θ^{⊥}}(M_{1}) ⇾^{∗} π_{Θ^{⊥}}(M_{2}).

The projection construction can be used to show a connection between the syntactic function space S4 [Γ ⊢ F ⊃ G] and HomΔ̂(S4 [Γ ⊢ F], S4 [Γ ⊢ G]). The first direction is easy:

Definition 38 (Syntactic application ⋆). The syntactic application map ⋆ from S4 [Γ ⊢ F ⊃ G]×S4 [Γ ⊢ F] to S4 [Γ ⊢ G] (written infix) is defined by M ⋆_{−1}N ˆ=MN, ⋆_{q} ˆ=□^{q+1}⋆_{−1}.

Lemma 39. For every substitutive function f from [Γ ⊢ F_{1}] × … × [Γ ⊢ F_{n}] to [Γ ⊢ F], the family of functions (□^{q+1}f)_{q⩾−1} is an a.s. map from S4 [Γ ⊢ F_{1}]×…× S4 [Γ ⊢ F_{n}] to S4 [Γ ⊢ F].

Proof. Write f_{q} for □^{q+1}f. Recall (Lemma 17) that, as soon as f is substitutive, then □f ∘ □g = □(f ∘ g).

Let M_{1} ∈ S4 [Γ ⊢ F_{1}]_{q}, …, M_{n} ∈ S4 [Γ ⊢ F_{n}]_{q}. For any i with 0 ⩽ i ⩽ q, ∂_{q}^{i}(f_{q}(M_{1}, …, M_{n})) = □^{i}d(□^{q+1}f(M_{1}, …, M_{n})) = □^{i}(d ∘ □^{q+1−i}f)(M_{1}, …, M_{n}). So ∂_{q}^{i} ∘ f_{q} = □^{i}(d ∘ □^{q+1−i}f). But

d(□^{q+1−i}f(N_{1}, …, N_{n})) = d □^{q−i}f(dx_{1}, …, dx_{n}) · {x_{1} := N_{1}, …, x_{n} := N_{n}}
≈ □^{q−i}f(dx_{1}, …, dx_{n}){x_{1} := N_{1}, …, x_{n} := N_{n}}
= □^{q−i}f(dN_{1}, …, dN_{n}) (since f is substitutive)

so d ∘ □^{q+1−i}f = □^{q−i}f ∘ d. Therefore ∂_{q}^{i} ∘ f_{q} = □^{i}(d ∘ □^{q+1−i}f) = □^{i}(□^{q−i}f ∘ d) = □^{q}f ∘ □^{i}d = f_{q−1} ∘ ∂_{q}^{i} (using the fact that □^{q−i}f is substitutive).

Similarly, we claim that s_{q}^{0}(□^{k+1}f(N_{1}, …, N_{n})) ≈ □^{k+2}f(s_{q}^{0}N_{1}, …, s_{q}^{0}N_{n}). It will follow that s_{q}^{i} ∘ f_{q} = f_{q+1} ∘ s_{q}^{i}. The claim is proved by induction on k ⩾ 0. If k = 0, then

s_{q}^{0}(□f(N_{1}, …, N_{n})) = x · {x := f(dy_{1}, …, dy_{n}) · {y_{1} := N_{1}, …, y_{n} := N_{n}}}
≈ f(dy_{1}, …, dy_{n}) · {y_{1} := N_{1}, …, y_{n} := N_{n}}

while

□^{2}f(s_{q}^{0}N_{1}, …, s_{q}^{0}N_{n})
= □f(dx_{1}, …, dx_{n}) · {x_{1} := s_{q}^{0}N_{1}, …, x_{n} := s_{q}^{0}N_{n}}
= f(dz_{1}, …, dz_{n}) · {z_{1} := dx_{1}, …, z_{n} := dx_{n}}

{x_{1} := y_{1} · {y_{1} := N_{1}}, …, x_{n} := y_{n} · {y_{n} := N_{n}}}

≈ f(dz_{1}, …, dz_{n}) · {z_{1} := d y_{1} , …, z_{n} := d y_{n} } · {y_{1} := N_{1}, …, y_{n} := N_{n}}
≈ f(dz_{1}, …, dz_{n}) · {z_{1} := y_{1}, …, z_{n} := y_{n}} · {y_{1} := N_{1}, …, y_{n} := N_{n}}
= f(dy_{1}, …, dy_{n}) · {y_{1} := N_{1}, …, y_{n} := N_{n}}  (by α-renaming)

In the inductive case, s_{q}^{0}(□^{k+1}f(N_{1}, …, N_{n})) = s_{q}^{0}(□(□^{k}f)(N_{1}, …, N_{n})) ≈ □^{2}(□^{k}f)(s_{q}^{0}N_{1}, …, s_{q}^{0}N_{n}) (by the above, replacing f by □^{k}f) = □^{k+2}f(s_{q}^{0}N_{1}, …, s_{q}^{0}N_{n}), as desired.

Corollary 40. The syntactic application map ⋆ is an a.s. map.

The following shows how we may compute ⋆:

Lemma 41. Let M ∈ S4 [Γ ⊢ F ⊃ G]_{q}, N ∈ S4 [Γ ⊢ F]_{q} be η-long normal:

M ˆ= … M_{1} · θ_{q} . . . · θ_{1} · θ_{0}

N ˆ= … N_{1} · θ′_{q} . . . · θ′_{1} · θ′_{0}

Then, provided dom θ_{i} ∩ dom θ′_{i} = ∅ for every i, 0 ⩽ i ⩽ q,

M ⋆_{q} N ≈ … M_{1}N_{1} · (θ_{q}, θ′_{q}) . . . · (θ_{1}, θ′_{1}) · (θ_{0}, θ′_{0})

Proof. This is clear if q = −1. If q = 0, M ⋆_{0} N = M_{1}N_{1} · (θ_{0}, θ′_{0}) by Lemma 19. Otherwise, this follows by the q = 0 case, using Theorem 30.

¿From Corollary 40, it follows that application is uniquely determined by its values on components (simplices of dimension −1) and points (dimension 0). It also follows that Λ(⋆) is an a.s. map from S4 [Γ ⊢ F ⊃ G] to HomΔ̂(S4 [Γ ⊢ F], S4 [Γ ⊢ G]).

There is a kind of converse to syntactic application. Intuitively, in the λ-calculus (the non-modal case), not only can you apply a term M to a term N, you can also build λx · M from M: this term λx · M is such that, once applied to N, you get M{x := N}. We can do almost the same thing here, except M has to be in some plane for this to work.

Proposition 42. For any 0-simplex P in any a.s. set, define (P)_{q} by

(P)_{−1} ˆ=∂_{0}^{0}P  (P)_{0} ˆ=P  (P)_{q+1} ˆ=s_{0} ((P)_{q}) (q ⩾ 0)

Say that a q-simplex M of S4 [Γ, x : □F ⊢ G] is abstractable on x if and only if π_{0}M can be written as M_{0}{y := dx} for some term M_{0} such that Γ, y : F ⊢ M_{0} : G is typable (in particular, x is not free in M_{0}), and M is in the plane (x : □F)^{⊥} of S4 [Γ, x : □F ⊢ G].

Then there is an a.s. map from the sub-a.s. set of terms M in S4 [Γ, x : □F ⊢ G] that are abstractable on x to terms λx^{q} · M, such that (λx^{q} · M) ⋆^{q} (x)_{q} ≈ M.

Proof. Note that in syntactic a.s. sets as studied here, we may define (P)_{q} more

synthetically as … dP …, where dP is enclosed in q + 1 boxes.

Case q = 0. Let us define λx^{q} · M when q = 0. Write the η-long normal form of M as M_{1} · θ. Since M is in (x : □F)^{⊥}, for every free variable z of M_{1} such that x is free in zθ, zθ = x. Let x_{1}, …, x_{k} be those free variables of M_{1} such that x_{1}θ = … = x_{k}θ = x. The restriction θ^{∗} of θ to the remaining variables maps variables to terms where x is not free.

Moreover, by assumption M_{1}θ = M_{0}{y := dx}, so x only occurs as direct argument of d in M_{1}θ. By the definition of x_{1}, …, x_{k}, there is a term M_{2}, obtained from M_{1} by replacing each dx_{i} by y, such that M_{2}θ^{∗} = M_{0}. Moreover, by construction M_{2} is η-long normal of type G under Γ, y : F, so:

λx^{0} · M ˆ= λy · M_{2} · θ^{∗}  (15)

is a 0-simplex of the desired type. This is also η-long normal since fv(λy · M_{2}) = fv(M_{2}) \ {y} = (fv(M_{1}) \ {x_{1}, …, x_{k}} ∪ {y}) \ {y} = fv(M_{1}) \ {x_{1}, …, x_{k}} = dom θ \ {x_{1}, …, x_{k}} = dom θ^{∗}, and λy · M_{2} is linear since every free variable in M_{2} except possibly y occurs exactly once.

We check that (λx^{0} · M) ⋆^{0} (x)^{0} ≈ M:

(λx^{0} · M) ⋆^{0} (x)_{0} = dz(dz′) · {z := λx^{0} · M, z′ := (x)_{0}}
≈ d λy · M_{2} (d dx ) · (θ^{∗}, {x := x})  (by ( □ ))
≈ (λy · M_{2})(dx) · (θ^{∗}, {x := x})  (by (d))
≈ M_{2}{y := dx} · (θ^{∗}, {x := x})  (by (β))
≈ M_{1} · (θ^{∗}, {x_{1} := x, …, x_{k} := x})  (by (ctr))
= M_{1} · θ = M

General Case. To extend λx^{q} · M to q = −1, use Proposition 32. To extend this to q ⩾ 1, check that M ↦ λx^{0} · M is ⇾^{∗}-monotonic and use Theorem 30. Assume indeed M ⇾^{=} M′ are 0-simplices, where M ˆ= M_{1} · θ and M′ ˆ= M′_{1} · θ′.

Then there is a 1-simplex N · ϑ_{1} · ϑ_{0} such that Nϑ_{1} = M_{1}, ϑ_{0} = θ, and N = M′_{1}, ϑ_{1} ·ϑ_{0} = θ′. In other words, there is a 1-simplex M′_{1} · ϑ_{1} ·θ such that M′_{1}ϑ_{1} = M_{1}

and ϑ_{1} · θ = θ′.

Since M is in (x : □F)^{⊥}, let x_{1}, …, x_{k} be the free variables of M_{1} such that x_{i}θ = x, 1 ⩽ i ⩽ k, as above. Similarly, let x′_{1}, …, x′_{k′} be the free variables of M′_{1} such that x′_{i′}θ′ = x, 1 ⩽ i′ ⩽ k′.

Observe that for every i′ with 1 ⩽ i′ ⩽ k′, x′_{i′}ϑ_{1} is such that (x′_{i′}ϑ_{1})θ = x′_{i′}ϑ_{1}θ = x′_{i′}θ′ = x, so: (a) x′_{i′}ϑ_{1} is some x_{i}, 1 ⩽ i ⩽ k. Conversely, if x_{i} is free in some z′ϑ_{1}, z′ ∈ dom ϑ_{1}, then x is free in z′ϑ_{1}θ = z′θ′, so z′ is some x′_{i′}. In brief: (b) if x_{i} ∈ fv(z′ϑ_{1}), z′ ∈ dom ϑ_{1}, then z′ = x′_{i′} for some i′. So we may write ϑ_{1} as the disjoint union of the restriction ϑ_{1}^{∗} of ϑ_{1} to dom ϑ_{1} \ {x′_{1}, …, x′_{k′}} with a one-to-one (by (b)) substitution mapping each x′_{i′} to some x_{i} (by (a)). In particular, k′ = k and without loss of generality, we may assume x′_{i}ϑ_{1} = x_{i} for every i, 1 ⩽ i ⩽ k. Moreover, by (b) no x_{i} is free in any z′ϑ_{1}^{∗}, z′ ∈ dom ϑ_{1}^{∗}.

Let θ^{∗} be the restriction of θ to fv(M_{1})\{x_{1}, …, x_{k}}, θ′^{∗} be that of θ′ to fv(M′_{1})\ {x′_{1}, …, x′_{k}}. Let M_{2} be obtained from M_{1} by replacing each dx_{i} by y, and M′_{2} be obtained from M′_{1} by replacing each dx′_{i} by y. Finally, let

P ˆ= λy · M′_{2} · ϑ_{1}^{∗} · θ^{∗}

We first claim that P is a valid 1-simplex. Indeed, λy · M′_{2} is linear; fv(λy · M′_{2}) =

fv(M′_{2}) \ {y} = fv(M′_{1}) \ {x′_{1}, …, x′_{k}} = dom ϑ_{1} \ {x′_{1}, …, x′_{k}} = dom ϑ_{1}^{∗}; λy · M′_{2} ·

ϑ_{1}^{∗} is linear, since M′_{1} · ϑ_{1} is; and fv ( λy · M′_{2} · ϑ_{1}^{∗}) = ⋃_{z′∈fv(λy·M′_{2})} fv(z′ϑ_{1}^{∗}) =

⋃_{z′∈fv(M′_{1})\{x′_{1},...,x′_{k}}} fv(z′ϑ_{1}^{∗}) = ⋃_{z′∈fv(M′_{1})} fv(z′ϑ_{1}) \ {x_{1}, …, x_{k}} (since ϑ_{1} is ϑ_{1}^{∗} ⊎

{x′_{1} := x_{1}, …, x′_{k} := x_{k}} and no x_{i} is free in any z′ϑ_{1}^{∗}) = fv ( M′_{1} · ϑ_{1})\{x_{1}, …, x_{k}}

= dom θ \ {x_{1}, …, x_{k}} = dom θ^{∗}.

We then claim that ∂_{1}^{1}P = λx^{0} · M and ∂_{1}^{0}P = λx^{0} · M′.

For the first claim, notice that M′_{2}ϑ_{1}^{∗} is obtained from M′_{1}ϑ_{1}^{∗} by replacing each dx′_{i} by y, so M′_{2}ϑ_{1} is obtained from M′_{1}ϑ_{1} by replacing each dx_{i} by y. Since M′_{1}ϑ_{1} = M_{1} and M_{2} is obtained by replacing each dx_{i} in M_{1} by y, it follows that M′_{2}ϑ_{1} = M_{2}.

Therefore ∂_{1}^{1}P = (λy · M′_{2})ϑ_{1}^{∗} · θ^{∗} = λy · M′_{2}ϑ_{1} · θ^{∗} = λy · M_{2} · θ^{∗} = λx^{0} · M.

For the second claim, since ϑ_{1} · θ = θ′ and ϑ_{1} = ϑ_{1}^{∗} ⊎ {x′_{1} := x_{1}, …, x′_{k} := x_{k}}, θ = θ^{∗} ⊎ {x_{1} := x, …, x_{k} := x}, θ′ = θ′^{∗} ⊎ {x′_{1} := x, …, x′_{k} := x}, and no x_{i} is free in any z′ϑ_{1}^{∗}, z′ ∈ dom ϑ_{1}^{∗}, it follows that ϑ_{1}^{∗} · θ^{∗} ⊎ {x_{1} := x, …, x_{k} := x} =

θ′^{∗} ⊎ {x_{1} := x, …, x_{k} := x}, whence ϑ_{1}^{∗} · θ^{∗} = θ′^{∗}. So ∂_{1}^{0}P = λy · M′_{2} · (ϑ_{1}^{∗} · θ^{∗}) =

λy · M′_{2} · θ′^{∗} = λx^{0} · M′.

Therefore M ⇾^{=} M′. It follows that M ↦ λx^{0} · M is indeed ⇾^{∗}-monotonic, hence extends to a unique a.s. map in every dimension.

It can be shown that Λ(⋆)_{q} is injective for every q, and we leave this to the reader. But we can say more, at the price of considering slightly looser a.s. sets:

Definition 43 (S4 [F]). Let (S4 [F])_{q}, q ⩾ −1, be the set of all ≈-equivalence classes of λ_{S4}-terms M such that Γ ⊢ M : □^{q+1}F is derivable for some boxed context Γ. This gives rise to an a.s. set S4 [F] ˆ=((S4 [F])_{q⩾−1}, (∂_{q}^{i})_{0⩽i⩽q}, (s_{q}^{i})_{0⩽i⩽q})

Then, the ⋆ map extends naturally to an a.s. map, written ∗, from S4 [F ⊃ G] × S4 [F] to S4 [G].

Note that we have defined simplices as typable λ_{S4}-terms, not typing derivations. The difference can be illustrated as follows: the variable x for instance is one λ_{S4}- term, while all typing derivations of Γ, x : F ⊢ x : F by (Ax) when Γ varies are all distinct. This will be made clearer, using categorical language, in Proposition 67.

The injectivity of Λ(∗) yields an embedding of S4 [F ⊃ G] into HomΔ̂(S4 [F], S4 [G]). We shall show that this can be turned into the inclusion part of a strong retraction of HomΔ̂(S4 [F], S4 [G]) onto S4 [F ⊃ G]. First, we note some general results:

Definition 44 (Hull). Let K be an a.s. set, and A ⊆ K_{−1}. The hull \overline{A} is the a.s. subset of K whose q-simplices are all q-simplices x of K such that π_{0}x ∈ A.

This inherits face and degeneracy operators from K. Every a.s. set splits as a sum of hulls:

Proposition 45. Every a.s. set K splits as a sum ∐_{x∈K_{−1}} \overline{\{x\}}. In particular, for every A ⊆ K_{−1}, K = \overline{A} ⨿ \overline{(K_{−1} \ A)}.

The following lemma is the first one where the change from S4 [Γ ⊢ F] to S4 [F] is required:

Lemma 46. Let A be any subset of S4 [F]_{−1}, and assume that there is a 0-simplex P in \overline{A}.

Then there is a strong retraction r_{A} of S4 [F] onto \overline{A}. In other words, r_{A} is an a.s. map such that, for every M ∈ \overline{A}, r_{A}(M) = M.

Proof. For any q-simplex M of S4 [F], then either M is in (\overline{A})_{q} and we let r_{A}(M)

be M, or M is in (\overline{S4 [F]_{−1} \ A})_{q} by Proposition 45, and we let r_{A}(M) be (P)_{q} ∈

S4 [F]_{q}. Note that r_{A}(M) is always in the hull of A.

Clearly, for every M ∈ \overline{A}, r_{A}(M) = M. It remains to show that r_{A} is a.s. If M is in (\overline{A})_{q}, and 0 ⩽ i ⩽ q, then ∂_{q}^{i}M is in (\overline{A})_{q−1}, so ∂_{q}^{i}(r_{A}(M)) = ∂_{q}^{i}M =

r_{A}(∂_{q}^{i}M). Otherwise M is in (\overline{S4 [F]_{−1} \ A})_{q}, so ∂_{q}^{i}M is in (\overline{S4 [F]_{−1} \ A})_{q−1}, there-

fore ∂_{q}^{i}(r_{A}(M)) = ∂_{q}^{i}(P)_{q} ≈ (P)_{q−1} = r_{A}(∂_{q}^{i}M). Similarly for s_{q}^{i}.

Proposition 47. S4 [F ⊃ G] is a strong retract of \overline{Im Λ(∗)_{−1}}.

More precisely, there is an a.s. map ℜ_{F ⊃G}^{1} from \overline{Im Λ(∗)_{−1}} to S4 [F ⊃ G] such that ℜ_{F ⊃G}^{1} ∘ Λ(∗) = id_{S4 [F ⊃G]}.

Proof. For every boxed context Γ, fix some variable ξ_{Γ} outside the domain of Γ.

Let f be any q-simplex of \overline{Im Λ(∗)_{−1}}. That is, first, f ∈ HomΔ̂(S4 [F], S4 [G])_{q}, and π_{0}f = Λ(∗)_{−1}(M) for some term M and some boxed context Γ such that Γ ⊢_{I} M : F ⊃ G is derivable in BN_{0}. Since M is η-long normal of type F ⊃ G, M must be of the form λy · M_{1}, with Γ, y : F ⊢_{I} M_{1} : G derivable in BN_{0}. To sum up:

Λ(∗)_{−1}(λy · M_{1}) = π_{0}f  (16)

Now App_{q}(f, (ξ_{Γ})_{q}) is a q-simplex of S4 [G]. Its component is π_{0}(App_{q}(f, (ξ_{Γ})_{q})), which equals App_{−1}(π_{0}f, dξ_{Γ}) = App_{−1}(Λ(∗)_{−1}(λy · M_{1}), dξ_{Γ}) (by (16)) = (λy · M_{1}) ∗_{−1} dξ_{Γ} (by the combinator equations, in particular (l)) = (λy · M_{1})(dξ_{Γ}) ≈ M_{1}{y := dξ_{Γ}}.

As far as typing is concerned, since Γ, y : F ⊢_{I} M_{1} : G is derivable in BN_{0}, Γ, ξ_{Γ} : □F ⊢ M_{1}{y := dξ_{Γ}} is, too. So π_{0}(App_{q}(f, (ξ_{Γ})_{q})) is in S4 [Γ, ξ_{Γ} : □F ⊢ G]_{−1}, from which it follows that App_{q}(f, (ξ_{Γ})_{q}) is in S4 [Γ, ξ_{Γ} : □F ⊢ G]_{q}.

Using Proposition 37, let M′ ˆ=π_{(ξ_{Γ}:□F)}_{⊥}(App_{q}(f, (ξ_{Γ})_{q})). This is an element of S4 [Γ, ξ_{Γ} : □F ⊢ G]_{q}. Since projection is a.s., it preserves components, so π_{0}(M′) = π_{0}(App_{q}(f, (ξ_{Γ})_{q})) = M_{1}{y := dξ_{Γ}}. By construction M′ is in (ξ_{Γ} : □F)^{⊥}, so M′ = π_{(ξ_{Γ}:□F)}_{⊥}(App_{q}(f, (ξ_{Γ})_{q})) is abstractable on ξ_{Γ}. We may therefore use Proposition 42, and let:

ℜ_{F ⊃G}^{1}(f) ˆ=λ^{q}ξ_{Γ} · π_{(ξ_{Γ}:□F)}_{⊥}(App_{q}(f, (ξ_{Γ})_{q}))  (17)

This is clearly a.s., as a composition of a.s. maps.

Check that ℜ_{F ⊃G}^{1} is a left inverse to Λ(∗). It is enough to check this in dimension 0, by Theorem 30 and Proposition 32, since ℜ_{F ⊃G}^{1} is a.s. So let f be any 0-simplex in Im(Λ(∗)_{0}), i.e., f = Λ(∗)_{0}(P) with P ∈ S4 [F ⊃ G]_{0}. Write P in a unique way as the η-long normal form λy · P_{1} · θ. Then:

ℜ_{F ⊃G}^{1}(f) = λ^{0}ξ_{Γ} · π_{(ξ_{Γ}:□F)}_{⊥}(App_{0}(f, (ξ_{Γ})_{0}))
= λ^{0}ξ_{Γ} · π_{(ξ_{Γ}:□F)}_{⊥}(P ∗_{0} (ξ_{Γ})_{0})
= λ^{0}ξ_{Γ} · π_{(ξ_{Γ}:□F)}_{⊥}( P_{1}{y := dξ_{Γ}} · θ)
= λ^{0}ξ_{Γ} · P_{1}{y := dξ_{Γ}} · θ (since P_{1}{y := dξ_{Γ}} · θ is in (ξ_{Γ} : □F)^{⊥})
= λy · P_{1} · θ (by (15))
= P

where for readability we have not converted P_{1}{y := dξ_{Γ}} · θ to its η-long normal form as we ought to (P_{1}{y := dξ_{Γ}} is in general not linear in ξ_{Γ}).

Combining Lemma 46 with A ˆ= Im(Λ(∗)_{−1}) and Proposition 47, we get:

Corollary 48 (Strong Functional Retraction). S4 [F ⊃ G] is a strong retract of the a.s. set HomΔ̂(S4 [F], S4 [G]): there is an augmented simplicial map ℜ_{F ⊃G} from HomΔ̂(S4 [F], S4 [G]) to S4 [F ⊃ G] such that ℜ_{F ⊃G} ∘ Λ(∗) = id_{S4 [F ⊃G]}.

Proof. Take ℜ_{F ⊃G} as ℜ_{F ⊃G}^{1}∘r_{Im(Λ(∗)_{−1})}. Lemma 46 applies because there is indeed a 0-simplex in \overline{Im(Λ(∗)_{−1})}, e.g., Λ(∗)_{0}(x), where x : □(F ⊃ G) ⊢ x : □(F ⊃ G), so x ∈ S4 [x : □(F ⊃ G) ⊢ F ⊃ G]_{0} ⊆ S4 [F ⊃ G]_{0}.

5. Augmented Simplicial and Other Models

There is a natural interpretation of (non-modal) types and typed λ-terms in the category Set of sets and total functions. Interpret base types as sets, interpret F ⊃ G as the set of all total functions from F to G. Then λ-terms, or more precisely derivations of x_{1} : F_{1}, …, x_{n} : F_{n} ⊢ M : F, are interpreted as total functions from F_{1} × … × F_{n} to F. The variable x_{i} gets interpreted as the ith projection, application of M to N is interpreted as the function mapping g ∈ F_{1} × … × F_{n} to M(g)(N(g)), and abstraction λx·M : F ⊃ G is interpreted as the function mapping g ∈ F_{1} × … × F_{n} to the function mapping x ∈ F to M(g, x) (currying). This is arguably the intended semantics of λ-terms.

In particular, if M and N are convertible λ-terms by the (β) and (η) rules (they are βη-equivalent), then they have the same interpretation. However, this interpretation is far from being onto: note that there are only countably many λterms, while as soon as some base type A gets interpreted as an infinite set, A ⊃ A will not be countable, and (A ⊃ A) ⊃ A will neither be countable nor even of the cardinality of the powerset of ℕ.

Nonetheless, it can be proved that this interpretation is equationally complete:

Theorem 49 ([16]). If the two typed λ-terms M and N, of the same type F, have the same set-theoretic interpretation for every choice of the interpretation of base types, then M and N are βη-equivalent.

In fact, there is even a fixed set-theoretic interpretation such that, if M and N have the same value in this interpretation, then they are βη-equivalent. Extending this result to the modal case will be the topic of Section 5.3 and subsequent ones.

5.1. The (□, d, s) Comonad on Δ̂, and Strict CS4 Categories

In the S4 case, given the fact that S4 [Γ ⊢ F] is an augmented simplicial set, it is natural to investigate the extension of the above constructions to intuitionistic S4 on the one hand and the category of augmented simplicial sets on the other hand.

In general, intuitionistic S4 proofs can be interpreted in any CCC with a monoidal comonad. While the CCC structure of Δ̂, accounting for the non-modal part of S4 proofs, was recalled in Section 4, the monoidal comonad we use is:

Definition 50 (□ Comonad in Δ̂). For every a.s. set K, let □K denote the a.s. set such that (□K)_{q} ˆ=K_{q+1}, ∂_{(□K)_{q}}^{i} ˆ=∂_{K_{q+1}}^{i+1}, s_{(□K)_{q}}^{i} ˆ=s_{K_{q+1}}^{i+1}. For any a.s. map f : K → L, let □f : □K → □L be such that (□f)_{q} ˆ=f_{q+1}. Let d : □K → K and s : □K → □^{2}K be the a.s. maps such that (d)_{q} ˆ=∂_{K_{q+1}}^{0} and (s)_{q} ˆ=s_{K_{q+1}}^{0} respectively, q ⩾ −1.

CCCs with a monoidal comonad have already been argued to be the proper categorical models of intuitionistic S4 [7]. While Bierman and de Paiva only show that (β), (η), and (d) are sound, it is easy to check that the other equalities (gc), (ctr), ( □ ) and (η□) are also sound.

It is also easy to check that the monoidal comonad of Definition 50 satisfies □1 = 1, □(K × L) = □K × □L (up to natural isomorphisms that we will not make explicit, for readability purposes), and the following so-called strict monoidal comonad equations hold:

(n) □id = id (o) □(f ∘ g) = □f ∘ □g (p) d ∘ □f = f ∘ d (q) s ∘ □f = □^{2}f ∘ s
(r) □π_{1} = π_{1} (s) d ∘ s = id (t) □d ∘ s = id (u) □s ∘ s = s ∘ s
(v) □π_{2} = π_{2} (w) □⟨f, g⟩ = ⟨□f, □g⟩ (x) d ∘ ⟨f, g⟩ = ⟨d ∘ f, d ∘ g⟩
(y) s ∘ ⟨f, g⟩ = ⟨s ∘ f, s ∘ g⟩

Definition 51 (Strict CS4 Category). A strict CS4 category is any cartesianclosed category C together with a strict monoidal comonad (□, d, s).

Strict CS4 categories are the categories in which we can interpret typed λ_{S4}- terms. Bierman and de Paiva considered non-strict CS4 categories [7]. We shall only need the strict variant; this will make our exposition simpler. In particular Δ̂ with the comonad of Definition 50 is a strict CS4 category.

The □ functor on Δ̂ is related to Duskin and Illusie’s décalage functor ■ [46]. Standardly, décalage is dual to □. For every a.s. set K, the converse K̆ of K is obtained by letting (K̆)_{q} ˆ=K_{q}, ∂i ; K̆_{q} ˆ=∂_{K_{q}}^{q−i}, si ; K̆_{q} ˆ=s_{K_{q}}^{q−i}. That is, K̆ is obtained from K

by reversing the order of faces. Then ■K is the converse of □K̆. If □K in a sense means “in every future, K”, then it is natural to think of ■K as “in every past, K”. As announced in Section 2, we shall leave the task of investigating such other modalities to a future paper.

5.1.1. Topological Models There are many other interesting strict CS4 Categories. Of interest in topology in the category CGHaus of compactly generated topological spaces, a.k.a., Kelley spaces ([36] VII.8). (It is tempting to use the category Top of topological spaces, however Top is not a CCC. It has sometimes been argued that CGHaus was the right category to do topology in.) Recall that a Kelley space is a Hausdorff topological space X whose closed subsets are exactly those subsets A whose intersection with every compact subspace of X is closed in X. CGHaus has Kelley spaces as objects and continuous functions as morphisms. Moreover, for every Hausdorff space X, there is a smallest topology containing that of X that makes it Kelley. The resulting Kelley space K(X) is the kelleyfication of X, and is obtained by adding as closed sets every A ⊆ X whose intersection with every compact subspace of X is closed in X. The terminal object 1 in CGHaus is the one-point topological space, while the product of X and Y is the kelleyfication of the product of X and Y as topological spaces, and the internal hom Hom_{CGHaus}(X, Y) is the kelleyfication of the space of all continuous functions from X to Y with the compact-open topology. We may equip CGHaus with a structure of strict CS4 category as follows:

Definition 52 (□ Comonad in CGHaus). For every topological space X, the path space □X over X is the disjoint sum ∐_{x_{0}∈X} □_{x_{0}}X, where the □_{x_{0}}X is the space of all continuous functions α from [0, 1] to X such that α(0) = x_{0}, with the compact-open topology.

For every continuous function f : X → Y, let □f : □X → □Y be the function mapping each α ∈ □X to f ∘ α ∈ □Y.

The counit d maps every α ∈ □X to α(1) ∈ X.

The comultiplication s maps every α ∈ □X to the map t ↦ (t′ ↦ α(tt′)) in □^{2}X.

This comonad is in fact related to the décalage functor, through singular simplex and geometric realization functors. The path comonad is more often defined on pointed topological spaces, as □_{x_{0}}X, where x_{0} ∈ X is the point in X; □_{x_{0}}X is itself pointed, and the constant path at x_{0} is its point. This standard path comonad is right-adjoint to the cone comonad, and is fundamental in homotopy and homology, see e.g. [25]. We shall see that our path comonad is also right-adjoint to some cone monad (Proposition 54).

In terms of processes, we may think of α ∈ □X as some process that starts at time 0 and will produce a value at time 1. The counit d is the operator that extracts the final value of the process α as argument.

Proposition 53. The construction (□, d, s) of Definition 52 is a strict monoidal comonad on CGHaus, making it a strict CS4 category.

Proof. First show that □_{x_{0}}X is Kelley. Since [0, 1] is compact, it is locally compact Hausdorff; it is then well-known that the space of continuous functions from [0, 1] to X is Kelley: this is Hom_{CGHaus}([0, 1], X). (In general Hom_{CGHaus}(Y, X) is the kelleyfication of the space of continuous functions from Y to X, not the space itself.) Since {x_{0}} is closed in X, and the projection α ↦ α(0) is continuous, □_{x_{0}}X is closed in Hom_{CGHaus}([0, 1], X). As a closed subset of a Kelley space, □_{x_{0}}X is then Kelley, too. Since every coproduct of Kelley spaces is also Kelley, it follows that □X is Kelley.

Next we must show that □f is continuous whenever f : X → Y is. We first show the auxiliary: Claim A. For every function f : X → □Y, f is continuous if and only if, for every connected component C of X:

(i) for every x, y ∈ C, f(x)(0) = f(y)(0), and (ii) the restriction f_{|C} of f to C is continuous from C to Hom_{CGHaus}([0, 1], Y). Only if: since C is connected, f(C) is connected. But each □_{x_{0}}X is both open and closed in □X by construction, so f(C) ⊆ □_{x_{0}}X for some x_{0} ∈ X. By definition of □_{x_{0}}X, this means that f(x)(0) = x_{0} for every x ∈ C, whence (i). On the other hand, since f is continuous, f_{|C} is also continuous from C to □_{x_{0}}X for the x_{0} above. Since every subset of □_{x_{0}}X that is closed in Hom_{CGHaus}([0, 1], Y) is also closed in □_{x_{0}}X by definition, (ii) holds. (We use the fact that f is continuous if and only if the inverse image of every closed set is closed.)

If: let x_{0} be f(x)(0) for some (and therefore all, by (i)) x ∈ C. Then f(C) ⊆ □_{x_{0}}X. By (ii), and since every closed subset of □_{x_{0}}X is closed in Hom_{CGHaus}([0, 1], Y), f_{|C} is continuous from C to □_{x_{0}}X, hence to □X. For every open O of □X, f^{−1}(O) is the union of f_{|C}^{−1}(O) when C ranges over the connected components of X, and is therefore open. So f is indeed continuous from X to □Y. Claim A is proved.

Now let f : X → Y be continuous; we claim that □f is continuous, too. Let C be a connected component of □X. Since every □_{x_{0}}X is both open and closed in □X, C is included in some □_{x_{0}}X. So for every α, β ∈ C, □f(α)(0) = f(α(0)) = f(x_{0}) = f(β(0)) = □f(β)(0), therefore (i) holds. Moreover f_{|C} is trivially continuous from C to Hom_{CGHaus}([0, 1], Y), since f ∘ is a continuous operation (this is the morphism Λ(f ∘App) in CGHaus, which is a CCC). So Claim A applies, and □f is continuous.

Let us now show that d : □X → X is continuous. Let F be any closed subset of X, then d^{−1}(F) = {α ∈ □X|α(1) ∈ F } = ⋃_{x_{0}∈X}{α ∈ □_{x_{0}}X|α(1) ∈ F } = ⋃_{x_{0}∈X}{α ∈ Hom_{CGHaus}([0, 1], X)|α(0) = x_{0} ∧ α(1) ∈ F }. Since the functions from Hom_{CGHaus}([0, 1], X) to X mapping α to α(0) and α(1) respectively are continuous, each {α ∈ Hom_{CGHaus}([0, 1], X)|α(0) = x_{0} ∧ α(1) ∈ F } is closed in Hom_{CGHaus}([0, 1], X); hence in □_{x_{0}}X. Since a set is closed in a sum space if and only if its intersection with every summand is closed in the summand, d^{−1}(F) is closed.

Let us show that s : □X → □^{2}X is continuous. Let C be any connected component of □X. In particular C ⊆ □_{x_{0}}X for some x_{0}. So for every α ∈ C, α(0) = x_{0}, therefore s(α)(0) is the map t′ ↦ α(0t′), i.e., the constant map t′ ↦ x_{0}. As this is independent of α, (i) holds. On the other hand, let F be any closed subset of Hom_{CGHaus}([0, 1], □X). Then, letting f_{0} be the constant map t′ ↦ x_{0}, s_{|C}^{−1}(F) = s_{|C}^{−1}(F ∩ □_{f_{0}}□X) = s_{|C}^{−1}(F ∩ □_{f_{0}}□_{x_{0}}X) is closed in Hom_{CGHaus}([0, 1], X). Indeed □_{f_{0}}□_{x_{0}}X is closed in Hom_{CGHaus}([0, 1], Hom_{CGHaus}([0, 1], X)), and s_{|C} is continuous from Hom_{CGHaus}([0, 1], X) to Hom_{CGHaus}([0, 1], Hom_{CGHaus}([0, 1], X)), as a composition of continuous maps. So s_{|C}^{−1}(F) is also closed in C, hence (ii) holds. By Claim A s is continuous.

We now claim that □ is strict monoidal. The terminal object ! in CGHaus is any singleton {•}; □{•} is the space of all paths from • to • in {•}, and is therefore also a singleton set. On the other hand, products are slightly harder to deal with. Let X ∗ Y denote the product of X and Y as topological spaces; then X × Y is the kelleyfication of X ∗ Y. We claim that the pair of functions:

F : □(X × Y) → □X × □Y
γ ↦ (π_{1} ∘ γ, π_{2} ∘ γ)
G : □X × □Y → □(X × Y)
(α, β) ↦ (t ↦ (α(t), β(t)))

defines a natural isomorphism between □(X × Y) and □X and □Y. That they are inverse of each other is clear, it remains to show that they are continuous. For F, since × is a product in CGHaus, it is enough to show that γ ↦ π_{1} ∘γ is continuous from □(X × Y) to □X, and similarly for γ ↦ π_{2} ∘ γ. Apply Claim A: let C be any connected component of □(X × Y). Since each □_{(x_{0},y_{0})}(X × Y) is both open and closed in □(X ×Y), C is included in some □_{(x_{0},y_{0})}(X ×Y) for some x_{0} ∈ X, y_{0} ∈ Y. So γ ↦ π_{1} ∘ γ maps any γ ∈ C to some path whose value at 0 is x_{0}, and is therefore independent of γ: (i) holds. And (ii) is obvious, so F is continuous. For G, this is subtler, and we require to prove the following first:

Claim B. Every connected component C of X × Y is a subset of some product A ∗ B, where A is a connected component of X and B a connected component of Y.

Indeed, every connected component of X, resp. Y, is both open and closed in X, resp. Y. So every product A ∗ B is both open and closed in X ∗ Y, when A and B are connected components. Since the topology of X × Y is finer than that of X ∗ Y, A ∗ B is also both open and closed in X × Y. Let S be the set of pairs (A, B) of connected components such that C ∩ (A ∗ B) ≠ ∅. Note that the union of all A ∗ B for (A, B) ∈ S covers C. Since C ∩ (A ∗ B) is both open and closed in S and C is connected, there can be at most one pair A, B of connected components such that C ∩ (A ∗ B) ≠ ∅. It follows that C ⊆ A ∗ B. Claim B is proved.

To show that G is continuous, apply Claim A. For every connected component C of □X×□Y, using Claim B, C is included in some product of connected components of □X and □Y respectively. In particular C ⊆ □_{x_{0}}X ∗ □_{y_{0}}Y for some x_{0} ∈ X, y_{0} ∈ Y. It follows that for every (α, β) ∈ C, G(α, β)(0) = (α(0), β(0)) = (x_{0}, y_{0}) is independent of α and β. So (i) holds. Also, (ii) holds trivially. Therefore G is continuous.

It remains to check equations (n)–(y), which are easy and left to the reader.

We have said that □ was dual to a cone functor. We let the reader check the following, taking ♦X as ([0, 1] × X)/ ↭, where ↭ is the smallest equivalence relation such that (0, x) ↭ (0, y) provided x and y lie in the same connected component of X, and writing |t, x| for the equivalence class of (t, x), ♦f be the function mapping |t, x| to |t, f(x)|, 𝔢 map x to |1, x|, and 𝔪 map |t_{1}, |t_{2}, x|| to |t_{1}t_{2}, x|.

Proposition 54. There is a strong monad (♦, 𝔢, 𝔪) (the cone monad) on the category CGHaus of Kelley spaces such that ♦ ⊣ □.

Recalling the discussion of Section 2, this gives a way of interpreting Moggi’s computational lambda-calculus in labeled Kelley spaces, together with λ_{S4}, and preserving a duality between the □ and ♦ forms of talking about computations and values (the adjunction ♦ ⊣ □). Such a cone monad also exists in Δ̂, but is more complex (it can be built as the join [14] from a one-point a.s. set, for example.)

It is instructive to see that if X is a space of points, □X is a space of paths, then □^{2}X is a space of singular 2-simplices, and in general □^{q}X will be a space of singular q-simplices.

Let’s examine □^{2}X first. This is a space of paths β, such that each β(t), t ∈ [0, 1] is itself a path, so β is a kind of square, up to deformation. However, β is continuous and [0, 1] is connected, so the range of β is connected as well. But the range of β is a subset of □X, which is the direct sum of spaces □_{x_{0}}X, x_{0} ∈ X. In any direct sum of topological spaces, every summand is both open and closed, hence every connected subspace is in fact a subspace of some summand. In our case, this means that the range of β is a subset of some □_{x_{0}}X. In other words, β(t)(0) = x_{0} for every t, so the range of β assumes the shape of a triangle, up to deformation: see Figure 6.

Note that this phenomenon is entirely due to the strange topology we take on □X, which separates completely paths α that do not have the same α(0). Had we just taken □X to be the set of paths in X with the compact-open topology, □^{q}X would have been a set of cubes, not simplices.

Figure 6: Extended singular simplices

In general, define XSing_{q}(X), for q ⩾ −1, as the set of all extended singular q-simplices in X:

Definition 55 (Extended Singular Simplices, XSing). For every q ⩾ −1, the extended singular q-simplices are the continuous maps from Δ^{+}_{q} to F, where Δ^{+}_{q} ˆ={(t_{0}, …, t_{q}) | t_{0} ⩾ 0, …, t_{q} ⩾ 0, t_{0} + … + t_{q} ⩽ 1} is the standard extended q-simplex.

Δ^{+}_{−1} is the singleton containing only the empty tuple (). Otherwise, Δ^{+}_{q} is a polyhedron whose vertices are (0, …, 0) first, and second the points e_{0}, …, e_{q}, where e_{i} ˆ=(t_{0}, …, t_{q}) with t_{i} = 1 and t_{j} = 0 for all j ≠ i. This is analogous to the more usual notion of standard q-simplices Δ_{q}, for q ⩾ 0, which are the subpolyhedra with vertices e_{0}, …, e_{q}, namely Δ_{q} ˆ={(t_{0}, …, t_{q}) | t_{0} ⩾ 0, …, t_{q} ⩾ 0, t_{0} +…+t_{q} = 1}. The singular q-simplices of X are the continuous maps from Δ_{q} to X. See Figure 7 for an illustration of what the standard simplices, and standard extended simplices, look like.

Figure 7: Standard and extended simplices

The topology on XSing_{q}(X) is given as follows. When q = −1, XSing_{q}(X) is isomorphic to X. Otherwise, XSing_{q}(X) is viewed as the topological sum of all spaces XSing_{q}^{γ}(X) ˆ={f ∈ Hom_{CGHaus}(Δ^{+}_{q}, X) | f_{|Δ_{q}} = γ}, when γ ranges over all singular q-simplices of X. We let the interested reader check that XSing_{q}(X) is in fact homeomorphic to □^{q}X.

Note that (extended) simplices over a space of functions X → Y also have an elegant geometric interpretation. While X → Y is a set of continuous functions, □(X → Y) is a set of continuous paths from functions f to functions g in X → Y, so □(X → Y) is a set of homotopies between continuous functions from X to Y. The elements of □^{q}(X → Y), q ⩾ 1, are then known as higher-order homotopies: □^{2}(X → Y) is the set of homotopies between homotopies, etc. This is a classical construction in algebraic topology [39].

In terms of proof theory, there is a translation of intuitionistic proofs to S4 proofs which replaces every base type A by □A and every implication by a corresponding boxed implication. At the level of proof terms, this yields the SKInT calculus of [19], which interprets (slightly more than) Plotkin’s call-by-value λ-calculus [45]. The present constructions give rise to a model in terms of paths (elements of base types) and homotopies (implications) for SKInT. This is left to the reader.

5.1.2. Models in Categories of Orders, Cpos, and Categories More cogent to computer science are models of the λ-calculus based on complete partial orders. Here, too, we may define strict monoidal comonads as follows. First recall that Ord, the category whose objects are partial orders and whose morphisms are monotonic functions, is a CCC. Similarly, Cat, the category of small categories, is a CCC. The category Cpo of complete partial orders (cpos) has cpos as objects and continuous functions as morphisms. Recall that a cpo is any partial order in which every infinite increasing chain x_{0} ⩽ x_{1} ⩽ … ⩽ x_{i} ⩽ … has a least upper bound. (We don’t require our cpos to be pointed, i.e., to have a least element.) A function is continuous provided it preserves all least upper bounds of increasing chains; in particular, a continuous function is monotonic. Again, Cpo is a CCC. A variant is the category DCpo of directed cpos, where it is instead required that all non-empty directed subsets have a least upper bound; a directed subset E is one where any two elements in E have a least upper bound in E. Continuous functions are then required to preserve least upper bounds of all directed sets. Again, DCpo is a CCC.

Definition 56 (□ Comonad in Ord, Cpo, DCpo). For every partial order (X, ⩽), let □X be the set of all pairs (x_{0}, x_{1}) of elements of X such that x_{0} ⩽ x_{1}, ordered by (x_{0}, x_{1}) ⩽ (y_{0}, y_{1}) if and only if x_{0} = y_{0} (not x_{0} ⩽ y_{0}) and x_{1} ⩽ y_{1}. For every monotonic function f : X → Y (resp. continuous), let □f map (x_{0}, x_{1}) to (f(x_{0}), f(x_{1})).

The counit d : □X → X maps (x_{0}, x_{1}) to x_{1}.

The comultiplication s : □X → □^{2}X maps (x_{0}, x_{1}) to ((x_{0}, x_{0}), (x_{0}, x_{1})).

It is easily checked that this defines a strict monoidal comonad on Ord, Cpo, DCpo. As for the topological case, we may give a synthetic description of □^{q}X: this is isomorphic to the partial order (resp. cpo, resp. dcpo) of all chains x_{−1} ⩽ x_{0} ⩽ x_{1} ⩽ … ⩽ x_{q} of elements of X, ordered by:

(x_{−1}, x_{0}, …, x_{q}) ⩽ (x′_{−1}, x′_{0}, …, x′_{q})

if and only if x_{−1} = x′_{−1}, x_{0} = x′_{0}, …, x_{q−1} = x′_{q−1}, and x_{q} ⩽ x′_{q}. Just like iterating □ in the topological case allowed us to retrieve a form of of singular simplex functor, we retrieve a form of nerve functor.

In passing, we invite the reader to check that there is also a cone monad ♦ in Ord, Cpo and DCpo: ♦X is X with a new bottom element added below every connected component of X. (Connected components are the equivalence classes of the symmetric closure of ⩽.) The unit X → ♦X is the natural inclusion of orders. The multiplication ♦^{2}X → ♦X squashes the additional bottoms of ♦^{2}X to the ones just above that come from ♦X. Again, this is a strong monad left adjoint to □; in pointed cpos, this is known as the lifting monad.

We leave it to the reader to check that similar constructions work in Cat: for every small category C, let □C be the category of all morphisms of C; morphisms from X → X_{0} to X → X_{1} are all commuting triangles:

\xymatrix{X \ar[d] \ar[dr] \\ X_{0} \ar[r] & X_{1}}

In short, □C is the coproduct of all coslices over C. The counit is given by: d is the functor mapping X → X_{0} to X_{0}, and the diagram above to the morphism X_{0} → X_{1} in C. Comultiplication maps every object X → X_{0} in C to the obvious

commuting triangle X \overrightarrow{→} X_{0}, and morphisms as given by the triangle above to

commuting tetrahedra:

\xymatrix{X \ar[r] \ar[dr] \ar[d] & X_{1} \\ X_{0} \ar[r]_{id} \ar[ur] & X_{0} \ar[u]}

5.2. Interpreting S4 Proofs into CCCs with Monoidal Comonads

Fix an arbitrary strict CS4 category C, calling its strict monoidal comonad (□, d, s). Our prime example is Δ̂, but we do not restrict to it here. We reuse the CCC notations of Section 4 and the strict monoidal comonad notations of Section 5.1, together with equations (a)–(m) and (n)–(y).

Extend the set-theoretic interpretation of λ-terms to an interpretation of formulas as objects in C, and of terms as morphisms in C; this interpretation is shown in Figure 8. This is parameterized by an environment ρ mapping each base type A ∈ Σ to some object ρ(A). Our notations match standard meaning functions in denotational semantics.

We let X_{1}×…×X_{n} ˆ=(… (1×X_{1})×…×X_{n−1})×X_{n}, and ⟨f_{1}, …, f_{n}⟩ ˆ=⟨⟨… ⟨!, f_{1}⟩ …, f_{n−1}⟩, f_{n}⟩. We actually make an abuse of language by considering that this is an interpretation of typed λ_{S4}-terms instead of of typing derivations.

If Γ is x_{1} : F_{1}, …, x_{n} : F_{n}, we also let C ⟦Γ⟧ ρ be the product C ⟦F_{1}⟧ ρ × … × C ⟦F_{n}⟧ ρ.

C ⟦A⟧ ρ ˆ=ρ(A) C ⟦F ⊃ G⟧ ρ ˆ=Hom_{C}(C ⟦F ⟧ ρ, C ⟦G⟧ ρ) C ⟦□F ⟧ ρ ˆ=□C ⟦F ⟧ρ
C ⟦Γ ⊢ x_{i} : F_{i}⟧ ρ ˆ= π_{2} \overbrace{∘π_{1} ∘ … ∘ π_{1}}^{n−i} where Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}
C ⟦Γ ⊢ MN : G⟧ ρ ˆ= App ∘ ⟨C ⟦Γ ⊢ M : F ⊃ G⟧ ρ, C ⟦Γ ⊢ N : F ⟧ ρ⟩
C ⟦Γ ⊢ λx · M : F ⊃ G⟧ ρ ˆ= Λ(C ⟦Γ, x : F ⊢ M : G⟧ ρ)
C ⟦Γ ⊢ dM : F ⟧ ρ ˆ= d ∘ C ⟦Γ ⊢ M : □F ⟧ ρ
C ⟦Γ ⊢ M · θ : □G⟧ ρ ˆ= □C ⟦Θ ⊢ M : G⟧ ρ ∘ s

∘⟨C ⟦Γ ⊢ N_{1} : □F_{1}⟧ ρ, …, C ⟦Γ ⊢ N_{n} : □F_{n}⟧ ρ⟩

where Θ ˆ=x_{1} : □F_{1}, …, x_{n} : □F_{n},
θ ˆ={x_{1} := N_{1}, …, x_{n} := N_{n}}

Figure 8: Interpreting S4 proof terms

Lemma 57 (Soundness). The interpretation of Figure 8 is sound in every strict CS4 category C: if Γ ⊢ M : F is derivable, then C ⟦M⟧ ρ is a morphism from C ⟦Γ⟧ ρ to C ⟦F ⟧ ρ; and if M ≈ N then C ⟦M⟧ ρ = C ⟦N⟧ ρ.

Proof. The typing part is immediate. For the equality part, standard arguments [10] show that:

C ⟦Γ ⊢ M{x_{1} := N_{1}, …, x_{n} := N_{n}} : F ⟧ ρ  (18)
= C ⟦x_{1} : F_{1}, …, x_{n} : F_{n} ⊢ M : F ⟧ ρ
∘⟨C ⟦Γ ⊢ N_{1} : F_{1}⟧ ρ, …, C ⟦Γ ⊢ N_{n} : F_{n}⟧ ρ⟩

where the indicated sequents are derivable; and that:

C ⟦Γ, x : F ⊢ M : G⟧ ρ = C ⟦Γ ⊢ M : G⟧ ρ ∘ π_{1}

if x is not free in M. By standard but tedious calculations, we then check that if M → N then C ⟦M⟧ ρ = C ⟦N⟧ ρ, which entails the second claim.

If we are allowed to vary the strict CS4 category C, then there are converses to Lemma 57. The idea is that we can always define a syntactic category C as follows:

Definition 58 (S4_{Σ} Category). Let S4_{Σ} be the category whose objects are contexts mapping variables to types built on the set Σ of base types, and whose morphisms are:

Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n} \overline{\begin{matrix}θ ˆ=\{y_{1} := M_{1}, …, y_{m} := M_{m}\} \\ ≻ \end{matrix}} Θ ˆ=y_{1} : G_{1}, …, y_{m} : G_{m}

where θ is a substitution such that Γ ⊢ M_{j} : G_{j} for every j, 1 ⩽ j ⩽ m, modulo ≈.

The identity on Γ is the identity substitution id_{Γ} ˆ={x_{1} := x_{1}, …, x_{n} := x_{n}}, and composition θ ∘ θ′ is substitution concatenation θ · θ′.

This is a CCC with a strict monoidal comonad. The terminal object 1 is the empty context, and the unique morphism Γ⟶^{!}1 is the empty substitution. To define products, notice that contexts are isomorphic up to renaming of variables. In other words, x_{1} : F_{1}, …, x_{n} : F_{n} is isomorphic to x′_{1} : F_{1}, …, x′_{n} : F_{n}. This allows us to only define Γ × Γ′ when Γ and Γ′ have disjoint domains. Then Γ × Γ′ is the concatenation Γ, Γ′ of contexts, and for any Θ⟶^{θ}Γ and Θ⟶^{θ}Γ′, ⟨θ, θ′⟩ is the morphism (θ, θ′). Projections are restrictions:

\begin{matrix}Γ × Γ′ & \overline{π_{1} ˆ=\{x_{1} := x_{1}, …, x_{n} := x_{n}\} ≻} & Γ \\ Γ × Γ′ & \overline{π_{2} ˆ=\{x′_{1} := x′_{1}, …, x′_{n′} := x′_{n′}\} ≻} & Γ′ \end{matrix}

Given that Γ = x_{1} : F_{1}, …, x_{n} : F_{n} and Γ′ = x′_{1} : F′_{1}, …, x′_{n′} : F′_{n′}, the internal hom object Hom_{S4_{Σ}}(Γ, Γ′) is the context z_{1} : F_{1} ⊃ … ⊃ F_{n} ⊃ F′_{1}, …, z_{n′} :

F_{1} ⊃ … ⊃ F_{n} ⊃ F′_{n′}. Application Hom_{S4_{Σ}}(Γ, Γ′) × Γ⟶^{App}Γ′ is built from syntactic application, as {x′_{1} := z_{1}x_{1} … x_{n}, …, x′_{n′} := z_{n′}x_{1} … x_{n}}, while abstraction is built from λ-abstraction as follows. For every Θ × Γ⟶^{θ}Γ′, where Γ and Γ′ are as above, and Θ ˆ=y_{1} : G_{1}, …, y_{m} : G_{m},

Θ  \overline{\begin{aligned}\{ & z_{1} := λx_{1}, …, x_{n} · x′_{1}θ, \\ & …, \\ & z_{n′} := λx_{1}, …, x_{n} · x′_{n′}θ & \} \end{aligned}≻} Hom_{S4_{Σ}}(Γ, Γ′)

This only uses the non-modal part of S4, and in particular only the computation rules (β) and (η).

The strict monoidal comonad (□, d, s) on S4_{Σ} is defined using the S4 □ modality: on objects, □(x_{1} : F_{1}, …, x_{n} : F_{n}) is defined as x_{1} : □F_{1}, …, x_{n} : □F_{n}; on morphisms, for any θ as given in Definition 58, □θ is:

□Γ \overline{□θ ˆ=\{y_{1} := □M_{1}, …, y_{m} := □M_{m}\} ≻} □Θ

where □M is M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} for any M such that Γ ⊢ M : G is

derivable. The counit d is:

□Γ \overline{d ˆ=\{x_{1} := dx_{1}, …, x_{n} := dx_{n}\}≻} Γ

while comultiplication is:

□Γ \overline{\begin{matrix}s ˆ=\{x_{1} := sx_{1}, …, x_{n} := sx_{n}\} \\ ≻ \end{matrix}} □^{2}Γ

Recall that sM is x · {x := M}. It trivially follows:

Proposition 59 (Existential Completeness). Let ρ map every base type A ∈ Σ to the context z : A. If there is a morphism from S4_{Σ} ⟦Γ⟧ ρ to S4_{Σ} ⟦F ⟧ ρ in S4_{Σ} then F is provable from Γ, i.e., there is a λ_{S4}-term M such that Γ ⊢ M : F is derivable.

Proposition 60 (Evaluation Functor). For every strict CS4 category C, and every ρ : Σ → C, C ⟦ ⟧ ρ extends ρ to a representation of strict CS4 categories from S4_{Σ} to C.

Proof. For every morphism define C ⟦θ⟧ ρ as ⟨C ⟦Γ ⊢ M_{1} : G_{1}⟧ ρ, …, C ⟦Γ ⊢ M_{m} : G_{m}⟧ ρ⟩. This is functorial: indeed C ⟦id_{Γ}⟧ ρ = ⟨π_{2} ∘ π_{1}^{m−1}, …, π_{2} ∘ π_{1}, π_{2}⟩ = id, and C ⟦ ⟧ ρ preserves composition by (18). This preserves cartesian products by construction.

Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}  \overline{θ ˆ=\{y_{1} := M_{1}, …, y_{m} := M_{m}\} ≻} y_{1} : G_{1}, …, y_{m} : G_{m}

This preserves □. Indeed,

C ⟦□Γ ⊢ □M : □F ⟧ ρ
= C ⟦□Γ ⊢ M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} : □F ⟧ ρ
= □C ⟦Γ ⊢ M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} : F ⟧ ρ
∘s ∘ ⟨π_{2} ∘ π_{1}^{m−1}, …, π_{2} ∘ π_{1}, s ∘ π_{2}⟩
= □C ⟦Γ ⊢ M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} : F ⟧ ρ ∘ s
= □ (C ⟦Γ ⊢ M : F ⟧ ρ ∘ ⟨d ∘ π_{2} ∘ π_{1}^{m−1}, …, d ∘ π_{2} ∘ π_{1}, d ∘ π_{2}⟩) ∘ s
= □(C ⟦Γ ⊢ M : F ⟧ ρ ∘ d) ∘ s
= □C ⟦Γ ⊢ M : F ⟧ ρ ∘ □d ∘ s = □C ⟦Γ ⊢ M : F ⟧ ρ (by (t))

So:

C ⟦□θ⟧ ρ = ⟨C ⟦□Γ ⊢ □M_{1} : □G_{1}⟧ ρ, …, C ⟦□Γ ⊢ □M_{m}⟧ ρ⟩
= ⟨□C ⟦Γ ⊢ M_{1} : G_{1}⟧ ρ, …, □C ⟦Γ ⊢ M_{m} : G_{m}⟧ ρ⟩
= □C ⟦θ⟧ ρ (by (w))

C ⟦ ⟧ ρ preserves d:

C ⟦d⟧ ρ = ⟨C ⟦□Γ ⊢ dx_{1} : F_{1}⟧ ρ, …, C ⟦□Γ ⊢ dx_{n} : F_{n}⟧ ρ⟩
= ⟨d ∘ π_{2} ∘ π_{1}^{n−1}, …, d ∘ π_{2} ∘ π_{1}, d ∘ π_{2}⟩
= d ∘ ⟨π_{2} ∘ π_{1}^{n−1}, …, π_{2} ∘ π_{1}, π_{2}⟩ = d

C ⟦ ⟧ ρ preserves s. Indeed,

C ⟦Γ ⊢ sM : □^{2}F ⟧ ρ = C ⟦Γ ⊢ x · {x := M} : □^{2}F ⟧ ρ
= □C ⟦x : □F ⊢ x : □F ⟧ ρ ∘ s ∘ C ⟦Γ ⊢ M : □F ⟧ ρ
= □id ∘ s ∘ C ⟦Γ ⊢ M : □F ⟧ ρ
= s ∘ C ⟦Γ ⊢ M : □F ⟧ ρ

So:

C ⟦s⟧ ρ = ⟨s ∘ π_{2} ∘ π_{1}^{n−1}, …, s ∘ π_{2} ∘ π_{1}, s ∘ π_{2}⟩
= s ∘ ⟨π_{2} ∘ π_{1}^{n−1}, …, π_{2} ∘ π_{1}, π_{2}⟩ = s

The functor C ⟦ ⟧ ρ also preserves internal homs, application App and abstraction Λ. This is standard, tedious and uninstructive, hence omitted.

Proposition 61 (Free Strict CS4 Category). S4_{Σ} is the free strict CS4 category on Σ.

More precisely, for every set Σ of base types, seen as a discrete category, let ⊆ denote the natural inclusion functor of Σ into S4_{Σ}. Then for every strict CS4 category C, for every functor ρ : Σ → C, there is a unique functor Φ that makes the following diagram commute:

\xymatrix{Σ \ar[r]^{⊆} \ar[d]_{ρ} & S4_{Σ} \ar[dl]^{Φ} \\ C}

Furthermore, Φ is exactly the C ⟦ ⟧ ρ functor as defined in Figure 8.

Proof. Uniqueness: assume Φ exists, we shall show that it is uniquely determined. On objects, Φ must map every formula F to C ⟦F ⟧ ρ, and in general every context Γ to C ⟦Γ⟧ ρ. On morphisms, since Φ must preserve products, Φ is uniquely determined by the images of morphisms in S4_{Σ} of the form

Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}  \overline{\begin{matrix}\{y_{1} := M_{1}, …, y_{m} := M_{m}\} \\ ≻ \end{matrix}} Θ ˆ=y_{1} : G_{1}, …, y_{m} : G_{m}

with m = 1. In this case, equate the morphism with the judgment Γ ⊢ M_{1} : G_{1}. Then Φ is uniquely determined by its values on typed λ_{S4}-terms. (For readability, we make an abuse of language by equating terms with their typing derivations.)

Since Φ must preserve □ and s, we must have:

Φ ( M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} ) = □Φ(M)
Φ ( x · {x := M}) = s ∘ Φ(M)

Since, using ( □ ), (d), and possibly (gc):

M · {x_{1} := N_{1}, …, x_{n} := N_{n}}

≈ ( M{x_{1} := dx_{1}, …, x_{n} := dx_{n}} ) {x_{1} := y_{1} · {y_{1} := N_{1}}, …,

x_{n} := y_{n} · {y_{n} := N_{n}}}

it follows that:

Φ ( M · {x_{1} := N_{1}, …, x_{n} := N_{n}}) = □Φ(M) ∘ s ∘ ⟨Φ(N_{1}), …, Φ(N_{n})⟩

Similarly, since Φ must preserve d, we must have Φ(dM) = d ∘ Φ(M). We recognize the clauses for C ⟦ ⟧ ρ for boxes and d terms given in Figure 8. The case of internal homs, application and abstraction are equally easy and standard, whence Φ must be C ⟦ ⟧ ρ.

Existence: taking Φ ˆ=C ⟦ ⟧ ρ, this is by Lemma 57 and Proposition 60.

Corollary 62. Let ⊆ denote the canonical inclusion Σ ⊆ S4_{Σ}, mapping each base type A to A, seen as a formula. Then S4_{Σ} ⟦Γ ⊢ M : F ⟧ (⊆) ≈ M.

Proof. Apply Proposition 61 with C ˆ=S4_{Σ}, ρ ˆ=(⊆).

Corollary 62 immediately implies:

Proposition 63 (Equational Completeness). Let M, N be two λ_{S4}-terms such that Γ ⊢ M : F and Γ ⊢ N : F are derivable.

If S4_{Σ} ⟦Γ ⊢ M : F ⟧ (⊆) = S4_{Σ} ⟦Γ ⊢ N : F ⟧ (⊆), then M ≈ N.

While S4_{Σ} is characterized as the free strict CS4 category, we end this section by elucidating the construction of the augmented simplicial set S4 [F] of Definition 43 from a categorical point of view. First, we note:

Lemma 64. There is a functor S4 [ ] mapping every formula F to S4 [F], and more generally every context Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n} to S4 [Γ] ˆ=S4 [F_{1}] × … × S4 [F_{n}], and every morphism

Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n} \begin{matrix}θ ˆ=\{y_{1} := M_{1}, …, y_{m} := M_{m}\} \\ ≻ \end{matrix} Θ ˆ=y_{1} : G_{1}, …, y_{m} : G_{m}

to the morphism S4 [θ] in Δ̂ which, as an augmented simplicial map, sends (N_{1}, …, N_{n}) ∈ S4 [Γ]_{q} to (□^{q+1}M_{1}φ, …, □^{q+1}M_{m}φ), where φ ˆ={x_{1} := N_{1}, …, x_{n} := N_{n}}.

Moreover, S4 [ ] is faithful, preserves all finite products and the given comonads in the source and target categories.

Proof. That it is a functor follows from equations (n) and (o). It clearly preserves all finite products and maps the syntactic comonad (□, d, s) to the (dual) décalage comonad (□, d, s) in Δ̂, as an easy check shows. Finally, it is faithful: in the definition of S4 [θ] above, we retrieve θ uniquely from S4 [θ] by looking at the image of the tuple (x_{1}, …, x_{n}) by S4 [θ]_{−1}.

We can give an even more abstract description of S4 [ ] as follows, which is essentially a way of generalizing the familiar hom-set functor Hom_{C}( , ) to the augmented simplicial case. In this way, we shall see that it is related to the standard resolution of any comonad ([36], VII.6):

Definition 65 (Resolution Functor Res). Let (C, □, d, s) be any strict CS4 category. There is a resolution functor Res_{C} : C^{o} × C → Δ̂ which maps every pair A, B of objects in C to the augmented simplicial set ((Hom_{C}(A, □^{q+1}B))_{q⩾−1}, ∂_{q}^{i} ˆ=(□^{i}d ∘

), s_{q}^{i} ˆ=(□^{i}s ∘ )), and every pair of morphisms A′⟶^{f}A, B⟶^{g}B′ to the a.s. map Res_{C}(f, g) given in dimension q ⩾ −1 by Res_{C}(f, g)_{q}(a) ˆ=□^{q+1}g ∘ a ∘ f for every a ∈ Hom_{C}(A, □^{q+1}B).

For instance, Res_{S4_{Σ}}(1, F) is the augmented simplicial set of ground λ_{S4}-terms of type □^{q+1}F, q ⩾ −1. (A term is ground provided it has no free variable.) However we have seen in Lemma 46 that this would not be enough for our purposes. The minimal augmented simplicial set that seems to work is as follows:

Definition 66 (Contracting Resolution Functor CRes). Let (C, □, d, s) be a small strict CS4 category. Then the contracting resolution functor CRes_{C} : C → Δ̂ is the colimit Lim_{⟶}(Λ(Res_{C}) ∘ □) in the category Hom_{Cat}(C, Δ̂) of functors from C

to Δ̂.

This definition makes sense, provided we take Λ as meaning abstraction in Cat: while CRes_{C} is a functor from C^{o} × C to Δ̂, Λ(CRes_{C}) is a functor from C^{o} to Hom_{Cat}(C, Δ̂); since □ is an endofunctor in C, it also defines an endofunctor in C^{o}. Finally, the indicated colimit exists because Hom_{Cat}(C, Δ̂) = Hom_{Cat}(C, Hom_{Cat}(Δ^{o}, Set)) ≅ Hom_{Cat}(C × Δ^{o}, Set) is a category of presheaves, hence a topos, hence is small cocomplete; and C, therefore also C^{o} is small.

Geometrically, the idea is that instead of taking resolutions from a one-point space 1 (as in Res_{C}(1, )), we take all resolutions from enough spaces with a contracting homotopy, properly amalgamated. Recall that a contracting homotopy on an augmented simplicial set K ˆ=(K_{q})_{q⩾−1} is an a.s. map from K to □K that is a right inverse to d in Δ̂. More concretely, this is a family of maps s_{q}^{−1} : K_{q} → K_{q+1}, q ⩾ −1, such that s_{q+1}^{−1} ∘s_{q}^{j} = s_{q+1}^{j+1} ∘s_{q}^{−1} and s_{q−1}^{−1} ∘∂_{q}^{j} = ∂_{q+1}^{j+1} ∘s_{q}^{−1}, for all 0 ⩽ j ⩽ q, and ∂_{q+1}^{0} ∘ s_{q}^{−1} = id. (This is exactly what is needed to build the more standard notion of contracting homotopy in simplicial homology.) Then a trivial way of ensuring that Res_{C}(A, B) has a contracting homotopy is to take A of the form □A′: indeed, for any f ∈ Res_{C}(□A′, B)_{q} = Hom_{C}(□A′, □^{q+1}B), we may then define s_{q}^{−1}(f) as □f ∘ s.

Proof-theoretically, when C is S4_{Σ}, s_{q}^{−1}(M) is the term M . This is the manifestation of the (□I) rule. At the level of programs, this is Lisp’s quote operator.

Proposition 67. For every context Θ, the a.s. set S4 [Θ] is exactly CRes_{S4_{Σ}}(Θ).

Proof. We deal with the case where Θ is of the form z : F for a single formula F, for readability purposes. The general case is similar.

Colimits in functor categories are taken pointwise, so CRes_{S4_{Σ}}(F) is the colimit of the functor that maps every context Γ to the a.s. set Res_{S4_{Σ}}(□Γ, F) of all λ_{S4}-terms M such that □Γ ⊢ M : □^{q+1}F, modulo ≈. On the one hand, S4 [F] is the apex of a cocone consisting of morphisms Res_{S4_{Σ}}(□Γ, F) ⟶ S4 [F] that map each typing derivation of □Γ ⊢ M : □^{q+1}F to the term M itself. On the other hand, we claim that S4 [F] is universal among all such apexes. Let indeed K be any a.s. set such that there are morphisms Res_{S4_{Σ}}(□Γ, F)⟶^{f_{Γ}}K, where Γ ranges over contexts; and such that these morphisms define a cocone: whenever Γ⟶^{θ}Γ′ is a morphism in S4_{Σ},

for every q ⩾ −1, (□Γ′⟶^{M}F) ∈ Res_{S4_{Σ}}(□Γ′, F)_{q}, f_{Γ′}(□Γ′⟶^{M}F) = f_{Γ}(□Γ ⟶^{M·□θ}F).

Taking for θ all substitutions mapping variables to variables, and noticing that for any variable x, □x = dx ≈ x, it follows that f_{Γ} depends only on M, not on

□Γ′⟶^{M}F: this defines the unique morphism from S4 [F] to K. Therefore S4 [F] is a colimit of the desired functor. By the uniqueness of colimits (up to isomorphism), the result obtains.

5.3. A Review of Logical Relations

While the C ⟦ ⟧ interpretation is complete when we are allowed to take S4_{Σ} for C, we are interested in taking more geometrical categories for C, in particular Δ̂.

Let us first review the standard way of proving Friedman’s Theorem 49 ([40], Chapter 8) using logical relations. We shall then discuss why this proof cannot be replayed directly in our case, and do appropriate modifications.

Friedman’s result is for the non-modal part of λ_{S4}, the λ-calculus with βηequality, interpreted in Set. Let us spell out the relevant part of the interpretation of Figure 8 in detail. Given a map from base types A ∈ Σ to sets ρ(A), let Set ⟦F ⊃ G⟧ ρ be the set of all functions from Set ⟦F ⟧ ρ to Set ⟦G⟧ ρ. Then Set ⟦Γ⟧ ρ, where Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}, is a mapping from each variable x_{i} to Set ⟦F_{i}⟧ ρ: this is a Γ-environment ε. The interpretation in Set then maps every typing derivation of a λ-term M of type F in Γ, and every Γ-environment ε to an element Set ⟦Γ ⊢ M : F ⟧ ρε (for short, Set ⟦M⟧ ρε) of Set ⟦F ⟧ ρ: Set ⟦x⟧ ρε is ε(x), Set ⟦MN⟧ ρε is Set ⟦M⟧ ρε applied to Set ⟦N⟧ ρε, and Set ⟦Γ ⊢ λx · M : F ⊃ G⟧ ρε is the function that maps each v ∈ Set ⟦F ⟧ ρ to Set ⟦M⟧ ρ(ε[x ↦ v]).

Let Set[F] be defined as the set of all λ-terms of type F, modulo βη-conversion. We get an interpretation of λ-terms in the free CCC over Σ by mapping every term M to Set[M]θ ˆ=Mθ, where the Γ-environment θ is just a substitution.

A logical relation is a family of binary relations R^{F} indexed by formulae F, between Set[F] and Set ⟦F ⟧ ρ, such that M R^{F ⊃G} f if and only if MN R^{G} f(a) for every M and a such that N R^{F} a. (In general, logical relations are relations indexed by types between Henkin models, or between CCCs. We specialize the notion to our problem at hand.) The fundamental lemma of logical relations (the Basic Lemma of [40]) states that, when ε is a Γ-environment (Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}) and θ a substitution mapping each x_{i} to a term of type F_{i}, whenever x_{i}θ R^{F_{i}} ε(x_{i}) for each i, then Set[M]θ R^{F} Set ⟦M⟧ ρε for any term M of type F in Γ. In other words, as soon as environments are related through the logical relation, then so are the values of any term in both models.

To show that Set ⟦ ⟧ ρ is equationally complete, it is enough to show that we can build a functional logical relation, i.e., one such that for every a ∈ Set ⟦F ⟧ ρ, there is at most one M ∈ Set[F] (up to ≈) such that M R^{F} a. Note that any logical relation is uniquely determined by the relations R^{A} with A ∈ Σ. The trick is to choose R^{A} so that not only R^{A} but every R^{F} is functional. It turns out that asking that R^{F} be functional only does not carry through, and we must require R^{F} to be functional and onto: for every M ∈ Set[F], there must be at least one a ∈ Set ⟦F ⟧ ρ such that M R^{F} a. Under these assumptions, R^{F ⊃G} is then functional and onto as soon as R^{F} and R^{G} are. First, it is functional: choose f ∈ Set ⟦F ⊃ G⟧ ρ, a function from Set ⟦F ⟧ ρ to Set ⟦G⟧ ρ, then every term M such that M R^{F ⊃G} f must be such that for every N R^{F} a, MN R^{G} f(a). Using the Axiom of Choice and the fact that R^{F} is onto, we may define a function i_{F} : Set[F] → Set ⟦F ⟧ ρ such that N R^{F} i_{F} (N). Then M must be such that for every N, MN R^{G} f(i_{F} (N)). Since R^{G} is functional, we may define a projection p_{G} : Set ⟦F ⟧ ρ → Set[F] such that P R^{G} a implies P = p_{G}(a) (when there is no P such that P R^{G} a, p_{G}(a) is arbitrary). So M must be such that for every N, MN = p_{G}(f(i_{F} (N))). This determines MN uniquely, hence M too, provided it exists. So R^{F ⊃G} is functional. To show that it is onto, map M ∈ Set[F ⊃ G] to the function f ∈ Set ⟦F ⊃ G⟧ ρ mapping a to i_{G}(M p_{F} (a)).

This is essentially the line of proof that we shall follow. However, in our case Set is replaced by Δ̂, where the Axiom of Choice is invalid: if p : K → L is an epi in Δ̂, there is no a.s. map i : L → K in general such that p ∘ i = id. Therefore we have to build i_{F} and p_{F} explicitly by induction on formulae. The important property that needs to be preserved for each formula F is what we shall call the Bounding Lemma: if a = i_{F} (M) then M R^{F} a, and if M R^{F} a then M = p_{F} (a). Retracing the argument above, we find that this requires us to define i_{F ⊃G}(M) as the function mapping a to i_{G}(M p_{F} (a)), however the obvious definition for p_{F ⊃G}: p_{F ⊃G}(f) ˆ=λx · p_{G}(f(i_{F} (x))) is wrong. This is because this is incompatible with α-renaming in general, and therefore does not map functions to ≈-classes of λterms. Indeed, compatibility with α-renaming imposes that λx·p_{G}(f(i_{F} (x))) = λy · p_{G}(f(i_{F} (x))){x := y}, but there is no reason why p_{G} ∘ f ∘ i_{F} should be substitutive. The solution is to define p_{F ⊃G} by p_{F ⊃G}(f) ˆ=ℜ_{F ⊃G}(N ↦ p_{G}(f(i_{F} (N)))), where ℜ_{F ⊃G} is a retraction of the set of functions from Set[F] to Set[G] onto the syntactic function space Set[F ⊃ G]—retraction meaning that ℜ_{F ⊃G}(N ↦ MN) should be the term M exactly. This is exactly what we have taken the pain of constructing in the augmented simplicial case in Corollary 48.

One final note before we embark on actually proving the theorem. The right notion of logical relation here is one of Kripke logical relation, a more complex notion than ordinary logical relations. Moreover, contrarily to more usual cases, the set of worlds we use for this Kripke logical relation cannot just be a preorder: it has to be a category, in fact the augmented simplicial category Δ. Concretely, we have to use families of relations R_{q}^{F} indexed by both formulae F and dimensions q ⩾ −1, such that:

(a.s.) for every a, a′, if a R_{q}^{F} a′ then, for every i, 0 ⩽ i ⩽ q, ∂_{q}^{i}a R_{q−1}^{F} ∂_{q}^{i}a′ and s_{q}^{i}a R_{q+1}^{F} s_{q}^{i}a′;

(□ logical) for every a, a′, a R_{q}^{□F} a′ if and only if a R_{q+1}^{F} a′.

(⊃ logical) for every f, f′, f R_{q}^{F ⊃G} f′ if and only if for every monotonic function μ : [p] → [q], for every a, a′ such that a R_{p}^{F} a′,

□^{p+1}App(μ̂(f), a) R_{p}^{G} □^{p+1}App(μ̂(f′), a′)

where μ̂ is defined in the unique way so that δ̂_{q}^{i} = ∂_{q}^{i}, σ̂_{q}^{i} = s_{q}^{i}, îd = id, and

{ \atop μ ∘ μ′} = μ̂′ ∘ μ̂.

The latter condition is particularly unwieldy. We prefer to use a more categorical notion, which will factor out all irrelevant details. It turns out that logical relations and Kripke logical relations are special cases of subscones [41, 1]: these are the right notion here.

5.4. Scones and Subscones

Given any two categories C and D having all finite cartesian products, and such that D has all pullbacks, given any functor 𝔉 : C → D that preserves all finite cartesian products, the subscone D↓^{∩}𝔉 [41] has as objects all triples (d, c, m) where d is an object of D, c is an object of C, and

d ^{⊂} m ≻ 𝔉(c)

is mono in D. The scone D ↓ 𝔉 is defined similarly, only without the requirement that m be mono.

Let C be any strict CS4 category. Given any set Σ of base types, and a mapping that assigns each base type an object in C (this can be seen as a functor from Σ, seen as the trivial category with elements of Σ as objects and only identity morphisms):

Σ  \overline{ρ ≻} C

there is a unique representation of strict CS4 categories C ⟦ ⟧ ρ from the free strict CS4 category S4_{Σ} on Σ to C:

\xymatrix{Σ \ar[r]^{⊆} \ar[d]_{ρ} & S4_{Σ} \ar[dl]^{C⟦ ⟧ρ} \\ C}

where ⊆ denotes the canonical inclusion functor from Σ to S4_{Σ}.

If, in the diagram above, we replace C by a subscone category D↓^{∩}𝔉, we get a diagram:

\xymatrix{Σ \ar[r]^{⊆} \ar[d]_{ρ̃} & S4_{Σ} \ar[dl]^{(D↓^{∩}𝔉)⟦ ⟧ρ̃} \\ D↓^{∩}𝔉}  (19)

for each given ρ̃, and where (D↓^{∩}𝔉) ⟦ ⟧ ρ̃ is uniquely determined as a representation of strict CS4 categories: this will be the right notion of Kripke logical relation.

It is well-known ([41], Proposition 4.2) that, provided that C and D are cartesianclosed, and D has equalizers (i.e., D is finitely complete), and provided 𝔉 preserves finite products, then D↓^{∩}𝔉 is a CCC, and the forgetful functor U : D↓^{∩}𝔉 ⟶ C, which maps every object (d, c, m) to c, is a representation of CCCs. (Similarly for the scone D ↓ 𝔉.) We make explicit the construction of terminal objects, products and internal homs in D↓^{∩}𝔉:

5.4.0.1. Terminal object. This is (1_{D}, 1_{C}, id).

5.4.0.2. Binary products. The product of (d, c, m) with (d′, c′, m′) is (d×d′, c× c′, m × m′).

5.4.0.3. Internal homs. Build (d′′, c′′, m′′) = Hom_{D↓^{∩}𝔉}((d, c, m), (d′, c′, m′)) as follows. (The careful reader will note that the construction is the same in the scone D ↓ 𝔉.) First, c′′ ˆ=Hom_{C}(c, c′).

Then, we build two morphisms. We build the first one from:

𝔉(Hom_{C}(c, c′)) × d \overline{\begin{matrix}id × m \\ ≻ \end{matrix}} 𝔉(Hom_{C}(c, c′)) × 𝔉(c) \overline{𝔉(App)  ≻} 𝔉(c′)

by currying, getting:

The second one is built from:

again by currying:

𝔉(Hom_{C}(c, c′))  \overline{Λ(𝔉(App) ∘ (id × m)) ≻} Hom_{D}(d, 𝔉(c′))  (20)

Hom_{D}(d, d′) × d  \overline{App  ≻} d′ ^{⊂} m′ ≻ 𝔉(c′)

Hom_{D}(d, d′)  \overline{Λ(m′ ∘ App) ≻} Hom_{D}(d, 𝔉(c′))  (21)

We claim that this morphism is mono. Indeed, consider two morphisms f, g such that Λ(m′ ∘App)∘f = Λ(m′ ∘App)∘g. Applying App∘( ×id) on the left-hand side, we get App ∘ ((Λ(m′ ∘ App) ∘ f) × id) = App ∘ (Λ(m′ ∘ App ∘ (f × id)) × id) (by (k′)) = m′ ∘ App ∘ (f × id) (by (l′′)). Applying to both sides of the equation, we therefore get m′ ∘ App ∘ (f × id) = m′ ∘ App ∘ (g × id), therefore App ∘ (f × id) = App ∘ (g × id), because m′ is mono. Applying Λ on both sides, the left-hand side simplifies to f and the right-hand side to g by (m′), therefore f = g. So Λ(m′ ∘ App) is indeed mono.

We now build (d′′, c′′, m′′) by the following pullback diagram:

d′′ ^{⊂}  m′′  ≻ 𝔉(Hom_{C}(c, c′))

Hom_{D}(d, d′) \begin{matrix}s \\ ⋎ \end{matrix}  ^{⊂}  \begin{matrix}Λ(m′ ∘ App) \\ (21) \end{matrix}  ≻ Hom_{D}(d, 𝔉(c′)) \begin{matrix}Λ(𝔉(App) ∘ (id × m)) & (20) \\ ⋎ \end{matrix}

where the upper morphism m′′ is mono because pullbacks preserve monos.

Application in the subscone is given by the pair of morphisms App ∘ (s × id) from d′′ × d to d′ and App from c′′ × c to c′.

Conversely, given any morphism (u, v) in the subscone from (d_{0}, c_{0}, m_{0})×(d, c, m) to (d′, c′, m′), we build its curried morphism from (d_{0}, c_{0}, m_{0}) to (d′′, c′′, m′′) as follows. Recall that since (u, v) is a morphism, the following square commutes:

\begin{aligned}d_{0} × d & ^{⊂} \begin{matrix}m_{0} × m \\ ≻ \end{matrix} & 𝔉(c_{0}) × 𝔉(c) \\ d′ & \begin{matrix}u \\ ⋎ \end{matrix} & ^{⊂}  m′  ≻ & 𝔉(c′) & \begin{matrix}𝔉(v) \\ ⋎ \end{matrix} \end{aligned}

The curried version of the morphism (u, v) is then (û, Λ(v)), where û is given as the unique morphism that makes the following diagram commute:

\xymatrix{d_{0} \ar[ddr]_{Λ(u)} \ar@{-->}[dr]^{û} \ar[rr]^{m_{0}} &  & 𝔉(c_{0}) \ar[d]^{𝔉(Λ(v))} \\  & d′′ \ar[r]^{m′′} \ar[d]^{s} & 𝔉(c′′) \ar[d]_{Λ(𝔉(App)∘(id×m))} \\  & Hom_{D}(d, d′) \ar[r]_{Λ(m′∘App)} & Hom_{D}(d, 𝔉(c′))}

where the bottom pullback diagram is given by the definition of internal homs in the subscone. (The outer diagram commutes: Λ(m′ ∘App)∘Λ(u) = Λ(m′ ∘App∘(Λ(u)× id)) [by (k′)] = Λ(m′ ∘ u) [by (l′′)] = Λ(𝔉(v) ∘ (m_{0} × m)) since (u, v) is a morphism, while Λ(𝔉(App)∘(id×m))∘𝔉(Λ(v))∘m_{0} = Λ(𝔉(App)∘(id×m)∘((𝔉(Λ(v))∘m_{0})×id)) [by (k′)] = Λ(𝔉(App)∘(𝔉(Λ(v))×id)∘(m_{0}×m)) = Λ(𝔉(App∘(Λ(v)×id))∘(m_{0}×m)) [because 𝔉 is a functor that preserves products] = Λ(𝔉(v) ∘ (m_{0} × m)) [by (l′′)].)

5.4.0.4. Comonad (□, d, s). Whereas there is at most one CCC structure on any given category, there are in general many choices for a strict monoidal comonad. A standard choice for defining a comonad on D↓^{∩}𝔉 based on a given comonad (□, d, s) on C works by defining □(d, c, m) as (d′, □c, m′), where d′ and m′ are given by the pullback diagram:

\begin{matrix}d′ & \overline{m′≻} & 𝔉(□c) \\ d & ⋎ & ^{⊂} m ≻ & 𝔉(c) & \begin{matrix}𝔉(d) \\ ⋎ \end{matrix} \end{matrix}

This would not work for our purposes: intuitively, if (d, c, m) represents a relation R^{F}, defining R^{□F} this way as (d′, □c, m′) would mean replacing the (□ logical) condition by: for every a, a′, a R_{q}^{□F} a′ if and only if ∂_{q}^{0}a R_{q}^{F} ∂_{q}^{0}a′. However with this definition R^{□F} would be too large, and the second implication M R^{F} a ⟹ M = p_{F} (a) of the Bounding Lemma would not hold in general. Note that this would also be unsatisfying as this definition does not use the comonad we may have on D.

Instead, we notice that there is a simpler solution as soon as D also comes equipped with a comonad, provided 𝔉 preserves □, d and s (we shall say that 𝔉 preserves the comonad (□, d, s)), and also that □ preserves monos. Then letting □(d, c, m) be (□d, □c, □m) defines an object in the subscone. Indeed, □m is a morphism from □d to □𝔉(c) = 𝔉(□c), and is mono since m is and □ preserves monos. This is what will work here. (In the case of scones, the requirement that □ preserves monos is not necessary.)

This simple case will work for completeness in the augmented simplicial case, which is the only case we shall deal with here. Let us just mention here the right construction to use in more general cases where 𝔉(□c) and □𝔉(c) are not isomorphic. In particular in the case of topological spaces, we shall only have a mono ℑ_{c} from 𝔉(□c) to □𝔉(c) for each object c. We then insist on the condition that ℑ is a distributivity law for comonads (the name is by analogy with distributivity laws for monads as in [24]; they originated in [49]), and that □ preserves pullbacks along the distributivity law. The role of such distributivity laws will be apparent from the proof of Proposition 69.

This appeal to distributivity law subsumes the above, simple case where 𝔉 preserves the comonad □: just take ℑ_{c} to be the identity. This is clearly a distributivity law, and pullbacks will be preserved vacuously.

Definition 68 (Distributivity Law). Let C and D are strict CS4 categories, and 𝔉 : C → D a functor.

A distributivity law of 𝔉 with respect to the two comonads □ on C and D is a natural transformation ℑ from 𝔉□ to □𝔉 such that the following equations hold:

d ∘ ℑ_{c} = 𝔉(d)  (22)
s ∘ ℑ_{c} = □ℑ_{c} ∘ ℑ_{□c} ∘ 𝔉(s)  (23)

In diagrams:

\xymatrix{ &  & 𝔉(□^{2}c) \ar[d]^{ℑ_{□c}} \\  & 𝔉(□c) \ar[ur]^{𝔉(s)} \ar[dl]_{𝔉(d)} \ar[d]^{ℑ_{c}} & □𝔉(□c) \ar[d]^{□ℑ_{c}} \\ 𝔉(c) & □𝔉(c) \ar[l]^{d} \ar[r]_{s} & □^{2}𝔉(c)}

We say, additionally, that □ preserves pullbacks along ℑ, if and only if for each object c of C, for every pullback:

\begin{matrix}d′ & \overline{m′≻} & 𝔉(□c) \\ □d & \begin{matrix}s \\ ⋎ \end{matrix} & \overline{_{□m ≻}} & □(𝔉(c)) & \begin{matrix}ℑ_{c} \\ ⋎ \end{matrix} \end{matrix}

the following commuting square is again a pullback:

\begin{matrix}□d′ & \overline{\begin{matrix}□m′ \\ ≻ \end{matrix}} & □𝔉(□c) \\ □^{2}d & \begin{matrix}□s \\ ⋎ \end{matrix} & \overline{_{□^{2}m ≻}} & □^{2}(𝔉(c)) & \begin{matrix}□ℑ_{c} \\ ⋎ \end{matrix} \end{matrix}

Proposition 69. Assume that C and D are strict CS4 categories, that 𝔉 : C → D preserves finite products, that D is finitely complete, that □ preserves monos and pullbacks along ℑ, where ℑ is a distributivity law of 𝔉 wrt. □.

Then the subscone D↓^{∩}𝔉 is a strict CS4 category when equipped with the comonad (□, d, s) defined by:

• On objects, □(d, c, m) is given as the unique morphism (d′, □c, m′) that makes the following a pullback diagram:

\begin{matrix}d′ & \overline{m′≻} & 𝔉(□c) \\ □d & m̂ ; ⋎ & \overline{_{□m≻}} & □𝔉(c) & \begin{matrix}ℑ_{c} \\ ⋎ \end{matrix} \end{matrix}  (24)

On morphisms, if (u, v) is a morphism from (d_{1}, c_{1}, m_{1}) to (d_{2}, c_{2}, m_{2}), then □(u, v) is the unique morphism (û, □v) that makes the following diagram commute:

[figure: d′_{1}; m′_{1}; m̂_{1}; û; 𝔉(□c_{1}); ℑ_{c_{1}}; 𝔉(□v); d′_{2}; m′_{2}; m̂_{2}; 𝔉(□c_{2}); ℑ_{c_{2}}; □d_{1}; □u; □m_{1}; □𝔉(c_{1}); □𝔉(v); □d_{2}; □m_{2}; □𝔉(c_{2})]  (25)

where the front face defines □(d_{2}, c_{2}, m_{2}), the back face defines □(d_{1}, c_{1}, m_{1}), the bottom face is by the definition of (u, v) as a morphism, the right face is by naturality of ℑ, and û is then determined uniquely by the fact that the front face is a pullback.

• The counit d from □(d, c, m) to (d, c, m) is (d ∘ m̂, d), where m̂ is given as in Diagram (24).

• Comultiplication s is (s̄, s) where s′ is uniquely determined so that the following diagram commutes:

[figure: d′; m̂; m′; s̄; 𝔉(□c); 𝔉(s); d′′; m′′; m̂′; 𝔉(□^{2}c); ℑ_{□c}; (26.1); □d′; □m′; □m̂; □𝔉(□c); □ℑ_{c}; (26.2); □d; s; □^{2}d; □^{2}m; □^{2}𝔉(c)]  (26)

where (26.1) is the defining square for □(d′, □c, m′) = □^{2}(d, c, m) and (26.2) is the image under □ of the defining square for □(d, c, m).

Moreover, the forgetful functor U : D↓^{∩}𝔉 ⟶ C mapping every object (d, c, m) in the scone (resp. subscone) to c and every morphism (u, v) to v is a representation of strict CS4 categories.

Proof. The CCC structure on D ↓ 𝔉 (resp. D↓^{∩}𝔉) as well as the fact that U is a representation of CCCs is well-known. Let us check the comonad.

First, in Diagram (24) since m is mono, □m is, too, because □ preserves monos; so m′ must be mono, since pullbacks preserve monos. It follows that (d′, □c, m) is indeed an object in D↓^{∩}𝔉.

We claim that □ is a functor: this is because □ on morphisms is defined as the solution to a universal problem. Moreover, U(□(d, c, m)) = □c, so U preserves □.

Then, d = (d ∘ m̂, d) is well-defined. Indeed, pile the definition (24) of □(d, c, m) atop the square saying that d ∘ □m = m ∘ d:

d′  \overline{m′≻} 𝔉(□c)

□d m̂ ; ⋎ \overline{_{□m≻}} □𝔉(c) \begin{matrix}ℑ_{c} \\ ⋎ \end{matrix}

d \begin{matrix}d \\ ⋎ \end{matrix}  \overline{_{m ≻}} 𝔉(c) \begin{matrix}d \\ ⋎ \end{matrix}

Since d ∘ ℑ_{c} = 𝔉(d) by (22), this implies that m ∘ (d ∘ m̂) = 𝔉(d) ∘ m′, which means exactly that (d ∘ m̂, d) is a morphism from (d′, □c, m′) to (d, c, m). Also, U maps d = (d ∘ m̂, d) to d in C: U preserves d.

To show that s is well-defined is a bit more intricate. Since □ preserves pullbacks along ℑ, (26.2) is a pullback diagram, so the square obtained by piling (26.1) above (26.2) is again a pullback square. Then s̄ will be uniquely defined as soon as we show that the outer square commutes. Indeed, the leftmost path from d′ to □^{2}𝔉(c) is □^{2}m∘s∘m̂ = s∘□m∘m̂ by (q), while the rightmost path is □ℑ_{c} ∘ℑ_{□c} ∘𝔉(s)∘m′ = s ∘ ℑ_{c} ∘ m′ by (23). These two are equal since □m ∘ m̂ = ℑ_{c} ∘ m′ by the definition of □(d, c, m) (Diagram (24)). Moreover, U(s) = s, as Diagram (26) indicates.

It remains to check the comonad equations (n)–(y). We have already checked (n), (o); (r), (v), (w), (x), (y) follow from the fact that □ and 𝔉 preserve finite products. The others are all checked in the same fashion.

Let us check (p): d ∘ □f = f ∘ d. Write the morphism f as (u, v), from (d, c, m) to (d′, c′, m′). Then □f is given by (û, □v) as shown in Diagram (25). Writing the top face of the latter diagram above the square saying that d is a morphism in the subscone yields the diagram below (left), where we have taken the notations of Diagram (25). On the other hand, putting the definition of d in the subscone atop the defining square for (u, v) yields the diagram on the right:

d′_{1}  \overline{\begin{matrix}m′_{1} \\ ≻ \end{matrix}} 𝔉(□c_{1})  d′_{1}  \overline{\begin{matrix}m′_{1} \\ ≻ \end{matrix}} 𝔉(□c_{1})

d′_{2} û ; ⋎  \overline{\begin{matrix}m′_{2} \\ ≻ \end{matrix}} 𝔉(□c_{2}) \begin{matrix}𝔉(□v) \\ ⋎ \end{matrix}  d_{1} \begin{matrix}d & ∘m̂_{1} \\ ⋎ \end{matrix} \overline{m_{1} ≻} 𝔉(c_{1}) \begin{matrix}𝔉(d) \\ ⋎ \end{matrix}

d_{2} \begin{aligned}d ∘ m̂_{2} \\ & ⋎ \end{aligned}  \overline{_{m_{2} ≻}} 𝔉(c_{2}) \begin{matrix}𝔉(d) \\ ⋎ \end{matrix}  d_{2} \begin{matrix}u \\ ⋎ \end{matrix}  \overline{_{m_{2} ≻}} 𝔉(c_{2}) \begin{matrix}𝔉(v) \\ ⋎ \end{matrix}

Since d∘□v = v∘d, the righmost paths from d′_{1} to 𝔉(c_{2}) in each diagram are equal, so the leftmost ones are equal, too. Since m_{2} is mono, the left vertical paths (from d′_{1} to d_{2}) are equal. This means exactly that (d ∘ m̂_{2}) ∘ û = u ∘ (d ∘ m̂_{1}), therefore d ∘ □(u, v) = (u, v) ∘ d in the subscone.

Equations (q), (u) are checked similarly.

Equation (s) follows from the diagram:

d′  \overline{m′≻} 𝔉(□c)

d′′ s̄ ; ⋎ \overline{\begin{matrix}m′′ \\ ≻ \end{matrix}} 𝔉(□^{2}c) \begin{matrix}𝔉(s) \\ ⋎ \end{matrix}

d′ \begin{aligned}d ∘ m̂′ \\ & ⋎ \end{aligned}  \overline{_{m′≻}} 𝔉(□c) \begin{matrix}𝔉(d) \\ ⋎ \end{matrix}

where the lower square is the definition of d from □^{2}(d, c, m) = □(d′, □c, m′) = (d′′, □^{2}c, m′′) to □(d, c, m) = (d′, □c, m′). The rightmost path from 𝔉(□c) to 𝔉(□c) is 𝔉(d) ∘ 𝔉(s) = 𝔉(d ∘ s) = 𝔉(id) = id. So m′ = m′ ∘ (d ∘ m̂′) ∘ s̄. Since m′ is mono, (d ∘ m̂′) ∘ s̄ = id, so d ∘ s = id in the subscone.

Equation (t) is dealt with similarly.

5.5. The Basic Lemma

The argument here is the same as [41]. Given any functor Σ⟶^{ρ̃}D↓^{∩}𝔉, we get a functor from Σ to C by composition with U. By the freeness of S4_{Σ}, there are unique functors C ⟦ ⟧ ρ (where ρ ˆ=U ∘ ρ̃) and (D↓^{∩}𝔉) ⟦ ⟧ ρ̃ which make the upper left and upper right triangles in the following diagram (which is a diagram in the category Cat of categories) commute:

[figure: Σ; ⊆; ρ̃; ρ; S4_{Σ}; C⟦ ⟧ρ; (D↓^{∩}𝔉)⟦ ⟧ρ̃; D↓^{∩}𝔉; U; C]

Since U is a representation of strict CS4 categories, U ∘ (D↓^{∩}𝔉) ⟦ ⟧ ρ̃, too, therefore by the uniqueness of the C ⟦ ⟧ ρ arrow on the right as a representation of strict CS4 categories, we get:

Lemma 70 (Basic Lemma). U ∘ (D↓^{∩}𝔉) ⟦ ⟧ ρ̃ = C ⟦ ⟧ (U ∘ ρ̃)

5.6. The Bounding Lemma

Now we consider the case where C is of the form C_{1} × D, and 𝔉 ˆ=𝔉_{1} ⊗ id, where 𝔉_{1} : C_{1} → D is a functor that preserves all finite products, and ℑ^{1} is a distributivity law of 𝔉_{1} wrt. □. (Whenever 𝔉_{1} : C_{1} → D, 𝔉_{2} : C_{2} → D, we let 𝔉_{1} ⊗ 𝔉_{2} be the functor mapping C_{1}, C_{2} to 𝔉_{1}(C_{1}) × 𝔉_{2}(C_{2}).)

Typically, C_{1} will be S4_{Σ}, 𝔉_{1} ˆ=CRes_{S4_{Σ}}, D ˆ=Δ̂, and ℑ_{(c_{1},d)} ˆ=(ℑ_{c_{1}}^{1}, id_{d})—in this case ℑ_{c_{1}}^{1} will be an identity morphism, and therefore ℑ_{(c_{1},d)} as well.

We shall prove: Lemma 71 (Bounding Lemma). Let C_{1} and D be strict CS4 categories, 𝔉_{1} : C_{1} → D preserve finite products. Assume also that D is finitely complete and that □ preserves monos in D as well as pullbacks along some distributivity law ℑ^{1} of 𝔉_{1} wrt. □. Fix ρ_{1} : Σ → C_{1}. Assume finally that for every formulae F and G, Hom_{D}(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1})) retracts strongly onto 𝔉_{1}(C_{1} ⟦F ⊃ G⟧ ρ_{1}), meaning that there is a family of morphisms ℜ_{F ⊃G} in D such that the following diagram commutes:

Hom_{D}(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1})) ≺ Λ(𝔉_{1}(App))  𝔉_{1}(C_{1} ⟦F ⊃ G⟧ ρ_{1})

Hom_{D}(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1})) \begin{matrix}id \\ ⋎ \end{matrix}  \overline{_{ℜ_{F ⊃G}  ≻}} 𝔉_{1}(C_{1} ⟦F ⊃ G⟧ ρ_{1}) \begin{matrix}id \\ ⋎ \end{matrix}

(27)

and similarly, that for every formula F, □𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}) retracts strongly onto 𝔉_{1}(C_{1} ⟦□F ⟧ ρ_{1}), meaning that there is a family of morphisms ℜ_{□F} such that the following diagram commutes:

\begin{matrix}□𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}) & ≺ℑ_{C_{1}⟦F ⟧ρ_{1}}^{1} & 𝔉_{1}(C_{1} ⟦□F⟧ ρ_{1}) \\ □𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}) & \begin{matrix}id \\ ⋎ \end{matrix} & \overline{ℜ_{□F} ≻} & 𝔉_{1}(C_{1} ⟦□F⟧ ρ_{1}) & \begin{matrix}id \\ ⋎ \end{matrix} \end{matrix}  (28)

Let ρ_{2} : Σ → D be 𝔉_{1} ∘ ρ_{1}, and ρ̃ : Σ → D↓^{∩}(𝔉_{1} ⊗ id) map every A ∈ Σ to (ρ_{2}(A), (ρ_{1}(A), ρ_{2}(A)), ⟨id, id⟩).

For every formula F, write (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦F ⟧ ρ̃ as (D_{F} , (C_{1} ⟦F ⟧ ρ_{1}, D ⟦F ⟧ ρ_{2}), ⟨m′_{F} , m′′_{F} ⟩).

Then there are families of morphisms i_{F} and p_{F} in D, and monos h_{F}^{1} and h_{F}^{2} that make the following diagrams commute for each formula F:

[figure: 𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}); 𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}); id; h_{F}^{1}; i_{F}; D_{F}; m′_{F}; h_{F}^{2}; m′′_{F}; D ⟦F ⟧ ρ_{2}; p_{F}; id; D ⟦F ⟧ ρ_{2}]  (29)

Proof. We first build i_{F} and p_{F} for each formula F so that p_{F} ∘ i_{F} = id. This is indeed required for the result to hold, since Diagram 29 implies p_{F} ∘ h_{F}^{2} ∘ h_{F}^{1} = id and id ∘ h_{F}^{2} ∘ h_{F}^{1} = i_{F}.

When F is a base type A ∈ Σ, define i_{A} and p_{A} in D so that the following diagrams commute:

\begin{matrix}ρ_{2}(A) = 𝔉_{1}(ρ_{1}(A)) & ≺ i_{A} & 𝔉_{1}(ρ_{1}(A)) \\ ρ_{2}(A) & \begin{matrix}id \\ ⋎ \end{matrix} & \overline{_{p_{A} ≻}} & ρ_{2}(A) = 𝔉_{1}(ρ_{1}(A)) & \begin{matrix}id \\ ⋎ \end{matrix} \end{matrix}

by just taking i_{A} and p_{A} to be id.

When F = □G, let i_{□G} ˆ=□i_{G} ∘ ℑ_{C_{1}⟦G⟧ρ_{1}}^{1}, p_{□G} ˆ=ℜ_{□G} ∘ □p_{G}, so p_{□G} ∘ i_{□G} = ℜ_{□G} ∘ □p_{G} ∘ □i_{G} ∘ ℑ_{C_{1}⟦G⟧ρ_{1}}^{1} = ℜ_{□G} ∘ □(p_{G} ∘ i_{G}) ∘ ℑ_{C_{1}⟦G⟧ρ_{1}}^{1} = ℜ_{□G} ∘ □id ∘ ℑ_{C_{1}⟦G⟧ρ_{1}}^{1} = ℜ_{□G} ∘ ℑ_{C_{1}⟦G⟧ρ_{1}}^{1} = id.

When F is of the form G ⊃ H, we build i_{F} and p_{F} in the unique type-consistent way. I.e., we have the following diagram:

D ⟦H⟧ ρ_{2} ≺  i_{H}  𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})

\begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}), 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \\ ×D ⟦G⟧ ρ_{2} \end{matrix}  \overline{_{id × p_{G}≻}} \begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}), 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \\ ×𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) \end{matrix}^{⋏App}

using i_{H} and p_{G} from the induction hypothesis. Apply Λ to the resulting composite morphism, and compose with Λ(𝔉_{1}(App)); this yields i_{G⊃H}, defined as:

D ⟦G ⊃ H⟧ ρ_{2} ≺ \begin{matrix}Λ(i_{H} ∘ App \\ ∘(id × p_{G})) \end{matrix} \begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}), \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \end{matrix} ≺ Λ(𝔉_{1}(App)) 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1})

Similarly, we define a morphism p_{G⊃H} from D ⟦G ⊃ H⟧ ρ_{2} to 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) as the composite:

D ⟦G ⊃ H⟧ ρ_{2}  \overline{\begin{matrix}Λ(p_{H} ∘ App \\ ∘(id × i_{G})) \end{matrix} ; ≻} \begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}), \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \end{matrix} \overline{_{ℜ_{G⊃H} ≻}} 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1})

Superposing both diagrams, together with (27), we get:

D ⟦G ⊃ H⟧ ρ_{2} ≺ \begin{matrix}Λ(i_{H} ∘ App \\ ∘(id × p_{G})) \end{matrix} \begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), \\ 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1})) \end{matrix} ≺ Λ(𝔉_{1}(App)) 𝔉_{1}(C_{1} ⟦F ⊃ G⟧ ρ_{1})

D ⟦G ⊃ H⟧ ρ_{2} \begin{matrix}id \\ ⋎ \end{matrix}  \begin{matrix}Λ(p_{H} ∘ App \\ ∘(id × i_{G})) \end{matrix} ; ≻ \begin{matrix}Hom_{D}(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), \\ 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1})) \end{matrix} \begin{matrix}id \\ ⋎ \end{matrix}  \overline{_{ℜ_{F ⊃G} ≻}} 𝔉_{1}(C_{1} ⟦F ⊃ G⟧ ρ_{1}) \begin{matrix}id \\ ⋎ \end{matrix}

where i_{G⊃H} is the top line, p_{G⊃H} is the bottom line, the right square commutes by (27), and the left square commutes, as calculation shows (left to the reader; hint: use p_{H} ∘ i_{H} = id, p_{G} ∘ i_{G} = id). So p_{G⊃H} ∘ i_{G⊃H} = id.

We now build h_{F}^{1} and h_{F}^{2} . Note that as soon as Diagram 29 commutes, h_{F}^{1} and h_{F}^{2} will automatically be mono. Indeed, since p_{F} ∘i_{F} = id, i_{F} is mono; as i_{F} = m′′_{F} ∘h_{F}^{1} , h_{F}^{1} will be mono, too. Similarly, since ⟨m′_{F} , m′′_{F} ⟩ is a mono (because it is part of the definition of an object in the subscone), and ⟨m′_{F} , m′′_{F} ⟩ = ⟨p_{F} , id⟩ ∘ h_{F}^{2} , h_{F}^{2} will be a mono, too.

Also, that h_{F}^{1} and h_{F}^{2} are mono will imply that h̃_{F}^{1} ˆ=(h_{F}^{1} , id) and h̃_{F}^{2} ˆ=(h_{F}^{2} , id) will be mono in (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦F ⟧ ρ̃. Therefore, that Diagram 29 is commutative is equivalent to showing the existence of the following diagram in D↓^{∩}(𝔉_{1} ⊗ id):

Ĩ_{F} ^{⊂}  \begin{matrix}(h_{F}^{1} , id) \\ ≻ \end{matrix} (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦F ⟧ ρ̃ ^{⊂}(h_{F}^{2} , id) ≻ P̃_{F}

where

Ĩ_{F} ˆ=(𝔉_{1}(C_{1} ⟦F ⟧ ρ_{1}), (C_{1} ⟦F ⟧ ρ_{1}, D ⟦F ⟧ ρ_{2}), ⟨id, i_{F} ⟩)
P̃_{F} ˆ=(D ⟦F ⟧ ρ_{1}, (C_{1} ⟦F ⟧ ρ_{1}, D ⟦F ⟧ ρ_{2}), ⟨p_{F} , id⟩)

We build h_{F}^{1} and h_{F}^{2} by structural induction on F.

If F is a base type A, notice that i_{A} = p_{A} = m′_{A} = m′′_{A} = id, so take h_{A}^{1} ˆ=h_{A}^{2} ˆ=id. If F is a box formula □G. Recall first that p_{□G} = ℜ_{□G}∘□p_{G}, and i_{□G} = □i_{G}∘ℑ^{1}

(we drop indices to ℑ^{1} to avoid clutter). On the other hand, the definition of □ in the subscone is by the following pullback diagram:

\begin{matrix}D_{□G} & \overline{\begin{matrix}⟨m′_{□G}, m′′_{□G}⟩ \\ ≻ \end{matrix}} & 𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1}) × D ⟦□G⟧ ρ_{2} \\ □D_{G} & { \atop ⟨m′_{G}, m′′_{G}⟩} ; ⋎ & \overline{_{⟨□m′_{G}, □m′′_{G}⟩ ≻}} & □𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) × □D ⟦G⟧ ρ_{2} & \begin{matrix}ℑ^{1} × id \\ ⋎ \end{matrix} \end{matrix}  (30)

This allows us to define h_{□G}^{1} by the universal property of the pullback:

\xymatrix{𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1} \ar@{-->}[drr]^{⟨id,□i_{G}∘ℑ^{1}⟩} \ar@{-->}[dr]_{h_{□G}^{1}} \ar[ddr]_{□h_{G}^{1}∘ℑ^{1}} \\  & D_{□G} \ar[r]^{⟨m′_{□G},m′′_{□G}⟩} \ar[d]^{{ \atop ⟨m′_{G},m′′_{G}⟩}} & 𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1}) × D ⟦□G⟧ ρ_{2} \ar[d]^{ℑ^{1}×id} \\  & □D_{G} \ar[r]_{⟨□m′_{G},□m′′_{G}⟩} & □𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) × □D ⟦G⟧ ρ_{2}}

The upper triangle is exactly the left part of the diagram we are looking for:

\xymatrix{ & 𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1}) \\ 𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1}) \ar[ur]^{id} \ar[r]^{h_{□G}^{1}} \ar[dr]_{i_{□G}} & D_{□G} \ar[u]_{m′_{□G}} \ar[d]^{m′′_{□G}} \\  & D ⟦□G⟧ ρ_{2}}

On the other hand, the right part is given by h_{□G}^{2} ˆ=m′′_{□G}, provided we can show that p_{□G} ∘ m′′_{□G} = m′_{□G}. To show this, note that we can rewrite Diagram (30) as:

\begin{aligned}𝔉_{1}(C_{1} ⟦□G⟧ ρ_{1}) & ≺ m′_{□G} & D_{□G} & \overline{\begin{matrix}m′′_{□G} \\ ≻ \end{matrix}} & D ⟦□G⟧ ρ_{2} \\ □𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) & \begin{aligned}ℑ^{1} \\ & ⋎ \end{aligned} & ≺ □m′_{G} & □D_{G} & { \atop ⟨m′_{G}, m′′_{G}⟩} ; ⋎ & \overline{_{□m′′_{G}≻}} & D ⟦□G⟧ ρ_{2} & \begin{matrix}id \\ ⋎ \end{matrix} \end{aligned}

Since by induction hypothesis p_{G} ∘ m′′_{G} = m′_{G}, adding the morphism □p_{G} from the lower right D ⟦□G⟧ ρ_{2} to the lower left □𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) makes another commutative diagram. It follows that (reading from the topmost D_{□G} to the lower left □𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) in two different ways) □p_{G}∘m′′_{□G} = ℑ^{1}∘m′_{□G}. Composing with ℜ_{□G} on the left we get ℜ_{□G} ∘□p_{G} ∘m′′_{□G} = ℜ_{□G} ∘ℑ^{1} ∘m′_{□G}, that is, p_{□G} ∘m′′_{□G} = m′_{□G}, as desired. This terminates the box case.

If F is an arrow type G ⊃ H. We first build h_{G⊃H}^{1}. Construct the morphism:

\begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) × 𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) & ≺ id × m′_{G} & 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) × D_{G} \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}) & \begin{matrix}𝔉_{1}(App) \\ ⋎ \end{matrix} & \overline{h_{H}^{1} ≻} & D_{H} \end{matrix}

in D. For short, let us call this morphism u temporarily.

Also construct the morphism v ˆ=(App, App) from (C_{1} ⟦G ⊃ H⟧ ρ_{1}, D ⟦G ⊃ H⟧ ρ_{2}) × (C_{1} ⟦G⟧ ρ_{1}, D ⟦G⟧ ρ_{2}) to (C_{1} ⟦H⟧ ρ_{1}, D ⟦H⟧ ρ_{2}) in C_{1} × D.

We claim that (u, v) is a morphism in D↓^{∩}(𝔉_{1} ⊗ id) (if so, this is from Ĩ_{G⊃H} × (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦G⟧ ρ̃ to (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦H⟧ ρ̃). This requires us to show that the following diagram commutes (where we have split products so as to increase readability):

\begin{aligned}\begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ ×𝔉_{1}(C_{1} ⟦G⟧ ρ_{1}) \end{matrix} & ≺id × m′_{G} & \begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ ×D_{G} \end{matrix} & \overline{\begin{matrix}i_{G⊃H} \\ ×m′′_{G} \end{matrix} ≻} & \begin{matrix}D ⟦G ⊃ H⟧ ρ_{2} \\ ×D ⟦G⟧ ρ_{2} \end{matrix} \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}) & \begin{matrix}𝔉_{1}(App) \\ ⋎ \end{matrix} & ≺  m′_{H} & D_{H} & \begin{matrix}u \\ ⋎ \end{matrix} & \overline{_{m′′_{H}  ≻}} & D ⟦H⟧ ρ_{2} & \begin{matrix}App \\ ⋎ \end{matrix} \end{aligned} (31)

The left square of (31) commutes because m′_{H} ∘ h_{H}^{1} is the identity on D_{H}, by induction hypothesis, so

m′_{H} ∘ u = m′_{H} ∘ h_{H}^{1} ∘ 𝔉_{1}(App) ∘ (id × m′_{G}) = 𝔉_{1}(App) ∘ (id × m′_{G})

For the right square of (31), note that App ∘ (i_{G⊃H} × id) = i_{H} ∘ 𝔉_{1}(App) ∘ (id × p_{G}), by the definition of i_{G⊃H}. Composing with id × m′′_{G} on the right, it follows App ∘ (i_{G⊃H} × m′′_{G}) = i_{H} ∘ 𝔉_{1}(App) ∘ (id × (p_{G} ∘ m′′_{G})). However p_{G} ∘ m′′_{G} = m′_{G} by induction hypothesis. So we get:

App ∘ (i_{G⊃H} × m′′_{G}) = i_{H} ∘ 𝔉_{1}(App) ∘ (id × m′_{G})

Since m′′_{H} ∘ h_{H}^{1} = i_{H} by induction hypothesis, the right-hand side is exactly m′′_{H} ∘ u, so the right square of (31) commutes.

As (31) commutes, (u, v) is indeed a morphism in D↓^{∩}(𝔉_{1} ⊗ id). We may then curry it in D↓^{∩}(𝔉_{1} ⊗ id), getting a morphism from Ĩ_{G⊃H} to the internal hom object Hom_{D↓^{∩}(𝔉_{1}⊗id)}((D↓^{∩}(𝔉_{1} ⊗ id)) ⟦G⟧ ρ̃, (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦H⟧ ρ̃), that is, from Ĩ_{G⊃H} to (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦G ⊃ H⟧ ρ̃.

Let us call this latter morphism h̃_{G⊃H}^{1}. As recalled in Paragraph 5.4.0.3, this morphism is of the form (û, Λ(v)), where Λ(v) is taken in the product category C_{1} × D. Since v was application is this category, Λ(v) = id. So h̃_{G⊃H}^{1} is of the required form (h_{G⊃H}^{1}, id); i.e., we let h_{G⊃H}^{1} be û. Because this is a morphism in D↓^{∩}(𝔉_{1} ⊗ id), the following diagram commutes:

\begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) & \overline{⟨id, i_{G⊃H}⟩ ≻} & 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) × D ⟦G ⊃ H⟧ ρ_{2} \\ D_{G⊃H} & \begin{aligned}h_{G⊃H}^{1} \\ & ⋎ \end{aligned} & \overline{_{⟨m′_{G⊃H}, m′′_{G⊃H}⟩ ≻}} & 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) × D ⟦G ⊃ H⟧ ρ_{2} & \begin{matrix}id \\ ⋎ \end{matrix} \end{matrix}

This is exactly the left part of the desired diagram:

\xymatrix{ & 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ 𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \ar[ur]^{id} \ar[dr]_{i_{G⊃H}} \ar[r]^{h_{G⊃H}^{1}} & D_{G⊃H} \ar[u]_{m′_{G⊃H}} \ar[d]^{m′′_{G⊃H}} \\  & D ⟦G ⊃ H⟧ ρ_{2}}

Let us now build h_{G⊃H}^{2}. Define h_{G⊃H}^{2} ˆ=m′′_{G⊃H}. Adapting the definition of internal homs to the subscone category D↓^{∩}(𝔉_{1} ⊗ id), and using a few trivial isomorphisms, (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦G ⊃ H⟧ ρ̃ is given by the following pullback diagram:

D_{G⊃H}  \overline{⟨m′_{G⊃H}, m′′_{G⊃H}⟩  ≻} \begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ ×D ⟦G ⊃ H⟧ ρ_{2} \end{matrix}

Hom_{D}(D_{G}, D_{H}) \begin{aligned}s_{G⊃H} \\ & ⋎ \end{aligned}  \overline{_{⟨Λ(m′_{H} ∘ App), Λ(m′′_{H} ∘ App)⟩  ≻}} \begin{matrix}Hom_{D}(D_{G}, 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \\ ×Hom_{D}(D_{G}, D ⟦H⟧ ρ_{2}) \end{matrix} \begin{matrix}Λ(𝔉_{1}(App) ∘ (id × m′_{G})) × Λ(App & ∘(id × m′′_{G})) \\ ⋎ \end{matrix}

Splitting products, we may rewrite this as:

𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) ≺ m′_{G⊃H}  D_{G⊃H}  \overline{m′′_{G⊃H} ≻} D ⟦G ⊃ H⟧ ρ_{2}

Hom_{D}(D_{G}, 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \begin{matrix}Λ(𝔉_{1}(App) ∘ (id × m′_{G})) \\ ⋎ \end{matrix} ≺ \begin{matrix}Λ(m′_{H} \\ ∘App) \end{matrix} Hom_{D}(D_{G}, D_{H}) \begin{matrix}s_{G⊃H} \\ ⋎ \end{matrix}  \overline{\begin{matrix}Λ(m′′_{H} \\ ∘App) \end{matrix} ; ≻} Hom_{D}(D_{G}, D ⟦H⟧ ρ_{2}) \begin{matrix}Λ(App ∘ (id × m′′_{G})) \\ ⋎ \end{matrix}

Take the product with D_{G}:

\begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ ×D_{G} \end{matrix} ≺ m′_{G⊃H} × id  D_{G⊃H} × D_{G}  \overline{m′′_{G⊃H} × id ≻} \begin{matrix}D ⟦G ⊃ H⟧ ρ_{2} \\ ×D_{G} \end{matrix}

\begin{matrix}Hom_{D}(D_{G}, \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \\ ×D_{G} \end{matrix} \begin{matrix}Λ(𝔉_{1}(App) & ∘(id × m′_{G})) × id \\ ⋎ \end{matrix} ≺  \begin{matrix}Λ(m′_{H}∘ \\ App) × id \end{matrix} \begin{matrix}Hom_{D}(D_{G}, D_{H}) \\ ×D_{G} \end{matrix} \begin{matrix}s_{G⊃H} × id \\ ⋎ \end{matrix}  \overline{\begin{matrix}Λ(m′′_{H}∘ \\ App) × id \end{matrix}  ≻} \begin{matrix}Hom_{D}(D_{G}, \\ D ⟦H⟧ ρ_{2}) \\ ×D_{G} \end{matrix} \begin{matrix}Λ(App ∘ (id × m′′_{G})) × id \\ ⋎ \end{matrix}

Putting this above the following diagram:

\begin{matrix}Hom_{D}(D_{G}, \\ 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1})) \\ ×D_{G} \end{matrix} ≺ \begin{matrix}Λ(m′_{H}∘ \\ App) × id \end{matrix} \begin{matrix}Hom_{D}(D_{G}, D_{H}) \\ ×D_{G} \end{matrix} \overline{\begin{matrix}Λ(m′′_{H}∘ \\ App) × id \end{matrix} ≻} \begin{matrix}Hom_{D}(D_{G}, \\ D ⟦H⟧ ρ_{2}) \\ ×D_{G} \end{matrix}

𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}) \begin{matrix}App \\ ⋎ \end{matrix}  ≺  m′_{H}  D_{H} \begin{matrix}App \\ ⋎ \end{matrix}  \overline{_{m′′_{H}  ≻}} D ⟦H⟧ ρ_{2} \begin{matrix}App \\ ⋎ \end{matrix}

which is easily seen to commute, we obtain:

\begin{matrix}𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ ×D_{G} \end{matrix} ≺m′_{G⊃H} × id D_{G⊃H} × D_{G}  \overline{m′′_{G⊃H} × id≻} \begin{matrix}D ⟦G ⊃ H⟧ ρ_{2} \\ ×D_{G} \end{matrix}

𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}) \begin{matrix}𝔉_{1}(App) ∘ (id × m′_{G}) \\ ⋎ \end{matrix} ≺  m′_{H}  D_{H} \begin{aligned}s_{G⊃H} \\ & ⋎ \end{aligned}  \overline{_{m′′_{H}  ≻}} D ⟦H⟧ ρ_{2} \begin{matrix}App ∘ (id × m′′_{G}) \\ ⋎ \end{matrix}

(32)

Indeed, the leftmost vertical morphism is App ∘ (Λ(𝔉_{1}(App) ∘ (id × m′_{G})) × id) = 𝔉_{1}(App) ∘ (id × m′_{G}), while the rightmost vertical morphism is obtained similarly.

By induction hypothesis m′_{H} = p_{H} ∘ m′′_{H}. So we may complete Diagram (32) by adding a p_{H} arrow from the lower right D ⟦H⟧ ρ_{2} to the lower left 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}), and get a commutative diagram again. Looking at the leftmost and the rightmost paths from the upper D_{G⊃H} × D_{G} to the lower left 𝔉_{1}(C_{1} ⟦H⟧ ρ_{1}), it follows:

𝔉_{1}(App) ∘ (id × m′_{G}) ∘ (m′_{G⊃H} × id) = p_{H} ∘ App ∘ (id × m′′_{G}) ∘ (m′′_{G⊃H} × id)

Composing with id×h_{G}^{1} on the right and simplifying, we obtain 𝔉_{1}(App)∘(m′_{G⊃H} × (m′_{G}∘h_{G}^{1})) = p_{H} ∘App∘(m′′_{G⊃H} ×(m′′_{G}∘h_{G}^{1})). By induction hypothesis m′_{G}∘h_{G}^{1} = id, and m′′_{G} ∘ h_{G}^{1} = i_{G}, so:

𝔉_{1}(App) ∘ (m′_{G⊃H} × id) = p_{H} ∘ App ∘ (m′′_{G⊃H} × i_{G})  (33)

This entails that Λ(p_{H} ∘ App ∘ (id × i_{G})) ∘ m′′_{G⊃H} = Λ(p_{H} ∘ App ∘ (id × i_{G}) ∘ (m′′_{G⊃H} × id)) = Λ(p_{H} ∘ App ∘ (m′′_{G⊃H} × i_{G})) = Λ(𝔉_{1}(App) ∘ (m′_{G⊃H} × id)) (using (33)) = Λ(𝔉_{1}(App)) ∘ m′_{G⊃H}. Composing with ℜ_{G⊃H} on the left, remembering that ℜ_{G⊃H} ∘ Λ(𝔉_{1}(App)) = id (Diagram (27)), it obtains:

ℜ_{G⊃H} ∘ Λ(p_{H} ∘ App ∘ (id × i_{G})) ∘ m′′_{G⊃H} = m′_{G⊃H}

That is, p_{G⊃H} ∘ m′′_{G⊃H} = m′_{G⊃H}.

On the other hand, recall that h_{G⊃H}^{2} = m′′_{G⊃H}. So we have got the right part of the desired diagram:

\xymatrix{𝔉_{1}(C_{1} ⟦G ⊃ H⟧ ρ_{1}) \\ D_{G⊃H} \ar[u]_{m′_{G⊃H}} \ar[r]^{h_{G⊃H}^{2}} \ar[d]^{m′′_{G⊃H}} & D ⟦G ⊃ H⟧ ρ_{2} \ar[ul]_{p_{G⊃H}} \ar[dl]^{id} \\ D ⟦G ⊃ H⟧ ρ_{2}}

This terminates the implication case.

5.7. Equational Completeness We can now prove:

Theorem 72 (Equational Completeness). Let D be a strict CS4 category, 𝔉_{1} : S4_{Σ} → D preserve finite products. Assume also that D is finitely complete, that □ preserves monos in D as well as pullbacks along some distributivity law ℑ^{1} of 𝔉_{1} wrt. □, and that for every formulae F and G, Hom_{D}(𝔉_{1}(S4_{Σ} ⟦F ⟧ (⊆)), 𝔉_{1}(S4_{Σ} ⟦G⟧ (⊆))) retracts strongly onto 𝔉_{1}(S4_{Σ} ⟦F ⊃ G⟧ (⊆)), and □𝔉_{1}(S4_{Σ} ⟦F ⟧ (⊆)) retracts strongly onto 𝔉_{1}(S4_{Σ} ⟦□F ⟧ (⊆)), where ⊆ is the canonical inclusion of Σ into S4_{Σ}.

Assume finally that 𝔉_{1} is faithful on morphisms with domain the empty context. Then there is a valuation ρ_{2} : Σ → D such that, for every λ_{S4}-terms M and N

of type F under Γ, M ≈ N if and only if D ⟦M⟧ ρ_{2} = D ⟦N⟧ ρ_{2}.

Proof. The only if direction is soundness (Lemma 57). Let us deal with the if direction. Without loss of generality, assume M and N ground, and Γ the empty context: if Γ is not empty, say Γ ˆ=x_{1} : F_{1}, …, x_{n} : F_{n}, we reduce to the empty case by reasoning on λx_{1}, …, x_{n} · M and λx_{1}, …, x_{n} · N instead of M and N. Take C_{1} ˆ=S4_{Σ}, ρ_{1} be ⊆. As in Lemma 71, let ρ_{2} be 𝔉_{1} ∘ ρ_{1}, and ρ̃ map A ∈ Σ to (ρ_{2}(A), (ρ_{1}(A), ρ_{2}(A)), ⟨id, id⟩).

By the Basic Lemma (Lemma 70),

U((D↓^{∩}(𝔉_{1} ⊗ id)) ⟦F ⟧ ρ̃) = (S4_{Σ} ⟦F ⟧ ρ_{1}, D ⟦F ⟧ ρ_{2})

where the forgetful functor U maps each morphism (u, v) in the subscone to v. Expanding the definition of U in this case, for every type derivation of ⊢ M : F, the morphism (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦M⟧ ρ̃ from 1 to (D↓^{∩}(𝔉_{1} ⊗ id)) ⟦F ⟧ ρ̃ can be written (u, v), where the Basic Lemma demands that v = S4_{Σ} ⟦M⟧ ρ_{1} × D ⟦M⟧ ρ_{2}. Since (u, v) is a morphism in D↓^{∩}(𝔉_{1} ⊗ id), the following diagram commutes:

\begin{aligned}1 & ^{⊂}  id  ≻ & 1 \\ D_{F} & \begin{matrix}u \\ ⋎ \end{matrix} & ^{⊂}  ⟨m′_{F} , m′′_{F} ⟩≻ & 𝔉_{1}(S4_{Σ} ⟦F ⟧ ρ_{1}) × D ⟦F ⟧ ρ_{2} & \begin{matrix}𝔉_{1}(S4_{Σ} ⟦M⟧ ρ_{1}) & ×D ⟦M⟧ ρ_{2} \\ ⋎ \end{matrix} \end{aligned}

That is,

m′_{F} ∘ u = 𝔉_{1}(S4_{Σ} ⟦M⟧ ρ_{1}) m′′_{F} ∘ u = D ⟦M⟧ ρ_{2}

By the Bounding Lemma (Lemma 71, Diagram (29)), p_{F} ∘ m′′_{F} = m′_{F}, so:

𝔉_{1}(S4_{Σ} ⟦M⟧ ρ_{1}) = p_{F} ∘ D ⟦M⟧ ρ_{2}

As this holds for every M such that ⊢ M : F is derivable, it follows immediately that if we take any two such terms M and N, such that D ⟦M⟧ ρ_{2} = D ⟦N⟧ ρ_{2}, then 𝔉_{1}(S4_{Σ} ⟦M⟧ ρ_{1}) = 𝔉_{1}(S4_{Σ} ⟦N⟧ ρ_{1}). Since 𝔉_{1} is faithful on morphisms with domain the empty context, S4_{Σ} ⟦M⟧ ρ_{1} = S4_{Σ} ⟦N⟧ ρ_{1}. Since ρ_{1} = (⊆), by Proposition 63, M ≈ N.

Corollary 73 (Equational Completeness in Δ̂). There is a valuation ρ_{2} : Σ → Δ̂ such that, for every λ_{S4}-terms M and N of type F under Γ, M ≈ N if and only if Δ̂ ⟦M⟧ ρ_{2} = Δ̂ ⟦N⟧ ρ_{2}.

Proof. Let us check all hypotheses. First, Δ̂ is a strict CS4 category using Definition 50. Take 𝔉_{1} ˆ=S4 [ ] (alternatively, the contracting resolution functor CRes_{S4_{Σ}}). By Lemma 64, 𝔉_{1} preserves all finite products and the (□, d, s) comonad (so the canonical isomorphism from 𝔉_{1}(□c) to □𝔉_{1}(c) is a distributivity law ℑ^{1} of 𝔉_{1} wrt. □ along which □ preserves all pullbacks, too), and is faithful. Δ̂ is finitely complete (in fact a topos). And □ preserves monos: recall that a mono in Δ̂ is an a.s. map (f_{q})_{q⩾−1} such that every f_{q} is one-to-one ([15] 1.462); it follows that □, which maps (f_{q})_{q⩾−1} to (f_{q+1})_{q⩾−1}, preserves monos in Δ̂. □𝔉_{1}(S4_{Σ} ⟦F ⟧ (⊆)) retracts strongly onto 𝔉_{1}(S4_{Σ} ⟦□F ⟧ (⊆)), because they are canonically isomorphic. Finally, by Corollary 48, HomΔ̂(𝔉_{1}(S4_{Σ} ⟦F ⟧ (⊆)), 𝔉_{1}(S4_{Σ} ⟦G⟧ (⊆))) retracts strongly onto 𝔉_{1}(S4_{Σ} ⟦F ⊃ G⟧ (⊆)) (observe that 𝔉_{1}(S4_{Σ} ⟦F ⟧ (⊆)) = S4 [F], and similarly for G).

The case of topological models, or variants thereof, is still open.

Acknowledgments

The first author wishes to thank the people attending the Types’98 workshop, where he talked about a few ideas that eventually led to this work; among which Michael Mendler, Healfdene Goguen and James McKinna. We would also like to thank Tim Porter and Rajeev Goré for fruitful discussions, and Dana Scott, Sergei Artëmov, Eugenio Moggi, Grigori Mints and Valeria de Paiva, and the anonymous referees on an earlier version of this work for their remarks. We acknowledge Paul Taylor, whose diagrams package was used to draw the diagrams in this paper.

References

[1] Moez Alimohamed, A characterization of lambda definability in categorical models of implicit polymorphism, Theoretical Computer Science 146 (1995), no. 1–2, 5–23.

[2] Henk Barendregt, The lambda calculus, its syntax and semantics, Studies in Logic and the Foundations of Mathematics, vol. 103, North-Holland Publishing Company, Amsterdam, 1984.

[3] Kalyan Basu, The geometry of sequential computation I: A simplicial geometry of interaction, Institutsbericht, Technische Universität München, Institut für Informatik, August 1997.

[4] , The geometry of sequential computation II: Full abstraction for PCF, Institutsbericht, Technische Universität München, Institut für Informatik, August 1997.

[5] Alan Bawden and Jonathan Rees, Syntactic closures, 1988 ACM Conference on Lisp and Functional Programming, 1988, pp. 86–95.

[6] P. Nick Benton, Gavin M. Bierman, and Valeria C. V. de Paiva, Computational types from a logical perspective, Journal of Functional Programming 8 (1998), no. 2, 177–193.

[7] Gavin M. Bierman and Valeria de Paiva, Intuitionistic necessity revisited, Logic at Work (Amsterdam, the Netherlands), 1992, Revised version, Technical Report CSR-96-10, University of Birmingham, June 1996.

[8] Anders Björner, Topological methods, Handbook of Combinatorics (R. Graham, M. Grötschel, and L. Lovász, eds.), vol. 2, Elsevier Science B.V., 1995, pp. 1819–1872.

[9] Stephen Brookes and Shai Geva, Computational comonads and intensional semantics, Applications of Categories in Computer Science, Proceedings of the LMS Symposium (Durham) (M. P. Fourman, P. T. Johnstone, and A. M. Pitts, eds.), London Mathematical Society Lecture Notes, 1991.

[10] Pierre-Louis Curien, Categorical combinators, sequential algorithms, and functional programming, 2nd ed., Progress in Theoretical Computer Science, Birkhäuser, Boston, 1993.

[11] Rowan Davies and Frank Pfenning, A modal analysis of staged computation, 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 21–24 January 1996, pp. 258–270.

[12] Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation 3 (1987), 69–116.

[13] Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite systems, Handbook of Theoretical Computer Science (Jan van Leeuwen, ed.), Elsevier Science Publishers b.v., 1990, pp. 243–320.

[14] Philip J. Ehlers and Tim Porter, Joins for (augmented) simplicial sets, Bangor Maths Preprint 98.07, Bangor University, February 1998, Submitted to the Journal of Pure and Applied Algebra.

[15] Peter J. Freyd and Andre Scedrov, Categories, allegories, North-Holland Mathematical Library, vol. 39, North-Holland, Amsterdam, 1990.

[16] Harvey Friedman, Equality between functionals., Logic Colloquium 1972-73 (Rohit Parikh, ed.), Lecture Notes in Mathematics, vol. 453, Springer-Verlag, 1975, pp. 22–37.

[17] Jean-Yves Girard, Linear logic, Theoretical Computer Science 50 (1987), 1– 102.

[18] Jean-Yves Girard, Yves Lafont, and Paul Taylor, Proofs and types, Cambridge Tracts in Theoretical Computer Science, vol. 7, Cambridge University Press, 1989.

[19] Healfdene Goguen and Jean Goubault-Larrecq, Sequent combinators: A Hilbert system for the lambda calculus, Mathematical Structures in Computer Science 10 (2000), no. 1, 1–79.

[20] Jean Goubault-Larrecq, On computational interpretations of the modal logic S4 I. Cut elimination, Interner Bericht 1996-35, University of Karlsruhe, 1996.

[21] , On computational interpretations of the modal logic S4 II. The λ ev Q-calculus, Interner Bericht 1996-34, University of Karlsruhe, 1996.

[22] Jean Goubault-Larrecq and Éric Goubault, Order-theoretic, geometric and combinatorial models of intuitionistic S4 proofs, Presented at the 1st Workshop on Intuitionistic Modal Logics and Applications, Trento, Italy; also at the 1st Workshop on Geometric Methods in Concurrency Theory, Aalborg,

Denmark. Available at http://www.dyade.fr/fr/actions/vip/jgl/top.ps.gz, June

1999.

[23] , On the geometry of intuitionistic S4 proofs, Research Report LSV-01-8, Laboratoire Spécification et Vérification, ENS Cachan, France, Novem-

ber 2001, 107 pages, available at http://www.lsv.ens-cachan.fr/Publis/
RAPPORTS LSV/rr-lsv-2001-8.rr.ps.

[24] Jean Goubault-Larrecq, Sławomir Lasota, and David Nowak, Logical relations for monadic types, Proceedings of the 16th International Workshop on Computer Science Logic (CSL’02) (Edinburgh, Scotland), Springer-Verlag Lecture Notes in Computer Science, 2002, To appear.

[25] Marco Grandis, Homotopical algebra in homotopical categories, Applied Categorical Structures 2 (1994), 351–406.

[26] Timothy G. Griffin, A formulas-as-types notion of control, Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages (San Francisco, California), January 1990, pp. 47–58.

[27] Mauric Herlihy and Sergio Rajsbaum, Algebraic topology and distributed computing—A primer, Computer Science Today, Recent Trends and Developments (Jan van Leeuwen, ed.), Lecture Notes in Computer Science, vol. 1000, Springer-Verlag, 1995, pp. 203–217.

[28] Jonathan P. Hindley and J. Roger Seldin, Introduction to combinators and λ-calculus, London Mathematical Society Student Texts, vol. 1, Cambridge University Press, 1988.

[29] William A. Howard, The formulae-as-types notion of construction, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism (J. R. Hindley and J. P. Seldin, eds.), Academic Press, 1980, pp. 479–490.

[30] Gérard P. Huet, A unification algorithm for typed λ-calculus, Theoretical Computer Science 1 (1975), 27–57.

[31] Jean-Pierre Jouannaud and Claude Kirchner, Solving equations in abstract algebras: a rule-based survey of unification, Tech. report, LRI, CNRS UA 410: Al Khowarizmi, March 1990.

[32] Satoshi Kobayashi, Monad as modality, Theoretical Computer Science 175 (1997), no. 1, 29–74.

[33] Joachim Lambek and Phil J. Scott, Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics, vol. 7, Cambridge University Press, 1986.

[34] Pierre Leleu, A modal lambda calculus with iteration and case constructs, Technical Report RR-3322, Institut National de Recherche en Informatique et en Automatique (Inria), France, 1997.

[35] John Mac Carthy, P.W. Abrahams, D.J. Edwards, T.P. Hart, and M.I. Levin, LISP 1.5 programmer’s manual, MIT Press, 1962.

[36] Saunders Mac Lane, Categories for the working mathematician, Graduate Texts in Mathematics, vol. 5, Springer-Verlag, 1971.

[37] Simone Martini and Andrea Masini, A modal view of linear logic, Journal of Symbolic Logic 59 (1994), no. 3, 888–899.

[38] , A computational interpretation of modal proofs, Proof Theory of Modal Logic (H. Wansing, ed.), Kluwer, 1996, pp. 213–241.

[39] J. Peter May, Simplicial objects in algebraic topology, Chicago Lectures in Mathematics, The University of Chicago Press, 1967.

[40] John C. Mitchell, Foundations for programming languages, MIT Press, 1985.

[41] John C. Mitchell and Andre Scedrov, Notes on sconing and relators, Computer Science Logic ’92, Selected Papers (E. Boerger et al., ed.), 1993, Available by anonymous ftp from host ftp.cis.upenn.edu and the file pub/papers/scedrov/rel.dvi, pp. 352–378.

[42] Michel Parigot, λμ-calculus: an algorithmic interpretation of classical natural deduction, 3rd International Conference on Logic Programming and Automated Reasoning (Saint-Petersburg, USSR), Lecture Notes in Computer Science, vol. 417, Springer Verlag, July 1992.

[43] Frank Pfenning and Rowan Davies, A judgmental reconstruction of modal logic, Invited talk, 1st Workshop on Intuitionistic Modal Logics and Applications, Trento, Italy., July 1999, Submitted to Mathematical Structures

in Computer Science. Available at http://www-2.cs.cmu.edu/~fp/papers/
mscs00.ps.gz.

[44] Frank Pfenning and Hao-Chi Wong, On a modal λ-calculus for S4, 11th Conference on Mathematical Foundations of Programming Semantics, 1995, Extended Abstract.

[45] Gordon Plotkin, Call-by-name, call-by-value and the λ-calculus, Theoretical Computer Science 1 (1975), no. 2, 125–159.

[46] Tim Porter, Letter to the authors and Rajeev Goré, August 04th 1999, Available from T. Porter or the authors.

[47] Dag Prawitz, Natural deduction, a proof-theoretical study, Almqvist and Wiskell, Stockholm, 1965.

[48] M. E. Szabo, The collected papers of Gerhard Gentzen, North-Holland Publishing Company, Amsterdam, 1969.

[49] Daniele Turi, Functorial operational semantics and its denotational dual, Ph.D. thesis, Free University, Amsterdam, June 1996.

[50] Philip Wickline, Peter Lee, and Frank Pfenning, Modal types as staging specifications for run-time code generation, ACM SIGPLAN Notices 33 (1998), no. 5, 224–235.

[51] Frank Wolter and Michael Zakharyashev, Intuitionistic modal logic, Tech. report, The Institute of Computer Science, January 1999, To appear in Logic

     in Florence, 1995. Available at http://www.informatik.uni-leipzig.de/
     ~wolter/paper11.ps.

[52] Houman Zolfaghari and Gonzalo E. Reyes, Topos-theoretic approaches to modality, Category Theory, Lecture Notes in Mathematics, vol. 1488, Springer-Verlag, Como, Italy, 1990, pp. 359–378.

This article may be accessed via WWW at http://www.rmi.acnet.ge/hha/ or by anonymous ftp at

ftp://ftp.rmi.acnet.ge/pub/hha/volumes/2003/n2a6/v5n2a6.(dvi,ps,pdf)

Jean Goubault-Larrecq goubault@lsv.ens-cachan.fr
http://www.lsv.ens-cachan.fr/~goubault/

LSV/CNRS UMR 8643 & ENS Cachan 61, av. du président-Wilson F-94235 Cachan Cedex

Éric Goubault goubault@aigle.saclay.cea.fr
http://www.di.ens.fr/~goubault/

CEA (Recherche Technologique) LIST/DTSI/SLA F-91191 Gif-sur-Yvette