Equideductive Categories and their Logic

Paul Taylor

22 August 2013

1 Introduction

In this paper we study the interaction between equalisers and exponentials. Since these are both defined as right adjoints, their universal properties can be combined into a single one, so it is surprising that something as elementary as this seems not to have been investigated before in the categorical literature. Of course these structures co-exist in a topos or a locally cartesian closed category, but we are going to study less powerful structures with a view to managing the complexity that arises from this interaction. The equideductive categories that we shall introduce are not themselves cartesian closed but are embedded “in a nice way” in cartesian closed extensions.

Notation 1.1 We would like to write

[figure: {x : X | ∀y:Y . αxy = βxy}; X; α; β; Σ^{Y}]

for an equaliser targeted at an exponential. Then, if Y is itself the equaliser of γ, δ : B ⇉ Σ^{Z}, we also want to use the notation recursively, for example

{x : X | ∀y:B. (∀z:Z. γyz = δyz) =▷ αxy = βxy}.

The principal objective of this paper is to introduce a symbolic calculus that justifies these expressions. It is set out in Section 9.

This is an external logic of subobjects (constructions with equalisers etc.) that can be formulated in a suitable category. It does not assume that the category has a subobject classifier with its internal logic. Whilst the key object Σ will become the Sierpiński space or the subobject classifier in the leading examples of topology, set theory or recursion theory, the agreement between the internal and external logics must obviously depend on some additional property of Σ. We shall study this in a later paper [DD].

The universal property of the equaliser above can be expressed in a way that involves the product X × Y instead of the exponential Σ^{Y}. In the absence of a better name, we call this a “partial product”. We show in the next section how it captures infinitary intersections and universal quantification, as well as equalisers of exponentials in cartesian closed super-categories such as the Yoneda embedding.

Notice, before we begin to formalise Notation 1.1 as part of a new calculus, that these expressions with ∀ and =▷ are less general than we are accustomed to using elsewhere in logic:

Definition 1.2 Any expression ∀y. 𝔮(y) =▷ αxy = βxy that arises from equalisers of exponentials obeys the variable-binding rule:

every free variable that occurs in the antecedents (i.e. on the left) of =▷

must be bound by the quantifier.

Variables that only occur on the right of =▷ may remain free.

The reason why this happens is that the variables range over objects X and Y that are themselves fixed types, instead of being type-expressions that involve variables that range over other types. A type theorist or categorical logician may object that we are just being lazy here. The former would rewrite the fixed type Y as a dependent one Y [x], whilst the latter would implement this by replacing the product projection π_{0} : X × Y → X with a arbitrary map in the definition of a partial product.

We freely confess that we would like to avoid dependent types until we fully understand the situation without them. However, there are also more substantial reasons for adopting this rule, namely that such changes would yield a theory that is only suitable for set theory and not topology or recursion. The relevant counterexample is given in [BB], which also shows that we cannot ask for exponentials in every slice category, or dependent products with arbitrary parameters.

In fact, some of the results in our theory are only valid for predicates that satisfy the variablebinding rule. This is the case in particular for Lemma 10.12 here and for the properties of the “existential quantifier” � that we introduce in [BB]. On the other hand, it will be no handicap in [?], where we show that any equideductive category may be embedded in a very simple way into a cartesian closed one, because that construction will only use expressions that obey this rule.

Somewhat miraculously, several of the limitations that the rule imposes on the expressivity of the logic will be relaxed in [DD], where we add the lattice structure to Σ and require its order relation to agree with equideductive implication (=▷). For example, we find that there that variables whose type is discrete or Hausdorff are exempt from the variable-binding rule. This means that we shall not even need to modify this rule in our basic definition of partial products when we characterise set theory (i.e. the situation in which the category is an elementary topos) using equideductive logic.

Remark 1.3 Even though we do not ask that Σ be a lattice in this paper, we shall include some of the other categorical properties of the Sierpiński space and the subobject classifier in the definition of an equideductive category in Section 4, besides the interaction of equalisers of exponentials.

Consider the nested use of Notation 1.1 above. Although the main equation αxy = βxy is only intended to place a restriction on x for each of those y for which ∀z. γyz = δyz, the terms αxy and βxy must still be well formed for all y of type B.

More generally, when we write a program αxy, we intend it to behave in a certain way so long as y belongs to some subspace Y of legal input values. Nevertheless, this program will do something given any input value of y of its syntactic type B, even if this is to print an error message or to do something disastrous.

This property has long been familiar in general topology and elsewhere:

Definition 1.4 An object I is injective with respect to the map i : U → V if, for any map f : U → I, there is some “lifting” g : V → I with f = g · i,

U[figure: i] V
[figure: f; .......; g]
I

In order to justify the nested use of Notation 1.1, we therefore require Σ to be injective with respect to the inclusion X × Y → X × B.

Warning 1.5 When the equideductive category Q is embedded in a cartesian closed category S with equalisers in [?], we shall just ask for this property for maps in Q, because it will not generalise to S. In particular, we shall not expect Σ to be injective with respect to regular monos in the Yoneda embedding of Q (Proposition 2.12).

Remark 1.6 The injectives carry all of the computation that we need, so long as there are enough of them. In the traditional semantic structures, having enough injectives just means that any object can be expressed as an equaliser of them. However, if we look for examples based on recursion theory instead of set theory, the subspaces are not just defined using equations but by predicates with increasingly many alternating quantifiers (Corollary 3.19). This example requires iterated expression of objects in terms of injectives that must be reflected in both our categorical definition and the calculus that we introduce here.

Remark 1.7 Something else that we rather took for granted in writing αxy in Notation 1.1 was the λ-calculus. At least, we shall ask for exponentials of the form Σ^{A} for some sufficiently rich collection of objects A, although not the whole of the category. In topology, we are thinking of A as a locally compact space, whose topology is the exponential Σ^{A}, which is injective and is a continuous distributive lattice with the Scott topology. In recursion theory there is a similar object to the Sierpiński space that tests termination of programs. Whilst the category of affine varieties over a field has partial products, it does not have these exponentials.

The underlying form of computation using powers of Σ (as opposed to general exponentials) is called the restricted λ-calculus. The Abstract Stone Duality programme added lattice structure to this to provide a language for computably based locally compact topological spaces. From a symbolic perspective, injectivity will allow us to continue to use this language for the terms of our new logic. Then equations between such terms will provide the “atomic” predicates, and partial products a logic with ∀ and =▷ based on these. Therefore, even though the new programme will take us beyond locally compact spaces, they will still play a central role.

Hence the equideductive world consists of three nested categories, A ⊂ Q ⊂ S, whose objects loosely play the roles of locally compact, sober and equilogical spaces respectively in the more concrete models that are found in the existing literature. Categorically, A has exponentials Σ^{(−)} but not equalisers, whilst Q has equalisers but not exponentials, and S has both.

The category of affine varieties over a field K (the opposite of the category of commutative K-algebras and homomorphisms) has partial products when we take Σ to be the field as a variety (corresponding to the algebra of polynomials K[x] in one variable). There are also enough injectives as below. However, there are not enough exponentials, so maybe some other reification of functions is needed in this application.

Remark 1.8 Having collected these semantic ideas, we can begin to introduce some syntax for them. Section 5 presents the rules of the restricted λ-calculus that provides the object language of equideductive logic. Section 6 shows that these are equivalent to a category with products and exponentials of the form Σ^{A}. Whilst this material is familiar, we choose slightly different rules from the usual ones, because they will be more convenient in equideductive logic. The equivalence also provides a plan for the same task in the logic. We give the name urterm to the λ-terms because we use them as codes, whilst the morphisms of the categories that we construct are partial equivalence classes of urterms. Similarly, the objects of A are called urtypes in the syntax and urspaces in a concrete setting.

Section 7 shows that any urspace (exponentiable object) of an equideductive category is sober in the abstract sense that was introduced in [A]. That paper also showed that sobriety for ℕ is equivalent to definition by description, whilst it is Dedekind completeness for ℝ [I], so this concept is very important for expressing ordinary mathematics. Section 8 builds it in to the λ-calculus using the focus operation.

Remark 1.9 However, the focus operation leads to a lot of complications in the proof theory and other aspects of foundations, so we devote a lot of effort into removing them. There are two possible approaches to presenting a new calculus when one of the major goals is then to eliminate some of its features. One is to give a rich formulation that would be suitable for applications but prove theorems such as cut elimination to show that certain parts are redundant. This would, however, create unnecessary difficulties for our main task, which is to interpret the logic in a suitable category and then to show that the two are equivalent.

We shall therefore do the opposite, giving a relatively poorer formulation first and then showing how extra features such as focus can be added as definitional extensions. Both here and in later work, we take advantage of the minimal syntax to bootstrap mathematical applications in this way.

Those who are experienced in proof theory will be aware that these two ways of proceeding are equivalent. However, our situation is a good deal simpler than the classic case of eliminating cut from the sequent calculus (Gerhard Gentzen’s so-called Hauptsatz). Each of our definitional extensions (or, if you prefer, elimination lemmas) relates a richer calculus to one that is obviously simpler, whilst the lower-level versions of the proofs are not much longer than the ones in the more expressive language. This could, therefore, be seen as a simple one-pass translation that, when implemented on a machine, might be done “on the fly” during analysis of the input syntax.

Specifically, Section 8 only introduces focus axiomatically for base types and then defines it for products and exponentials. We also show how to substitute for and into focus-terms and how to apply other terms to them. This culminates in a partial normalisation theorem saying that focus is only needed once, on the outside of a term. Hence the bulk of a computation is expressed using “logical” urterms in the restricted λ-calculus. The focus operation, which is equivalent to definition by description for integers, drives this computation by demanding a result that satisfies the relevant property.

Remark 1.10 Section 9 graduates from the λ-calculus object language to equideductive logic itself. It is a kind of predicate calculus with ∀, =▷ and &. An extensionality law is used instead of the η- and equality-transmitting rules for the λ-calculus. At first we leave focus out of the object language because it involves more proof-theoretic complications, but we add it back in again and deal with these in Section 10.

Section 11 defines the interpretation of equideductive logic in an equideductive category. Conversely, Section 12 constructs the classifying category from the logic, using injective urtypes for simplicity. Then Section 13 shows how to extend pure equideductive logic to match any given equideductive category.

In Section 14 we introduce a “comprehension” syntax with a curly-bracket notation that makes a type from an urtype with a predicate. This way of introducing subobjects is what ordinary mathematicians seem to mean when they claim that they use “set theory” as the foundation for their subject. We will be able to use the same notation and methods of reasoning, although our predicate calculus is of course much weaker than the usual one.

This notation has numerous mathematical applications. In this paper we use it to complete the discussion of the classifying category and to construct those exponentials that exist. Equideductive logic without focus is a rather feeble fragment of type theory, but with it we have quite a natural proto-set theory, in which sobriety handles functions that are only conditionally defined.

Definition 1.11 Equideductive logic will have its own story to tell about equality in terms of deductions of equations. Before it does so, we shall need to consider various other notions. We shall therefore say that morphisms of a category are the same, whilst λ-terms are interchangeable.

2 Partial products

The universal property that provides the categorical basis for Notation 1.1 brings together various ideas of intersections of families of subobjects, universally quantified implication and equalisers of exponentials. Throughout, we work in a category Q that has all finite limits.

Definition 2.1 The map i : E → A is called (the inclusion of) the partial product of the parallel pair α, β : A × Y ⇉ Σ if

(a) the composites E × Y → A × Y ⇉ Σ are the same; and

(b) whenever a : Γ → A is another map for which the composites Γ × Y → A × Y ⇉ Σ are the

same, there is a unique map e : Γ → E such that a is the same as the composite i · e. E

[figure: .................; e; i]
[figure: Γ; a; A]

E × Y
[figure: .................; e × Y; i × Y]
[figure: Γ × Y; π_{0}; a × Y; A × Y; π_{0}; α; β; Σ]

Although partial products seem rather hybrid at first sight, they have arisen in numerous different contexts. The original one was a notion of dimension in topology, where it explained how the sphere S^{n+m} ⊂ ℝ^{n+m+1} is the “product” of spheres S^{n} and S^{m} [Pas65]. In categorical type theory, general dependent products (as in a locally cartesian closed category) can be reduced to partial products [Tay99, Thm 9.4.14]. For further background information on this notion, see [Nie82, DT87]

Beware, however, that the property above is a slightly modified special case of the standard formulation. Although we shall use this term throughout this paper, if you wish to refer to the idea, please repeat this warning that our usage is not standard.

We could perhaps call our notion a partial equaliser instead, but that would only evade the fact that these ideas really need a better name.

Example 2.2 The notion of partial product can be used to express the “external” intersection of a family of subobjects in a purely categorical way, without using the internal logic of Ω in a topos.

Let {U_{y} ⊂ A | y ∈ Y } be a family of subobjects of an object A, indexed by another object Y. Getting away from the set-theoretic notion of collection, we can encode this family as a single subobject V ≡ {(y, a) | a ∈ U_{y}} ⊂ A × Y. Suppose that the inclusion V ⊂ A × Y is a regular mono, i.e. the equaliser of some pair α, β : A × Y ⇉ Σ.

Now consider when another subobject Γ ⊂ A is contained in the intersection of the family:

Γ ⊂ ⋂_{y∈Y} U_{y} ⟺ ∀γ ∈ Γ. ∀y ∈ Y . γ ∈ U_{y}
⟺ ∀γ ∈ Γ. ∀y ∈ Y . (γ, y) ∈ V
⟺ Γ × Y ⊂ V
⟺ ∀γ ∈ Γ. ∀y ∈ Y . α(γ, y) = β(γ, y)
⟺ the composites Γ × Y → A × Y ⇉ Σ are the same.

The last line is the hypothesis of clause (b) in the definition of a partial product, so this gives a map Γ → E. The intersection ⋂ U_{y} is the greatest such Γ, namely E, because Γ has the above properties iff Γ ⊂ E. This is the special case of the universal property with an inclusion Γ ⊂ A rather than a general map Γ → A. □

Motivated by this example, we make the

Definition 2.3 By a subspace we shall mean a map i : E ↣ A that (is isomorphic to one that) arises as i : E → A in some partial product diagram.

Notwithstanding Lemmas 2.14 and 4.7, beware that this map need not in general be expressible as an equaliser E ↪ A ⇉ K. This is because there need not be any suitable target object K (such as the cokernel, i.e. the pushout of E → A against itself) in the category Q. The difference between equalisers and partial products is on of logical complexity, as we shall see from the recursive model in the next section.

We write M ⊂ Q for the class of subspace maps. When we use the word “subspace”, we expect this class to be a dominion [Ros86]:

(a) all isomorphisms should be M-maps;

(b) the maps in M should be monos;

(c) the pullback of an M-map along any map should again be an M-map; and

(d) the composite of any two M-maps should also be one.

We consider the last property in Section 4, but we can already prove the first three:

Lemma 2.4 If Σ has a point ⋆ : 1 → Σ then id_{A} : A ↣ A (or any isomorphism A′ ≅ A) is the partial product of ⋆, ⋆ : A × 1 ⇉ Σ. □

Lemma 2.5 Any subspace map E → A is mono. Proof Let e, e′ : Γ ⇉ E be such that a ≡ i · e is the same as i · e′. Then the morphisms

α · (a × Y), α · (i · e × Y),  α · (i × Y) · (e × Y),
β · (i × Y) · (e × Y) and β · (a × Y)

are the same, so a satisfies the pre-condition required for the universal property. Hence there is a unique e : Γ → E for which i · e is that same as a, which means that e′ is the same as e. □

Lemma 2.6 Partial product diagrams are stable under pullback.

F  \overline{}E
[figure: .........; j; ........................................; i]
[figure: Γ; C; u; A]

F × Y  \overline{}E × Y
[figure: .........]
[figure: Γ × Y; C × Y; u × Y; A × Y; α; β; Σ]

Proof Suppose that i : E ↣ A is the partial product of α, β : A × Y ⇉ Σ and let u : C → A be any map.

First suppose that the parellelogram at the top is a pullback. Given a map Γ → C with equal composites to Σ, there is a map Γ → E since E is a partial product and then Γ → F since F is a pullback.

Conversely, if F is formed as a partial product and we have maps Γ → C and Γ → E commuting at A then their composites to Γ are equal and the mediator Γ → F is given by the universal property of F as a partial product. Hence F is also a pullback. □

Such pullbacks of subspaces are traditionally known as inverse images. More abstractly, this result makes M a class of display maps [Tay99, Def. 8.3.2] that admits universal quantification along binary product projections. Syntactically, it will allow substitution for the free variable of type A in α and β.

Remark 2.7 Let i_{1} and i_{2} be the partial products of A × Y_{1} ⇉ Σ and A × Y_{2} ⇉ Σ. Then the intersection i_{1} ∩i_{2} is the partial product of A×(Y_{1} +Y_{2}) ⇉ Σ. That is, so long as the coproduct Y_{1} + Y_{2} exists in Q and A × (−) distributes over it. However, instead of relying on this, we shall treat intersection alongside partial product as a basic operation on subspaces.

If pullbacks are inverse images, what is the direct image for this notion of subspace?

Definition 2.8 A map e : Δ → Γ is Σ-epi if, for any object Y and maps ϕ, ψ : Γ × Y ⇉ Σ for which the composites ϕ · (e × Y) and ψ · (e × Y) are the same then ϕ and ψ were already the same.

Many roles have already been found in classical and synthetic domain theory [Hyl91, Tay91] for Σ-epis that are not surjective. The reason why we reject presheaf and PER models as “set theory” is that we intend to take the class of Σ-epis seriously and develop an “existential quantifier” � for them in [BB].

Proposition 2.9 The class E of Σ-epis is orthogonal to that of partial product inclusions (M). This means that, in any commutative trapezium (on the top face of the cube, i · f and g · e are the same), there is a unique fill-in v : Γ → E that makes the two triangles commute.

Δ  \overline{f} E
[figure: e; ..............; v; i]
[figure: Γ; g; A]

[figure: Δ × Y; π_{0}; f × Y; E × Y]
[figure: e × Y; ..............; v × Y; i × Y]
[figure: Γ × Y; π_{0}; g × Y; A × Y; π_{0}; α; β; Σ]

Proof Since the trapezium commutes and we have a partial product diagram, all paths from Δ × Y to Σ have the same composite. Then, since e is Σ-epi, the composites Γ × Y ⇉ Σ are also the same. Hence we may invoke the universal property of the partial product, which provides a unique v for which i · v is the same as g. Also, v · e is the same as f because i is mono. □

Remark 2.10 Whilst epis in a cartesian closed category are always stable under product, beware that a map may be epi in a subcategory without being epi in an enclosing category. Conversely, we are about to show how partial products capture equalisers of exponentials, so the class M consists of regular monos in the enclosing CCC, but these need not be expressible as equalisers in the subcategory.

The existence of partial products is not sufficient to make the class of Σ-epis stable under product, but this will follow from the other axioms that we shall add to definition of an equideductive category in Section 4. We shall find in [BB] that Σ-epis in such a category are the same as epis in the usual sense and that every morphism factorises as a Σ-epi followed by a partial product inclusion. In other words, these two classes form a factorisation system, in which orthogonality is the universal property.

Now we can return to partial products and enclosing CCCs, cf. Definition 4.3.

Lemma 2.11 Suppose that the exponential Σ^{Y} exists. Then the map E → A is the partial product of α, β : A × Y ⇉ Σ iff it is the equaliser of their exponential transposes A ⇉ Σ^{Y}.

E
[figure: ........................; e; i]
[figure: Γ; a; A; α̃; β̃; Σ^{Y}]
E × Y
[figure: ........................; i × Y]
[figure: Γ × Y; a × Y; A × Y; α̃ × Y; β̃ × Y; Σ^{Y} × Y]
[figure: α(a, y) = β(a, y)]

[figure: Σ; α; β; ev]

Proof By the defining universal property of the exponential Σ^{Y}, the transpose of the common composite Γ × Y → A × Y ⇉ Σ in the lower triangle is the common composite Γ → A ⇉ Σ^{Y} in the upper part of the diagram, but this tests the equaliser E. □

Notice that ev played no role in this proof. We do not need an enclosing cartesian closed category or the right-hand column of the diagram but can instead concentrate on the partial products in a subcategory.

In order to show the converse, i.e. that partial products may always be seen as equalisers of exponentials in some enclosing cartesian closed category, we use the Yoneda embedding into a presheaf category. This takes us into the traditional set-theoretic world, where we remain until the end of the next section, but after that the remainder of the paper avoids it. The construction of an enclosing cartesian closed category that we give in [?] is finitary and does not use set theory.

Lemma 2.12 Let Q be a small category with finite limits and partial products and S ≡ Set^{Q^{op}} be its topos of presheaves. Then the Yoneda embedding Q ↣ S, defined by Y ↦ Q(−, Y), takes partial products to equalisers of exponentials. Proof This functor is full and faithful and preserves products [Mac71] [Tay99, Thm. 4.8.12]. The value of the exponential presheaf Σ^{Y} at Γ ∈ Q must be

Σ^{Y} (Γ) ≅ Q(−, Γ) → Σ^{Y} ≅ Q(−, Γ) × Q(−, Y) → Q(−, Σ)
≅ Γ × Y → Σ ≡ Q(Γ × Y, Σ),

so Σ^{Y} ≡ Q(− × Y, Σ). Then maps α : A × Y → Σ in Q correspond bijectively to natural transformations ᾱ : Q(−, A) → Q(− × Y, Σ) ≡ Σ^{Y}. This correspondence is itself natural in A, i.e. with respect to a : Γ → A, so

α · (a × Y) = β · (a × Y) ⟺ \overline{α · (a × Y)} = \overline{β · (a × Y)} ⟺ ᾱ · a = β̄ · a.

For E to be the partial product in Q means that the first of these equations provides a unique e with a = i · i, whilst for E to be the equaliser in S means that the last does so. □

We can also characterise Σ-epis in the same terms:

Lemma 2.13 A map e : Δ → Γ in Q is Σ-epi iff the Yoneda embedding takes it to a map ē for which Σē is mono. Proof Definition 2.8 says that the action on hom-sets

Q(Γ × (−), Σ) ⟶ Q(Δ × (−), Σ)

given by pre-composition with a Σ-epi e is injective. □

The next result is a useful tool for finding partial products in some semantic categories.

Lemma 2.14 Let Q be any category with finite limits such that each object Y ∈ Q has some object SY ∈ Q and a natural 1–1 function

Q(− × Y, Σ) Q(−, SY).

Then Q has partial products and their inclusions are regular monos. Proof The required equaliser in the presheaf category Set^{Q^{op}} is

[figure: E; Q(−, A); Q(− × Y, Σ); Q(−, SY).]

Since the equaliser E′ ↣ A ⇉ SY exists in Q and the Yoneda embedding preserves it, we have E ≅ Q(−, E′), so E′ is the partial product in Q. □

Remark 2.15 The natural transformation above is an isomorphism iff SY is the exponential Σ^{Y} in Q (Definition 4.3), in which case the inverse is given by composition with ev : SY × Y → Σ. In an alternative approach to constructing cartesian closed extensions, Aurelio Carboni and Giuseppe Rosolini [CR00] define a weak exponential W of Y and Σ to be a map e : W × Y → Σ for which composition with e defines a natural transformation in the opposite direction,

Q(− × Y, Σ) [figure] Q(−, W),

that is componentwise surjective.

Another thing that we can do with categories embedded in a set-theoretic world is to form the isomorphism classes of subobjects and then collect these into a semilattice.

Notation 2.16 For any object Y ∈ Q, let Sub(Y) ≡ M/Y be the class of isomorphism classes of M-maps into Y. By Lemma 2.6, the pullback of an M-map along any f : Z → Y is another Mmap, so we have a functor with Sub(f) ≡ f^{∗} : Sub(Y) → Sub(Z). In the case f ≡ π_{0} : Y ×X → Y, f^{∗} has a right adjoint iff this is the partial product X =▷. Lemma 2.6 also says that this partial product satisfies a Beck–Chevalley condition:

[figure: X × Y′; π_{1}; Y′; Sub(X × Y′); X =▷; ⊤; \underline{×X}; Sub(Y′)]

[figure: X × Y; id × f; π_{1}; Y; f; Sub(X × Y); (id × f)^{∗}; X =▷; ⊤; \underline{×X}; Sub(Y); f^{∗}]

We shall see in [BB] that Sub(A) is a lattice with ⊤, ⊥, & and ⋎, whilst Sub(0) = 1 and Sub(X + Y) = Sub(X) × Sub(Y).

This setting also leads to partial products:

Proposition 2.17 Let Q be a category in which

(a) all finite limits exist;

(b) every map factorises as an epi followed by a regular mono;

(c) products preserve epis;

(d) considered as a semilattice map Sub(X) → Sub(X × Y) between the classes of regular monos into X and X × Y, the product (−) × Y has a right adjoint.

Then Q has partial products. □

Semilattice completeness then provides the required adjoint:

Corollary 2.18 Let Q be a complete and regularly well powered category in which regular monos compose and products preserve epis and unions of subobjects. Then Q has partial products. Proof These conditions say that Sub(X) is a set (rather than a class) and carries the structure of a complete lattice, for which (−) × Y is a homomorphism, so it has a right adjoint. □

3 Examples

Now we shall construct partial products in the categories of sets and of sober topological spaces and also in a model defined from recursion theory. The object Ω or Σ in these three categories is injective, whilst other sets, spaces and recursive types can be represented using them. These are the properties that we shall put together to give the definition of an equideductive category in the next section.

The category of all locales does not admit partial products [?], but the fact that all countably presented locales are spatial suggests that these may form another equideductive category. However, the notion of “countability” that is needed for this seems to be neither the classical one nor recursive enumerability.

Proposition 3.1 Any elementary topos Q with Σ ≡ Ω has partial products. Proof Any topos has all finite limits and exponentials. Hence it has partial products by Lemma 2.11, but it is worth spelling this out as an application of Lemma 2.14. Any morphism A×Y → Σ classifies a subobject of the rectangle A×Y, so it may also be seen as a binary relation A ↽ ⇀ Y or as a function ᾱ : A → P(Y) by

ᾱx ≡ {y | αxy}, so y ∈ ᾱx ⟺ αxy.

Moreover, this correspondence is 1–1: α = β : A × Y → Σ iff ᾱ = β̄ : A → P(Y), because this is what equality of subsets means. (It is surjective too, but this is not significant and will not happen in the other examples.) It is also natural, i.e. it respects precomposition with any map a : Γ → A:

α(az) = {y | α(az)y} = {y | (α · (a × id))zy},

so Lemma 2.14 gives the partial product.

Remark 3.2 In Example 2.2 we saw how partial products capture external intersection of families of subobjects. In a topos, suppose that the subobject V ⊂ A × Y is classified by α : A × Y → Σ, so V is the equaliser of α and β ≡ ⊤. Then the intersection E ⊂ A is classified by ∀_{Y} α ≡ ∀y ∈ Y . (α(a, y) = ⊤).

If Γ ↣ A is classified by ψ then ψ · π_{1} ⩽ α whilst ψ ⩽ ∀_{Y} α. Hence (−) · π_{1} ⊣ ∀_{Y} (−).

In the Proposition, since

ᾱx = β̄x ⟺ ∀y:Y . (y ∈ ᾱx ⇔ y ∈ β̄x) ⟺ ∀y:Y . (αxy ⇔ βxy),

the quantifier ∀ has its usual logical meaning for the set Y.

Proposition 3.3 The object Ω and in general any powerset P(A) ≡ Ω^{A} in a topos is injective. Proof Any subsubset is a subset. □

Proposition 3.4 The full subcategory of a topos whose objects are powersets is closed under finite products and exponentials Ω^{(−)}. □

Proposition 3.5 Any topos has enough injectives, in the sense that any object X may be expressed as an equaliser of powersets,

[figure: X; Ω^{A}; Ω^{B}.]  □

We can apply similar arguments to the traditional category Sp of topological spaces and continuous functions, now taking Σ to be the Sierpiński space.

Proposition 3.6 The category Sp has partial products. Proof Its maps X → Σ correspond to open subspaces of X and we write O(X) for the lattice of them. Hence maps α : A × Y → Σ classify open subspaces W ⊂ A × Y in the Tychonov topology on the product of the underlying sets. Following the previous example, we define a natural 1–1 function |A| → O(Y) by

ᾱx ≡ {y : Y | αxy} = ⋃ ; {V ∈ O(Y) | ∃U ∈ O(A). x ∈ U & U × V ⊂ W },

which yields an open subset because W is a union of open rectangles like U × V. (To see that this union is directed, consider U × V ≡ A × ∅ ⊂ W and (U_{1} ∩ U_{2}) × (V_{1} ∪ V_{2}) ⊂ W.)

In order to make ᾱ into a morphism of Q (continuous function), we need to assign a topology to the set O(Y). There are several ways of doing this, but unlike P(Y) in Set, the result only obeys the universal property of the exponential Σ^{Y} (Definition 4.3) when Y is locally compact. However, in order to apply Lemma 2.14, we only need ᾱ : A → O(Y) to be an Q-map (continuous function) that is mono and natural in A.

If V ⊂ O(Y) is a Scott open family of open subspaces then

ᾱ^{−1}(V) = {x ∈ A | ⋃ ; {V ∈ O(Y) | ∃U ∈ O(A). x ∈ U & U × V ⊂ W } ∈ V}
= {x ∈ A | ∃V ∈ V. ∃U ∈ O(A). x ∈ U & U × V ⊂ W }
= ⋃ {U ∈ O(A) | ∃V ∈ V. U × V ⊂ W } ⊂ A

is open too, so ᾱ is continuous. It is mono and natural because this is the case for points, so once again ∀ is the ordinary universal quantifier. □

Proposition 3.7 The Sierpiński space Σ and more generally any continuous lattice with the Scott topology is injective with respect to subspace inclusions [Sco72]. □

Proposition 3.8 The full subcategory of algebraic lattices with the Scott topology is closed under finite products and exponentials Σ^{(−)}. □

However, we have to modify our choice of category:

Proposition 3.9 A space X may be expressed as an equaliser of algebraic lattices,

[figure: X; Σ^{A}; Σ^{B},]

iff it is sober (in the traditional sense, rather than our abstract one in Section 7). Proof The partial product is sober because it is given by an equaliser of sober spaces, which form a reflective subcategory [Joh82, Cor. II 1.7(ii)]. □

Remark 3.10 Sob satisfies the previous results.

Remark 3.11 Our third example comes from recursion theory. It is a simplification of the construction of a cartesian closed category of partial equivalence relations (PERs) on a partial combinatory algebra. Indeed, the notion of equideductive category was motivated by the fact that the construction of equalisers in PER models leaves the quotient part of the PER untouched.

In order to emphasise the role of quantifier complexity, we would like to work with ℕ rather than some less familiar recursive–topological object. However, it is much more convenient to use the set 𝕋 of binary trees because 𝕋 × 𝕋 + 1 ≅ 𝕋 ≅ List (𝕋), with the usual notation [h|t] for pairs and [a, b, c, …] for lists. The lattice R of recursively enumerable subsets of 𝕋 will have to be an object in our model, and we represent it as the quotient of 𝕋 by a single equivalence relation, ∼. However, after that, we only need PERs that are subrelations of ∼.

We rely on the existing literature to provide the details of the categorical structure.

Notation 3.12 Stephen Kleene [Kle43] showed that there is a decidable primitive recursive predicate T with the following property: Any recursively enumerable or Σ_{1}^{0} predicate ϕ on 𝕋 has a Kleene normal form, i.e. some number (“program”) p such that

ϕ(x) ⟺ p̄(x) ≡ ∃h. T [p, x|h].

The predicate T and codes p are derived structurally from whatever programming language we use to define computation. We introduce special programs called combinators as needed to do this; they usually just re-arrange branches of the tree.

Inclusion between RE subsets is represented by a preorder relation between their representing programs,

(p ≼ q) ≡ (∀x. p̄(x) ⇒ q̄(x)) ≡ ∀xh. ∃k. ¬T [p, x|h] ∨ T [q, x|k],

which is a Π_{2}^{0}-formula in p, q : 𝕋. These codes represent the same RE subset iff

(p ∼ q) ≡ (p ≼ q) ∧ (q ≼ p).

The lattice R of RE subsets of 𝕋 is then the quotient poset of the preorder (𝕋, ≼).

A recursive function R → R is by definition a recursive function F : 𝕋 → 𝕋 that respects ∼. Then by Kleene’s theorem there is a program p with

∃h. T [F x, y|h] ⟺ ∃k. T [p, x, y|k].

Conversely, the (total primitive) recursive function Gx ≡ [α, p, x] gives rise to p as above, where we define a combinator α so that T [[α, p, x], y|h] ≡ T [p, x, y|h], and then F ∼ G. Hence we may use either representation.

Definition 3.13 The crude recursive model is the category of subsets of R and total computable functions between them that respect ∼.

More precisely, an object of this category is a context consisting of a finite set x⃗ of variables (of type 𝕋) and a first order predicate 𝔭(x⃗). We shall be interested in the quantifier complexity this predicate, i.e. the number of alternations of ∀ and ∃, these being allowed to range over 𝕋.

A morphism f⃗ : [x⃗, 𝔭(x⃗)] ⟶ [y⃗, 𝔮(y⃗)] is an equivalence class of sequences of computable functions f_{j}(x⃗), one for each variable y_{j}, such that

x⃗, 𝔭(x⃗)  ⊢ f⃗(x⃗)↓ and 𝔮(f⃗(x⃗))
x⃗, x′, f⃗(x⃗)↓, x⃗ ≼ x′ ⊢ f⃗(x′)↓ and f⃗(x⃗) ≼ f⃗(x′),

where f⃗ and g⃗ define the same morphism if ∀x⃗. 𝔭(x⃗) =▷ f⃗(x⃗) ∼ g⃗(x⃗).

If the morphism is represented by identity maps then it is called a crude inclusion. It is crude in the sense that it need may but need not be a partial product inclusion.

Lemma 3.14 The crude recursive model is a category in which composition is defined by substitution, whilst finite products are given by concatenation of the lists of variables and conjunction of the predicates. □

Lemma 3.15 The object R ≡ [x, ⊤] is injective with respect to crude inclusions. Moreover every object has a crude inclusion into R. □

Lemma 3.16 Σ ◁ R and Σ^{R} ◁ R, also ℕ and R = Σ^{ℕ}. □

Lemma 3.17 Equalisers are given by

[figure: [x⃗, 𝔭(x⃗) & (f⃗(x⃗) ∼ g⃗(x⃗))]; [x⃗, 𝔭(x⃗)]; f⃗; g⃗; [y⃗, 𝔮(y⃗)]; [y⃗]]

and so have the same quantifier complexity as the given objects. □

Lemma 3.18 Partial products are given by diagrams of the form

E ≡ [x⃗, 𝔭(x⃗) & 𝔯(x⃗)]  Y ≡ [y⃗, 𝔮(y⃗)]
[figure: .................; e⃗; i⃗]
[figure: Γ; a⃗; A ≡ [x⃗, 𝔭(x⃗)]]

E × Y
[figure: .................; e⃗ × Y; i⃗ × Y]
[figure: Γ × Y; π_{0}; a⃗ × Y; A × Y; π_{0}; f; g; Σ ◁ R]

where 𝔯(x⃗) ≡ ∀y⃗. 𝔮(y⃗) ⇒ f(x⃗, y⃗) ∼ g(x⃗, y⃗). Proof With 𝔯(x⃗) given in this way, the partial product obeys the rule

Γ ⊢ a⃗, 𝔭(a⃗) Γ, y⃗, 𝔮(y⃗) ⊢ fa⃗ ∼ ga⃗ ; = ; Γ ⊢ 𝔭(a⃗) & 𝔯(a⃗).  □

Corollary 3.19 The quantifier complexity of the characteristic predicates of

(a) retracts of R^{n} is decidable;

(b) open subspaces of R is at most Σ_{1}^{0};

(c) finite limits of copies of R is at most Π_{2}^{0};

(d) partial products of R is at most Π_{3}^{0}; and

(e) partial products nested k deep is at most Π_{k+2}^{0}. Therefore not all partial product inclusions (the class M) need be representable as equalisers, notwithstanding the factorisation of general maps into (product-stable) epis and partial product inclusions. □

We also give a sketch of the proof of the existence of the necessary exponentials.

Proposition 3.20 The exponential R^{R} exists in the crude recursive model and has R^{R} ◁ R. Proof We have to define a natural retraction

(f : Γ × R → R) ◁ (g : Γ → R).

It is convenient to represent morphisms by programs for recursively enumerable predicates as above and we introduce combinators λ and @ such that

T [f, γ, p, x|h] ⟺ T [[λ, f|γ], [p, x]|h] ⟺ T [@, [λ, f|γ], p, x|h].  □

Definition 3.21 The recursive model is the full subcategory consisting of objects that are definable from R using partial products. We leave it to the interested reader to characterise those first order predicates that arise in this way and find examples that do not or which require more than a specified depth of nesting.

Theorem 3.22 The recursive model is an equideductive category. □

4 Equideductive categories

The definition of an equideductive category that we shall now give was motivated by the leading examples in the previous section. In particular, although the topological and recursive model do not have general function-spaces, they do have a full subcategory A of objects A for which the exponential Σ^{A} exists and is injective. In the topological case, such spaces A are locally compact and their exponentials Σ^{A} are continuous distributive lattices with the Scott topology.

Remark 4.1 We showed in Section 2 how partial product inclusions (M-maps) can be considered as “subspaces”, but we still have to show that they compose. Considering the partial product diagram (Definition 2.1) that gives rise to the inclusion F ↣ E, we could prove this by lifting the defining maps like this:

[figure: E × B; A × B]
[figure: α; ..........]

Σ As a special case of Lemma 2.6, if E ↣ A is in M then so is E × B ↣ A × B for any object B. We what we need therefore is

Axiom 4.2 The object Σ is injective with respect to M-maps, i.e. it has the lifting property above.

If Σ is injective then so too are its exponentials Σ^{A}. But, before proving this, we state the definition because we shall need to refer to it quite frequently.

Definition 4.3 The object Σ^{A} is the exponential of A, if for any map σ : Γ × A → Σ there is a unique exponential transpose σ̃ : Γ → Σ^{A} such that ev · (σ̃ × A) is the same as σ:

[figure: Δ × A; u × A; Γ × A; σ; Σ]
[figure: ............; σ̃ × A; ev]
Σ^{A} × A

We shall call the object A exponentiable if such an exponential Σ^{A} exists. It will be important in the definition of an equideductive category that every object Γ respect the universal property of Σ^{A}, even if Γ is not itself exponentiable. The standard use of the term exponentiable requires Y^{A} for every object Y of the category; we construct this in an equideductive category in Proposition ??.

It is also convenient to write ev′ for ev with its arguments switched; then the transpose of ev′ is called η.

Lemma 4.4 Transposition is natural with respect to precomposition with u : Γ → Δ in the sense that

the transpose of σ · (u × A) is σ̃ · u.  □

Lemma 4.5 Let B be any exponentiable object. Then Σ^{B} is also injective with respect to M.

[figure: E; A]
[figure: α̃; ..........]
Σ^{B}

Proof Exponential transposition takes the triangle with vertex Σ^{B} into the one in Remark 4.1. Since the class M is closed under product with any object B and Σ is injective with respect to M-maps, there is a map A × B → Σ and so one A → Σ^{B} [Joh82, Lemma VII 4.10]. □

In order to make use of the subcategory A to work with the whole of Q we need

Axiom 4.6

There are enough injectives: each Q-object has an M-map X ↣ Σ^{B} for some exponentiable object B.

This is enough as it stands in Set and Sob, but the recursive and abstract models are more complicated. We saw in the recursive one that this complexity agrees with that of the quantifiers in the characteristic predicates. In general, X ↣ Σ^{B} may the inclusion of a partial product defined by a parallel pair Σ^{B} × Y ⇉ Σ for which Y need not be an urspace.

We therefore require that each object X be expressible, not just using a single M-map, but by a finite sequence of such steps.

Recall from Lemma 2.5 that M is contained in the class of all monos, but it also contains all regular monos:

Lemma 4.7 Every equaliser in Q is a partial product, i.e. the class M contains all regular monos. Proof The equaliser E ↣ X ⇉ Y ↣ Σ^{A} is targeted at an exponential, so it is a partial product.

□

In the traditional concrete category described in the previous section, Lemma 2.14 applies: any M-map can conversely be expressed as equaliser X ↣ Σ^{B} ⇉ Σ^{C} where both B and C belong to A. In other words, M consists exactly of the regular monos in Q.

Remark 4.8 Notice that we have tested the exponential Σ^{B} with maps from arbitrary objects E of the category Q, not just from other As; this will become very important later in this paper.

We therefore ask for closure under exponentials as an axiom:

Definition 4.9 A class of urspaces is a full subcategory A ⊂ Q of a category with finite limits and a chosen object Σ such that

(a) the objects 1 and Σ of Q belong to A;

(b) A ⊂ Q is closed under binary product; and

(c) A has exponentials Σ^{(−)} (but not necessarily all B^{A}) and objects of Q respect them, as in Definition 4.3, where each Σ^{A} also belongs to A.

There is a contrast between Q and A in that Q has equalisers but not necessarily exponentials, whilst A has exponentials Σ^{A} but not necessarily equalisers.

In this situation we get our first glimpse of how useful the new logic is, because it can say when two functions ϕ, ψ : A ⇉ Σ are equal. Beware, however, that this extensionality property must be interpreted formally in the logic: it does not mean that there are enough morphisms 1 → A to distinguish ϕ from ψ. For example, any topos has this structure, but need not be well pointed.

Lemma 4.10 Suppose that the exponential Σ^{A} exists in Q and is respected by all objects of Q. Then the partial product ∀y:A. (ϕy = ψy) is the diagonal (ϕ = ψ) of Σ^{A} × Σ^{A}.

Σ^{A}
[figure: .................; f̃; Δ]
[figure: Γ; (ϕ, ψ); Σ^{A} × Σ^{A}]

Σ^{A} × A  \overline{ev}
[figure: .................; f̃× A; Δ × A]
[figure: Γ × A; π_{0}; (ϕ, ψ) × A; Σ^{A} × Σ^{A} × A; π_{01}; ev · π_{02}; ev · π_{12}; Σ]

\overline{f}

Proof We need to show that the diagram above is a partial product, with A, Σ^{A} and Σ^{A} in place of Y, A and E in Definition 2.1. If the lower triangle commutes then ϕ and ψ are both exponential transposes of the common composite f, so ϕ = f̃ = ψ. □

Putting all of these assumptions on Q and A together, we make the

Definition 4.11 An equideductive category consists of

(a) a category Q with all finite limits;

(b) a pointed object ⋆ : 1 → Σ in Q; and

(c) a full subcategory A ⊂ Q of urspaces; such that

(d) A ⊂ Q is closed under products;

(e) Σ and all powers Σ^{A} for A ∈ A exist in Q and belong to A;

(f) Q has partial products based on the object Σ;

(g) Σ is injective with respect to all of the maps in the class M; and

(h) there are enough injectives, in the “well founded” sense of Axiom 4.6, where

(i) M is the class of monos defined by the partial products and intersections; and

(j) all objects Γ ∈ Q respect the universal properties mentioned. The point ⋆ was used in Lemma 2.4 and will be needed in [BB], but is not used again in this paper.

Examples 4.12 Set, any topos, Sob and the recursive model are equideductive categories but Loc is not.

Recall that, for the subcategory A of urspaces in each of these semantic models, there is a choice between

(a) all sets in Set or all locally compact spaces in Sob, and

(b) just the full powersets or just the algebraic lattices equipped with the Scott topology. As we move towards consideration of the symbolic language, we shall find that the smaller

class is more useful for computation, whilst the larger is better for expressing mathematics. We therefore consider the relationship between them.

Lemma 4.13 If the exponential Σ^{X} exists in an equideductive category Q then there is some urspace A ∈ A and maps i : X → A and I : Σ^{X} → Σ^{A} with Σ^{i} · I = id_{Σ^{X}}. Proof Since there are enough injectives, there are an urspace B and a M-map J : Σ^{X} ↣ Σ^{B}. But Σ^{X} is itself injective by Lemma 4.5, so there is some P : Σ^{B} ↠ Σ^{X} with P · J = id_{Σ^{X}}. Then the transpose i : X → A ≡ Σ^{Σ^{B}} of P and I ≡ J · η_{Σ^{A}} : Σ^{X} → Σ^{A} satisfy Σ^{i} · I = id_{Σ^{X}}. □

Proposition 4.14 The class of all exponentiable objects in an equideductive category provides another class of urspaces. Proof Any retract of an exponentiable object is also exponentiable. Also, if Σ^{X} exists then so does Σ^{Σ^{X}}, because if X is a Σ-split subspace of A then Σ^{X} is a retract of Σ^{A}. □

Proposition 4.15 The class of all injective objects in an equideductive category provides a class of urspaces. Proof An object is injective iff it is a retract of an exponential. Hence products and exponentials of injectives are injective.. □

5 The restricted lambda calculus

Now we begin to develop a symbolic language for the categorical structure that we have described. In this section we start with the exponentials, for which we only consider Σ^{A} and not general B^{A}. This is motivated by the importance of open subspaces in topology and the idea that termination is the fundamental observable property in computation, but also by the connection with injectives in Lemma 4.5.

We spell out this well known material in some detail because it serves as a plan for our treatment of the ∀=▷ language for partial products later.

However, since equality in equideductive logic is an “interrogative” notion that is different from “factual” rewriting in the λ-calculus, we shall refer to (the symmetric transitive closure of) the latter as interchangeability and write ↔ instead of = for it.

The restricted λ-calculus will provide the arena for computation, whereas the richer calculus is that of proof. The latter will have more complicated types or contexts that are defined by predicates, and terms or morphisms represented by partial equivalence classes. For this reason we shall use the prefix “ur” (meaning original) for the underlying calculus.

Remark 5.1 Recall that products and exponentials are defined by the bijections

Γ ⟶^{a} A Γ ⟶^{b} B ; = ; Γ ⟶^{⟨a,b⟩} A × B or Γ ⊢ a ↔ π_{0}p : A Γ ⊢ b ↔ π_{1}p : B ; = ; Γ ⊢ p ↔ ⟨a, b⟩ : A × B

and Γ × A ⟶^{σ} Σ ; = ; Γ ⟶^{σ̃} Σ^{A} or Γ, x : A ⊢ σ ↔ ϕx ≡ ev(ϕ, x) : Σ ; = ; Γ ⊢ ϕ ↔ λx. σ : Σ^{A}

where ⟨a, b⟩ is the unique p such that a = π_{0}p and b = π_{1}p and σ̃ is the transpose of σ (Definition 4.3), being unique such that σ = ev · (σ̃ × A).

There are two different ways of forcing these correspondences to be bijective. In symbolic logic the usual approach is to state the the beta- and eta-laws,

(λx. σ)x ↔ σ and λx. ϕx ↔ ϕ.
π_{0}⟨a, b⟩ ↔ a, π_{1}⟨a, b⟩ ↔ b and ⟨π_{0}p, π_{1}p⟩ ↔ p,

and also require the operations to transmit interchangeability and substitute.

In category theory, on the other hand, the product A × B is defined by saying that for any two maps a and b there is a unique map p that satisfies the β-rules π_{0} · p ↔ a and π_{1} · p ↔ b. We refer to this uniqueness condition as the extensionality rule, which can also be seen as saying that the maps π_{0} and π_{1} are jointly mono.

In equideductive logic we intend to use extensionality rules for both connectives. This property for Σ^{(−)} is given semantically by Lemma 4.10, but this uses partial products and so is outside the scope of this section. We are therefore obliged to use the λη-rule here and prove that the two formulations are equivalent later. Since there is no difficulty with using extensionality to define ×, that is what we do in both calculi (Axiom 5.8).

Axiom 5.2 The anatomy of the restricted λ-calculus consists of

(a) urtypes, A, which are generated from base types such as 0, 1 and ℕ by × and Σ^{(−)} (which is written (−) → Σ elsewhere);

(b) urcontexts, Γ, which are just lists of distinct variables, to each of which is assigned an urtype (there are no equations yet); (c) urterms, a, which are generated from variables, ⋆, ⟨ , ⟩, π_{0}, π_{1}, λ, ev and operation symbols,

according to the rules below;

(d) urterm-formation judgements, Γ ⊢ a : A, which assert that the urterm a is well formed, only contains (freely) the variables in the urcontext Γ, and is of urtype A;

(e) interchange judgements, Γ ⊢ a ↔ b : A, which say both that the urterms are well formed and that one may be replaced by the other; such judgements are generated from particular interchanges and the rules of the calculus.

Remark 5.3 We may assume that operation symbols and particular interchanges have base types or Σ as their result types. However, we need to generate part of the language in order to define their argument types and the urterms that may be interchanged. We write L for the collection of base types, operation symbols and particular interchanges of a particular language. By adding these things, Proposition 6.6 adapts the pure calculus to match any given category with products and exponentials.

Axiom 5.4 There are structural rules that manipulate judgements. For the variables in the urcontext, these are:

(a) identity: any variable from the urcontext is a well formed urterm of its urtype;

(b) weakening: new urtyped variables may be added to the urcontext of any valid judgement of either kind;

(c) exchange: the variables in the urcontext may be permuted, so we regard the list as unordered;

(d) contraction: if two variables in an urcontext have the same urtype then one may be substituted for the other, which is deleted from the urcontext (as on the left below);

{Γ, x, y : A ⊢ b : B \atop Γ, x : A ⊢ [x/y]^{∗}b : B}  {Γ ⊢ a : A Δ, x : A ⊢ b : B \atop Γ, Δ ⊢ [a/x]^{∗}b : B}

(e) cut (on the right above), in which Γ, Δ is the union of the lists (with repetitions removed) and [a/x]^{∗}b denotes substitution of the urterm a for the variable x in the urterm b, avoiding capture by λ-abstraction. We explain why we use a star in the notation for substitution in Section 11.

Axiom 5.5 There are also structural rules for manipulating interchanges:

(a) they are reflexive, symmetric and transitive;

(b) they admit weakening, exchange and contraction of the variables in the urcontext; and

(c) they admit cut or substitution, both of an urterm into an interchange and vice versa:

{Γ ⊢ a : A Δ, x : A ⊢ c ↔ d : C \atop Γ, Δ ⊢ [a/x]^{∗}c ↔ [a/x]^{∗}d : C}  {Γ ⊢ a ↔ b : A Δ, x : A ⊢ c : C \atop Γ, Δ ⊢ [a/x]^{∗}c ↔ [b/x]^{∗}c : C}

(There are no equations in Γ yet.)

Axiom 5.6 In this setting, we can say how urterms may be formed. Even though products of arbitrary pairs of objects may be formed in an equideductive category, for the time being we only introduce the × syntax for urtypes. Then we employ the symbols ⋆ : 1, π_{0}, π_{1} and ⟨ , ⟩ in the usual way.

On the other hand, the λ-calculus is usually presented in a form that allows successive abstractions (λI), but we prefer to take all exponentials at Σ. A single λ may therefore bind any number of variables at the same time, whilst application may take multiple arguments:

Γ, x⃗ : A⃗ ⊢ σ : Σ ; λI ; Γ ⊢ λx⃗:A⃗. σ : ΣA⃗  Γ ⊢ ϕ : ΣA⃗  Δ ⊢ a⃗ : A⃗ ; λE ; Γ, Δ ⊢ ϕa⃗ : Σ

Using product urtypes, we may combine a list of arguments into a single one. Partial application (i.e. to a shorter list) may be achieved by padding it out with variables that are then re-abstracted.

Remark 5.7 Associated with each of the urtype connectives are

(a) the introduction and elimination rules for urterms, which we have just given;

(b) beta- and either eta- or extensionality-rules that specify the interchanges that make these operations inverse; and

(c) interchange-transmitting rules that say that they respect interchanges between urterms.

Axiom 5.8 The interchangeability rules for the singleton 1 and product A × B are

Γ ⊢ a : 1 ; 1-ext ; Γ ⊢ a ↔ ⋆ : 1 Γ ⊢ p ↔ q : A × B ; ×E_{0}↔ ; Γ ⊢ π_{0}p ↔ π_{0}q : A Γ ⊢ p ↔ q : A × B ; ×E_{1}↔ ; Γ ⊢ π_{1}p ↔ π_{1}q : B

Γ ⊢ a : A Γ ⊢ b : B ; ×β_{0} ; Γ ⊢ π_{0}⟨a, b⟩ ↔ a : A  Γ ⊢ a : A Γ ⊢ b : B ; ×β_{1} ; Γ ⊢ π_{1}⟨a, b⟩ ↔ b : B

Γ ⊢ p, q : A × B Γ ⊢ π_{0}p ↔ π_{0}q : A Γ ⊢ π_{1}p ↔ π_{1}q : B ×-ext

Γ ⊢ p ↔ q : A × B

Lemma 5.9 Interchangeability for A × B satisfies the interchange-transmitting and η-rules,

a_{1} ↔ a_{2} : A  b_{1} ↔ b_{2} : B ; ×I↔ ; ⟨a_{1}, b_{1}⟩ ↔ ⟨a_{2}, b_{2}⟩ : A × B  p : A × B ; ×η ; ⟨π_{0}p, π_{1}p⟩ ↔ p : A × B

Proof In both cases, first use both ×β_{0} and ×β_{1}, then transitivity of ↔ and finally ×-ext. □

Axiom 5.10 We need to be more careful about the rules for interchangeability of λ-terms because we shall handle equality differently in equideductive logic, where this Axiom will become Lemma 9.14.

Γ, x⃗ : A⃗ ⊢ σ ↔ τ : Σ
λI↔
Γ ⊢ (λx⃗:A⃗. σ) ↔ (λx⃗:A⃗. τ) : ΣA⃗
Γ ⊢ ϕ ↔ ψ : ΣA⃗ Δ ⊢ a⃗ : A⃗ ; λE↔_{0} ; Γ, Δ ⊢ (ϕa⃗) ↔ (ψa⃗) : Σ  Γ ⊢ ϕ : ΣA⃗ Δ ⊢ a⃗ ↔ b⃗ : A⃗ ; λE↔_{1} ; Γ, Δ ⊢ (ϕa⃗) ↔ (ϕb⃗) : Σ

Γ ⊢ a⃗ : A⃗ Γ, x⃗ : A⃗ ⊢ σ : Σ ; λβ ; Γ ⊢ (λx⃗:A⃗. σ)a⃗ ↔ [a⃗/x⃗]^{∗}σ : Σ  Γ ⊢ ϕ : ΣA⃗ ; λη ; Γ ⊢ (λx⃗:A⃗. ϕx⃗) ↔ ϕ : ΣA⃗

6 Equivalence

Having described the restricted λ-calculus symbolically, we can consider its relationship to category theory. However, whilst the interpretation of the λ-calculus is usually given in a cartesian closed category, here we shall use the subcategory A of urspaces (Notation 4.9) in an equideductive one.

We first go from syntax to semantics. For a category A to be a suitable target for such an interpretation, it must of course have the relevant structure (products and powers of Σ), but it also has to have a choice of this amongst the many available isomorphic copies. We return to this rather distracting point at the end of the section.

Proposition 6.1 Let A be a category with chosen finite products and exponentials, together with a suitable interpretation of the base types and operation symbols of a particular language L as objects and morphisms of A that satisfy the particular interchanges. Then the restricted λ-calculus has an interpretation or denotation ⟦−⟧ in which interchangeable urterms in the calculus are denoted by the same morphism in the category. Proof The urtypes and urcontexts are interpreted by structural recursion as follows:

(a) the interpretations of the base types of L as objects of A are given;

(b) the product and exponential urtypes in the symbolic calculus are interpreted by the structure of the same name in the category:

⟦1⟧ ≡ 1 ⟦A × B⟧ ≡ ⟦A⟧ × ⟦B⟧ ⟦ΣA⃗⟧ ≡ Σ^{⟦A_{1}⟧×···×⟦A_{n}⟧};

(c) each urcontext is interpreted as the product of the interpretations of its urtypes:

⟦Γ⟧ ≡ ⟦x_{1} : A_{1}, …, x_{n} : A_{n}⟧ ≡ ⟦A_{1}⟧ × ⋯ × ⟦A_{n}⟧.

Then an urterm in urcontext, Γ ⊢ a : A, is interpreted as a morphism ⟦Γ⟧ ⟶^{⟦a⟧} ⟦A⟧ in A, by structural recursion on its formation rules, as follows:

(d) if x : A is one of the urtyped variables in the urcontext Γ then its interpretation is the relevant product projection, ⟦x⟧ : ⟦Γ, x : A⟧ = ⟦Γ⟧ × ⟦A⟧ ⟶^{π_{1}} ⟦A⟧;

(e) weakening of the judgement Γ ⊢ a : A by an urtyped variable y : B is obtained by pre-

composition with the product projection, ⟦Γ, y : B⟧ = ⟦Γ⟧ × ⟦B⟧ ⟶^{π_{0}} ⟦Γ⟧ ⟶^{⟦a⟧} ⟦A⟧;

(f) contraction of a judgement Γ, y : B, z : B ⊢ a : A by identifying two variables of the same urtype is interpreted by pre-composing a diagonal,

⟦Γ, y : B⟧ = ⟦Γ⟧ × ⟦B⟧ ⟶^{Δ} ⟦Γ⟧ × ⟦B⟧ × ⟦B⟧ = ⟦Γ, y : B, z : B⟧ ⟶^{⟦a⟧} ⟦A⟧;

(g) exchange is given by switching the appropriate factors of the product;

(h) the interpretation of the cut rule in Definition 5.5(c) combines the maps

[figure: ⟦Γ⟧; ⟦a⟧; ⟦A⟧; and; ⟦Δ⟧ × ⟦A⟧; ⟦b⟧; ⟦B⟧]

into

[figure: ⟦Δ⟧ × ⟦Γ⟧; ⟦Δ⟧ × ⟦a⟧; ⟦Δ⟧ × ⟦A⟧; ⟦b⟧; ⟦B⟧]

using categorical product and composition;

(i) pairing and projections are interpreted using the categorical correspondence in Remark 5.1;

(j) the operation symbols of L have given interpretations as morphisms of the category, but note that we need to generate part of the interpretation in order to specify these “given

interpretations”;

(k) application (to variables) and λ-abstraction are interpreted by exponential transposition, as in Remark 5.1; and

(l) application to general expressions is derived from this using cut.

Finally, given a proof that two urterms are interchangeable in the calculus, we must show (again by induction on the structure of the proof) that they are denoted by the same morphism in the category. Recall that interchange judgements cannot (yet) depend on equational hypotheses.

(m) Reflexivity, symmetry and transitivity for morphisms are as for urterms;

(n) product satisfies ×β_{0}, ×β_{1} and ×-extensionality because the categorical definition says that any pair ⟨a, b⟩ is the unique map for which π_{0}⟨a, b⟩ = a and π_{1}⟨a, b⟩ = b;

(o) the interchange-transmitting rules ×E_{0}↔, ×E_{1}↔, λE↔_{0} and λE↔_{1} hold because ×E_{0}, ×E_{1} and λE are defined by composition with π_{0}, π_{1} and ev, but if pairs of maps are correspondingly the same in a category then so are their composites;

(p) the particular interchanges for the operation symbols of L are given to be valid in the category;

(q) the λβ-rule is expressed by the square on the left below: the clockwise composite is ev( ˜⟦σ⟧, ⟦a⟧) and the anticlockwise one is ⟦[a/x]^{∗}σ⟧ by (h); this square commutes because the upper left triangle does by the properties of × and the lower one is Definition 4.3 of the transpose;

[figure: Γ; ⟨ ˜⟦σ⟧, ⟦a⟧⟩; Σ^{A} × A; Γ × A; ˜⟦σ⟧ × A; Σ^{A} × A]
[figure: ˜⟦σ⟧ × A; ⟦σ⟧]
[figure: Γ × A; ⟨id, ⟦a⟧⟩; ⟦σ⟧; Σ; ev; Σ; ev]

(r) the λη-rule is the triangle on the right, which is also the definition of the transpose;

(s) for the structural rules applied to interchanges, in place of one of the arrows in 6.1(h), we have two that are the same, so they have the same composite with the other map. □

Remark 6.2 This interpretation may be developed without modification in the subcategory A ⊂ Q of urspaces in an equideductive category, because A was required to be closed under the urtype-forming operations 1, × and Σ^{(−)} that we need. When we extend the theory to equideductive logic in Section 11 it will be important that all objects Γ ∈ Q respect the universal properties of these type connectives. It will also be necessary to re-work the final section of the proof (parts m–s), because we shall handle equations there differently from interchangeability here. □

The category in which the language is interpreted need not come from outside, but may be obtained from the language itself.

Definition 6.3 The category of contexts and substitutions Cn_{L}^{λ} has

(a) as objects, the urcontexts Γ;

(b) as morphisms [b⃗/y⃗] : Γ → Δ ≡ [y⃗ : B⃗], strings of interchangeability classes of urterms Γ ⊢ b⃗ : B⃗ or substitutions [b⃗/x⃗];

(c) as identity on Γ ≡ [x⃗ : A⃗], the string x⃗ of variables;

(d) as composite, the substituted string [b⃗/y⃗]^{∗}c⃗ of urterms or combined substitution [c⃗/z⃗] · [b⃗/y⃗] ≡ [[b⃗/y⃗]^{∗}c⃗/z⃗].

Instead of defining its morphisms as strings b⃗ of urterms, [Tay99, §4.7] gives a more principled approach to the construction of Cn_{L}^{λ}. In this, the category is generated from an elementary sketch whose arrows are product projections and splittings of them, subject to an equivalence relation that is essentially the well known substitution lemma. This sketch is defined directly from the syntax of a language — the generating maps correspond to the urtypes and urterms — even when this has dependent types [Tay99, Ch. VIII].

Lemma 6.4 The structure Cn_{L}^{λ} is a category that has a choice of products and exponentials. Proof Axiom 5.5 provides the categorical structure: interchangeability is an equivalence relation that is respected by cut, which is itself associative and behaves appropriately for variables. The products of single-variable urcontexts [x : A] × [y : B] are given by products of the urtypes, [p : A × B]. Alternatively, products of multiple-variable urcontexts [x⃗ : A⃗] × [y⃗ : B⃗] are obtained by (renaming any common variables and) concatenating the urcontexts, [x⃗ : A⃗, y⃗ : B⃗]. The exponential Σ^{[x⃗:A⃗]} is [ϕ : Σ^{ΠA⃗}]. □

Theorem 6.5 Cn_{L}^{λ} is the classifying category for the restricted λ-calculus generated by the language L:

(a) it is itself a category with chosen products and Σ^{(−)};

(b) it has an interpretation of the calculus;

(c) any interpretation of the calculus in a category A with chosen × and Σ^{(−)} extends to a functor Cn_{L}^{∀} → Q that preserve this structure, uniquely up to unique natural isomorphism; and

(d) any such structure-preserving functor restricts to an interpretation of the language in Q. Proof Every object of Cn_{L}^{λ} (context) is a finite product of single-variable urcontexts [x : A], each of which corresponds to an urtype, whilst all of the functors in question preserve products. It is therefore enough to consider objects or urcontexts like [x : A] and morphisms into them, which are single urterms Γ ⊢ a : A. The extension of the interpretation from single urtypes and urterms to urcontexts depends on the choice of products, but any two such choices are uniquely naturally isomorphic. □

For the inverse construction, we need to augment the λ-calculus with a name for each object, morphism, product and exponential.

Definition 6.6 Let A be any category with products and exponentials (for example the subcategory A ⊂ Q of urspaces in an equideductive category). Then the proper language of A has

(a) a base type ⌜A⌝ for each object A ∈ A;

(b) an operation symbol x : ⌜A⌝ ⊢ ⌜f⌝x : ⌜B⌝ for each morphism f : A → B in A;

(c) a particular interchange x : ⌜A⌝ ⊢ ⌜g⌝(⌜f⌝x) ↔ ⌜g · f⌝x : ⌜C⌝ for each composite A →^{f} B →^{g} C in A;

(d) an operation symbol x : ⌜A⌝, y : ⌜B⌝ ⊢ pair(x, y) : ⌜A × B⌝ with

(e) particular interchanges

x : ⌜A⌝, y : ⌜B⌝ ⊢ ⌜π_{0}⌝( pair(x, y)) ↔ x : ⌜A⌝
x : ⌜A⌝, y : ⌜B⌝ ⊢ ⌜π_{1}⌝( pair(x, y)) ↔ y : ⌜B⌝
p : ⌜A × B⌝  ⊢ pair (⌜π_{0}⌝p, ⌜π_{1}⌝p)) ↔ p : ⌜A × B⌝

for each pair of objects A, B ∈ A; and

(f) an operation symbol ϕ : Σ^{⌜A⌝} ⊢ abs ϕ : ⌜Σ^{A}⌝ with

(g) particular interchanges

ϕ : Σ^{⌜A⌝}, x : ⌜A⌝ ⊢ ⌜ev⌝( abs ϕ, x) ↔ ϕx : Σ
f : ⌜Σ^{A}⌝  ⊢ abs (λx:⌜A⌝. ⌜ev⌝(f, x)) ↔ f : ⌜Σ^{A}⌝

for each object A ∈ A.

Remark 6.7 Many authors call this the internal language, but this name is not consistent with other categorical terminology. One can formalise notions of “language” mathematically just as one can a group. Such formalisations admit interpretations in categories with suitable structure, for example there are internal groups in any category with products, the leading example being topological groups. Likewise there are internal models of mathematically formalised notions of language in appropriate categories, which would in particular also have to have free monoid functors. The resulting notion of internal language could, for example, be useful in a categorical study of Gödel’s theorem. However, this is not what we are using here.

Theorem 6.8 For any category A with finite products and Σ^{(−)}, the functor ⌜−⌝ : A → Cn_{L}^{λ} defines a weak equivalence with the category of contexts and substitutions of its proper language. That is, ⌜−⌝ is full, faithful and essentially surjective. It is a strong equivalence, having a pseudoinverse ⟦−⟧ : Cn_{L}^{λ} → A with

ϵ_{A} : ⟦x : ⌜A⌝⟧ = A and η_{Γ} : ⌜⟦Γ⟧⌝ ≅ Γ,

iff A has a choice of the necessary structure. Proof This is discussed in detail in [Tay99, §7.6]. so we just sketch the strategy here.

Suppose first that A has a choice of structure. Then requirements like ⟦⌜A⌝⟧ = A provide the base cases of the recursive definition of ⟦−⟧ : Cn_{L}^{λ} → A in Proposition 6.1. The isomorphism ⌜⟦Γ⟧⌝ ≅ Γ is also defined from the particular operation-symbols and interchanges by recursion on (the proof that the urtypes are well formed in) Γ.

Naturality of this isomorphism with respect to Γ is not trivial: it is equivalent to ⌜−⌝ : A → Cn_{L}^{λ} being full and faithful and needs to be proved for each connective. In our case (× and Σ^{(−)}) this can be done using the normal form.

Without the choice of structure, we must show that any x : ⌜A⌝ ⊢ fx : ⌜B⌝ is fx = ⌜g⌝x for some unique morphism g : A → B in A, and each urcontext Γ has Γ ≅ ⌜A⌝ for some object A ∈ A. The proof for a particular urterm or urcontext is a finite part of the general result, i.e. it requires the existence of finitely many instances of the categorical structure in A. However, since the identities of these instances are not exported from the proof in the statement of the theorem, no choice of them is needed. □

Corollary 6.9 The interpretation ⟦−⟧ : Cn_{L}^{λ} → A is full and faithful: any map f : ⟦Γ⟧ → ⟦A⟧ in A is the interpretation of an urterm

Γ ≡ [s⃗ : C⃗] ⊢ a ≡ η_{A}^{−1} (⌜e⌝ (η_{Γ} z⃗)) : A.

[figure: ⟦Γ⟧; Γ; η_{Γ} ; ≅; ⌜⟦Γ⟧⌝; ⟦A⟧; f; A; a; . . . . . . . . . . . . . . . . .; η_{A} ; ≅; ⌜⟦A⟧⌝; ⌜f⌝]

If Γ ⊢ b : A has the same interpretation then the interchange Γ ⊢ a ↔ b : A is provable from the proper language. □

7 Sobriety

The contravariant functor Σ^{(−)} warrants deeper study. It is self-adjoint on the full subcategory of exponentiable objects on which it is defined (Proposition 4.14), so the covariant double exponential Σ^{Σ^{(−)}} is part of a monad, whose unit η_{X} is x ↦ λϕ. ϕx in λ-notation (Definition 4.3). The situation where η_{A} is an equaliser was investigated in [A], introducing a new term-forming operation called focus into the symbolic language. This built on the notion of repleteness in synthetic domain theory that was introduced by Martin Hyland [Hyl91] and relied on an orthogonality property similar to our Proposition 2.9.

Our approach in this paper is different from earlier one in [A]. Whereas that constructed a new category to make the objects sober, in this section we shall work within a given equideductive category and prove as a theorem that every exponentiable object of it is sober.

The symbolic language that we have so far (the restricted λ-calculus) is not strong enough to carry the argument. In particular, it cannot express equalisers, so we still have to work in a categorical style here. We can use the proper restricted λ-calculus of the subcategory A ⊂ Q of urspaces for those parts of the development that only use exponentiable objects.

Remark 7.1 Recall from [A] that if the exponentials Σ^{A} and Σ^{B} exist then they are algebras for the Σ^{Σ^{(−)}} monad. Moreover, for any f : A → B, the map H ≡ Σ^{f} is a homomorphism. This means that it makes the square on the left commute, by naturality of Σ^{η} with respect to f:

Σ^{3}B ≡ Σ^{Σ^{Σ^{B}}}  \overline{\begin{matrix}Σ^{Σ^{H}} \\  \end{matrix}}Σ^{3}A ≡ Σ^{Σ^{Σ^{A}}}
[figure: A; P; Σ^{Σ^{B}}; ηΣ^{2}B; Σ^{2}ηB; Σ^{4}B ≡ Σ^{Σ^{Σ^{Σ^{B}}}}]
[figure: Σ^{B}; Σ^{η_{B}}; H; Σ^{A}; Σ^{η_{A}}]

Equivalently, the transpose P ≡ H̃ has the same composite with ηΣ^{2}B as with Σ^{2}ηB. The easiest way to see this is to use the restricted λ-calculus from the previous section, because then H and P differ only in the order of their arguments. Since the towers of exponentials are rather unwieldy, we abbreviate them as Σ^{n}.

We can turn the requirement that the composites be the same into a symbolic interchange:

Definition 7.2 A term Γ ⊢ P : Σ^{Σ^{A}} of the restricted λ-calculus is called prime for the exponentiable object A if it is provable that

Γ, Φ : Σ^{3}A ⊢ ΦP ↔ P (λx. Φ(λϕ. ϕx)) : Σ.

In particular, any term Γ ⊢ a : A of exponentiable type gives rise the prime P ≡ λϕ. ϕa.

Lemma 7.3 For Δ, x : A ⊢ fx : B, if Γ ⊢ P : Σ^{Σ^{A}} is prime then so too is

Γ, Δ ⊢ Q ≡ (Σ^{Σ^{f}})P ≡ λψ. P (λx. ψ(fx)) : Σ^{Σ^{B}}.

Proof Categorically, this is because ηΣ^{2}(−) and Σ^{2}η_{(−)} are natural transformations, i.e. the two squares on the right commute:

[figure: Δ × A; η_{A} · π_{1}; Σ^{Σ^{A}}; ηΣ^{2}A; Σ^{2}η_{A}; Σ^{4}A]
[figure: P]

Γ

[figure: Q]
[figure: B; f; η_{B}; Σ^{Σ^{B}}; Σ^{Σ^{f}}; ηΣ^{2}B; Σ^{2}η_{B}; Σ^{4}B; Σ^{4}f]

Symbolically, consider the urcontext Γ, Δ, Ψ : Σ^{3}B. Then

Ψ((Σ^{Σ^{f}})P ) ≡ Ψ(λψ. P (λx. ψb))
≡ ΦP ↔ P (λx. Φ(λϕ. ϕx))
≡ P (λx. Ψ(λψ. (λϕ. ϕx)(λx. ψb)))
↔ P (λx. Ψ(λψ. ψb)) ≡ ((Σ^{Σ^{f}})P )(λy. Ψ.(λψ. ψy)),

using primality of P with respect to the expression Φ that is defined by the second line. □

Definition 7.4 For any exponentiable object A of an equideductive category, let Ā ∈ Q be the subspace of primes for A, which is defined by the equaliser

A
[figure: η_{A}]
[figure: Ā; ϵ; j; Σ^{2}A; ηΣ^{2}A; Σ^{2}ηA; Σ^{4}A]

Then j : Ā ↣ Σ^{2}A is in M by Lemma 4.7, and we say that A is sober if the mediator ϵ : A → Ā is an isomorphism.

The following key lemma belongs to the tradition of synthetic domain theory and may be needed in some other setting in future. We therefore note that it holds whenever the Definition is meaningful and Σ is injective with respect to j × Y.

Lemma 7.5 The exponential ΣĀ exists in the presheaf topos Set^{Q^{op}} and Σ^{ϵ} : ΣĀ ≅ Σ^{A}. Hence ϵ : A → Ā is Σ-epi in Q. Proof The Yoneda embedding preserves the exponentials Σ^{n}A and the equaliser in the Definition and all exponentials exist in a topos. Then

[figure: Σ^{A}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ηΣ^{A}; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; \underline{Ση_{A}}; Σ^{3}A; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ηΣ^{3}A; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; \underline{ΣηΣ^{2}A}; \underline{Σ^{3}ηA}; Σ^{5}A]
[figure: Σ^{j}]
[figure: ΣĀY; Σ^{ϵ}; .; .; .; .; .; .; .; .; .; .; .; \underline{ϕ̃}; \underline{ψ̃}; Y; Φ̃; Ψ̃]

the top row is a split coequaliser. Therefore there is a mediator k : Σ^{A} ↪ ΣĀ such that

Σ^{j} = k · Σ^{η_{A}},  Σ^{η_{A}} = Σ^{e} · Σ^{j}  and Σ^{e} · k = id_{Σ^{A}}.

Also, injectivity of Σ means that the natural transformation

Σ^{j}(Y) : Σ^{3}A(Γ) ≡ Q(Γ × Σ^{Σ^{A}}, Σ) ⟶ ΣĀ(Γ) ≡ Q(Γ × Ā, Σ)

is componentwise surjective, cf. Lemma 2.12. Hence k · Σ^{ϵ} is componentwise the same as the identity, so it is the identity. In particular, the natural transformation

Σ^{ϵ}(Y) : ΣĀ(Y) ≡ Q(Ā × Y) ⟶ Σ^{A}(Y) ≡ Q(A × Y)

given by composition with ϵ × Y is mono, which means that ϵ is Σ-epi by Lemma 2.13. □

We can also give a bare-hands proof that avoids the Yoneda embedding and set theory. We need to be careful because Y and â priori Ā need not themselves be exponentiable, but they do have to respect the iterated exponentials and equaliser that we are using.

Lemma 7.6 The map ϵ : A → Ā is Σ-epi.

[figure: A × Y; η_{A} × Y; Σ^{Σ^{A}} × Y; ηΣ^{2}A × Y; Σ^{2}ηA × Y; Σ^{4}A × Y]
[figure: j × Y]
[figure: Ā × Y; ϵ × Y; ϕ; ψ; Σ; Φ; Ψ]

Proof For Definition 2.8 we must show that, for any object Y ∈ Q and morphisms ϕ, ψ : Ā × Y ⇉ Σ, if the composites ϕ · (ϵ × Y) and ψ · (ϵ × Y) are the same (θ) then so already were ϕ and ψ.

By Lemma 4.7, the equaliser inclusion j × Y is in M, so by injectivity of Σ (Axiom 4.2) the maps ϕ, ψ lift to Φ, Ψ, so that Φ · (j × Y) and Ψ · (j × Y) are the same as ϕ and ψ respectively. The upper triangle above commutes by construction, so all paths from A × Y to Σ have the same composite, θ.

Consider the exponential transpose Φ̃ of Φ (Definition 4.3), which is defined by the lower right commutative triangle below:

A × Σ^{3}A ^{A × Φ̃}  A × Y
[figure: η_{A} × Σ^{3}A; η_{A} × Y]
Σ^{Σ^{A}} × Σ^{3}A ^{Σ^{Σ^{A}} × Φ̃}  Σ^{Σ^{A}} × Y
[figure: ev′; Φ]
[figure: A × Σ^{A}; A × Σ^{η_{A}}; ev′; Σ; θ]

The triangle on the right commutes by definition of θ. The parallelogram that overlaps it commutes because it is the product of the morphisms η_{A} and Φ̃. The big triangle on the lower left commutes by a λ-calculation that is valid because all of its vertices are exponentiable and the common composite takes (a, Ξ) to Ξ(λξ. ξa). Hence the square commutes from A × Y to Σ, which makes Σ^{η_{A}} · Φ̃ the transpose of θ. The same is true of Σ^{η_{A}} · Ψ̃, but transposes are unique, so the two triangles on the left below commute:

[figure: Ā × Y; Ā × Φ̃; Ā × Ψ̃; Ā × Σ^{3}A; j × Σ^{3}A; Σ^{Σ^{A}} × Σ^{3}A; ηΣ^{Σ^{A}} × Σ^{3}A; Σ^{2}ηA × Σ^{3}A; Σ^{4}A × Σ^{3}A]
[figure: Ā × θ̃; ev′]
[figure: Ā × Σ^{A}; Ā × Σ^{η_{A}}; j × Σ^{A}; Σ^{Σ^{A}} × Σ^{A}; Σ^{Σ^{A}} × Σ^{η_{A}}; ev; Σ; ev]

The square in the middle commutes because it is the product of the morphisms j and Σ^{η_{A}}. On the right, the lower square (via Σ^{2}ηA × Σ^{3}A) and the upper triangle (involving ηΣ^{2}A × Σ^{3}A and ev′) commute by λ-calculations that are valid because all the vertices are exponentiable. The common composite of the former takes (F, Ξ) to F (λa. Ξ(λξ. ξa)) whilst the latter defines η (Definition 4.3).

By construction, j has the same composite with ηΣ^{2}A as with Σ^{2}ηA, so the composites from Ā × Σ^{3}A to Σ^{4}A × Σ^{3}A along the top are the same. Hence all paths from Ā × Y to Σ have the same composite. We rewrite this along the lower path around the diagram below:

[figure: Ā × Y; j × A; Σ^{Σ^{A}} × Y; Φ; Σ]
[figure: ev′]
[figure: Ā × Σ^{3}A; Ā × Φ̃; j × Σ^{Σ^{A}}; Σ^{Σ^{A}} × Σ^{3}A; Σ^{Σ^{A}} × Φ̃]

in which the triangle is the definition of Φ̃ and the square is the product of this and j. The composite along the top is ϕ by construction, but this is the same as ψ since we could have used Ψ instead of Φ. □

Proposition 7.7 Every exponentiable object of an equideductive category is sober.

A  [figure: ϵ] Ā
[figure: j; ..........................................................................]
Σ^{Σ^{A}}  \overline{Σ^{Σ^{i}}} Σ^{3}B
[figure: η_{A}; η_{Σ^{B}}; Σ^{η_{B}}]
[figure: A; f ≡ id; i; Σ^{B}; id; Σ^{B}; g]

Proof We must find the inverse of ϵ : A → Ā. Since there are enough injectives (Axiom 4.6), there is a partial product inclusion (M-map) i : A ↣ Σ^{B}. Then ϵ and i form a square with f ≡ id and g ≡ Σ^{η_{B}} · Σ^{Σ^{i}} · j that commutes by naturality of η and its unit equation. By the previous lemma, ϵ is Σ-epi, so by orthogonality (Proposition 2.9) there is a unique fill-in Ā → A. This is the inverse of ϵ since we already know that it is Σ-epi. □

Corollary 7.8 The map η : A → Σ^{Σ^{A}} is a regular mono, so it is in M. □

Lemma 7.9 A map f : A → B between exponentiable objects in an equideductive category is epi iff Σ^{f} : Σ^{B} → Σ^{A} is mono and this case f × C is also epi.

Proof The target X of the pair has an M-map (mono) into an urtype Σ^{C} by Axiom 4.6. Then the double transpose of the diagram on the left gives the result:

[figure: A; f; B; h; k; X; Σ^{C}; Σ^{A}; Σ^{f}; Σ^{B}; \underline{h̃}; \underline{k̃}; C]

It follows easily that f × C is also epi. □

Theorem 7.10 The functor Σ^{(−)} : B → B^{op} reflects invertibility: if Σ^{f} is invertible, so is f.

Σ^{B}  B
[figure: G̃]
[figure: Σ^{A}; G; ≅; Σ^{f}; A; f; . . . . . . . . .; ĩd ≡ η_{A}; Σ^{Σ^{A}}; Σ^{4}A]

Proof Let f : A → B with G : Σ^{A} → Σ^{B} inverse to Σ^{f}. The double exponential transpose of Σ^{f} ·G = id is G̃·f = ĩd = η_{A}, which has the same composite with Σ^{2}η_{A} and ηΣ^{Σ^{A}}. Since f is epi by the Lemma, G̃ also has the same composite, so it factors through the equaliser, providing f^{−1}. □

8 The sober lambda calculus

We can build the categorical notion of sobriety into the syntactic calculus by adding a new termforming operation. The premises of the formation rules are the term P itself and the interchange judgement that says that this is prime. This extension potentially makes the proof theory of the calculus much more complicated, so we devote a lot of effort to eliminating these difficulties. In doing this, it will be useful to distinguish these more general terms from the urterms of the restricted λ-calculus (Section 5), in which focus was not allowed.

Axiom 8.1 The sober λ-calculus adds a new term-forming operation focus to Axiom 5.2(c) of the restricted λ-calculus. For any base type A, its introduction rule is

Γ ⊢ P : Σ^{Σ^{A}} Γ, Φ : Σ^{3}A ⊢ ΦP ↔ P (λx. Φ(λϕ. ϕx))
Γ ⊢ focus_{A} P : A

so P must be prime. The β-rule, also for prime P, is

Γ, ϕ : Σ^{A} ⊢ ϕ(focus_{A} P) ↔ P ϕ : Σ

and the η-rule is x : A ⊢ focus_{A}(λϕ. ϕx) ↔ x : A.

Instead of asserting interchange-transmission rules directly, we use

{Γ ⊢ a : A Γ ⊢ b : A Γ ⊢ λϕ. ϕa ↔ λϕ. ϕb \atop Γ ⊢ a ↔ b}  T_{0}

We also extend

(a) Axioms 5.6 and 5.8 for pairing (×I) and

(b) Axioms 5.4(a–d) and 5.5(a,b), the structural rules for urterms and interchanges with the exception of cut to terms involving focus. Hence we may form ⟨focus P, …⟩ but not apply π_{0}, π_{1}, λ or ev to focus.

Remark 8.2 Notice that there is a restriction on the applicability of the introduction rule for focus, just as there was on λI (namely that λ may only be applied to urterms of type Σ) in Axiom 5.6. However, once the term focus P has been validly formed, it (or, rather, its β-rule) may be used without further restriction.

Example 8.3 In Theorem 7.10, f^{−1}b = focus (λϕ. Gϕb).

Lemma 8.4 The focus operation transmits interchanges (focus ↔) and also satisfies

a ↔ focus P ; = ; (λϕ. ϕa) ↔ P

and focus P ↔ focus Q = P ↔ Q

Proof If Γ ⊢ P ↔ Q : Σ^{Σ^{A}} then

Γ ⊢ λϕ. ϕ(focus P) ↔ λϕ. P ϕ ↔ P ↔ Q ↔ λϕ. Qϕ ↔ λϕ. ϕ(focus Q),

so the T_{0}-rule applies and we have Γ ⊢ focus P ↔ focus Q. The other parts follow from the β and η-rules. □

Remark 8.5 Instead of axiomatising them directly, we treat the other features of the calculus as definitional extensions:

(a) application of λ-terms and operation symbols to focus-terms,

(b) focus at product types and therefore π_{i}(focus R),

(c) focus at exponential types and therefore λx. (focus P),

(d) cut or substitution of terms for variables and

(e) cut for interchanges.

Remark 8.6 We use focus β to define λ-application to focus-terms:

ϕ(focus P) ≡ P ϕ
(λx. σ)(focus P) ≡ P (λx. σ) ≡ [focus P/x]^{∗}σ.

Similarly, application of an operation-symbol is given by

r(focus P) ≡ focus (λψ. P (λx. ψ(rx))).

These symbols and λ-terms may have more than one argument and we have allowed pairing of terms that involve focus. However, since focus itself has only been defined for base types, we must extract the arguments one at a time, for example,

θ⟨focus P, focus Q) ≡ P (λx. θ⟨x, focus Q⟩) ≡ \{ \begin{matrix}P (λx. Q(λy. θ⟨x, y⟩)) \\ Q(λy. P (λx. θ⟨x, y⟩)), \end{matrix}

where we have a choice about how much of the surrounding expression is regarded as being applied focus Q, but they are interchangeable because P and Q are prime. This is an aspect of the subtle interaction of the Σ^{Σ^{(−)}} with products that is explored at length in [A] and [Füh99, Sel01, Thi97].

Lemma 8.7 focus_{1} P ≡ ⋆ and

focus_{A×B} R ≡ ⟨ focus_{A}(λϕ. R(λp. ϕ(π_{0}p))), focus_{B}(λψ. R(λp. ψ(π_{1}p)))⟩.

Proof Let R : Σ^{2}(A × B) be prime. Then

P ≡ (Σ^{2}π_{0})R ≡ λϕ. R(λxy. ϕx) : Σ^{Σ^{A}} and Q ≡ (Σ^{2}π_{1})R ≡ λψ. R(λxy. ψy) : Σ^{Σ^{B}}

are also prime by Lemma 7.3. To show that this satisfies the extended focus β-rule, let θ : Σ^{A×B}; then focus-elimination for P and then Q as above gives

θ⟨focus P, focus Q⟩ ↔ P (λx. θ⟨x, focus Q⟩) ↔ P (λx. Q(λy. θxy)) ↔ ΘR

where (sic) Θ ≡ λH. H(λx′y′. H(λx′′y′′. θx′y′′)),

so, since R is prime, ΘR ↔ R(λxy. Θ(λθ′. θ′xy)) ↔ R(λxy. θxy) ↔ Rθ.

For the extended focus η-rule, if R ≡ λθ. θ⟨x, y⟩ then

focus_{A×B} R ≡ ⟨ focus_{A} (λϕ. (λθ. θ⟨x, y⟩)(λp. ϕ(π_{0}p))), … ⟩
↔ ⟨ focus_{A} (λϕ. (λp. ϕ(π_{0}p))⟨x, y⟩), … ⟩
↔ ⟨ focus_{A} (λϕ. ϕ(π_{0}⟨x, y⟩)), … ⟩
↔ ⟨ focus_{A} (λϕ. ϕx), … ⟩ ↔ ⟨x, y⟩.  □

Lemma 8.8 focus_{ΣA⃗} P ≡ λx⃗. P(λϕ. ϕx⃗) (Lemma A 8.8). Proof Consider FΦ ≡ F (λx⃗. Φ(λϕ. ϕx⃗)) in the definition of primality of P, so

F (focus_{ΣA⃗} P) ≡ F (λx⃗. P(λϕ. ϕx⃗)) ≡ FP
↔ P(λϕ. F(λG. Gϕ)) ↔ P(λϕ. F (λx⃗. ϕx⃗)) ≡ PF,

which justifies the extended focus β-rule and says how to apply F to a focus-term. For the extended focus η-rule,

focus(λF. F ϕ) ≡ λx⃗. (λF. F ϕ)(λψ. ψx⃗)
↔ λx⃗. (λψ. ψx⃗)ϕ ↔ λx⃗. ϕx⃗ ↔ ϕ.

Application of this focus-term to a string of arguments is given by

(focus P)a⃗ ≡ (λϕ. ϕa⃗)(focus P) ≡ P(λϕ. ϕa⃗) ≡ (λx⃗. P(λϕ. ϕx⃗))a⃗.  □

To summarise, the focus operation is only needed on the outside of the urterm, if at all:

Theorem 8.9 Any well formed term of the sober λ-calculus is interchangeable with

(a) σ if it is of urtype Σ;

(b) focus P, if it is of base type;

(c) λx⃗. σ, if it is of exponential urtype; or

(d) ⟨a, b⟩, if it is of product urtype; where σ and P are urterms (without focus) and a and b are also of this form (Proposition A 8.10).

□

Remark 8.10 Generalising the cut rule to allow terms with focus is a lot more complicated because of the primality pre-condition and this problem will get worse in equideductive logic. Therefore, instead of asserting the more general form of cut as an axiom, we now derive the rule

{Γ ⊢ a : A x : A, Δ ⊢ b : B \atop Γ, Δ ⊢ [a/x]^{∗}b : B}

in the two cases where focus is the outermost operation of a or of b. We must then show that our definitions obey Axiom 5.5(c), transmitting the interchanges

focus P ↔ focus P′, a ↔ focus P, a ↔ a′

and similarly with b, b′, Q and Q′, but most of these follow from Lemma 8.4 and the fact that our formulae already respect non-focus interchanges.

The first case is not so much substitution of a focus term for occurrences of the variable x inside the term b as around it.

Lemma 8.11 [focus_{A} P/x]^{∗}b ≡ focus_{B} (λψ. P (λx. ψb)). Proof We treat the term x : A, Δ ⊢ b ≡ fx : B as a morphism f : A → B between exponentiable objects and use Lemma 7.3, which comes from naturality of η. Then we we may define

f(focus_{A} P) ≡ [focus_{A} P/x]^{∗}(fx) ≡ focus_{B} ((Σ^{Σ^{f}})P )

because, in the urcontext Γ, Δ, ψ : Σ^{B},

ψ( focus_{B}((Σ^{Σ^{f}})P)) ↔ ((Σ^{Σ^{f}})P)ψ ↔ P (ψ · f),

which is what we require for (ψ · f)(focus_{A} P). The one non-trivial interchange is a ↔ focus P, from which we deduce P ↔ λϕ. ϕa,

P (λx. ψb) ↔ (λϕ. ϕa)(λx. ψb) ↔ (λx. ψb)a ↔ ψ[a/x]^{∗}b

and so focus (λψ. P (λx. ψb)) ↔ focus (λψ. ψ([a/x]^{∗}b)) ↔ [a/x]^{∗}b.  □

For subsitution into a focus term, recall from Remark 7.1 that a morphism is prime diagrammatically if it has equal composites with a certain outgoing pair, so any precomposition with it has the same property:

Lemma 8.12 [a/x]^{∗}(focus_{B} Q) ≡ focus_{B} ([a/x^{∗}Q]).

Proof If x : A, Δ ⊢ Q : Σ^{Σ^{B}} is prime then so is Γ, Δ ⊢ [a/x]^{∗}Q : Σ^{Σ^{B}} because

Φ([a/x]^{∗}Q) ↔ [a/x]^{∗}(ΦQ) ↔ [a/x]^{∗}(Q(λx. Φ(λΦ. ϕx)))
↔ ([a/x]^{∗}Q)(λx. Φ(λΦ. ϕx)))

in the urcontext Γ, Δ, Φ : Σ^{3}B, so the definition is legitimate. For the focus β-rule,

ϕ( focus([a/x]^{∗}Q)) ↔ ([a/x]^{∗}Q)ϕ ↔ [a/x]^{∗}(Qϕ) ↔ [a/x]^{∗}(ϕ(focus Q)),

which is what we require for ϕ([a/x]^{∗}(focus Q)). The interchange b ↔ focus Q gives Q ↔ λψ. ψb and

[a/x]^{∗}Q ↔ λψ. ψ([a/x]^{∗}b) and so focus ([a/x]^{∗}Q) ↔ [a/x]^{∗}b.  □

Corollary 8.13 [focus P/a]^{∗}(focus Q) ↔ focus (λψ. P (λx. Qψ)). Proof This follows from Lemma 8.11 since ψ(focus Q) ↔ Qψ, but also from Lemmas 8.12 and 8.8 and λβ. □

Now we return from syntax to category theory.

Theorem 8.14 The sober λ-calculus may be interpreted in any equideductive category.

Proof The interpretation ⟦A⟧ of any urtype A is already required to be exponentiable. It is therefore sober by Proposition 7.7, so we have an equaliser diagram in Q:

⟦Γ⟧
[figure: ⟦P ⟧]
[figure: ⟦A⟧; ⟦focus P ⟧; . . . . . . . .; η_{⟦A⟧}; Σ^{2}⟦A⟧ = ⟦Σ^{Σ^{A}}⟧; ηΣ^{2}⟦A⟧; Σ^{2}η⟦A⟧; Σ^{4}⟦A⟧ = ⟦Σ^{4}A⟧]

The interpretation ⟦P ⟧ of any prime Γ ⊢ P : Σ^{Σ^{A}} is a map that has the same composite with the parallel pair, so it factors through the equaliser. The focus β-rule is commutativity of the triangle. The interchange-transmitting rule (focus ↔) is valid because η is the inclusion of an equaliser and therefore mono. In the case P ≡ λϕ. ϕa, the mediator is ⟦a⟧, so the η-rule is also valid. □

Whilst we previously required all objects ⟦Γ⟧ of Q to respect exponentials and equalisers, we did not actually rely on this in this proof, although we have done in earlier results. This is because an urcontext Γ so far consists only of urtyped variables and no equations, so its interpretation ⟦Γ⟧ is an urspace. This is somewhat unnatural given that primality itself is an equation, so equideductive logic will allow such equations as hypotheses. The stronger requirement will then become relevant in Lemma 11.11.

Remark 8.15 The category of contexts and substitutions Cn_{L}^{sob} for the sober λ-calculus can be constructed in a similar way to Theorem 6.3. The objects (urcontexts) are the same, whilst the term language is enriched by the focus operation.

However, since focus is only needed on the outside of a term, another way to construct the category is as the opposite of the Kleisli category for the Σ^{(−)} ⊣ Σ^{(−)} monad. This is how it was done in [A] and essentially in [Füh99, Sel01, Thi97].

Theorem 8.16 Let A be a category that has products, Σ^{(−)} and all objects sober. Then A is equivalent to Cn_{L}^{sob} for its proper language. Proof By Theorem 6.8, A ≃ Cn_{L}^{λ} → Cn_{L}^{sob} for the proper restricted λ-calculus of A, so we need to define the pseudo-inverse functor Cn_{L}^{sob} → Cn_{L}^{λ}. These two categories have the same objects and we just have to interpret the new operation focus_{⌜}_{A}_{⌝}, which recognises in the syntax the semantic sobriety of the object A ∈ A. □

This completes the discussion of the object language, so we are now ready to introduce equideductive predicates.

9 Equideductive logic

The symbolic language (pairing, λ-abstraction, application and focus) that we have introduced so far accounts for parts (b–e) of Definition 4.11 for an equideductive category. In this section we describe the new calculus that justifies Notation 1.1 for partial products (parts a and f), although we leave out focus until the next section.

Remark 9.1 First we put our new logic in the setting of type theories in general. It is a two-level dependent type theory that (like the many-sorted first order predicate calculus that it suggests) has a division of contexts into

(a) urtypes, with no dependency, even amongst the urtypes themselves, and

(b) predicates, depending on (variables that range over) urtypes but not predicates.

Urtypes are related by terms. Although these are essentially those of the sober λ-calculus, we do not adopt the interchange rules that we stated before. This is because the burden of reasoning about equality of terms will instead be transferred on to the new theory of predicates. We show that the old axioms become theorems of the new calculus.

Predicates are similarly related by proofs. Unlike terms, these are anonymous (or irrelevant), i.e. we do not distinguish between two proofs of the same predicate, at least as we study the calculus in this paper.

Axiom 9.2 In equideductive logic, cf. Axiom 5.2,

(a) the urtypes are the same as before (Axiom 5.2(a)), being generated from base types such as 0, 1 and ℕ by × and Σ^{(−)};

(b) a context is a list of distinct urtyped variables, i.e. an urcontext in the sense of Axiom 5.2(b), together with a list of urpredicates, whose free variables are amongst those in the urcontext;

(c) the terms and term-formation judgements are those of the restricted λ-calculus (Axiom 5.6), to which we shall add focus in the next section;

(d) the structural rules for variables are as in Axiom 5.4, but since there may be predicates 𝔯⃗(y, z⃗) in the contexts (on the left of ⊢ in a judgement as well as the right), these too undergo substitution in the cut rule (Axiom 9.7):

{x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b : B y : B, z⃗ : C⃗, 𝔮⃗(y), 𝔯⃗(y, z⃗) ⊢ d : D \atop x⃗ : A⃗, z⃗ : C⃗, 𝔭⃗(x⃗), 𝔮⃗(b), 𝔯⃗(b, z⃗) ⊢ [b/y]^{∗}d : D}

(Cut with predicates doesn’t actually have any effect on urterms.)

The principal generalisation is from interchanges to predicates, which also have their own judgements and structural rules that we list below. Because of the difficulties that focus causes, in this section we define urpredicates without allowing it. When we do add it, in the next section, the generalisation is only a syntactic one because the terms that are involved are of type Σ, so it will be possible to eliminate focus from them.

It will be more important in equideductive logic than in the familiar predicate calculus to know exactly what the arguments of a predicate are, so we state them explicitly as x⃗. When we have proved the rules for the product we shall be able to use a single argument instead of a string. By a predicate “on” an urtype, we mean that this is the type of its argument.

Axiom 9.3 The urpredicates of equideductive logic are generated as follows:

(a) ⊤ is an urpredicate on any urtype;

(b) if 𝔭(y⃗) is an urpredicate on B⃗ (i.e. with free variables y⃗ : B⃗) and x⃗ : A⃗ ⊢ f⃗(x⃗) : B⃗ are urterms of the restricted λ-calculus then 𝔭(f⃗(x⃗)) is an urpredicate on A⃗;

(c) in particular, considering A⃗, B⃗ ⊢ A⃗, any urpredicate 𝔭(x⃗) on A⃗ is also 𝔭(x⃗, y⃗) on A⃗, B⃗, so we may freely add arguments on which 𝔭 doesn’t actually depend;

(d) if 𝔭(x⃗) and 𝔮(x⃗) are urpredicates on A⃗ then so is 𝔭(x⃗) & 𝔮(x⃗);

(e) if 𝔮⃗(y⃗) are urpredicates on B⃗ (where the variables y⃗ are distinct from x⃗)

and x⃗ : A⃗, y⃗ : B⃗ ⊢ α, β : Σ are urterms (not involving focus) then

𝔭(x⃗) ≡ ∀y⃗:B⃗. 𝔮⃗(y⃗) =▷ (αx⃗y⃗ = βx⃗y⃗)

is an urpredicate on A⃗;

(f) we omit the symbol =▷ if there are no antecedents 𝔮⃗ to put on the left of it; and

(g) we omit ∀ if there are no bound variables y⃗, but because of the variable binding rule we can only form an unquantified implication 𝔮 =▷ αx⃗ = βx⃗ when the antecedent 𝔮 has no free variables;

(h) in particular, any equation 𝔭(x⃗) ≡ (αx⃗ = βx⃗) between urterms of type Σ is an urpredicate on A⃗.

Example 9.4 For any urterm Γ ⊢ P : Σ^{Σ^{A}}, we express Definition 7.2 in equideductive logic as the urpredicate

prime(P) ≡ ∀Φ:Σ^{3}A. ΦP = P (λx. Φ(λϕ. ϕx)).

Remark 9.5 The use of ∀=▷ is governed by the variable-binding rule (Definition 1.2): all of the variables that occur on the left of =▷ must be bound by ∀. This means that =▷ is much less than Heyting implication: it is really just conjunction indexed by {y⃗ : B⃗ | 𝔭⃗(y⃗)}. It is also a reason for stating the free variables in urpredicates explicitly. (In fact, the predicates with no free variables at all do form a Heyting algebra, including disjunction, as we shall see in [BB].)

Amongst the various operators, our convention is that application binds most tightly, followed by λ-abstraction, equality (=), conjunction (&), disjunction (⋎), implication (=▷), quantification (∀, �) and finally the turnstile (⊢).

Remark 9.6 We shall introduce more general notation for predicates in Notation 9.10 and in later papers, but these will be definitional extensions that may always be put back into the form that we have described. An urpredicate is a conjunction of quantified implications, each of which has an equation of urtype Σ on the right of =▷, and (recursively) a similar conjunction on the left. Therefore, in order to prove something for all predicates, we only need to consider the three cases

⊤,  𝔭(x⃗) & 𝔮(x⃗),  ∀y⃗. 𝔮⃗(y⃗) =▷ (αx⃗y⃗ = βx⃗y⃗),

in which αx⃗y⃗ and βx⃗y⃗ are urterms of type Σ, not involving focus. We shall sometimes treat (unquantified and unqualified) equations on their own as a fourth case.

The theory of the (restricted) λ-calculus in Section 5 was about interchanges between urterms, which could not be quantified and only appeared on the right of ⊢. In equideductive logic we have predicates instead of interchanges and replace the structural rules in Axiom 5.5 by

Axiom 9.7 The structural rules for urpredicates are

(a) reflexivity, symmetry and transitivity of equality;

(b) hypothesis: any urpredicate from the context, i.e. on the left of ⊢, may be asserted as a judgement, i.e. copied to the right of ⊢;

(c) weakening: any urpredicate whose free variables already belong to a context may be added to it;

(d) exchange and contraction: the urpredicates in a context may be permuted and repetitions may be deleted, so the list is just a set, i.e. we ignore order and multiplicity;

(e) cut of an urterm for a variable induces a substitution into the urpredicates on both sides of the ⊢:

{x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b : B y : B, z⃗ : C⃗, 𝔮⃗(y), 𝔯⃗(y, z⃗) ⊢ 𝔰⃗(y, z⃗) \atop x⃗ : A⃗, z⃗ : C⃗, 𝔭⃗(x⃗), 𝔮⃗(b), 𝔯⃗(b, z⃗) ⊢ 𝔰⃗(b, z⃗)}

(f) cut for a predicate into another predicate:

{x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ 𝔮(x⃗)  x⃗ : A⃗, z⃗ : C⃗, 𝔮(x⃗), 𝔯⃗(x⃗, z⃗) ⊢ 𝔰⃗(x, z⃗) \atop x⃗ : A⃗, z⃗ : C⃗, 𝔭⃗(x⃗), 𝔯⃗(x, z⃗) ⊢ 𝔰⃗(x, z⃗)}

(g) cut for a predicate into term-formation,

{x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ 𝔮(x⃗)  x⃗ : A⃗, z⃗ : C⃗, 𝔮(x⃗), 𝔯⃗(x⃗, z⃗) ⊢ d : D \atop x⃗ : A⃗, z⃗ : C⃗, 𝔭⃗(x⃗), 𝔯⃗(x, z⃗) ⊢ d : D}

will only become relevant when we introduce focus. The four versions of cut may be combined into one:

{x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b⃗ : B⃗, 𝔮⃗(b⃗) y⃗ : B⃗, z⃗ : C⃗, 𝔮⃗(y⃗), 𝔯⃗(y⃗, z⃗) ⊢ d⃗: D⃗, 𝔰⃗(d⃗) \atop x⃗ : A⃗, z⃗ : C⃗, 𝔭⃗(x⃗), 𝔯⃗(b⃗, z⃗) ⊢ [b⃗/y⃗]^{∗}d⃗: D⃗, 𝔰⃗([b⃗/y⃗]^{∗}d⃗)}

Turning to the main features of the logic, we shall use cut wherever necessary, without comment. Issues such as cut elimination are not the subject of the present paper and we would like to keep the formality of the deduction to a minimum when we prove theorems about equideductive categories. So we shall blur the distinctions amongst right or introduction, and left or elimination rules, and those using variables or urterms. On the other hand, a future study of the proof theory of equideductive logic may yield interesting alternative models of it.

Axiom 9.8 The logical rules for ⊤ and & are

Γ ⊢ ⊤  Γ, 𝔭(x⃗), 𝔮(x⃗) ⊢ 𝔭(x⃗) & 𝔮(x⃗)  ⊤I, &I
Γ, 𝔭(x⃗) & 𝔮(x⃗) ⊢ 𝔭(x⃗)  Γ, 𝔭(x⃗) & 𝔮(x⃗) ⊢ 𝔮(x⃗)  &E

or

Γ ⊢ 𝔯(x⃗) ; = ; Γ, ⊤ ⊢ 𝔯(x⃗)  Γ, 𝔭(x⃗), 𝔮(x⃗) ⊢ 𝔯(x⃗) ; = ; Γ, 𝔭(x⃗) & 𝔮(x⃗) ⊢ 𝔯(x⃗)  &I, &E

Axiom 9.9 The logical rules for ∀ =▷ are

Γ, y⃗ : A⃗, 𝔭⃗(y⃗) ⊢ αy⃗ = βy⃗ ; = ; Γ ⊢ ∀y⃗:A⃗. 𝔭⃗(y⃗) =▷ αy⃗ = βy⃗  ∀I, ∀E

Beware that, in order to satisfy the variable-binding rule, the 𝔭⃗(y⃗) must not depend on any of the variables in Γ, although α and β may do so. Conversely, since the variables y⃗ are bound, all of the predicates on the left of ⊢ that depend on them must be moved to the left of =▷.

The upward part of this two-way ∀I rule is ∀E for variables (a ≡ y); this is the most convenient formulation for showing how to interpret the logic in a category (Proposition 11.9). We recover the ∀E-rule for urterms from it using cut:

{Γ ⊢ a⃗ : A⃗ Γ ⊢ 𝔭⃗(a⃗) Γ ⊢ ∀y⃗:A⃗. 𝔭⃗(y⃗) =▷ αy⃗ = βy⃗ \atop Γ ⊢ αa⃗ = βa⃗}  ∀E

Another useful form of the elimination rule is

Γ, 𝔭(a⃗), ∀y⃗. 𝔭(y⃗) =▷ ϕy⃗ = ψy⃗ ⊢ ϕa⃗ = ψa⃗.  ∀E

As our first definitional extension, we can generalise implication to allow general predicates instead of just equations on the right of =▷.

Notation 9.10 ∀y. 𝔭(y) =▷ 𝔮(x, y) is defined as

\begin{matrix}⊤ & if & 𝔮(x, y) ≡ ⊤ \\ (∀y. 𝔭(y) =▷ 𝔯(x, y)) & (∀y. 𝔭(y) =▷ 𝔰(x, y)) & if & 𝔮(x, y) ≡ 𝔯(x, y) & 𝔰(x, y) \\ ∀y. ∀z. 𝔭(y) & 𝔯(z) =▷ αxyz = βxyz & if & 𝔮(x, y) ≡ ∀z. 𝔯(z) =▷ αxyz = βxyz. \end{matrix}

Proposition 9.11 These definitions satisfy the introduction and elimination rules in Definition 9.9, but with general predicates on the right. Proof By the ⊤ rule and weakening, (∀y. 𝔭(y) =▷ ⊤) ⊣⊢ ⊤. For conjunction,

Γ, y : B, 𝔭(y) ⊢ 𝔯(x, y) & 𝔰(x, y)

=

Γ, y : B, 𝔭(y) ⊢ 𝔯(x, y) ; = ; Γ ⊢ ∀y. 𝔭(y) =▷ 𝔯(x, y)  Γ, y : B, 𝔭(y) ⊢ 𝔰(x, y) ; = ; Γ ⊢ ∀y. 𝔭(y) =▷ 𝔰(x, y)

= Γ ⊢ (∀y. 𝔭(y) =▷ 𝔯(x, y)) & (∀y. 𝔭(y) =▷ 𝔰(x, y))

For nested implication,

Γ, y : B, 𝔭(y) ⊢ ∀z. 𝔯(z) =▷ αxyz = βxyz = Γ, y : B, 𝔭(y), z : C, 𝔯(z) ⊢ αxyz = βxyz = Γ, ⟨y, z⟩ : B × C, 𝔭(y) & 𝔯(z) ⊢ αxyz = βxyz = Γ ⊢ ∀yz. 𝔭(y) & 𝔯(z) =▷ αxyz = βxyz

This shows why we needed multiple quantifiers and hypotheses in Definition 9.3(e). □

Turning to the rules for λ-terms, recall from Remark 5.1 that there are different ways of formulating those for equality. We used one of these in the restricted λ-calculus (Axiom 5.10), but in equideductive logic the other is more appropriate:

Axiom 9.12 Exponentials satisfy their β- and extensionality rules:

{Γ ⊢ a⃗ : A⃗  Γ, x⃗ : A⃗ ⊢ σ : Σ \atop Γ ⊢ (λx⃗. σ)a⃗ = [a⃗/x⃗]^{∗}σ}  λβ

and ϕ, ψ : ΣA⃗, F : Σ^{ΣA⃗}, ∀x⃗. ϕx⃗ = ψx⃗ ⊢ F ϕ = F ψ.  λ-ext

Whereas extensionality for × said that π_{0} and π_{1} are jointly mono, for λ it says the same for the family of maps {evx⃗ : Σ^{∏ A⃗} → Σ | x⃗ : A⃗}.

We use exponentials and a principle that is attributed to Gottfried Leibniz to extend the definition of equality from Σ to general urtypes:

Definition 9.13 Equality of terms of any urtype,

a = b : A,  is defined as ∀ϕ:Σ^{A}. ϕa = ϕb,  T_{0}

for which reflexivity, symmetry and transitivity follow from Axiom 9.7(a), together with ∀E/I. Since equality at general urtypes is defined by quantification, Proposition 9.11 allows us to use it on the right of =▷, making another definitional extension of the notation for predicates.

The remaining rules of the restricted λ-calculus follow:

Lemma 9.14 Equality for ϕ, ψ : Σ^{A} satisfies

ϕ = ψ ⊣⊢ ∀F. F ϕ = F ψ ⊣⊢ ∀x:A. ϕx = ψx  (∗)

and the equality-transmitting and η-rules for the restricted λ-calculus (cf. Axiom 5.10). Proof The forward direction of (∗) uses ∀E with F ≡ λθ. θx and the converse is λ-ext. Then this rule gives

ϕ = ψ : Σ^{A}, x : A ⊢ ϕx = ψx : Σ,  λE=_{0}

whilst ϕ : Σ^{A}, a = b : A ⊢ ϕa = ϕb : Σ  λE=_{1}

comes from the Leibnizian definition of a = b : A, with ∀E. Then

Γ, ϕ : Σ^{A} ⊢ ϕ = λa. ϕa : Σ^{A}  λη

is ∀a′. ϕa′ = (λa. ϕa)a′ by λβ and (∗) again. Finally, in the rule

{Γ, x⃗ : A⃗ ⊢ σ = τ : Σ \atop Γ ⊢ (λx⃗. σ) = (λx⃗. τ)}  λI=

the top line is equivalent to ∀x. (λx. σ)x = (λx. τ)x by λη and ∀I. This is the same as the bottom line by (∗). Again we use cut to recover forms similar to Axiom 5.10. □

Proposition 9.15 Γ, 𝔭(a), a = b ⊢ 𝔭(b). Proof By Remark 9.6, we must consider the three cases in which 𝔭 is ⊤ (trivial), a conjunction (take the parts separately) or a quantified implication. The last follows from

Γ, ∀y′. 𝔮(y′) =▷ αay′ = βay′, a = b, 𝔮(y) ⊢ αby = βby

using ∀E, λE=_{1} and then λE=_{0}. □

Axiom 9.16 Products satisfy their β- and extensionality rules,

x : A, y : B ⊢ π_{0}⟨x, y⟩ = x : A,  π_{1}⟨x, y⟩ = y : B  ×β

and p, q : A × B, π_{0}p = π_{0}q : A, π_{1}p = π_{1}q : B ⊢ p = q : A × B,  ×-ext

as in Axiom 5.8. For the nullary product we only need to say that

x : 1 ⊢ x = ⋆ : 1.  1-ext

Lemma 9.17 The product A × B also satisfies its equality-transmitting and η-rules. Proof Putting θ ≡ ϕ · π_{0} in Definition 9.13 for equality gives ×E_{0}=,

p = q : X × Y ⊣⊢ ∀θ. θp = θq ⊢ ∀ϕ. ϕ(π_{0}p) = ϕ(π_{0}q) ⊣⊢ π_{0}p = π_{0}q,

and similarly π_{1}p = π_{1}q. The proofs of ×I= and ×η are the same as in Lemma 5.9, but with equality (=) instead of interchangeability (↔). □

Remark 9.18 In the restricted λ-calculus we made allowance for additional base types, operationsymbols and particular interchanges (Remark 5.3). In equideductive logic, there may also be particular axioms, instead of just equations. These may be expressed in any of the following forms:

(a) equations Γ ⊢ σ = τ of type Σ, possibly with equideductive premises,

(b) equations Γ ⊢ a = b of any type A,

(c) closed, unconditional predicates ⊢ 𝔭(), or

(d) general judgements, x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ 𝔮(x⃗), which are inter-provable using the rules that we have stated in this section. The particular interchanges of the restricted λ-calculus are examples of (b) where Γ is an urcontext (with no predicates). In equideductive logic, on the other hand, we prefer to take (a) as canonical. Whereas in Definition 6.6 we took particular interchanges to be at base urtypes A, we now prefer just to use Σ, interpreting the previous convention by means of Leibnizian equality and an additional variable ϕ : Σ^{A} in the context. In Section 13 we shall use particular axioms to force the logic to match any given equideductive category.

10 Sobriety in equideductive logic

We now introduce focus into equideductive logic as we did for the restricted λ-calculus in Section 8 and then show how to eliminate the proof-theoretic difficulties that it causes.

Axiom 10.1 Sobriety is expressed by the introduction and β-rules

Γ ⊢ P : Σ^{Σ^{A}} Γ ⊢ prime(P)
Γ ⊢ focus_{A} P : A

Γ ⊢ P : Σ^{Σ^{A}} Γ ⊢ prime(P)
Γ, ϕ : Σ^{A} ⊢ ϕ(focus_{A} P) = P ϕ

for any base type A, where the predicate prime(P) was defined in Example 9.4. We have already stated the T_{0} rule as Definition 9.13. To these we add pairing and the structural rules apart from cut, as before.

Since equideductive logic allows hypotheses in the context, unlike the sober λ-calculus in Section 8, an urterm may now be conditionally prime, i.e. primality can depend on such hypotheses. It may also be combined with other equideductive predicates.

Instead of giving axioms for predicates involving focus, we shall show that they may be obtained as a definition extension, as we did when defining focus for product and exponential types. We also define cuts and substitutions of focus-terms into predicates.

The lemmas that did this in Section 8 remain valid with equideductive equality in place of interchangeability and when primality is allowed to be conditional on hypotheses.

.

Lemma 10.2 For any Γ ⊢ a : A, the term Γ ⊢ P ≡ λϕ. ϕa satisfies Γ ⊢ prime(P). Proof By λβ, in the context Γ, Φ : Σ^{3}A,

P (λx. Φ(λψ. ψx)) ≡ (λϕ. ϕa)(λx. Φ(λψ. ψx)) = Φ(λψ. ψa) ≡ ΦP,

so Γ ⊢ ∀Φ. ΦP = P (λx. Φ(λψ. ψx)) by Axiom 9.9. □

Lemma 10.3 Sobriety obeys its η- and equality-transmitting laws (Axiom 8.1). Proof The η-rule

x : A ⊢ focus_{A}(λϕ. ϕx) = x : A,  focus η

which is well formed by the previous lemma, follows from the focus β- and λβ-rules,

x : A, θ : Σ^{A} ⊢ θ( focus_{A}(λϕ. ϕx)) = (λϕ. ϕx)θ = θx,

and Definition 9.13 for equality at urtype A. The equality-transmitting rule for focus is

P = Q ⊣⊢ ∀ϕ. P ϕ = Qϕ ⊣⊢ ∀ϕ. ϕ(focus P) = ϕ(focus Q) ⊣⊢ focus P = focus Q, focus =

which comes from Lemma 9.14, focus β and the definition of equality, cf. Lemma 8.4. □

Theorem 10.4 Any two terms that are definable and provably interchangeable in the sober λcalculus obey the equality predicate in equideductive logic. □

The cut rule in the λ-calculus supplies a term to be substituted for a free variable in the context, but in a predicate calculus like equideductive logic it may also provide a proof for a hypothesis (Axiom 9.7(f,g)). We must therefore show how to define or eliminate the new cuts that assert predicates. However, there is only one of these in Axiom 10.1:

Lemma 10.5 The equation ϕ(focus P) = P ϕ is redundant as a hypothesis in the contexts of a proof, so it may simply be deleted from them.

Proof This equation is only well formed according to Definition 10.15 if prime(P) is already provable from the earlier part of the context in which it appears. It ought therefore to be redundant because it is an axiom (focus β).

Suppose that we simply delete this equation wherever it occurs as a hypothesis in the contexts of a proof. All of the steps of the proof remain valid, with the exception of any instances of the hypothesis rule (Axiom 9.7(b)) that copy this equation from the left to the right of ⊢. These steps may be replaced by copies of the proof of prime(P) in the appropriate context, followed by the focus β-rule. □

This completes the definitional extension of allowing the focus operation:

Theorem 10.6 The contexts and predicates in Definition 10.15 (possibly involving focus) satisfy the structural and logical rules that were given for urpredicates (without it) in the previous section.

□

When we define the classifying category Cn_{L}^{∀} in Section 12 we will need to identify its injective objects. Their syntactic characterisation will be as follows:

Definition 10.7 An urtype B is called syntactically injective if, whenever a term

x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b : B

is provably well formed in equideductive logic (possibly using focus) there is some urterm (without focus),

x⃗ : A⃗ ⊢ c : B,

that is already provably well formed in the restricted λ-calculus (Section 5) and the equation

x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b = c : B

is provable in equideductive logic.

Lemma 10.8 The type Σ is syntactically injective. Proof Let x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ σ : Σ be a term that may involve focus. We may eliminate this by the normalisation theorem, possibly relying on the hypotheses 𝔭⃗(x⃗), to obtain an urterm τ. This may contain the variables x⃗ : A⃗ but is unconditionally well formed. It is equal to σ under the given hypotheses. □

Lemma 10.9 Any exponential Σ^{B} is syntactically injective. Any product or retract of syntactically injective types is again syntactically injective. □

Proposition 10.10 The following are equivalent for an urtype A:

(a) A is syntactically injective;

(b) focus_{A} is representable by an urterm F : Σ^{Σ^{A}} ⊢ a_{F} : A;

(c) A is a retract of some exponential Σ^{B}. Proof [a⊢b]: The syntactic injectivity property applied to

P : Σ^{Σ^{A}}, prime(P) ⊢ focus P : A

yields an urterm F : Σ^{Σ^{A}} ⊢ a_{F} : A such that

P : Σ^{Σ^{A}}, prime(P) ⊢ a_{P} = focus P,

so P ϕ = ϕ(focus P) = ϕ(a_{P}). Beware that, although one can deduce from this result that syntactically injective types are exponentiable, whilst F is a free variable in the term a_{F}, the restricted λ-calculus does not allow us to form λF. a_{F}.

[b⊢c]: This term makes A ◁ Σ^{Σ^{A}}. [c⊢a]: By the previous result. □

Any urtype A may therefore be embedded in a syntactically injective object, namely Σ^{Σ^{A}}, but if we are going to use this instead of A itself then we also have to replace predicates on A by those on Σ^{Σ^{A}}.

Notation 10.11 For F : Σ^{Σ^{A}}, write 𝔭̄(F) ≡ ∀ϕψ. (∀x. 𝔭(x) =▷ ϕx = ψx) =▷ F ϕ = F ψ.

Lemma 10.12 This satisfies a “double negation” property:

x : A, 𝔭(x) ⊣⊢ 𝔭̄(λϕ. ϕx) ≡ ∀ϕψ. (∀x′. 𝔭(x′) =▷ ϕx′ = ψx′) =▷ ϕx = ψx.

Proof The forward direction is essentially ∀E. The most complicated case of the converse is

𝔭(x) ≡ ∀y. 𝔮(y) =▷ αxy = βxy.

Using ∀E,

x′ : A, y : B, 𝔮(y), ∀y′. 𝔮(y′) =▷ αx′y′ = βx′y′ ⊢ αx′y = βx′y,

so by ∀I,

y : B, 𝔮(y) ⊢ ∀x′. (∀y′. 𝔮(y′) =▷ αx′y′ = βx′y′) =▷ αx′y = βx′y,

which is y : B, 𝔮(y) ⊢ ∀x′. 𝔭(x′) =▷ αx′y = βx′y.

Together with this, ϕ ≡ λx′. αx′y and ψ ≡ λx′. βx′y in 𝔭̄(λθ. θx) give

x : A, 𝔭̄(λθ. θx), y : B, 𝔮(y) ⊢ ϕx = αxy = βxy = ψy,

so x : A, 𝔭̄(λθ. θx) ⊢ (∀y. 𝔮(y) =▷ αxy = βxy) ≡ 𝔭(x).

The case of 𝔭(x) ≡ ⊤ is ∀E. If 𝔭(x) ≡ 𝔮(x) & 𝔯(x) then 𝔭(x) ⊢ 𝔮(x) so 𝔭̄(λθ. θx) ⊢ 𝔮̄(λθ. θx) ⊢ 𝔮(x). These exhaust the possibilities by Remark 9.6. □

Warning 10.13 This can only be done if the sub-formula 𝔮 does not depend on x, so the variablebinding rule (Definition 1.2) is essential.

Hence we may embed any context in an injective object like this:

Lemma 10.14 For any term x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ b : B, 𝔮(b) in equideductive logic, there is an urterm

x⃗ : A⃗ ⊢ (Qx⃗) : Σ^{Σ^{B}}

that is definable in the restricted λ-calculus and satisfies

x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ (Qx⃗ = λψ. ψb), prime(Qx⃗), 𝔮̄(Qx⃗)

in equideductive logic. Conversely, every such urterm

x⃗ : A⃗ ⊢ Qx⃗ : Σ^{Σ^{A}} such that x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ prime(Qx⃗), 𝔮̄(Qx⃗)

arises in this way from a term b ≡ focus(Qx⃗) with 𝔮(b).

The (ur)terms Q and b are unique in the sense that any alternatives Q′ and b′ satisfy

x⃗ : A⃗, 𝔭⃗(x⃗) ⊢ Qx⃗ = Q′x⃗ : Σ^{Σ^{B}} or b = b′ : B.

Proof By Example 10.9(d) there is an urterm (Qx⃗) that is defined without hypotheses and is conditionally equal to λψ. ψb. Hence it is conditionally prime by Lemma 10.2 and Proposition 9.15. It satisfies 𝔮̄(Qx⃗) by Lemma 10.12.

Conversely, if x⃗ : A⃗, 𝔭(x⃗) ⊢ prime(Qx⃗) then

x⃗ : A, 𝔭(x⃗) ⊢ b ≡ focus(Qx⃗) : B

is well formed by Axiom 10.1 and satisfies

x⃗ : A, 𝔭(x⃗) ⊢ Qx⃗ = λϕ. ϕb, 𝔮(b)

by focus β and Lemma 10.12. It is unique by Lemma 10.3. □

Definition 10.15 Predicates and contexts possibly containing focus are defined by the following rules:

{Γ, y⃗ : B⃗, 𝔮⃗(y⃗) ⊢ σ, τ : Σ \atop Γ ⊢ ∀y⃗. 𝔮⃗(y⃗) =▷ σ = τ pred}

where the proofs that the terms σ and τ are well formed may involve applying focus to other terms that are prime conditionally on 𝔮⃗(y⃗), although of course we also allow the possibility that this sequence be empty; and

Γ ctxt x ∉ Γ A type

[Γ, x : A] ctxt

Γ ⊢ 𝔭 pred
[Γ, 𝔭] ctxt

Informally, for any term, predicate or context involving focus P to be well formed, prime(P) must be provable from the hypotheses to its left, in which we include the (quantified) antecedents of =▷. (The exchange rule has to be restricted to make this meaningful.)

This more general definition of predicate must be accompanied by corresponding generalisations of the ∀-rules. On the other hand, we may have inserted focus into an urpredicate by a (generalised) cut or substitution for a variable. We therefore have to show that these two proof rules commute, or rather define the first in terms of the second:

Lemma 10.16 If P is prime and 𝔭(x) ≡ ∀y⃗. q⃗(y⃗) =▷ αy⃗x = βy⃗x then the predicate

∀y⃗. q⃗(y⃗) =▷ P (λx. αy⃗x) = P (λx. βy⃗x)

serves for 𝔭(focus P). Proof The cut that is needed to define this,

Γ ⊢ P : Σ^{Σ^{A}}, prime(P)
Γ ⊢ focus P : A

x : A, Δ, y⃗ : B⃗, q⃗(y⃗) ⊢ αy⃗x = βy⃗x = x : A, Δ ⊢ 𝔭(x) ≡ ∀y⃗:B⃗. q⃗(y⃗) =▷ αy⃗x = βy⃗x

Γ, Δ ⊢ 𝔭(focus P)

is implemented by

{Γ ⊢ P : Σ^{Σ^{A}}  x : A, Δ, y⃗ : B⃗, q⃗(y⃗) ⊢ αy⃗x = βy⃗x ; = ; x : A, Δ, q⃗(y⃗) ⊢ λy⃗. αy⃗x = λy⃗. βy⃗x \atop Γ, Δ, q⃗(y⃗) ⊢ P (λy⃗. αy⃗x) = P (λy⃗. βy⃗x)}
Γ, Δ ⊢ ∀y⃗. q⃗(y⃗) =▷ P (λx. αy⃗x) = P (λx. βy⃗x)

□

11 Interpretation in an equideductive category

Now we return to the category theory to show that our new logic can be interpreted in it, following the plan that we set out in Section 6. As before, we assume given an interpretation of the base types and operation-symbols of a language L in the subcategory A ⊂ Q of urspaces, to which we add some particular axioms. We only need to interpret the minimal version of the logic that we set out in Section 9, but we shall also describe the behaviour of focus, which we introduced as a definitional extension in the previous section.

Remark 11.1 We may adopt parts (a–l) of Proposition 6.1 directly in order to interpret Axiom 9.2, that is,

(a) urtypes,

(b) urcontexts (lists of urtypes, without predicates),

(c) urterms (without focus) and

(d) the structural rules for variables. In particular, the urtypes are interpreted as urspaces in A ⊂ Q as before. Recall that these have to be exponentiable and therefore sober in that category.

Lemma 11.2 The interpretation ⟦A⟧ of any syntactically injective urtype A of L_{∀} must be an injective object of Q. Proof By Proposition 10.10, A is a retract of an exponential urtype, so ⟦A⟧ is a retract of an exponential urspace of Q, which is injective by Lemma 4.5. □

By the remaining parts of Proposition 6.1, we still have

Lemma 11.3 If two urterms x⃗ : A⃗ ⊢ b, c : B are interchangeable in the sense of the restricted λ-calculus then they are denoted by the same morphism ⟦b⟧ = ⟦c⟧ : Π⟦A⃗⟧ ⇉ ⟦B⟧ in Q. □

However, interchangeability of urterms in the restricted λ-calculus is not the same thing as obeying an equality predicate in equideductive logic. We therefore need to convert the interpretation of one calculus into the other. We begin with those things that can be done using finite limits (products, pullbacks and equalisers) in the category Q.

Lemma 11.4 The intepretation takes any syntactic product cone of urtypes

[figure: A; π_{0}; A × B; π_{1}; B]

to a categorical product of urspaces in A ⊂ Q. Moreover, maps from any object of Q to this product respect its universal property. Hence the rules for × stated in Axiom 9.16 and Lemma 9.17 are sound, i.e. if two urterms satisfy the equality predicate then they have the same denotation, without invoking the proof of this Lemma. □

Next, recall from Section 9 that an urpredicate is defined in an urcontext (a list of variables without hypotheses) as an equation between urterms (without focus) on the right of a quantified implication.

Definition 11.5 The denotation of an urpredicate is an M-map from a general Q-object into an A-object, defined by structural recursion as follows:

(a) The true predicate, ⊤, defines the total subspace, ⟦x⃗ : A⃗, ⊤⟧ ≅ ΠA⃗, and satisfies Axiom 9.8.

(b) When 𝔭(x⃗) is an equation x⃗ : A⃗ ⊢ b = c : B, the denotation is given by the equaliser,

[figure: ⟦x⃗ : A⃗, b = c⟧; ΠA⃗; ⟦b⟧; ⟦c⟧; B.]

Notice that this interprets equality at arbitrary urtypes, not just Σ, so we will have to show (in Lemma 11.12) that this agrees with Definition 9.13.

(c) Conjunction, &, is given by the intersection or pullback,

[figure: ⟦x⃗ : A⃗, 𝔭(x⃗) & 𝔮(x⃗)⟧; ⟦x⃗ : A⃗, 𝔮(x⃗)⟧; ⟦x⃗ : A⃗, 𝔭(x⃗)⟧; ΠA⃗.]

(d) We shall interpret ∀=▷ in Proposition 11.9. A context Γ ≡ [x⃗ : A, 𝔭⃗(x⃗)] containing predicates is also interpreted by a subspace of the product ∏ A⃗, using similar pullback diagrams.

Definition 11.6 An equideductive judgement Γ ≡ [x⃗ : A⃗, 𝔭⃗(x⃗)] ⊢ 𝔯(x⃗) is valid in the interpretation if there is an inclusion (commutative triangle)

⟦Γ⟧[figure: .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .] ⟦𝔯⟧
[figure: ⟦𝔭⟧; ⟦𝔯⟧]
∏ A_{i}

of the subspace of ∏ A⃗ that is the denotation of Γ in the denotation of 𝔯. The existence or otherwise of such a map is a question of fact in Q and is not additional structure.

We say that an equideductive category Q is a model of a system of particular axioms (Remark 9.18) if they are valid this sense. We also have to show that each of the rules is sound, i.e. that if its premises are valid then so is its conclusion.

Lemma 11.7 An equality judgement Γ ⊢ b = c : B betweem urterms is valid in Q iff they have the same denotation ⟦b⟧ = ⟦c⟧ : ⟦Γ⟧ ⇉ ⟦B⟧ as morphisms of Q.

⟦Γ⟧
[figure]
[figure: ⟦b = c⟧; . . . . . . . .; ∏ ⟦A⃗⟧; ⟦b⟧; ⟦c⟧; ⟦B⟧]

Proof The denotations of the urterms are the composites ⟦Γ⟧ ⇉ ⟦B⟧ and that of the equality predicate is the equaliser. The two urterms therefore have the same denotation (these composites are the same) iff they factor through the equaliser (the predicate is valid). □

Lemma 11.8 The structural rules except cut (Axiom 9.7) and the logical rules for ⊤, & and × (Axioms 9.8 and 9.16) are sound. Proof From the diagrams in Definition 11.5,

(a) the hypothesis rule is interpreted by the inclusion from the intersection;

(b) weakening is given by pre-composition of an inclusion;

(c) reflexivity is given by the diagonal;

(d) exchange, contraction, symmetry and transitivity are properties of this intersection; and

(e) the rules for ⊤ and & are also interpreted in Definition 11.5.

This leaves products. We deduce the equideductive ×β-rule by applying Lemma 11.7 to the rule of the same name in the restricted λ-calculus, which is valid by Lemma 11.3. The ×-extensionality rule illustrates the interpretation of urpredicates: The denotation of the left hand side is the intersection of the equalisers

[figure: •; Γ; p; q; A × B; π_{0}; A; and; •; Γ; p; q; A × B; π_{1}; B,]

whilst the right hand side is the equaliser • ↣ Γ ⇉ A × B of p and q, but these are isomorphic finite limits in the category Q. □

Now we add the ideas of Section 2 to the finite limits that we have used so far.

Proposition 11.9 The connectives ∀ and =▷ (Axiom 9.9)

Γ, y : B, 𝔮(y) ⊢ αxy = βxy = Γ ⊢ ∀y:B. 𝔮(y) =▷ αxy = βxy

are soundly interpreted by the following partial product diagram (cf. Definition 2.1):

E ≡ ⟦x : A, ∀y:B. 𝔮(y) =▷ αxy = βxy⟧
[figure: ....................; bottom line; bottom right]
[figure: ⟦Γ⟧; ⟦a⟧; ⟦A⟧]

E × Y  Y ≡ ⟦y : B, 𝔮(y)⟧
[figure: ....................]
[figure: ⟦Γ⟧ × Y; ⟦a⟧ × Y; ⟦A⟧ × Y]
.................... top line
[figure: D ≡ ⟦x : A, y : B, αxy = βxy⟧; top right; ⟦A⟧ × ⟦B⟧; α; β; Σ]

Proof We construct the partial product and show that the rules are sound. The inclusions in the middle column are contexts with urpredicates (Definition 11.5). The trapezium commutes because the composites from E × Y to Σ are the same, whilst the object D is the equaliser of α and β. Somehow this gives the ∀E rule. The univeral property provides the dotted maps on the left, which asset validity of the judgements that form the ∀I rule (Proposition 11.8). □

The next stage brings in the categorical ideas from Section 4 (exponentials of urspaces) and the symbolic ones in Section 5 (the restricted λ-calculus), replacing parts (k,l,q) of Proposition 6.1. These depend on ∀=▷ because of the way in which we axiomatised the λ-calculus in Section 9.

Proposition 11.10 The rules for the λ-calculus (Axiom 9.12) are valid in this interpretation. Proof By Lemma 11.3, urterms that are interchangeable using the λβ-rule have the same denotation, so the equality predicate between them is ⊤ by Lemma 11.7. By Lemma 4.10, the (*) property in Lemma 9.14,

∀x. ϕx = ψx ⊣⊢ ϕ = ψ,

is valid in the equideductive category. Extensionality, the η- and equality-transmitting rules follow from this by Lemma 11.7 since Definition 11.5(b) interpreted equality at general urtypes, not just Σ. □

Apart from Leibnizian equality and cut, this completes the interpretation of the part of the logic that we introduced in Section 9, so now we add sobriety from Sections 8 and 10.

Lemma 11.11 The operation focus of equideductive logic (Axiom 10.1 and the extensions in Lemmas ?? and 8.7) is interpreted in an equideductive category in the same way as that of the sober λ-calculus. Proof The interpretation ⟦A⟧ of any urtype must be exponentiable and therefore sober, so it defines an equaliser diagram as in Theorem 8.14. The difference is that primality may now depend on equational hypotheses, because the introduction rule for focus in equideductive logic allows a general context Γ on the left. The interpretation ⟦Γ⟧ of this context may therefore be an arbitrary object of Q, not just of A, but in the definition of an equideductive category we required that all objects respect the universal properties. The mediator to the equaliser therefore respects the focus β-rule (Axiom 10.1) and the other rules follow from Lemma 10.3. □

Since Leibnizian equality (Definition 9.13) may be seen as the equality-transmitting rule for focus, these ideas also yield

Lemma 11.12 Equality at general urtypes is valid. Proof One direction follows from Lemma 11.7. Conversely, let Γ ⊢ a, b : A be urterms for which the equideductive predicate Γ ⊢ ∀ϕ. ϕa = ϕb denotes ⊤. Then Γ, ϕ : Σ^{A} ⊢ a = b also denotes ⊤ by Proposition 11.9 and Γ ⊢ λϕ. ϕa = λϕ. ϕb denotes ⊤ by Proposition 11.10. By Lemma 11.7, the equaliser of the composites ⟦Γ⟧ ⇉ ⟦Σ^{Σ^{A}}⟧ in

[figure: ⟦λϕ. ϕa = λϕ. ϕb⟧; ⟦Γ⟧; ⟦a⟧; ⟦b⟧; ⟦A⟧; η; ⟦Σ^{Σ^{A}}⟧]

is ⟦Γ⟧, so these composites are the same. The interpretation ⟦A⟧ of a urtype in an equideductive category is an urspace, which is sober by Proposition 7.7. Therefore the map η is mono, so ⟦a⟧ and ⟦b⟧ : ⟦Γ⟧ ⇉ ⟦A⟧ are also the same. Hence their equaliser is also the whole of ⟦Γ⟧, which means that the denotation of Γ ⊢ a = b is ⊤. □

12 The classifying category

Now we shall construct the category of contexts and substitutions Cn_{L}^{∀} for equideductive logic, as we did for the restricted λ-calculus in Definition 6.3. Then the interpretations of L in an equideductive category Q that we considered in the previous section correspond to structurepreserving functors ⟦−⟧ : Cn_{L}^{∀} → Q.

Remark 12.1 Following the example of Cn_{L}^{λ} directly, we might expect the objects of Cn_{L}^{∀} to be contexts and the morphisms to be strings of provable judgements like

x⃗ : A⃗, 𝔭(x⃗) ⊢ b⃗ : B⃗, 𝔯(b⃗).

However, there are problems of existence and uniqueness if we do this:

(a) there need be no valid derivation of the terms x⃗ : A⃗ ⊢ b⃗ : B⃗ without using the hypothesis 𝔭(x⃗), since formation of b⃗ may involve sub-terms focus P for which the proofs of the primality equations for the P depend on the 𝔭(x⃗); and

(b) there may be many intrinsically different terms that represent what should be a single morphism.

Since the unconditional urterm x⃗ : A⃗ ⊢ b⃗ : B⃗ would fill in the dotted map in the square

[figure: [x⃗ : A⃗, 𝔭(x⃗)]; [y⃗ : B⃗, 𝔮(y⃗)]; [x⃗ : A⃗]; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; .; ?; [y⃗ : B⃗]]

the property that we need for (a) is injectivity of B⃗. We studied this semantically in Section 4: the injective urspaces in Sob are the continuous lattices, whereas the most general ones are locally compact spaces. Definition 10.7 provided the analogous syntactic idea, which is what we shall use.

Unfortunately, we therby lose the verbatim interpretation of the base types of the language L, but we shall repair this in Section 14. For (b), a morphism must be an equivalence class of urterms.

Definition 12.2 In Cn_{L}^{∀}, cf. Definition 6.3 for Cn_{L}^{λ},

(a) an object is a context

[x_{1} : A_{1}, …, x_{n} : A_{n}, 𝔭(x⃗)]

where A⃗ are syntactically injective urtypes and 𝔭(x⃗) is an urpredicate (without focus);

(b) an urspace is an object for which 𝔭(x⃗) is ⊤;

(c) a morphism

f⃗: [x⃗ : A⃗, 𝔭(x⃗)] ⟶ [y⃗ : B⃗, 𝔯(y⃗)]

is an equivalence class of strings of urterms (without focus)

x⃗ : A⃗ ⊢ f_{j}x⃗ : B_{j} such that x⃗ : A⃗, 𝔭(x⃗) ⊢ 𝔯(f⃗x⃗),

where f⃗ represents the same morphism as g⃗ if

x⃗ : A⃗, 𝔭(x⃗) ⊢ f⃗x⃗ = g⃗ x⃗;

(d) the identity morphism on [x⃗ : A⃗, 𝔭(x⃗)] is the string x⃗ : A⃗ ⊢ x_{j} ≡ π_{j}x⃗ : A_{j};

(e) if x⃗ : A⃗, 𝔭(x⃗) ⊢ 𝔮(x⃗) then there is a canonical inclusion [x⃗ : A⃗, 𝔭(x⃗)] ↣ [x⃗ : A⃗, 𝔮(x⃗)] that is defined in the same way as the identity;

(f) composition is given by substitution, as it was in Cn_{L}^{λ};

(g) we write 1 ≡ [⊤] for the empty urcontext with the true predicate; and

(h) we also write Σ for the object [σ : Σ, ⊤], where the constant ⋆ : Σ defines a morphism 1 → Σ.

Lemma 12.3 The structure Cn_{L}^{∀} is a category with a choice of products. Proof To the proof of Lemma 6.4 we add that the identity is well formed because 𝔯 ≡ 𝔭 and composition respects well-formedness by Axiom 9.7(f).

Proof It is necessary to show that “f⃗ = g⃗ ” is an equivalence relation, that the identity satisfies the well-formedness condition, that composition respects both of these things and that the identity and associativity axioms hold up to equivalence. □

Although we cannot interpret the language L directly in Cn_{L}^{∀} because we have only used injective urtypes, we can lift interpretations in other categories:

Lemma 12.4 Let ⟦−⟧ be an interpretation of the language L in an equideductive category Q. Then the interpretation of the contexts that we have used as objects and of strings of terms defines a functor ⟦−⟧ : Cn_{L}^{∀} → Q. Proof Definition 11.5 provides the interpretation of the objects (contexts) and Remark 11.1 that of morphisms (urterms). □

Along with proving that Cn_{L}^{∀} has the structure of an equideductive category we shall also show that the functor ⟦−⟧ preserves this structure.

Lemma 12.5 The category Cn_{L}^{∀} has all finite products and the functor ⟦−⟧ : Cn_{L}^{∀} → Q preserves them. The product of two urspaces is another urspace. Proof The terminal object is 1, to which the only incoming morphism is the empty string. Binary products in Cn_{L}^{∀} are defined by

[x⃗ : A⃗, 𝔭(x⃗)] × [y⃗ : B⃗, 𝔯(y⃗)] ≡ [x⃗ : A⃗, y⃗ : B⃗, 𝔭(x⃗) & 𝔯(y⃗)],

so in particular the product of two urspaces is another urspace since ⊤ & ⊤ ⊣⊢ ⊤. Pairing and projections are given by combining and eliminating sub-strings. Since such strings of urterms may be defined in any context, ther latter respects such products. The interpretation preserves this by Lemma 11.4. □

Lemma 12.6 The category Cn_{L}^{∀} has equalisers and the functor ⟦−⟧ : Cn_{L}^{∀} → Q preserves them.

[figure: E ≡ [x⃗ : A⃗, 𝔭(x⃗) & f⃗x⃗ = g⃗x⃗ ]; X ≡ [x⃗ : A⃗, 𝔭(x⃗)]; f⃗; g⃗; Y ≡ [y⃗ : B⃗, 𝔯(y⃗)]]

Proof The construction is illustrated by the diagram. In this, 𝔯 is irrelevant because we may take the equality to be at type ΠB. The interpretation Cn_{L}^{∀} → Q preserves this structure by Definition 11.5(b). □

Lemma 12.7 The full subcategory A ⊂ Cn_{L}^{∀} of urspaces has exponentials Σ^{(−)}, whose universal property is respected by all objects of Cn_{L}^{∀} and preserved by ⟦−⟧. Proof By λ-abstraction there is a natural bijection between morphisms

[y⃗ : B⃗, 𝔮(y⃗)] × [x⃗ : A⃗, ⊤] ⟶ Σ ≡ [σ : Σ, ⊤] and [y⃗ : B⃗, 𝔮(y⃗)] ⟶ [ϕ : ΣA⃗, ⊤].  □

Lemma 12.8 The category Cn_{L}^{∀} has partial products (Definition 2.1) and their inclusions are (isomorphic to) canonical inclusions.

E ≡ [x⃗ : A⃗, 𝔯(x⃗)]
[figure: ....................; f⃗; i]
Γ ≡ [z⃗ : C⃗, 𝔰(z⃗)]  \overline{f⃗}  \overline{}[x⃗ : A⃗, 𝔭(x⃗)] ≡ X

E × Y ≡ [x⃗, y⃗, 𝔯(x⃗) & 𝔮(y⃗)]
[figure: ....................]
[figure: Γ × Y ≡ [z⃗, y⃗, 𝔰(z⃗) & 𝔮(y⃗)]; f⃗ × Y; [x⃗, y⃗, 𝔭(x⃗) & 𝔮(y⃗)] ≡ X × Y]

....................

[figure: [z⃗ : C⃗, y⃗ : B⃗]; [x⃗, y⃗, αx⃗y⃗ = βx⃗y⃗]; [x⃗ : A⃗, y⃗ : B⃗]; α; β; Σ]

where 𝔯(x⃗) ≡ 𝔭(x⃗) & ∀y⃗. 𝔮(y⃗) =▷ αx⃗y⃗ = βx⃗y⃗.

All objects of Cn_{L}^{∀} respect partial products and the interpretation Cn_{L}^{∀} → Q preserves them. Proof The universal property is tested by a morphism Γ → X that is a string of urterms z⃗ : C⃗ ⊢ f⃗z⃗ : A⃗ such that

z⃗ : C⃗, 𝔰(z⃗) ⊢ 𝔭(f⃗z⃗) and z⃗ : C⃗, y⃗ : B⃗, 𝔰(z⃗), 𝔮(y⃗) ⊢ α(f⃗z⃗)y⃗ = β(f⃗z⃗)y⃗,
so  z⃗ : C⃗, 𝔰(z⃗) ⊢ ∀y⃗. 𝔮(y⃗) =▷ α(f⃗z⃗)y⃗ = β(f⃗z⃗)y⃗,

which, together with 𝔭(f⃗z⃗), is 𝔯(f⃗z⃗). Hence the mediator Γ → E is defined by the same string f⃗. □

Lemma 12.9 All objects of Cn_{L}^{∀} are generated from urspaces by pullbacks and partial products, whilst all canonical inclusions arise from partial products. Proof We use recursion on the defining urpredicate of the object, by Remark 9.6:

(a) {A | ⊤} is an urspace;

(b) {A | 𝔭 & 𝔮} is the intersection (pullback) of {A | 𝔭} and {A | 𝔮} rooted at A (cf. Definition 11.5(c)); and

(c) {x : A | ∀y. 𝔭(y) =▷ αxy = βxy} is a partial product whose types involve simpler predicates. □

Lemma 12.10 All urspaces in the sense of Definition 12.2(b), in particular Σ, are injective. There are enough injectives, in the well founded sense of Axiom 4.6.

[figure: [x : A, 𝔭(x)]; id; [x : A, 𝔮(x)]; id; [x : A, ⊤]; [y : B, ⊤]; f; = = = = = =; [y : B, ⊤]; f; . . . . . . . .; = = = = = =; [y : B, ⊤]; f]

Proof Partial product inclusions are the same as canonical inclusions by Proposition 12.8 and Lemma 12.9. By Definition 12.2(c), a morphism [x : A, 𝔭(x)] → [y : B, ⊤] is represented by some urterm x : A ⊢ fx : B, which also represents morphisms [x : A, ⊤] → [y : B, ⊤] and [x : A, 𝔮(x)] → [y : B, ⊤]. Since the same urterm represents all of the morphisms, they make the diagram commute. Hence [y : B, ⊤] is injective. There are enough injectives, because by Definition 12.2(a) any object is of the form [y : B, 𝔮(y)] and has a canonical or partial product inclusion into [y : B, ⊤]. This is well founded by Lemma 12.9. □

Proposition 12.11 The category Cn_{L}^{∀} is equideductive. Moreover, any interpretation of L in an equideductive category Q extends to a functor ⟦−⟧ : Cn_{L}^{∀} → Q that preserves the structure and this extension is unique up to unique isomorphism. □

In Section 14 we shall show how to interpret the non-injective types of the language L in the category Cn_{L}^{∀} and hence justify calling it the classifying category for the logic.

13 Completeness

We show in this section that the equideductive logic that we described in Sections 9–10 is complete for the notion of equideductive category defined in Section 4. That is, any such category Q is equivalent to the classifying category Cn_{L_{∀}}^{∀} for its proper language L_{∀}. This builds on the corresponding results for the restricted λ-calculus in Section 6.

Definition 13.1 The proper language L_{∀} of an equideductive category Q consists of the proper λ-calculus L_{λ} of its subcategory of injective objects (Definition 6.6) together with a particular axiom (Remark 9.18)

Γ ⊢ σ = τ whenever the maps ⟦Γ⟧ [figure: ⟦σ⟧; ⟦τ⟧] Σ

are the same in Q. No global choice of structure is necessary to state this, just the existence of the finitely many pullbacks and partial products that are needed to define some interpretation of Γ, σ and τ in Q. This definition is invariant under isomorphism and therefore remains valid for other choices of pullbacks and partial products, so the maps ⟦σ⟧′, ⟦τ⟧′ : ⟦Γ⟧′ ⇉ Σ are also the same.

Lemma 13.2 If Q does have a choice of the structure for an equideductive category then there is a diagram of functors

[figure: A; ⌜−⌝; ≃; \underline{⟦−⟧_{λ}}; Cn_{L_{λ}}^{λ}; Q; ⟦−⟧_{∀}; Cn_{L_{∀}}^{∀}]

that commutes “on the nose” from A or Cn_{L_{λ}}^{λ} to Q, where

(a) L_{λ} is the proper language of A in the resticted λ-calculus (Definition 6.6), and

(b) Cn_{L_{λ}}^{λ} is its classifying category (Definition 6.3), so

(c) A ≃ Cn_{L_{λ}}^{λ} with ⟦⌜A⌝⟧ = A and η_{Γ} : Γ ≅ ⌜⟦Γ⟧⌝ by Theorem 6.8,

(d) L_{∀} is the proper language of Q as defined above,

(e) Cn_{L_{∀}}^{∀} is its classifying category, defined in the previous section, and

(f) ⟦−⟧_{∀} : Cn_{L_{∀}}^{∀} → Q is its interpretation, as in Section 11, since Q is a model of its own particular axioms. □

Notation 13.3 For any context Γ ≡ [z⃗ : C⃗, 𝔯(z⃗)], we write Γ_{0} ≡ [z⃗ : C⃗] for the ambient urcontext (without the predicate) and i_{Γ} : Γ ↣ Γ_{0} for its canonical inclusion. Then ⟦Γ_{0}⟧ is injective in Q by Lemma 11.2 and ⟦i_{Γ}⟧ is an M-map.

Lemma 13.4 Let Γ be any context and A any syntactically injective urtype of L_{∀}. Then any map e : ⟦Γ⟧ → ⟦A⟧ between their interpretations in Q is the interpretation of some urterm Γ ⊢ a : A.

⟦Γ⟧  Γ ≡ [z⃗ : C⃗, 𝔯(z⃗)]
[figure: e; ..............; a]
⟦A⟧  A
[figure: ..............; f; ..............; ⌜f⌝]
[figure: ⟦Γ_{0}⟧; ⟦i_{Γ}⟧; Γ_{0} ≡ [z⃗ : C⃗]; i_{Γ}]

Proof In the category Q, the objects ⟦Γ_{0}⟧ and ⟦A⟧ are injective and ⟦i_{Γ}⟧ : ⟦Γ⟧ ↣ ⟦Γ_{0}⟧ is an M-map, so e lifts to f : ⟦Γ_{0}⟧ → ⟦A⟧. Since this lies in the full subcategory A ⊂ Q, it is the interpretation of the urterm Γ_{0} ⊢ a ≡ ⌜f⌝z⃗ : A, by Corollary 6.9. Hence the given map e is the interpretation of the weakening of a by the predicate 𝔯(z⃗). □

Lemma 13.5 If the urterms Γ ⊢ a, b : A have the same interpretation as maps in Q then Γ ⊢ a = b : A is provable from L_{∀}. Proof The denotations in Q are the composites

[figure: ⟦Γ⟧; ⟦i_{Γ}⟧; ⟦Γ_{0}⟧; ⟦a⟧; ⟦b⟧; ⟦A⟧]

so the following composites are also the same in Q:

[figure: ⟦ϕ : Σ^{A}, Γ⟧; = = = =; Σ^{⟦A⟧} × ⟦Γ⟧; Σ^{⟦A⟧} × ⟦Γ_{0}⟧; id × ⟦a⟧; id × ⟦b⟧; Σ^{⟦A⟧} × ⟦A⟧; ev; Σ.]

Hence by Definition 13.1 the judgement

ϕ : Σ^{A}, Γ ⊢ ϕa = ϕb

is an axiom of the proper language L_{∀}. The Leibnizian equality Γ ⊢ a = b : A follows from this. □

Corollary 13.6 The interpretation

⟦−⟧ : Cn_{L_{∀}}^{∀}( Γ, [x : A] ) ⟶ Q( ⟦Γ⟧, ⟦A⟧ )

is full and faithful for any context Γ and syntactically injective urtype A in L_{∀}. Proof Recall from Definition 12.2 that a typical morphism of Cn_{L_{∀}}^{∀},

a⃗ : [z⃗ : C⃗, 𝔯(z⃗)] ⟶ [x : A],

is an equivalence class of urterms z⃗ : C⃗ ⊢ a : A where a represents the same morphism of Cn_{L_{∀}}^{∀} as b if

z⃗ : C⃗, 𝔯(z⃗) ⊢ a = b.

The result follows using the previous two lemmas. □

Next we extend this result to target contexts whose predicate is a quantified implication:

Lemma 13.7 Any Q-map e : ⟦Γ⟧ → ⟦x⃗ : A⃗, 𝔭(x⃗)⟧, where

𝔭(x⃗) ≡ ∀y⃗:B⃗. 𝔮(y⃗) =▷ α x⃗ y⃗ = β x⃗ y⃗,

is the interpretation of a unique morphism of Cn_{L_{∀}}^{∀}.

E ≡ ⟦x⃗ : A⃗, 𝔭(x⃗)⟧
[figure: e ∈ Q; ⟦i_{E}⟧]
[figure: ⟦Γ⟧; ⟦a⃗⟧; ⟦A⃗⟧]

E × Y
[figure: e × Y]
[figure: ⟦Γ⟧ × Y; ⟦a⃗⟧ × Y; ⟦A⃗⟧ × Y; ⟦α⟧; ⟦β⟧; Σ]

Proof The interpretation E ≡ ⟦x⃗ : A⃗, 𝔭(x⃗)⟧ is defined by a partial product in Q as shown and the map e is the mediator ⟦Γ⟧ → E. By Lemma 13.4, ⟦i_{E}⟧ · e is ⟦a⃗⟧ for some string of urterms Γ ⊢ a⃗ : A⃗. Then, considered as a morphism of Cn_{L_{∀}}^{∀}, this string is unique by Lemma 13.5. The question is therefore whether it satisfies Γ ⊢ 𝔭(a⃗).

Since e : ⟦Γ⟧ → E is given in Q, the composites

[figure: ⟦Γ, y⃗ : B⃗, 𝔮(y⃗)⟧; = = =; ⟦Γ⟧ × Y; ⟦a⃗⟧ × Y; ⟦A⃗⟧ × Y; ⟦α⟧; ⟦β⟧; Σ]

are the same in Q. Therefore, by Definition 13.1, the judgement

Γ, y⃗ : B⃗, 𝔮(y⃗) ⊢ α a⃗ y⃗ = β a⃗ y⃗

is an axiom of the proper language L_{∀} of Q and we deduce Γ ⊢ 𝔭(a⃗) by ∀I. □

Proposition 13.8 The interpretation ⟦−⟧ : Cn_{L_{∀}}^{∀} → Q is full and faithful.

Proof It remains to show that any Q-map e : ⟦Γ⟧ → ⟦x⃗ : A⃗, 𝔭(x⃗)⟧, where 𝔭(x⃗) is a general equideductive predicate, is the interpretation of some urterm Γ ⊢ a : A that satisfies Γ ⊢ 𝔭(a). Proof By Remark 9.6, 𝔭(x⃗) ⊣⊢ 𝔭_{1}(x⃗)&⋯&𝔭_{n}(x⃗), where each 𝔭_{k}(x⃗) is a quantified implication. Let i_{Δ} : [x⃗ : A⃗, 𝔭(x⃗)] ↣ [x⃗ : A⃗], so ⟦i_{Δ}⟧ · e is ⟦a⃗⟧ for some unique morphism Γ → [x⃗ : A⃗]. By the previous lemma, Γ ⊢ 𝔭_{k}(a⃗) for each k. Alternatively, ⟦x⃗ : A⃗, 𝔭(x⃗)⟧ is the pullback of the ⟦x⃗ : A⃗, 𝔭_{k}(x⃗)⟧ rooted at ⟦x⃗ : A⃗⟧. □

Theorem 13.9 Any equideductive category Q with a choice of structure is strongly equivalent to the classifying category for its proper language. Proof For weak equivalence it remains to observe that ⟦−⟧ is essentially surjective (each object of Q is isomorphic to the interpretation of some context in L_{∀}), because this is the well founded version of the requirement that there be enough injectives in an equideductive category. If we strengthen this requirement to make a choice of injectives then this choice provides the object part of the pseudo-inverse functor. □

Theorem 13.10 Let Q be an equideductive category without the requirement of a choice of structure and L_{∀} its proper language as defined above. Then Q is equivalent to Cn_{L_{∀}}^{∀} in the very weak sense that there is a span of functors Cn_{L_{∀}}^{∀} ← P → Q, each of which is full, faithful and essentially surjective. Proof An object of P is a context Γ (object of Cn_{L_{∀}}^{∀}) together with a diagram in Q. That is, an assignment of objects and morphisms of Q that are interpretations of the types and terms in the process of interpreting Γ in Q. For this, Q does not need a global choice of this structure: each finite assignment that has the relevant universal properties provides one of the objects of P. The object parts of the functors Cn_{L_{∀}}^{∀} ← P → Q select the whole context Γ and its interpretation in Q. The morphisms between objects of P must agree with both those in Cn_{L_{∀}}^{∀} and in Q. This is valid by a finite fragment of the proof of Proposition 13.8. □

14 Comprehension types

Whilst injectives considerably simplify foundational constructions, for mathematical applications we would like to be able to use non-injective urtypes and even treat the two-part contexts (urtypes with predicates) as first class objects. In this section we introduce a notation like subset-formation or comprehension in set theory and show how to define morphisms. For simplicity and for the same reasons that underly the adoption of the variable-binding rule (Warning ??), we do not allow dependent types here.

Definition 14.1 Let A be an urtype and 𝔭 a predicate on it. Then the type {x : A | 𝔭(x)}, or {A | 𝔭} for short, is formed by the rule

A type 𝔭 predicate on A

{x : A | 𝔭(x)} type {}F

Terms of this type obey the introduction rule

Γ ⊢ a : A Γ ⊢ 𝔭(a)
Γ ⊢ admit a : {A | 𝔭}

{}I

the elimination rules

x : {A | 𝔭} ⊢ ix : A,  𝔭(ix)  {}E

and the β-rule

x : A, 𝔭(x) ⊢ i(admit x) = x.  {}β

The equality predicate for terms of type {A | 𝔭} is defined in the same way as in Definition 9.13:

a = b : {A | 𝔭} ≡ ∀ϕ:Σ^{A}. ϕ(ia) = ψ(ia).

These new types are interpreted in an equideductive category in the same the same way as are contexts (Definition 11.5). In the topological model they are therefore general sober spaces, whereas the urtypes denote locally compact spaces.

Lemma 14.2 Equality is reflexive, symmetric and transitive. It obeys extensional and η-rules and it is transmitted by the introduction and elimination rules.

Proof The {}E= rule follows from the definition of equality,

a = b : {A | 𝔭} ⊢ ia = ib : A,

as do reflexivity, symmetry and transitivity. The {}I= and η-rules

a = b : A ⊢ admit a = admit b : {A | 𝔭} and a = admit(ix) : {A | 𝔭}

follow from this and the β-rule. The extensionality rule is

ia = ib : A ⊢ a = b : {A | 𝔭}.  □

Definition 14.3 The subtyping notation may be nested. For example,

{x : {α : Σ^{A}, β : Σ^{B} | 𝔭(α, β)}, y : {γ : Σ^{C}, δ : Σ^{D} | 𝔮(γ, δ)} | 𝔯(x, y)}
≡ {α : Σ^{A}, β : Σ^{B}, γ : Σ^{C}, δ : Σ^{D} | 𝔭(α, β) & 𝔮(γ, δ) & 𝔯(⟨α, β⟩, ⟨γ, δ⟩)}.

This is justified by showing that the nested introduction, elimination and equality rules agree with the composite ones.

Proposition 14.4 The range of the quantifier may be a type:

∀y:{B | 𝔭}. 𝔮(y) =▷ 𝔯(x, y) ≡ ∀y:B. 𝔭(y) & 𝔮(y) =▷ 𝔯(x, y).

Indeed, it may be a clearer to think of quantified implication as quantification without implication but over a type. Proof The following judgements are equivalent,

x : A, 𝔰(x), y : {B | 𝔭}, 𝔮(y) ⊢ 𝔯(x, y)
x : A, y : B, 𝔰(x), 𝔭(y), 𝔮(y) ⊢ 𝔯(x, y)
x : A, 𝔰(x)  ⊢ ∀y. 𝔭(y) & 𝔮(y) =▷ 𝔯(x, y),

by Definition 14.1 and Proposition 9.11, so the extended ∀ rules are satisfied. □

Proposition 14.5 ∀y:1. 𝔭(x, y) ⊣⊢ 𝔭(x, ⋆) and ∀yz. 𝔭(x, y, z) ⊣⊢ ∀y. ∀z. 𝔭(x, y, z). Proof The equivalence

x : A, 𝔰(x), y : 1 ⊢ 𝔭(x, y) = x : A, 𝔰(x) ⊢ 𝔭(x, ⋆)

downwards is given by ∀E and upwards by 1-ext (y : 1 ⊢ y = ⋆) and ∀I. The judgements

x : A, 𝔰(x)  ⊢ ∀⟨y, z⟩:Y × Z. 𝔭(x, y, z)
x : A, 𝔰(x), ⟨y, z⟩ : Y × Z ⊢ 𝔭(x, y, z)
x : A, 𝔰(x), y : Y, z : Z  ⊢ 𝔭(x, y, z)
x : A, 𝔰(x), y : Y  ⊢ ∀z:Z. 𝔭(x, y, z)
x : A, 𝔰(x)  ⊢ ∀y:Y . ∀z:Z. 𝔭(x, y, z)

are also equivalent by the previous result and the rules for pairing. □

Now we would like to treat types as objects of a category, for which we need to define the morphisms. However, now that we have dropped the injectivity assumption, we must face up to the difficulty that we mentioned in Remark 12.1.

Lemma 14.6 For any (not necessarily injective) urtype A and predicate 𝔭 on it, the diagram

[figure: [P : Σ^{Σ^{A}}, prime(P) & 𝔭̄(P)]; [P : Σ^{Σ^{A}}, 𝔭̄(P)]; [F : Σ^{4}A, ¯ 𝔭̄(F)].]

is an equaliser in Cn_{L}^{∀}. Also, there is a natural bijection between the terms of these types:

{x : A | 𝔭(x)} ^{η} {P : Σ^{Σ^{A}} | prime(P) & 𝔭̄(P)}.

Proof Lemmas 12.6 and 10.14. □

Proposition 14.7 Types provide the objects of a category C that is strongly equivalent to Cn_{L}^{∀}. In this, a morphism

{x : A | 𝔭(x)} ⟶ {y : B | 𝔮(y)}

is an equivalence class of urterms

x : A ⊢ Qx : Σ^{Σ^{B}} for which x : A, 𝔭(x) ⊢ prime(Qx) & 𝔮̄(Qx),

where Q_{1}x = Q_{2}x if

x : A, 𝔭(x) ⊢ Q_{1}x = Q_{2}x : Σ^{Σ^{B}}.

The identity on {A | 𝔭} has Qx ≡ λϕ. ϕx and the composite of P x with Qy is

x : A ⊢ Rx ≡ λθ. P (λy. Qyθ) : Σ^{Σ^{C}} .

Proof If B is syntactically injective then by Proposition 10.10 there is (unconditionally) an urterm b : B for which Q = λψ. ψb when prime(Q). Hence there is a full and faithful functor Cn_{L}^{∀} → C. Both of these categories have equalisers, whilst by the Lemma both [x : A, 𝔭(x)] ∈ C and [P : Σ^{Σ^{X}} ,¯(P) & prime(P)] ∈ Cn_{L}^{∀} ⊂ C are equalisers of the same pair of maps in C.

The typical morphism of C must be defined like this:

\{x : A | 𝔭(x)\}  \overline{b : B, 𝔮(b)} \{y : B | 𝔮(y)\}

[P : Σ^{Σ^{A}}, 𝔭̄(P) & prime(P)]^{η_{A}‖}  \overline{}[Q : Σ^{Σ^{B}}, 𝔮̄(Q) & prime(Q)]^{η_{B} ‖}

By the equivalence relation on representing urterms of morphisms of Cn_{L}^{∀}, the lower map is represented more simply by its values on x : A, whose characterisation is as given. The identity and composite may be verified by λ-calculations.

Hence they are isomorphic and we have an equivalence of categories. □

Theorem 14.8 The classifying category for equideductive logic is Cn_{L}^{∀}, cf. Theorem 6.5:

(a) Cn_{L}^{∀} is itself an equideductive category;

(b) equideductive logic and the language L are interpreted in C ≃ Cn_{L}^{∀};

(c) any interpretation ⟦−⟧ of the logic and L in an equideductive category Q extends to a functor ⟦−⟧ : Cn_{L}^{∀} → Q that preserves this structure, uniquely up to unique isomorphism; and

(d) any such functor restricts to an interpretation of the logic, uniquely up to unique isomorphism.

□

Remark 14.9 The construction that we used in Lemma 14.6,

T [x : A, 𝔭(x)] ≡ [P : Σ^{Σ^{A}}, 𝔭̄(P)],

is part of an endofunctor, indeed a monad, on Cn_{L}^{∀} that extends Σ^{Σ^{(−)}}. We shall see in [?] that it actually provides the double exponential of X ∈ Q ⊂ S in the enclosing cartesian closed category S. This is another way in which an equideductive category “lies nicely” within its cartesian closed extension. The Lemma showed that any such X ∈ Q ⊂ S is sober with respect to this extended exponential.

References

[CR00] Aurelio Carboni and Giuseppe Rosolini. Locally cartesian closed and exact completions. Journal of Pure and Applied Algebra, 154:103–116, 2000.

[DT87] Roy Dyckhoff and Walter Tholen. Exponentiable maps, partial products and pullback complements. Journal of Pure and Applied Algebra, 49:103–116, 1987.

[Füh99] Carsten Führmann. Direct models of the computational lambda-calculus. In Mathematical Foundations of Programming Semantics 15, number 20 in Electronic Notes in Theoretical Computer Science, 1999.

[Hyl91] J. Martin E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria-Cristina Pedicchio, and Giuseppe Rosolini, editors, Proceedings of the 1990 Como Category Conference, number 1488 in Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Joh82] Peter T. Johnstone. Stone Spaces. Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.

[Kle43] Stephen Kleene. Recursive predicates and quantifiers. Transations of the American Mathematical Society, 53:41–73, 1943. Reprinted in The Undecidable, pages 254–287, edited by Davis, 1965.

[Mac71] Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, Berlin, 1971.

[Nie82] Susan Niefield. Cartesianness: Topological spaces, uniform spaces and affine varieties. Journal of Pure and Applied Algebra, 23:147–167, 1982.

[Pas65] Boris Pasynkov. Partial topological products. Transactions of the Moscow Mathematical Society, 13:153–271, 1965.

[Ros86] Giuseppe Rosolini. Continuity and Effectiveness in Topoi. D. phil. thesis, University of Oxford, 1986.

[Sco72] Dana S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, number 274 in Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, Berlin, 1972.

[Sel01] Peter Selinger. Control categories and duality. Mathematical Structures in Computer Science, 11:207–260, 2001.

[Tay91] Paul Taylor. The fixed point property in synthetic domain theory. In Gilles Kahn, editor, Logic in Computer Science 6, pages 152–160. IEEE, 1991.

[Tay99] Paul Taylor. Practical Foundations of Mathematics. Number 59 in Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999.

[Thi97] Hayo Thielecke. Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh, 1997.

The papers on abstract Stone duality may be obtained from

                                  www.Paul Taylor.EU/ASD

[O] Paul Taylor, Foundations for Computable Topology. in Giovanni Sommaruga (ed.), Foundational Theories of Mathematics, Kluwer 2011.

[A] Paul Taylor, Sober spaces and continuations. Theory and Applications of Categories, 10(12):248–299, 2002.

[B] Paul Taylor, Subspaces in abstract Stone duality. Theory and Applications of Categories, 10(13):300–366, 2002.

[C] Paul Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284–338, 2000.

[E] Paul Taylor, Inside every model of Abstract Stone Duality lies an Arithmetic Universe. Electronic Notes in Theoretical Computer Science 122 (2005) 247-296.

[G] Paul Taylor, Computably based locally compact spaces. Logical Methods in Computer Science, 2 (2006) 1–70.

[I] Andrej Bauer and Paul Taylor, The Dedekind reals in abstract Stone duality. Mathematical Structures in Computer Science, 19 (2009) 757–838.

[J] Paul Taylor, A λ-calculus for real analysis. Journal of Logic and Analysis, 2(5), 1–115 (2010)

[K] Paul Taylor, Interval analysis without intervals. February 2006.

[L] Paul Taylor, Tychonov’s theorem in abstract Stone duality. September 2004.

[N] Paul Taylor, Computability in locally compact spaces. 2010.

[BB] Paul Taylor, An existential quantifier for topology. 2010.

[DD] Paul Taylor, The Phoa principle in equideductive topology. 2010.