Theory and Applications of Categories, Vol. 26, No. 18, 2012, pp. 453–500.

RANGE CATEGORIES II: TOWARDS REGULARITY

J.R.B. COCKETT, XIUZHAN GUO AND PIETER HOFSTRA

Abstract. In this paper, which is the second part of a study of partial map categories with images, we investigate the interaction between images and various other kinds of categorical structure and properties. In particular, we consider images in the context of partial products, meets and discreteness and survey a taxonomy of structures leading towards the partial map categories of regular categories. We also present a term logic for cartesian partial map categories with images and prove a soundness and completeness theorem for this logic. Finally, we exhibit several free constructions relating the different classes of categories under consideration.

1. Introduction

Background and Motivation In part I of this work we introduced the notion of a range category, which is a restriction category (an abstract category of partial maps) in which every morphism f : A → B not only has a domain of definition, embodied by a special idempotent \overline{f} : A → A on A, but also a range f̂: B → B, given by an idempotent on B. For convenience, the axioms for the restriction and for the range are repeated in Table 1.

Range categories were seen to be closely connected with factorization systems, in the following way. Whenever C is a category equipped with a stable system of monics M (meaning that the class M is closed under composition, contains all isomorphisms and is closed under pullback along arbitrary maps), then one may form the partial map category Par(C, M), whose objects are the same as those of C, but whose arrows are isomorphism classes of spans (m, f) where m ∈ M.

\xymatrix{ & A′ \ar[dl]_{m} \ar[dr]^{f} \\ A &  & B}

Composition, as in any span category, is done by pullback. For such a map (m, f) one may form \overline{(m, f)} = (m, m); maps of this form are the restriction idempotents in Par(C, M). As a restriction category, Par(C, M) has the distinguishing feature that all restriction idempotents split. In fact, the basic representational result for restriction categories says that any restriction category fully embeds into one of the form Par(C, M),

Cockett and Hofstra acknowledge support from an NSERC Discovery grant.

Received by the editors 2011-08-31 and, in revised form, 2012-09-05.

Transmitted by Stephen Lack. Published on 2012-09-09.

2010 Mathematics Subject Classification: 18A15, 18A32, 18D20.

Key words and phrases: Categories of partial maps, restriction category, factorization systems.

\begin{matrix}c \\ ◯ \end{matrix} J.R.B. Cockett, Xiuzhan Guo and Pieter Hofstra, 2012. Permission to copy for private use granted.

[R.1] f\overline{f} = f  [RR.1] \overline{f̂} = f̂
[R.2] \overline{g}\overline{f} = \overline{f}\overline{g} dom(f) = dom(g) [RR.2] f̂f = f
[R.3] \overline{g\overline{f}} = \overline{g}\overline{f} dom(f) = dom(g) [RR.3] ˆ \overline{g}f = \overline{g}f̂ codom(f) = dom(g)
[R.4] f\overline{gf} = \overline{g}f cod(f) = dom(g) [RR.4] ĝf̂ = ĝf codom(f) = dom(g)

Table 1: Restriction and Range Axioms

and that any restriction category with split restriction idempotents is precisely of this form. (See [Cockett & Lack 2002] for details.)

We found in part I that when C is a category equipped with an M-stable factorization system (E, M) (meaning: a factorization system in which the M-maps form a stable system of monics, so that the partial map category can be formed, and in which the Emaps are stable under pullback along M-maps) then the associated partial map category Par(C, M) is a range category. Conversely, any range category fully embeds (in a domain and range preserving way) into a category of the form Par(C, M), where M is part of such a factorization system.

The results raise the question of how range categories relate to regular categories. An early reference for regular categories is [Barr et al. 1971] and the important connection to regular logic is described in detail in [Butz 1998]. Regular categories may be described as finitely complete categories with a stable proper factorization system in which the Mmaps are precisely the monics (this forces it to be the regular epic/monic factorization). Kelly noted in [Kelly 1991] that the requirement that the M-maps be all the monics can almost be dropped. Indeed, for a finitely complete category with a stable proper factorization there is an associated bicategory of relations; the category of maps of the latter is then a regular category (which has the same category of relations) and is in fact the regular reflection of the original category.

There are, in fact, many categories which possess a stable proper factorization which is different from the regular epic-monic factorization. For example, in the category of topological spaces every map can be factored as an epic followed by a regular monic (even though this category is not regular). It is worth noting that the regular reflection has a rather dramatic effect in this case: it turns all bijective maps into isomorphisms, and hence makes every function continuous.

Significantly the theory of range categories – more precisely the theory of discrete range restriction categories – aligns itself to categories with a stable proper factorization system rather than to regular categories. Thus, the constructions we shall provide may be seen, from a more traditional perspective, as free constructions of categories with stable proper factorizations. It is notable that these categories have an elegant term logic which we also exhibit below.

The present paper, due to the above observations, may thus be seen as working the territory between discrete range categories and those arising as partial map categories of

[figure: Restriction Categories; Meets; Products; Ranges; Discreteness; Cartesian Ranges; Ranges + [RR.5]; Disc. Range Categories; Regularity]

Figure 1: Between restriction and regularity

regular categories. Among other things, this involves identifying various related classes of categories, and exploring the interaction between ranges and other types of structure, most notably partial products and meets. In Figure 1 we have indicated the various classes of categories we shall be concerned with, starting with ordinary restriction categories and ending with regular restriction categories. We shall prove that for most of the forgetful functors between these classes of categories, a left adjoint can be constructed, so that all of the relevant structure leading up to the partial map analogue of regular categories can be freely added. (The dotted lines indicate forgetful functors for which we do not exhibit an adjoint.) Since the regular completion of a category with finite limits has been studied in detail by various authors, we will also provide a comparison between that construction and our construction of the free regular restriction category on a discrete one.

Our next concern is to work out the standard representation for each of these classes of categories in terms of categories equipped with systems of monics. Thus, it is useful to have a dictionary between concepts on the abstract level of restriction categories and the concrete level of categories with systems of monics. In Figure 2 the entries of this dictionary relating to regularity are summarized. (The meaning of some of the concepts involved will become clear as the paper develops.)

Finally, we develop a term logic which is sound and complete for discrete cartesian range categories. It should perhaps be mentioned that one of the original motivations behind this work was to obtain such a logic, with the particular aim of facilitating reasoning

Restriction Category  Category C with system M of monics
Finite (restriction) products  Finite products in C
Discrete object A  Diagonal map Δ_{A} is in M
(Binary) Meets  C has equalizers and all regular monics are in M
Finite products + meets  C has finite limits and all reg. monics are in M

(equivalently: Discreteness)

Ranges  M-stable factorization system (E, M)
Ranges + [RR.5]  M-stable fact. system with E-maps epi
Cartesian + ranges (incl. BCC)  C finite products, E-maps closed under products
Discreteness + ranges  C lex, stable fact. syst. with reg. monics in M
Disc. + ranges + all monics are partial isos C is regular

Figure 2: Correspondence between structure on C and on Par(C, M)

in partial map categories of computable functions. Indeed, while the axioms for range categories are equational and concise, the term logic provides a much more intuitive way to establish results about such categories. As an added bonus, it also helps us construct various free categories.

Contributions The main contributions of the paper may be summarized as follows:

1. A useful new type of limit in the context of restriction categories is introduced, which we call a latent limit.

2. We introduce restriction categories with meets and show how these can be freely added.

3. The interaction between ranges and finite limits is analysed, and we present a free construction which adds ranges to a discrete restriction category.

4. We introduce term logics for various classes of restriction categories and prove a completeness theorem for these logics.

Outline Section 2 begins with a brief recapitulation of the theory of limits in the restriction context. After that, the new concept of latent limit is introduced; in particular, we consider latent pullbacks and establish a few elementary but useful facts which will be employed later in the paper. We then consider equality in restriction categories as well as the related notion of meets. The section concludes with the free construction of the meet completion of a restriction category.

In Section 3 we begin the analysis of the interaction between ranges and other structure by considering categories with ranges and products. The Beck-Chevalley Condition is introduced, and we relate cartesian range categories to stable factorization systems. After that, ranges are studied in discrete cartesian restriction categories, and we prove the main representational result stating that every discrete range category embeds into a partial map category of a finite limit category with a stable proper factorization system. We then investigate the difference between such categories and the partial map categories of regular categories, and show that the gap can be bridged using a categories of fractions construction. The section concludes by reconsidering the range completion of a restriction category (as presented in Part I of this paper) in the context of finite limits. It is shown that the construction can be adapted to provide a free discrete range category on a discrete cartesian restriction category, and that this construction is related to, but different from, the usual regular completion of a finite limit category.

In the last Section 4, we explore term logics for several of the classes of categories considered, namely cartesian restriction categories, discrete cartesian restriction categories and discrete cartesian range categories. For each we shall prove soundness and completeness.

2. Finite Limits

In this section we investigate finitely complete restriction categories. A general study of limits in restriction categories was conducted in [Cockett & Lack 2007], and we will briefly review the main ideas. We will have the need for a slight refinement of restriction limits, which we call latent limits; these will be introduced as well. Meets are a type of limit which have not received detailed attention so far, and thus we develop some of the basic theory, including the construction of the free category with meets. We also investigate discreteness, which formalizes the idea of a semi-decidable equality relation on objects in a category.

2.1. Background and Terminology We briefly review some material, notation and terminology concerning partial monics, partial isomorphisms and partial products in restriction categories. More details can be found in [Cockett & Lack 2002].

Notation We follow the notation of part I. The partial order on hom-sets in a restriction category will be denoted ≤. For an object A we write O(A) = \{e : A → A|e = \overline{e}\} for the meet-semilattice of restriction idempotents; the meet operation (which is given by composition) is denoted e ∧ e′. For a map f : A → B, we write f^{∗} : O(B) → O(A) for the meet-preserving mapping e ↦ \overline{ef}. When f is an open map (see part I), then the direct image mapping will be denoted by ∃_{f} : O(A) → O(B).

Given a restriction category C, we write Tot(C) for the subcategory of C total maps, i.e. those f with \overline{f} = 1. By Split(C), we denote the result of splitting all restriction idempotents in C.

Partial Monics In a restriction category C, a morphism m : A → B is called a partial monic when mf = mg implies \overline{m}f = \overline{m}g for all f, g : B → C. Notice that when m is total (i.e. \overline{m} = 1) then this simply says that m is monic. A partial inverse for m is a map n : B → A such that nm = \overline{m} and mn = \overline{n}. In this case we also write n = m^{−1}, and say that m (and hence also m^{−1}) is a partial isomorphism. It is easily seen that partial isomorphisms compose, and that all restriction idempotents \overline{e} = e are partial isomorphisms. Hence the partial isomorphisms in C form a subcategory; a category in which all morphisms are partial isomorphisms is called an inverse category.

A useful fact about partial isomorphisms is that they are open maps (see part I); concretely, for a partial isomorphism m : A → B the mapping ∃_{m} : O(A) → O(B) may be taken to be (m^{−1})^{∗}.

When a (total) monic m : A → B has a partial inverse, then A (together with m and its partial inverse) constitutes a splitting of the restriction idempotent mm^{−1} on B. In this case, m is called a restriction monic. In a restriction category of the form Par(C, M), the monics are of the form (1, m), where m is monic in C. Thus a monic (1, m) is a restriction monic precisely when m ∈ M.

Lax natural transformations We will have occasion to consider various types of functors between restriction categories, as well as various types of natural transformation between functors. We briefly introduce the relevant definitions and terminology.

Given two restriction categories C, D, we of course have the notion of a restriction functor, which is simply a functor preserving the restriction in the sense that F \overline{f} = \overline{F f}. A weaker concept is that of a restriction semifunctor (as introduced in [Cockett & Lack 2002]); this is a mapping F : Ob(C) → Ob(D) together with functors C(A, B) → D(F A, F B) satisfying F \overline{f} = \overline{F f} and F (gf) = F gF f (but not necessarily F 1 = 1). A lax natural transformation between two semifunctors F, G : C → D consists of a family α_{A} : F A → GA for which \overline{α_{A}} = F 1_{A}, such that for each f : A → B we have α_{B} ∘ F f = Gf ∘ α_{A} ∘ \overline{F f}. Since a restriction functor is in particular a semifunctor we may employ the same notion of lax natural transformation between restriction functors (in which case the component maps α_{A} are automatically total).

Restriction Limits We recall that limits in a restriction category are not ordinary limits in the underlying category, but are instead characterized by a 2-categorical universal property.

More precisely, a restriction category C has restriction limits of type D (where D is an ordinary small category) when the diagonal functor C → C^{D} has a right adjoint in the 2-category ℜ𝔠𝔞𝔱 of restriction categories, restriction functors and lax natural transformations. Here, C^{D} is the ordinary functor category. When a diagram in C of type D factors through the subcategory of total maps Tot(C) → C, then taking the restriction limit in C will actually give a genuine limit in Tot(C).

In [Cockett & Lack 2007] a more concrete description of restriction limits over finite diagrams was obtained: a restriction limit of S : D → C consists of an object L, equipped with a cone over p : ΔL ⇒ S with vertex L whose components are total; this cone is universal in the sense that for any lax cone q : ΔK ⇒ S with vertex K there is a unique r : K → L such that \overline{r} is the intersection of the domains of the components q_{C} of q, and such that p_{C}r ≤ q_{C} for all objects C of D.

In the case of the empty diagram, this gives the notion of a restriction terminal object (also called a partial terminal object): this is an object denoted 1, such that for each object A there is a unique total map !_{A} : A → 1 with the property that any map f : A → 1 factors as f =!_{A}\overline{f}. Hence a restriction terminal object classifies restriction idempotents on A.

In case of a product diagram, we arrive at the notion of a restriction product (or partial product): this is an object A × B equipped with total projection maps π_{A} : A × B → A, π_{B} : A × B → B such that for any pair f : X → A, g : X → B there is a unique map ⟨f, g⟩ : X → A × B for which π_{A}⟨f, g⟩ ≤ f, π_{B}⟨f, g⟩ ≤ g and \overline{⟨f, g⟩} = \overline{f}\overline{g}.

A restriction category with binary restriction products and a restriction terminal object will be called cartesian.

We shall also encounter restriction pullbacks: these are commutative squares

[figure: X; w; ≤; v; ≥; ⟨v,w⟩; P; q; p; B; g; A; f; C]

in which p and q are total, with the universal property that for any v : X → A, w : X → B with fv = gw there is a unique ⟨v, w⟩ : X → P with p⟨v, w⟩ ≤ v, q⟨v, w⟩ ≤ w and \overline{⟨v, w⟩} = \overline{fv} = \overline{gw}. The fact that the last condition regarding the domain of the mediating morphism ⟨v, w⟩ is not equal to \overline{v} \overline{w} stems from the fact we work with lax cones: secretly, there is a component q_{C} : X → C with fv ≤ q_{C}, gw ≤ q_{C}, whose domain cannot be forgotten.

Finally, a restriction equalizer of two maps f, g : A → B is a total map m : E → A such that fm = gm with the universal property that for any h : C → A with fh = gh there is a unique k : C → E with \overline{k} = \overline{h} and mk ≤ h.

2.2. Latent Limits There is a slightly weaker notion of limit which will also be used in this paper: this we call a latent limit. To motivate this, we first recall from [Cockett & Lack 2007] that there is a close connection between restriction limits and splitting of idempotents: indeed, a restriction limit of a diagram f : A → B is precisely a splitting of the domain of f. More generally, the existence of restriction limits of certain diagrams often force the splitting of certain idempotents. In non-split restriction categories therefore such limits are generally unlikely to exist. However, it may still be the case that the splitting of certain idempotents is the only obstruction. This is what latent limits are about.

2.3. Definition. A restriction category C has latent limits of type D when the diagonal functor C → C^{D} has a right adjoint in the 2-category of restriction categories, semifunctors and lax natural transformations.

A more concrete description for finite D is as follows: a latent limit of a diagram S : D → C consists of a cone p : ΔL ⇒ S over S (where now the components need not be total) satisfying \overline{p_{C}} = \overline{p_{D}} for all objects C, D of D. This cone is universal in the sense that for any lax cone q : K ⇒ S over S, there is a unique r : K → L such that

(i) p_{C}r ≤ q_{C} for all objects C of D

(ii) \overline{r} = ⋂_{C∈Ob(D)} \overline{q_{C}}

(iii) er = r, where e = ⋂_{C∈Ob(D)} \overline{p_{C}}

The relation between latent limits and restriction limits can then be stated as follows:

2.4. Proposition. A restriction category C has latent limits of type D if and only if its its idempotent splitting Split(C) has restriction limits of type D.

Proof. This is an immediate consequence of the fact that the 2-functor Split(−) is an equivalence of 2-categories (see [Cockett & Lack 2002]), so that adjunctions in the 2category of restriction categories, semifunctors and lax transformations correspond to adjunctions in the 2-category of split restriction categories, strict functors and lax transformations.

More concretely, given a latent limit (L, p) of S, a restriction limit is obtained simply by applying the universal property of (L, p) to itself, giving a map L → L. This is in fact a restriction idempotent, whose splitting gives the desired restriction limit. In case D is finite, we may instead use the idempotent e = ⋂_{C∈Ob(D)} \overline{p_{C}}.

We point out that while restriction limits are unique up to unique isomorphism, latent limits are only unique up to unique partial isomorphism.

Two special cases which will be relevant for the rest of this paper are latent pullbacks and latent equalizers. Explicitly, a commutative square with \overline{p} = \overline{fp} = \overline{gq} = \overline{q}

[figure: X; w; ≤; v; ≥; α; P; q; p; B; g; A; f; C]

is a latent pullback when it has the universal property that for each v : X → A, w : X → B with fv = gw there is a unique mediating map α : X → P with the following properties:

(i) pα ≤ v, qα ≤ w

(ii) \overline{α} = \overline{fv} = \overline{gw}

(iii) α = \overline{p}α

Latent pullbacks of partial isomorphisms always exist:

2.5. Lemma. Given a partial isomorphism h : C → D and an arbitrary map k : B → D. Then the latent pullback of h along k exists, and is again a partial isomorphism.

Proof. Form the diagram

\xymatrix{B \ar[r]^{\overline{h^{−1}k}} \ar[d]_{h^{−1}k} & B \ar[d]^{k} \\ C \ar[r]_{h} & D.}

The diagram commutes: we have

hh^{−1}k = \overline{h^{−1}}k = k\overline{h^{−}1}k.

Given v : X → C, w : X → B with hv = kw, we have

\overline{h^{−1}k}w = w\overline{h^{−1}kw} = w\overline{h^{−1}hv} = w\overline{hv}

and

h^{−1}kw = h^{−1}hv = \overline{h}v.

Thus we set α : X → B to be α = w\overline{hv}, and we have that h^{−1}kα ≤ v, \overline{h^{−1}k}α ≤ w, and finally \overline{α} = \overline{w\overline{hv}} = \overline{w\overline{kw}} = \overline{kw} = \overline{hv}.

In particular, we see that the operation k^{∗} : O(D) → O(B) is an instance of latent pullback.

The following result will be used later.

2.6. Lemma. In a cartesian restriction category, for any object B the functor − × B preserves all latent pullback squares which exist.

Proof. Straightforward.

A latent equalizer of f, g is a map m : E → A (not necessarily total) such that fm = gm, \overline{m} = \overline{fm} and with the universal property that for any h : C → A with fh = gh there is a unique k : C → E such that

(i) mk ≤ h

(ii) \overline{k} = \overline{fh} = \overline{gh}

(iii) \overline{m}h = h

A slightly different perspective on latent equalizers is presented in the next section.

2.7. Meets In the category Par of sets and partial functions we may, for each pair of parallel arrows f, g : X → Y, define a new map

f ∧ g : X → Y; x ↦ \{ \begin{matrix}f(x) & if f(x)↓, g(x)↓, f(x) = g(x) \\ ↑ & otherwise \end{matrix}

which is a restriction of both f and g, and which is defined precisely on those x ∈ X for which f(x) = g(x). This makes f ∧ g the meet of f and g in the ordering on maps X → Y. In this section we shall axiomatize and investigate meets.

2.8. Definition. A restriction category C is said to have meets when each homset of C has binary meets w.r.t. the restriction ordering, and when these meets are preserved by precomposition.

Note that we do not require homsets to have unit element for the meet operation. We also do not impose the condition that meets be preserved by postcomposition, i.e., that h(f ∧ g) = hf ∧ hg. An example of the failure of this equality can already be observed in sets and partial functions: let h : B → 1 be the unique total function and let f, g : A → B be distinct total functions. Then hf ∧ hg =!_{A}, but f ∧ g will not be total, since f and g do not agree on all of their arguments.

We may slightly reorganize the above definition:

2.9. Definition. A meet combinator on a restriction category C is an operation of type

[figure: A; f; B; A; g; B; A; f∧g; B]

satisfying the following three axioms:

[Meet. 1] f ∧ f = f

[Meet. 2] f ∧ g ≤ f and f ∧ g ≤ g

[Meet. 3] (f ∧ g)h = fh ∧ gh

The following lemma is then obvious:

2.10. Lemma. A restriction category has meets if and only if it has a meet combinator.

The following lemma captures some elementary facts about meets which will be used in various places in the paper.

2.11. Lemma. In a category with meets:

(i) (f ∧ g)\overline{h} = f\overline{h} ∧ g = f ∧ g\overline{h}

(ii) \overline{h}(f ∧ g) = \overline{h}f ∧ \overline{h}g

(iii) f\overline{f ∧ g} = g\overline{f ∧ g}

(iv) h is a partial monic if and only if h(f ∧ g) = hf ∧ hg for all f, g.

(v) gf = hf when \overline{g ∧ h}f = f.

Proof.

(i) If k ≤ f\overline{h} and k ≤ g then \overline{k} ≤ \overline{h}, and hence k ≤ g\overline{h} as well. Thus f\overline{h} ∧ k is the infimum of f\overline{h} and g\overline{h}.

(ii) First note that \overline{h}(\overline{h}f ∧ \overline{h}g) = \overline{h}f ∧ \overline{h}g, because for any k with k ≤ \overline{h}f and k ≤ \overline{h}g, we have \overline{h}k = k, so that k = \overline{h}k ≤ \overline{h}(\overline{h}f ∧ \overline{h}g). Then calculate

\overline{h}(f ∧ g)\overline{\overline{h}f ∧ \overline{h}g} = \overline{h}(f\overline{\overline{h}f ∧ \overline{h}g} ∧ g\overline{\overline{h}f ∧ \overline{h}g}) = \overline{h}(\overline{h}f ∧ \overline{h}g).

(iii) f\overline{f ∧ g} = f ∧ g = g ∧ f = g\overline{g ∧ f} = g\overline{f ∧ g}

(iv) Suppose first that h is a partial monic. Then for any k with k ≤ hf and k ≤ hg we have hf\overline{k} = k = hg\overline{k}, so \overline{h}f\overline{k} = \overline{h}g\overline{k} because h is partial monic. Then

h(f ∧ g)\overline{k} = h(f\overline{k} ∧ g\overline{k}) = h(\overline{h}f\overline{k} ∧ \overline{h}g\overline{k}) = h\overline{h}f\overline{k} = hf\overline{k} = k,

whence k ≤ h(f ∧ g), making h(f ∩ g) the infimum of hf and hg.

For the converse, consider hf = hg. Then

\overline{hf} = \overline{hf ∧ hg} = \overline{h(f ∧ g)} = \overline{\overline{h}(f ∧ g)} = \overline{\overline{h}f ∧ \overline{h}g}.

Thus \overline{h}f = \overline{h}f ∧ \overline{h}g, and similarly we get \overline{h}g = \overline{h}f ∧ \overline{h}g.

(v) If \overline{g ∧ h}f = f, then gf = g\overline{g ∧ h}f = h\overline{g ∧ h}f = hf.

The following is now straightforward:

2.12. Proposition. If C has meets, then so does Split(C), and the embedding C ↪ Split(C) preserves them.

Proof. Consider two parallel maps f, g : (X, e) → (Y, e′) in Split(C) (i.e., e, e′ are restriction idempotents and we have e′fe = f, e′ge = g). Form the meet f ∧ g in C; then (f ∧ g)e = fe ∧ ge = f ∧ g, and also e′(f ∧ g) = e′f ∧ e′g by Lemma 2.11, part (ii), whence also e′(f ∧ g) = f ∧ g. This proves that f ∧ g : (X, e) → (Y, e′) is a well-defined morphism in Split(C). Finally, it is straightforward to show that it is indeed the meet of f and g.

There is another possible axiomatization of this structure, which is based on the idea of an agreement operator, due to Jackson and Stokes in the context of semigroup theory [Jackson & Stokes 2003]. Such an operator has typing

\begin{matrix}f : A → B & g : A → B \\ f||g : A → A \end{matrix}

and should satisfy the axioms

(i) f(f||f) = f

(ii) (f||g) = (g||f)

(iii) f(f||g) = g(f||g)

(iv) (f||g)||(h||k) = (f||g)(h||k)

(v) (f||g)||(h||k) = (h(f||g))||k

(vi) (f||g)h = h(hf||hg)

The following is then a straightforward extension of the corresponding result in Jackson and Stokes:

2.13. Lemma. A restriction category has meets if and only if it has an agreement operator.

Proof. Given a meet operator, set f||g to be \overline{f ∧ g}. Conversely, given an agreement operator, set f ∧ g to be f(f||g).

Our goal is now characterize the partial map categories which have meets, giving in particular a representation theorem for categories with meets.

We fix a split restriction category C with meets, and consider the category Tot(C) of total maps. We shall first show that Tot(C) has equalizers.

2.14. Lemma. When C is a split restriction category with meets, Tot(C) has equalizers.

Proof. Given parallel maps f, g : A → B in Tot(C), consider first f ∧g in C. The domain of this map is an idempotent, which we may split. This gives us a monic i : Eq(f, g) → A. We claim that this is the equalizer of f and g in Tot(C). To see this, consider a total map k : C → A with fk = gk. To show that k factors through i, it suffices to show that k^{∗}(Eq(f, g)) = 1. But kf = kg implies that Eq(f, g)k = k, and the result follows.

Now C is equivalent to Par(Tot(C), M), where the special monics M in Tot(C) correspond to restriction idempotent inclusions in C (these are also called restriction monics, and may also be characterized intrinsically by the fact that these are partial isomorphisms). It can be seen from the above proof that the regular monics in Tot(C) come from restriction idempotent inclusions, and are hence in the class of special monics M. This is sufficient to characterize meets in C:

2.15. Theorem. A restriction category C has meets if and only if it is a full subcategory of a partial map category Par(D, M) where D has equalizers and where M contains all regular monics.

Proof. It remains to be shown that the conditions are sufficient for C to have meets. Of course, it suffices to show that Par(D, M) has meets, as C is a full subcategory and

as such inherits meets. So consider f, g : A → B, and factor these as \xymatrix{A \ar[r]^{i} & A′ \ar[r]^{f′} & B}

and \xymatrix{A \ar[r]^{j} & A′ \ar[r]^{g′} & B} where the first component is a restriction monic and the second is total. By restricting to the common domain of f and g we may assume that A′ = A′′. Then form the equalizer m : E → A′ in D. Since m ∈ M, we may now set f ∧ g to be the partial map (im, fi). It is readily verified that this has the correct properties.

2.16. Corollary. A restriction category C is a full subcategory of a partial map category Par(D, M) where D has finite limits and where M contains all regular monics if and only if C is cartesian and has meets.

We remark that it follows from the above that a category with restriction equalizers does not necessarily have meets: what is needed in addition is the fact that the regular monics (i.e., those which are equalizers in the total map category) are restriction monics.

2.17. Equality Our next goal is to bridge the gap between cartesian restriction categories and restriction categories with arbitrary finite restriction limits. The notion of equality will be the main focus in doing so.

Suppose that C is a cartesian restriction category. Every object comes equipped with a diagonal map Δ_{X} : X → X × X. This map is monic, but generally not a restriction monic (i.e., it need not be the splitting of a restriction idempotent). This leads to the following definition:

2.18. Definition. An object X in a cartesian restriction category is called discrete when the diagonal Δ_{X} has a partial inverse (thus making it a restriction monic).

This terminology stresses the topological intuition: restriction monics are open maps, and a topological space whose diagonal is open is precisely a discrete one. However, it would not be sufficient in general to define discrete objects to be those with open diagonal, because ranges, and hence also openness, may be trivial.

When X is discrete, we may consider the restriction idempotent Δ̂_{X} on X × X, and shall generally denote it by Eq_{X}. This idempotent is then thought of as an equality predicate on X. (This aspect will become central when we consider the term logic in Section 4.) It is common practice to call an object whose diagonal is a complemented subobject decidable (see e.g. [Johnstone 2002]); this means that we may also think of discrete objects as semi-decidable objects.

When every object of C is discrete, we call C discrete as well. In order to avoid confusion between this notion (which only applies to cartesian restriction categories) and that of a category whose arrows are all identities, we shall usually use the slightly heavy term “discrete cartesian restriction category”.

An easy but important consequence of this notion of discreteness is that it implies the presence of meets:

2.19. Lemma. Every discrete cartesian restriction category has meets.

Proof. Define, for f, g : A → B,

f ∧ g = πEq_{B}⟨f, g⟩

Since π_{1}Eq = π_{2}Eq it doesn’t matter which projection we use. The axioms for a meet combinator are easily verified:

[Meet.1] f ∧ f = π_{1}Eq⟨f, f⟩ = π_{1}⟨f, f⟩ = f since ⟨f, f⟩ factors through the diagonal.

[Meet.2] f\overline{f ∧ g} = f\overline{π_{1}Eq⟨f, g⟩} = f\overline{Eq⟨f, g⟩} = π_{1}⟨f, g⟩\overline{Eq⟨f, g⟩} = π_{1}Eq⟨f, g⟩. The inequality f ∧ g ≤ g is analogous.

[Meet.3] (f ∧ g)h = π_{1}Eq⟨f, g⟩h = π_{1}Eq⟨fh, gh⟩ = fh ∧ gh.

There is a converse to Lemma 2.19: whenever a cartesian category has meets it automatically has equality via

Eq_{X} = \overline{π_{1} ∧ π_{2}}.

Then π_{1}Eq_{X} = π_{1} ∧ π_{2} is a partial inverse to Δ_{X}, since

(π_{1} ∧ π_{2})Δ_{X} = π_{1}Δ_{X} ∧ π_{2}Δ_{X} = 1 ∧ 1 = 1

and on the other hand

\overline{Δ_{X}(π_{1} ∧ π_{2})} = \overline{π_{1} ∧ π_{2}} = Eq_{X}.

Thus we have:

2.20. Proposition. A cartesian restriction category has meets if and only if it is a discrete cartesian restriction category.

In such a category the diagonal maps are by definition restriction monics. Hence, categories of the form Par(C, M) are discrete if and only if C has finite products and all diagonal maps are in M. Thus we have the following representational result for discrete cartesian restriction categories:

2.21. Theorem. A cartesian restriction category is discrete if and only if it can be faithfully embedded into a category of the form Par(C, M), where C has finite limits and M contains all diagonal maps (or equivalently, contains all regular monics).

Note that in the presence of finite limits having all diagonals in M forces all regular monics to be in M, since each regular monic is a pullback of a diagonal map.

One of the consequences of the above is of course that a discrete cartesian restriction category has latent pullbacks. For future reference, we give an explicit description.

2.22. Lemma. In a discrete cartesian restriction category, the latent pullback of f along g may be constructed as follows:

\xymatrix{A × B \ar[r]^{π_{1}\overline{fπ_{0}∧gπ_{1}}} \ar[d]_{π_{0}\overline{fπ_{0}∧gπ_{1}}} & B \ar[d]^{g} \\ A \ar[r]_{f} & C}  (1)

Proof. Clearly the square commutes, and the two projections have the same domain. Given p : X → A, q : X → B with fp = gq, the map e⟨p, q⟩ : X → A × B, where e = \overline{fπ_{0} ∧ gπ_{1}} is the required mediating map.

2.23. Adding Meets We now show how meets can be freely added to a restriction category. This is done by formally adding new restriction idempotents, which act as the agreement domains. We point out that the corresponding problem for semigroups was treated in [Jackson & Stokes 2003], and that a version for inverse semigroups can be found in [Lawson 1998].

Formally, we construct from a restriction category C a new category Eq(C). In order to define the morphisms in this category, we first introduce the notion of a pair ideal; this is a collection I of pairs of parallel maps, each having the same domain, subject to the following closure conditions:

M.1 I, considered as a binary relation on morphisms, is transitive and symmetric

M.2 (g, h) ∈ I implies (\overline{g}, \overline{h}) ∈ I

M.3 (g, h) ∈ I, (f, k) ∈ I implies (g\overline{f}, h\overline{k}) ∈ I

M.4 (\overline{k}g, h) ∈ I implies (g, \overline{k}h) ∈ I.

M.5 I is upward closed: if (g, h) ∈ I, g′ ≥ g and h′ ≥ h then (g′, h′) ∈ I

M.6 I is a restricted left ideal: if (\overline{k}g, \overline{k}h) ∈ I then (kg, kh) ∈ I.

It should be stressed that we do not insist on reflexivity, so that a pair ideal is not an equivalence relation. Informally, we think of a pair ideal I as the domain arising by taking the intersection of all domains \overline{f ∧ g}, for (f, g) ∈ I. Note that we can derive, for example, that (f, g) ∈ I implies (f\overline{g}, g) ∈ I: first use symmetry to obtain (g, f) ∈ I; then use [M.3] to get (f\overline{g}, g\overline{f}) ∈ I, and then by [M.5] it follows that (f\overline{g}, g) ∈ I.

Clearly, given any collection U of pairs (g, h) of parallel maps, we may close under the clauses [M.1]–[M.6]; this closure will be denoted ⟨U⟩. Thus a pair ideal I is called finitely generated if it arises as the closure of a finite collection of parallel arrows. We shall also write f ∈ I to mean (f, f) ∈ I.

Next, consider a pair ideal I on A (in the sense that all pairs of maps in I both have domain A), and let f, f′ : A → B be two maps. We define

f ∼_{I} f′ ⇔ (f, f′) ∈ I

and say that f and f′ are I-equivalent if this condition holds.

Moreover, given an arrow f : A → B and a collection V of parallel maps with domain B, we set

f^{∗}(V) = ⟨(gf, hf)|(g, h) ∈ V ⟩.

2.24. Construction. The category Eq(C) has

Objects: those of C

Arrows: a morphism A → B is an equivalence class of pairs (I, f), where I is a finitely generated pair ideal and (\overline{f}, \overline{f}) ∈ I. Two such (I, f) and (I′, f′) are equivalent when I = I′, f ∼_{I} f′. We write [I, f] for the equivalence class of (I, f).

Identities: the identity morphism on A is [I_{A}, 1_{A}], where I_{A} is the pair ideal ⟨1_{A}, 1_{A}⟩.

Composition: the composite [J, g][I, f] is defined to be [⟨I ∪ f^{∗}(J)⟩, gf].

Restriction: define the restriction of [I, f] to be [I, \overline{f}].

Meets: the meet of [I, f] and [I′, f′] is defined to be [⟨I ∪ I′ ∪ {(f, f′)}⟩, f].

Given this definition of Eq(C):

2.25. Proposition. Eq(C) is the free restriction category with meets on C.

We split the proof into a series of lemmas:

2.26. Lemma. If (f, f′) ∈ I and (g, h) ∈ J then (gf, hf′) ∈ ⟨f^{∗}(J) ∪ I⟩.

Proof. First, using symmetry and transitivity we find that (h, h) ∈ J, hence by [M.2] also (\overline{h}, \overline{h}) ∈ J. Thus (\overline{h}f, \overline{h}f) ∈ f^{∗}(J), and therefore also (\overline{h}f, f) ∈ f^{∗}(J) by [M.4]. Since (f, f′) ∈ I, transitivity gives (\overline{h}f, f′) ∈ ⟨f^{∗}(J) ∪ I⟩. Using [M.4] again, we also get (\overline{h}f, \overline{h}f′) ∈ ⟨f^{∗}(J) ∪ I⟩, and applying [M.6] gives (hf, hf′) ∈ ⟨f^{∗}(J) ∪ I⟩. On the other hand, the assumption (g, h) ∈ J gives (gf, hf) ∈ f^{∗}(J), and now the result follows by transitivity.

2.27. Lemma. Composition, restriction and meet are well-defined on equivalence classes.

Proof. For restriction, we observe that if f ∼_{I} f′, we have \overline{f} ∼_{I} \overline{f′} by [M.2], so that [I, f] = [I, f′] ⇒ [I, \overline{f}] = [I, \overline{f′}].

For composition, suppose we have f ∼_{I} f′ and g ∼_{J} g′. We need to verify that gf ∼_{f^{∗}(J)} g′f′, i.e. that the pair (gf, g′f′) is in the pair ideal f^{∗}(J). But this follows right away from the above lemma. We omit the verification that composition is unital and associative.

To see that the meet operation is well-defined, consider [I, f] with f ∼_{I} f′ and [J, g] with g ∼_{J} g′. Then we need [⟨I ∪ J ∪ {(f, g)}⟩, f] = [⟨I ∪ J ∪ {(f′, g′)}⟩, f′]. Now since (f, f′) ∈ I and (g, g′) ∈ J, the ideal generated by I, J and (f, g) contains (f′, g′) by transitivity. Thus the two ideals are the same, and since (f, f′) is in the ideal, the two expressions represent the same map.

2.28. Lemma. Eq(C) is a restriction category.

Proof. [R.1] We need [I, f][I, \overline{f}] = [I ∪ \overline{f}^{∗}(I), f\overline{f}] = [I, f]. But \overline{f}^{∗}(I) = ⟨(g\overline{f}, h\overline{f})|(g, h) ∈ I⟩ = I since (g, h) ∈ I, (\overline{f}, \overline{f}) ∈ I implies (g\overline{f}, h\overline{f}) ∈ I.

[R.2] To see [I, \overline{f}][J, \overline{g}] = [J, \overline{g}][I, \overline{f}], it suffices to verify that I ∪ \overline{f}^{∗}(J) is contained in the ideal generated by J ∪ \overline{g}^{∗}(I). (The result then follows by symmetry.) First (m, n) ∈ I implies (m\overline{g}, n\overline{g}) ∈ \overline{g}^{∗}(I), and hence (m, n) ∈ \overline{g}^{∗}(I) by upclosure. Second, suppose that (m\overline{f}, n\overline{f}) ∈ \overline{f}^{∗}(J) with (m, n) ∈ J. Since \overline{f} ∈ I, we also have \overline{f} ∈ \overline{g}^{∗}I ⊆ J ∪ \overline{g}^{∗}(I). This gives (m\overline{f}, n\overline{f}) ∈ J ∪ \overline{g}^{∗}(I) as well.

[R.3] We have \overline{[I, f]\overline{[J, g]}} = \overline{[I, f][J, \overline{g}]} = [⟨J ∪ \overline{g}^{∗}(I)⟩, \overline{f\overline{g}}] = [⟨J ∪ \overline{g}^{∗}(I)⟩, \overline{f}\overline{g}] = \overline{[I, f]} \overline{[J, g]}.

[R.4] On the one hand we have

[I, f]\overline{[J, g][I, f]} = [I, f][⟨I ∪ f^{∗}(J)⟩, \overline{gf}] = [⟨I ∪ f^{∗}J ∪ (\overline{gf})^{∗}(I)⟩, f\overline{gf}].

On the other hand we have

[J, \overline{g}][I, f] = [⟨I ∪ f^{∗}(J)⟩, \overline{g}f].

It thus suffices to show that (\overline{gf})^{∗}(I) is contained in the ideal generated by I ∪ f^{∗}(J). Note that \overline{gf} ∈ f^{∗}(J). Thus for each (m, n) ∈ I, we get (m\overline{gf}, n\overline{gf}) ∈ ⟨I ∪ f^{∗}J⟩ by [M.3]. But that says precisely that (\overline{gf})^{∗}(I) = \{(m\overline{gf}, n\overline{gf})|(m, n) ∈ I\} is contained in ⟨I ∪ f^{∗}(J)⟩.

2.29. Lemma. Eq(C) satisfies the meet axioms.

Proof. [Meet.1] [I, f] ∧ [I, f] = [⟨I ∪ I ∪ {(f, f)}⟩, f] = [I, f] since f ∈ I.

[Meet.2] To show [I, f] ∧ [J, g] ≤ [I, f], calculate

[I, f]\overline{[I, f] ∧ [J, g]} = [I, f]\overline{[⟨I ∪ J ∪ \{(f, g)\}⟩, f]}
= [I, f][⟨I ∪ J ∪ \{(f, g)\}⟩, \overline{f}]
= [⟨I ∪ J ∪ \{(f, g)\} ∪ \overline{f}^{∗}(I)⟩, f\overline{f}]
= [⟨I ∪ J ∪ {(f, g)}⟩, f]
= [I, f] ∧ [J, g]

where we used the fact that since \overline{f} ∈ I, we have \overline{f}^{∗}(I) ⊆ I.

[Meet.3] To show ([I, f] ∧ [J, g])[K, h] = [I, f][K, h] ∧ [J, g][K, h] calculate

([I, f] ∧ [J, g])[K, h] = [⟨I ∪ J ∪ {(f, g)}⟩, f][K, h]
= [⟨K ∪ h^{∗}(I ∪ J ∪ {(f, g)})⟩, fh]
= [⟨K ∪ h^{∗}(I) ∪ h^{∗}(J) ∪ {(fh, gh)}⟩, fh]
= [⟨K ∪ h^{∗}(I), fh] ∧ [K ∪ h^{∗}(J)⟩, gh]
= [I, f][K, h] ∧ [J, g][K, h].

To conclude the proof of Proposition 2.25, we consider the inclusion functor η : C → Eq(C), which is the identity on objects and which sends a map f : A → B to [(f, f), f]. To see that this preserves composition, note that [(f, f), f][(g, g), g] = [⟨(g, g), (fg, fg)⟩, fg], so that we need g to be in the ideal generated by (fg, fg). But the latter contains (\overline{fg}, \overline{fg}), and hence by upclosure also (\overline{g}, \overline{g}). Then it also contains (g, g) by [M.5].

It is obvious to see that η preserves the restriction. So what remains is the universal property: given any other restriction functor F : C → D where D has meets, let F̃ : Eq(C) → D have the same action as F on objects, but send a map [I, f] to

F̃[I, f] = (F f) ∏_{(m,n)∈I} \overline{F m ∧ F n}.

The product in this expression is the composition of the idempotents \overline{F m ∧ F n}; since I is finitely generated we may choose a finite generating subset I′ ⊆ I and take the product over that set. By induction on the clauses [M.1] - [M.6] one shows straightforwardly that this is independent of the choice of generating subset. It is clear that F̃ preserves restriction and meets, and that its composite with η is F, and that it is unique with these properties.

We point out that the inclusion functor η : C → Eq(C) is faithful. To see this, note first that the pair ideal ⟨f, f⟩ may be rewritten as

⟨f, f⟩ = ⟨\overline{f}, \overline{f}⟩ = \{(h, k)|h\overline{f} = k\overline{f} and \overline{f} ≤ \overline{h} \overline{k}\}.

From this we see that (⟨f, f⟩, f) ∼ (⟨f, f⟩, g) if and only if f = \overline{f}g. Now suppose that η(f) = η(g), that is, (⟨f, f⟩, f) ∼ (⟨g, g⟩, g). Now from ⟨f, f⟩ = ⟨g, g⟩ we deduce that \overline{f} = \overline{g}. But then (⟨f, f⟩, f) ∼ (⟨f, f⟩, g), so that f = \overline{f}g, and by symmetry also g = \overline{g}f. But this proves that f = g, so that η is faithful as claimed.

By contrast, η is not full (otherwise it would be an isomorphism of categories). However, if we restrict attention to the total maps then η is full. Indeed, the total maps in Eq(C) are of the form [I, f] where \overline{f} = 1 and I = ⟨1, 1⟩. Clearly for such map we have that [⟨1, 1⟩, f] = [⟨f, f⟩, f].

2.30. Remark. In [Lawson 1998], a construction for adding meets to inverse semigroups is given. This construction is appreciably easier than the one above: the free inverse semigroup with meets on an inverse semigroup S may be taken to have as elements the upwards closed subsets of S. This construction also works for inverse categories: given an inverse category C, form a new category with the same objects, but where a map A → B is a finitely generated upwards closed subset of C(A, B). This is the free inverse category with meets on C. The reason why the construction is easier in the inverse case is that we have \overline{f ∧ g} = g^{−1}f ∧ 1, so that a pair ideal is completely determined by elements of the form (h, 1).

Suppose now that the category C has finite restriction products. Does Eq(C) then have products as well? We would like to define the pairing of two maps [I, f] : X → A and [J, g] : X → B to be the map [⟨I ∪ J⟩, ⟨f, g⟩] : X → A × B. (Here, the expression ⟨f, g⟩ of course refers to the pairing coming from the product in C, and has nothing to do with generation of ideals.) However, for this to be well-defined on equivalence classes we need to add another condition on pair ideals, namely

[M.7] (f, f′) ∈ I, (g, g′) ∈ I ⇒ (⟨f, g⟩, ⟨f′, g′⟩) ∈ I.

The resulting modification of construction 2.24 then gives rise to a category with meets and products Eq_{×}(C), and a functor η_{×} : C → Eq_{×}(C); it is readily seen that this functor preserves finite products and is universal amongst such functors into categories with meets and products.

We may summarize as follows. Write ℜ𝔠𝔞𝔱 for the 2-category of restriction categories, restriction functors and total lax natural transformations; write ℜ𝔠𝔞𝔱_{∧} for the sub-2-category whose objects are the meet restriction categories and whose arrows are meet-preserving restriction functors. Similarly, denote by ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱 the 2-category of restriction categories with finite product and product-preserving restriction functors, and by ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱_{∧} the sub-2-category on the cartesian meet restriction categories and meetpreserving functors (equivalently, by Proposition 2.20, the 2-category of discrete categories and product-preserving restriction functors).

2.31. Theorem. Both inclusions

ℜ𝔠𝔞𝔱_{∧} ↪ ℜ𝔠𝔞𝔱  and  ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱_{∧} ↪ ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱

have left biadjoints.

Proof. We have verified the action of the left biadjoint on objects; the action on arrows comes from the universal property proved above. The only thing which needs to be verified is the action on 2-cells. To this end, consider α : F ⇒ G : C → D. We wish to show that we get an induced 2-cell Eq(α) : Eq(F) ⇒ Eq(G) : Eq(C) → Eq(D). The component of this 2-cell at an object X is defined to be [⟨1, 1⟩, α_{X}]. This is evidently total. To see that this is natural, consider an arrow [I, f] : X → Y in Eq(C), and consider the square

[figure: F X; [⟨1,1⟩,α_{X}]; [F I,F f]; ≤; GX; [GI,Gf]; F Y; [⟨1,1⟩,α_{Y} ]; GY.]

We verify that this indeed commutes up to inequality. First observe that

F I = ⟨(F p, F q)|(p, q) ∈ I⟩
= ⟨(α_{Y} F p, α_{Y} F q)|(p, q) ∈ I⟩  since α_{Y} is total
≤ ⟨(Gp ∘ α_{X}, Gq ∘ α_{X})|(p, q) ∈ I⟩  by lax naturality of α
= α_{X}^{∗}(GI).

Then it follows that

[⟨1, 1⟩, α_{Y}][F I, F f] = [F I, α_{Y} F f]
≤ [α_{X}^{∗}(GI), (Gf)α_{X}]
= [GI, Gf][⟨1, 1⟩, α_{X}]

and we’re done.

3. Cartesian Range Categories

Having established some basic results concerning finite limits in restriction categories, we now look to combine this structure with ranges. We mainly focus on the interaction between ranges and products.

3.1. Beck-Chevalley Condition Although we will be mainly interested in the Beck-Chevalley Condition (BCC) in the context of range categories with products, most of the concepts involved make sense on the level of arbitrary range categories already. Recall that one possible viewpoint on a range category is that it is a category in which all maps are open, i.e. in which, for each f : A → B, the pullback functor f^{∗} : O(B) → O(A) has a Frobenius left adjoint f_{!} : O(A)/\overline{f} → O(B). (Equivalently (see part I), we may ask for a direct image map ∃_{f} : O(A) → O(B) satisfying some equations; in the remainder of the paper we will use the same notation ∃_{f} for both.) The Beck-Chevalley Condition asks for these left adjoints to be coherent with respect to these pullback functors. (See for example the textbook [Jacobs 1999] for an exposition of the BCC in the fibrational setting.)

3.2. Definition. Let C be a range category, and consider a commutative square hg = kf in C:

\xymatrix{A \ar[r]^{f} \ar[d]_{g} & B \ar[d]^{k} \\ C \ar[r]_{h} & D}

We say that the square satisfies the Beck-Chevalley Condition (BCC) when, for each restriction idempotent e ∈ O(C) with e ≤ \overline{h} we have

∃_{f}g^{∗}(e) = k^{∗}∃_{h}(e).

The first thing to note is that this definition is not symmetric, in the sense that it does not follow that for idempotents e′ ∈ O(B) we have ∃_{g}f^{∗}(e′) = h^{∗}∃_{k}(e′).

The second thing is that one half of the BCC equality holds automatically: we always have the inequality

∃_{f}g^{∗}(e) ≤ k^{∗}∃_{h}(e).

This is a standard calculation: for e ≤ \overline{h}:

e ≤ h^{∗}∃_{h}(e) ⇒ g^{∗}(e) ≤ g^{∗}h^{∗}∃_{h}(e)
⇔ g^{∗}(e) ≤ f^{∗}k^{∗}∃_{h}(e)
⇔ ∃_{f}g^{∗}(e) ≤ k^{∗}∃_{h}(e).

Obviously, one cannot expect in general that all commutative squares are BCC; commonly, one asks for the BCC for all pullback squares, or for pullback squares of projections. However, there are certain squares for which the BCC automatically holds.

3.3. Lemma. Given a partial isomorphism h : C → D and an arbitrary map k : B → D. Form the restricted pullback

\xymatrix{B \ar[r]^{k^{∗}\overline{h^{−1}}} \ar[d]_{h^{−1}k} & B \ar[d]^{k} \\ C \ar[r]_{h} & D}

Then the BCC holds for this square.

Proof. Consider e ≤ \overline{h}. We need to show that ∃_{k^{∗}(\overline{h′})}(h′k)^{∗}(e) ≤ k^{∗}∃_{h}(e). To this end, compute

∃_{k^{∗}(\overline{h^{−1}})}(h^{−1}k)^{∗}(e) = k^{∗}\overline{h^{−1}} ∧ k^{∗}(h^{−1})^{∗}(e)
= k^{∗}ĥ ∧ k^{∗}∃_{h}(e)
= k^{∗}∃_{h}(1) ∧ k^{∗}∃_{h}(e)
= k^{∗}∃_{h}(e).

The above can be generalized slightly: consider an arbitrary commutative square

\xymatrix{A \ar[r]^{f} \ar[d]_{g} & B \ar[d]^{k} \\ C \ar[r]_{h} & D}

where f and h are partial isomorphisms. Then:

3.4. Lemma. The above square satisfies the BCC if and only if k^{∗}(\overline{h^{−1}}) = \overline{k} \overline{f^{−1}}.

Proof. Consider a restriction idempotent e ≤ \overline{h}. We need to show that k^{∗}∃_{h}(e) = ∃_{f}g^{∗}(e). Since h and f are partial isomorphisms, we have ∃_{h} = (h^{−1})^{∗} and ∃_{f} = (f^{−1})^{∗}. Furthermore, we have the following equalities:

1. \overline{h}g = h^{−1}kf

2. eg = e\overline{h}g = eh^{−1}kf

3. ∃_{f}(\overline{wf}) = f̂ for any w ∈ O(B)

Indeed, we have \overline{h}g = h^{−1}hg = h^{−1}kf by commutativity of the square; the second item follows from the first because e ≤ \overline{h}; and for the third item compute ∃_{f}(\overline{wf}) = f̂\overline{wf} = ŵf = wf̂.

Then we have

∃_{f}g^{∗}(e) = ∃_{f}(\overline{eg})
= ∃_{f}(\overline{eh^{−1}kf})  by (2)
= \overline{eh^{−1}k}f̂  by (3)
= \overline{eh^{−1}k} \overline{f^{−1}}
= \overline{eh^{−1}k}  because \overline{h^{−1}(k)} = \overline{f^{−1}}
= k^{∗}(h^{−1})^{∗}(e)
= k^{∗}∃_{h}(e)

For the other direction, take e = \overline{h}, giving k^{∗}(\overline{h^{−1}}) = k^{∗}∃_{h}(\overline{h}) = ∃_{f}g^{∗}(\overline{h}) = \overline{\overline{h}gf^{−1}} = \overline{hgf^{−1}} = \overline{kf̂} = \overline{k}f̂ = \overline{k} \overline{f^{−1}}.

Another useful fact is that BCC squares compose, both horizontally and vertically. We state this for future reference:

3.5. Lemma. Consider commutative diagrams

[figure: •; 1; •; 2; •; •; •; •; and; •; 3; •; •; 4; •; •; •]

If 1 and 2 are BCC squares then so is the composite square; similarly, if 3 and 4 are BCC squares then so is their composite.

The proof is a straightforward exercise.

3.6. Ranges and Products As we have seen in Section 2, products in a restriction category may be specified by giving a right adjoint to the diagonal in the category ℜ𝔠𝔞𝔱_{l} of restriction categories, restriction functors and lax total natural transformations. In the case of range categories, it makes sense to impose the additional requirement that this right adjoint is a range functor, i.e. preserves both domains and ranges. Explicitly, this means that we need { \atop f × g} = f̂× ĝ. This is exactly what the BCC achieves:

3.7. Definition. A range category with finite partial products is said to be a cartesian range category when the Beck-Chevalley Condition holds for squares of the form

\xymatrix{A × X \ar[r]^{f×1} \ar[d]_{π_{A}} & B × X \ar[d]^{π_{B}} \\ A \ar[r]_{f} & B}  (2)

3.8. Lemma. The condition in the previous definition is equivalent to asking that { \atop f × g} = f̂× ĝ for all maps f, g.

Proof. If { \atop f × g} = f̂ × ĝ holds for all f, g, then to prove that (2) is a BCC square we compute, for e ∈ O(A),

∃_{f×1}π^{∗}(e) = ∃_{f×1}(e × X) = { \atop (f × 1)(e × 1)} = f̂e × 1 = π^{∗}∃_{f}(e).

Conversely, if all squares of the form (2) are BCC, then we know that { \atop f × 1} = f̂× 1 for all f and that { \atop 1 × g} = 1 × ĝ for all g. Then

{ \atop f × g} = { \atop (f × 1)(1 × g)} = \begin{matrix} \\ { \atop (f × 1)} & { \atop (1 × g)} \end{matrix}
= { \atop (f̂× 1)(1 × ĝ)} = { \atop f̂× ĝ}
= f̂× ĝ.

Next we characterize the categories whose partial map categories are cartesian range categories. Clearly, they will have finite products and an (E, M) factorization system in which all the M-maps are pullback-stable (as explained in part I). In this factorization system, a map is in E precisely when f̂ = 1. This leads to the following characterization:

3.9. Proposition. Let C be a category with finite products and an (E, M)-factorization system which is M-stable. Then Par(C, M) is a cartesian range category if and only if the E-maps are closed under binary products.

Proof. Suppose first that the BCC holds for projection squares. To show that the Emaps are closed under products it suffices to show that if f is in E, then so is f ×1. So we assume that f̂ = 1, and need to show that { \atop f × 1} = 1. But { \atop f × 1} = f̂× 1 by the previous lemma, so we’re done.

Conversely, suppose that the E-maps are closed under products. We want to show that the range operation preserves products of maps. By construction of ranges and of products in Par(C, M) it suffices to consider total maps. Thus the problem reduces to showing that given maps f, g in C, the (E, M)-factorization of f × g is the product of the factorizations of f and g. This follows readily from the assumption that E-maps are stable under products, since we already know that the M-maps are stable under products as well.

We point out that the analogous result for P-categories is given in [Rosolini 1998].

3.10. Ranges and Discreteness In a general range category, maps are not necessarily surjective onto their range. For example, any category is a range category under \overline{f} = 1, f̂ = 1. In order to rule out such examples, we may impose the condition

[RR.5] gf = hf ⇒ gf̂ = hf̂.

This condition was taken in [Di Paola & Heller 1987] and in [Rosolini 1998] to be part of the axioms for a range (together with [RR.2], but without [RR.1], [RR.3] or [RR.4]). As explained in Part 1 of this paper, [RR.5] is independent of the other range axioms, and [RR.1], [RR.2] and [RR.5] together imply the remaining axioms [RR.3] and [RR.4]. However, this condition is not independent from discreteness, as the following proposition shows.

3.11. Proposition. A cartesian range category is discrete if and only if it satisfies [RR.5].

Proof. We give an algebraic proof here; after the proof we explain how the result also follows directly from a well-known fact about factorization systems.

In one direction consider, for an object A, the map π_{0}Δ̂ : A×A → A. This is a partial inverse to Δ: we have π_{0}Δ̂Δ = π_{0}Δ = 1_{A}, and since π_{0}Δ = π_{1}Δ we get π_{0}Δ̂ = π_{1}Δ̂, whence Δπ_{0}Δ̂ = Δ̂.

For the converse, suppose that we are given that gf = hf. This implies that f = \overline{g ∧ h}f, and so

gf̂ = g{ \atop \overline{g ∧ h}f} = g\overline{g ∧ h}f̂ = h\overline{g ∧ h}f̂ = h{ \atop \overline{g ∧ h}f} = hf̂.

Alternatively, one may invoke the following result about factorization systems in categories with finite products (see [Adamek et al. 1990] for example):

3.12. Lemma. Let (E, M) be a factorization system on a finitely complete category. Then the following are equivalent:

(i) Each E-map is epic;

(ii) Each regular monic is in M;

(iii) Each section is in M;

(iv) Each diagonal is in M.

Proof. For (i) ⇒ (ii), suppose that f is an equalizer of g, h. Factor f = em, where e is epic by assumption. Then also mg = mh, so that m factors through f, giving an inverse of e. Thus e ∈ M, and hence also f ∈ M.

For (iv) ⇒ (i), suppose that f ∈ E, and that gf = hf. Then consider the commutative square

\xymatrix{A \ar[r]^{f} \ar[d]_{gf} & B \ar[d]^{⟨g,h⟩} \\ C \ar[r]_{Δ} & C × C}

Since the diagonal Δ is in M, orthogonality gives a diagonal filler p : B → C satisfying Δp = ⟨g, h⟩. Thus g = h, and f is epic.

Our aim is now to to show that discrete range categories correspond, under the representation from 3.9, to finitely complete categories equipped with an (E, M)-factorization system in which the E-maps are pullback-stable and the diagonal maps are in M. We already know from Section 2.2 that discreteness corresponds to finite limits, so we concentrate on the factorization system here. Before we do so, however, we point out that these results are closely related to those on the connection between factorization systems and fibred categories in the paper [Hughes & Jacobs 2002] by Hughes and Jacobs, who show that every factorization stable gives rise to a bifibration, which then satisfies the BCC precisely when the factorization system is stable. The proof we give here does not explicitly involve fibrations (although of course every restriction category comes naturally equipped with its fibration of idempotents) but it is closely related to the approach in loc. cit.

One of the key facts which we must establish first is that all pullback squares of total maps satisfy the BCC condition. We first prove a technical lemma concerning latent pullbacks; recall that in discrete categories all latent pullbacks exist.

3.13. Lemma. Let C be a discrete cartesian category.

(i) Partial monics are stable under latent pullback along arbitrary maps.

(ii) If in addition C is a discrete cartesian range category, then any latent pullback square satisfies the BCC.

Proof. Consider a latent pullback square, which, by (lemma 2.22) we may assume to be of the form

\xymatrix{A × B \ar[r]^{π_{1}\overline{fπ_{0}∧gπ_{1}}} \ar[d]_{π_{0}\overline{fπ_{0}∧gπ_{1}}} & B \ar[d]^{g} \\ A \ar[r]_{f} & C.}

Abbrebiate e = \overline{fπ_{0} ∧ gπ_{1}}.

(i) We use the universal property of the latent pullback. Suppose we have two maps

α, β : X → A × B

for which π_{1}eα = π_{1}eβ. We need to show that eα = eβ. But from the assumption it follows right away that \overline{eα} = \overline{eβ}. Hence eα and eβ have the same domain. In addition, they have the same composites with both projections:

π_{1}eα = π_{1}eβ ⇒ gπ_{1}eα = gπ_{2}eβ
⇒ fπ_{0}eα = fπ_{0}eβ
⇒ \overline{f}π_{0}eα = \overline{f}π_{0}eβ
⇒ π_{0}eα = π_{0}eβ

where the last step follows from the fact that e ≤ \overline{fπ_{0}}. Thus the maps eα and eβ must be equal.

(ii) We have already shown that latent pullback squares of partial isomorphisms along arbitrary maps satisfy the BCC. Since we are in a discrete cartesian category, the diagonal maps are partial isomorphisms, and hence stable under latent pullback, giving BCC squares as well. It is now a straightforward exercise to show that the BCC for an arbitrary latent pullback square is a formal consequence of the BCC for pullbacks of diagonals and of projections.

Suppose now that C has the property that all monics are partial isomorphisms. Then we can use the above lemma to deduce that all pullback squares in the total category are BCC: given a pullback square

\xymatrix{P \ar[r]^{p} \ar[d]_{q} & B \ar[d]^{g} \\ A \ar[r]_{f} & C}

in Tot(C) consider the latent pullback in C, and the induced comparison morphism:

[figure: P; p; q; ⟨p,q⟩; A × B; π_{1}e; π_{0}e; B; g; A; f; C]

The map ⟨p, q⟩ is monic, so splits in C by assumption. But because it is the equalizer in Tot(C) of fπ_{0} and gπ_{1}, it splits the idempotent e = \overline{π_{0}f ∧ π_{1}g}. In particular, we have ∃_{⟨p,q⟩}⟨p, q⟩^{∗}(e) = e. Since the two triangles commute on the nose and since the inner square is BCC, so is the outer square.

We now have everything in place for the main characterization:

3.14. Theorem. Let D be a category with a stable system of monics M. Then Par(D, M) is a discrete cartesian range category if and only if D has finite limits such that all diagonal maps (and hence all regular monics) are in M, and such that M is part of a stable factorization system.

Proof. If D and M have these properties, then Par(D, M) is discrete (Section 2) and has ranges (Part I). The fact that the E-maps are pullback-stable means that e ∈ E implies e × 1 ∈ E. By Proposition 3.7 this gives the BCC for Par(D, M).

Conversely, if Par(D, M) is discrete then D is finitely complete and M contains all diagonals (Section 2). The ranges give a factorization system (E, M) on D, where a map f ∈ E if and only if f̂ = 1. Then it remains to be shown that E-maps are pullback-stable. But this follows right away from the fact that all pullback squares of total maps satisfy the BCC.

3.15. Corollary. A restriction category is a discrete cartesian range category if and only if it embeds (in a restriction, range and meet-preserving way) into the partial map category of a category which has finite limits and a stable factorization system for which all regular monics are in M.

Notice that the factorization systems referred to in this corollary are automatically proper: by assumption the M-maps are monics, and the E-maps are epic because of Lemma 3.12.

3.16. Regularity A category D equipped with a stable factorization system (E, M) satisfying the conditions of the characterization above is not yet a regular category. For that, we need to know that the E-maps are precisely the regular epimorphisms. We did prove (Proposition 3.11) that [RR.5] holds, so that the E-maps are epimorphisms.

Thus there are two remaining issues: we need to know when E consists of all regular epis, and also when M contains all monics. These two are related however, as witnessed by the following result, which appears in [Kelly 1991] where it is attributed to Joyal; it is also implicit in [Hughes & Jacobs 2002]:

3.17. Proposition. In a category with finite limits, a stable factorization system (E, M) is the regular epi-mono factorization precisely when M is the class of all monics.

This immediately gives our main characterization:

3.18. Theorem. A discrete cartesian range category C admits a full embedding (preserving meets, products and ranges) into the partial map category of a regular category if and only if every partial monic is a partial isomorphism.

Of course, a restriction category satisfying the equivalent conditions of this theorem will be said to be a regular restriction category.

Proof. Given a regular category D, the partial map category Par(D, M) is a discrete range category, as we have seen earlier. A partial monic in Par(D, M) is a span (m, f) in which f is monic. Since by assumption this means that f ∈ M, we get that (f, m) is a partial inverse.

For the other direction, suppose that C satisfies the conditions. Then so does the idempotent splitting Split(C), and the embedding C → Split(C) preserves all structure. Moreover, we know already that the total map category Tot(Split(C)) is finitely complete and has a stable factorization system. Because all partial monics are restriction monics in C, that means that all monics in Tot(Split(C)) are in M). Hence the category is regular.

This result draws attention to the condition that all partial monics are partial isomorphisms. Given a discrete range category C, can we force this condition to hold, turning C into a regular restriction category? There are indeed several ways of achieving this. The first is directly adapted from work by Kelly [Kelly 1991], who investigated the difference between left exact categories with a proper stable factorization system and regular categories, and showed that the regular reflection of a proper stable factorization system can be described in terms of a category of fractions construction. More concretely, given a category C with finite limits and a proper stable factorization system (E, M), let Σ = E ∩ Mono; then C[Σ^{−1}] is the regular reflection of C.

In our setting, a similar category of fractions construction works. Given a discrete range category C, we consider the category r(C) whose objects are the same as those of C, but where a morphism A → B is an equivalence class of spans (m, f) from A to B where m is a partial monic and where \overline{m} = \overline{f}. Two such spans (m, f) and (n, g) are defined to be equivalent when there exist partial monics α, β making a commutative diagram

\xymatrix{ & C \ar[dl]_{m} \ar[dr]^{f} \\ A & X \ar[u]_{α} \ar[d]^{β} & C \\  & D \ar@{-->}[ul]^{n} \ar@{-->}[ur]_{g}}

for which \overline{α} = \overline{β}, α̂ = \overline{m}, β̂ = \overline{n}. Composition is as in the ordinary span construction, only using latent pullbacks. The restriction of (m, f) is defined to be (m, m), while the range is (f̂, f̂). Finally, there is a functor γ : C → r(C), which is the identity on objects and which sends a morphism f to the span (\overline{f}, f).

We then have

3.19. Theorem. Given a discrete range category C, r(C) is a regular restriction category, the functor γ : C → r(C) preserves ranges, products and meets, and is universal amongst such functors from C into regular restriction categories.

Proof. The verifications that r(C) is a regular restriction category can be carried out directly using some basic properties of latent pullbacks. However, these calculations are formally very similar to those for the ordinary category of fractions construction; hence we omit the details.

Another approach to forcing regularity is to work with a Grothendieck topology on C; Since this involves significant new technical developments which extend beyond the scope of the present paper, we leave this for another occasion.

3.20. The Range Completion of a Discrete Restriction Category The construction of the free regular category on a category C with finite limits is remarkably simple and elegant: the objects are maps in C , and an arrow f → g is an equivalence class of maps k

\xymatrix{Ker(f) \ar[d]_{p_{0}} \ar[d]^{p_{1}} \\ X \ar[d]_{f} \ar[r]^{[k]} & U \ar[d]^{g} \\ Y & V}

where gkp_{0} = gkp_{1}; two such maps k, k′ are equivalent when they have the same composite with g. (See [Carboni & Vitale 1998] for details.) An object f : X → Y in the completion is the formally adjoined image of f.

This raises the question how this construction is related to the constructions presented in the present papers. In the next section, a syntactic approach to adding ranges is presented, but this approach does not lend itself well to comparison with the usual regular completion. We therefore discuss a different viewpoint, which is based on the construction of the free range category as presented in part I of this paper.

Recall from part I, section 5, that the forgetful functor from range categories to restriction categories has a left biadjoint; to a restriction category C, we assign the free range category R(C), whose objects are those of C, but whose morphisms are equivalence classes of pairs [T, f], where T is a suitable kind of finite tree. This construction can be adapted so that it works for discrete cartesian restriction categories. The key observation is that in the presence of latent pullbacks, the trees used to represent the freely adjoined idempotents can be greatly simplified by adding a rule for manipulating trees.

To illustrate how this works, consider the tree

\xymatrix{C & D & F \ar[d]^{t} \\ B \ar[dr]_{k} \ar[u]^{r} \ar@{-->}[ur]_{s} &  & E \\  & \underline{A} \ar[ur]_{l}}

based on A. First of all, using the equivalence relation on trees as described in part I (which identifies trees if they represent the same idempotent) we may set m = k\overline{r}\overline{s} to get the simpler

\xymatrix{ &  & F \ar[d]^{t} \\ B \ar[dr]_{m} &  & E \\  & \underline{A} \ar[ur]_{l}}

Next, we form the latent pullback of t and l.

\xymatrix{ &  & F \ar[d]^{t} \\ B \ar[dr]_{m} & F′ \ar@{-->}[ur]^{l′} \ar[d]^{t′} & E \\  & \underline{A} \ar[ur]_{l}}

Since t′ now represents the same idempotent as the original branch consisting of l and t (because latent pullback squares satisfy the BCC!), we may forget about the latter. Finally, we combine the two ingoing branches m, t′ again using a latent pullback:

\xymatrix{P \ar[dr]^{m′} \ar[d]_{t′′} \\ B \ar[dr]_{m} & F′ \ar[d]^{t′} \\  & \underline{A}}

Now the idempotent represented by the branches m, t′ is the same as that represented by the single composite branch mt′′. Thus we have reduced the entire tree to a single ingoing map.

This means that in case of a discrete cartesian category C, adding ranges (while preserving the discreteness) has a different presentation, making use of the fact that each tree can be represented by a single arrow. Of course, there is still an equivalence relation on these arrows, since distinct morphisms may represent the same range. Most notably, the range represented by the single arrow f : B → A is the same as that represented by the composite fp, where p : B ×_{A} B → B is the projection from the latent pullback of f against itself. However, this needs to be generalized appropriately in order to ensure that composition, restriction and range are well-defined.

3.21. Construction. Let C be a discrete cartesian restriction category. Define a new category R_{d}(C) as follows:

Objects: Those of C

Morphisms: A morphism A → B is an equivalence class of spans (k, h) for which there exists an f with h = kf:

\xymatrix{ & X \ar[dl]_{k} \ar[dr]^{h} \\ A \ar@{-->}[rr]_{f} &  & B}

(We think of such a span as representing the morphism fk̂.) The equivalence relation on such pairs is generated as follows: consider a commutative diagram of the form

\xymatrix{P \ar[r]^{a′} \ar[d]_{m} & Q \ar[r]^{b′} \ar[d] & F \ar[d]^{b} \\ X \ar[r]^{a} \ar[ddr]_{h} \ar[dd]_{k} \ar[dr]^{v} & F \ar[r]^{b} & G \ar[d]^{c} \\  & D \ar[d]^{w} \ar[r]^{r} & H \\ A \ar@{-->}[r]_{f} & B}  (3)

where \overline{r}v = v and where the two top squares are latent pullbacks. Then (k, h) ∼ (mk, mh). The equivalence class of (k, h) will be denoted by [k, h].

Identities: The identity on an object A is [1, 1].

Composition: Given [k, h] : A → B and [l, j] : B → C, the composite is defined to be [kl′, jh′] as in the latent pullback

\xymatrix{ &  & P \ar[dr]^{h′} \ar[dl]_{l′} \\  & X \ar[dl]_{k} \ar[dr]^{h} &  & Y \ar[dl]_{l} \ar[dr]^{j} \\ A \ar@{-->}[rr]_{f} &  & B \ar@{-->}[rr]_{g} &  & C}  (4)

Restriction: The restriction of [k, h] is defined to be \overline{[k, h]} = [k, k].

Range: The range of [k, h] is defined to be { \atop [k, h]} = [h, h].

We begin by making the following observations, which often simplify reasoning:

3.22. Lemma. Each morphism in R_{d}(C) is represented by a span (k, h) for which \overline{k} = \overline{h}. Similarly, given a diagram of the form (3), we may assume without loss of generality that \overline{v} = \overline{k} = \overline{h}.

The second statement in the lemma means that imposing the extra condition \overline{v} = \overline{k} does not change the equivalence relation on spans.

Proof. For the first part, simply observe that (k, h) ∼ (k\overline{h}, h\overline{h}) = (k\overline{h}, h) because of the diagram

\xymatrix{X \ar[r]^{=} \ar[d]_{\overline{h}} & X \ar[r]^{\overline{h}} \ar[d]^{\overline{h}} & X \ar[d]^{\overline{h}} \\ X \ar[r]^{=} \ar[ddr]_{h} \ar[dd]_{k} \ar[dr]^{h} & X \ar[r]^{=} & X \ar[d]^{h} \\  & B \ar[d]^{=} \ar[r]^{=} & B \\ A \ar@{-->}[r]_{f} & B}

For the second statement, assume we are given a diagram of the form (3), witnessing (k, h) ∼ (km, hm). Then replace v by v\overline{k}; since the pullback of m along \overline{k} equals \overline{k}m, it follows that the resulting diagram witnesses (k, h) ∼ (k\overline{k}m, h\overline{k}m) = (km, hm) as well.

We also point out that it follows from the definition of the equivalence relation on spans that [k, h] = [kα, hα] whenever α is a partial isomorphism with \overline{α^{−1}} ≥ \overline{k}.

We now embark on the verifications that the above definitions give a well-defined range category.

3.23. Lemma. Composition in R_{d}(C) is well-defined.

Proof. Note first that composition does not depend on the choice of latent pullback, since latent pullbacks are unique up to unique partial isomorphism, and hence any two choices will give equivalent maps.

Next, consider morphisms [k, h] and [l, j], and suppose [k, h] = [km, hm] as per diagram (3). We want to show first that postcomposing with [l, j] does not depend on whether we use the representative (k, h) or (km, hm). To this end, first form the latent pullbacks

\xymatrix{P′ \ar[d]_{p′} \ar[r]^{m′} & X′ \ar[r]^{h′} \ar[d]^{l′} & Y \ar[d]^{l} \\ P \ar[r]_{m} & X \ar[r]_{h} & B}

Then [l, j][k, h] = [kl′, jh′], while [l, j][km, hm] = [p′mk, jh′m′], and we must show that these two are equal. Consider the following diagram:

\xymatrix{P′ \ar[r]^{p′} \ar[d]_{m′} & P \ar[d]_{m} \ar[r] & Q \ar[r] \ar[d] & F \ar[d]^{b} \\ X′ \ar[d]_{l′} \ar[drr]^{vl′} \ar[ddrr]_{jh′} \ar[r]^{l′} & X \ar[r]^{a} & F \ar[r]^{b} & G \ar[d]^{c} \\ X \ar[d]_{k} &  & D \ar[d]^{gw} \ar[r]_{r} & H \\ A \ar@{-->}[rr]_{gf} &  & C}

The three top squares are latent pullbacks and the rest of the diagram commutes, since gwvl′ = ghl′ = glh′ = jh′. Thus the diagram witnesses the desired equivalence.

A similar but slightly simpler calculation shows that precomposition is well-defined. We next show that restriction and range are well-defined.

3.24. Lemma. The restriction and range operations are well-defined.

Proof. Once more suppose that (k, h) ∼ (km, hm) as per diagram (3). It is immediate that the same diagram witnesses that (h, h) ∼ (hm, hm) so that the range is well-defined. It therefore remains to show that the restrictions (k, k) and (km, km) are equivalent. First consider the latent pullback

[figure: E; k; v; u; A′; f′; w′; D; w; A; f; B]

We may assume by Lemma 3.22 that \overline{v} = \overline{k} = \overline{fk} = \overline{wv}; it follows that \overline{u} = \overline{v} = \overline{k} so that the two triangles commute on the nose and not just up to inequality. Then consider

\xymatrix{P \ar[d]_{m} \ar[rr] &  & Q \ar[r] \ar[d] & F \ar[d]^{b} \\ X \ar[dd]_{k} \ar[dr]^{u} \ar[ddr]_{k} \ar[rr]_{a} &  & F \ar[r]_{b} & G \ar[d]^{c} \\  & A′ \ar[d]^{w′} \ar[r]_{f′} & D \ar[r]_{r} & H \\ A \ar@{-->}[r]_{1} & A}

which witnesses (1, k) ∼ (1, km), since \overline{rf′}u = u follows from \overline{rf′u} = \overline{rv} = \overline{v} = \overline{f′u} = \overline{u}.

3.25. Lemma. The above definitions make R_{d}(C) a range category.

Proof. We first verify the restriction axioms.

[R.1] Given (k, h), the composite [k, h]\overline{[k, h]} is represented by [kp_{0}, hp1], where p_{0}, p_{1} arise as in the latent pullback

\xymatrix{Q \ar[d]_{p_{0}} \ar[r]^{p_{1}} & X \ar[d]^{k} \\ X \ar[r]_{k} & A}

Now instantiate diagram (3) as follows:

\xymatrix{P \ar[d]_{p_{0}} \ar[r] & Q \ar[d]_{p_{0}} \ar[r]^{p_{1}} & X \ar[d]^{k} \\ X \ar[dd]_{k} \ar[dr]^{=} \ar[ddr]_{h} \ar[r]_{=} & X \ar[r]_{k} & A \ar[d]^{=} \\  & X \ar[r]_{k} \ar[d]^{h} & A \\ A \ar@{-->}[r]_{f} & B}

[R.2] This is immediate from the fact that the composite of two idempotents (k, k) and (l, l) is constructed as the latent pullback of k and l.

[R.3] Consider [k, h] and [l, j] having the same domain. Then \overline{[l, j][k, k]} is represented by (kl′, kl′), where l′ arises as the latent pullback of l along k. On the other hand, we have \overline{[l, j]} = [l, l], so that \overline{[l, j]} \overline{[k, h]} = [l, l][k, k] = [kl′, kl′].

[R.4] Consider maps [k, h] and [l, j], and their composite [l, j][k, h] = [kl′, jh′], where l′, j′ are the projections of the latent pullback of h and l. Then [k, h]\overline{[l, j][k, h]} is represented by the span

\xymatrix{ &  &  & Z′ \ar[dr]^{l′′} \ar[dl]_{p′_{0}} \\  &  & Z \ar[dl]_{l′} \ar[dr]^{l′} &  & Q \ar[dr]^{p_{1}} \ar[dl]_{p_{0}} \\  & X \ar[dl]_{k} &  & X \ar[dr]_{k} &  & X \ar[dl]^{k} \ar[dr]^{h} \\ A &  &  &  & A &  & B}

Then the following instantiation of diagram (3)

\xymatrix{Z′ \ar[d]_{p′_{0}} \ar[r]^{l′′} & Q \ar[d]^{p_{0}} \ar[r]^{p_{1}} & X \ar[d]^{k} \\ X′ \ar[d]_{l′} \ar[r]_{l′} \ar[dr]^{l′} \ar[ddr]_{lh′} & X \ar[r]_{k} & A \ar[d]^{f} \\ X \ar[d]_{k} & E \ar[d]^{h} \ar[r]_{h} & B \\ A \ar@{-->}[r]_{f} & B}

shows that [p′_{0}l′k, p′_{0}lh′] ∼ [l′k, lh′]. But the latter equals \overline{[l, j]}[k, h], while the former equals [k, h]\overline{[l, j][k, h]} since hp_{1}l′′ = fkp_{1}l′′ = fkl′p′_{0} = hl′p′_{0} = lh′p′_{0}.

Next, we turn to the range axioms.

[RR.1] Immediate, since { \atop [k, h]} = [h, h] which is idempotent.

[RR.2] Consider [k, h], and denote by q_{0}, q_{1} the projections of the latent pullback of h along itself. Then the following instantiation of diagram (3) shows that [k, h] = { \atop [k, h]}[k, h].

\xymatrix{P \ar[d]_{q_{0}} \ar[r] & P \ar[r]^{q_{1}} \ar[d]_{q_{0}} & X \ar[d]^{h} \\ X \ar[dd]_{k} \ar[dr]^{=} \ar[ddr]_{h} \ar[r]_{=} & X \ar[r]_{h} & B \ar[d]^{=} \\  & X \ar[d]^{h} \ar[r]_{h} & B \\ A \ar@{-->}[r]_{f} & B}

[RR.3] Straightforward.

[RR.4] Straightforward.

There is an inclusion functor

η : C → R_{d}(C)

which is the identity on objects and which sends a morphism f : A → B to [\overline{f}, f]. This is a restriction functor, but it also preserves the products (and hence all discrete structure):

3.26. Lemma. The category R_{d}(C) has finite products, and η preserves these products on the nose.

Proof. We only need to verify that product diagrams coming from C have the correct universal property in R_{d}(C). Given [k, h] : M → A and [l, j] : M → B, define their pairing to be [kp, ⟨hp, jq⟩] where p, q arise as in the latent pullback

\xymatrix{P \ar[d]_{p} \ar[r]^{q} & Y \ar[d]^{l} \\ X \ar[r]_{k} & M}

We have

\overline{[kp, ⟨hp, jq⟩]} = [kp, kp] = [k, k][l, l] = \overline{[k, h]} \overline{[l, j]}

as needed. Clearly [1, π_{A}][kp, ⟨hp, jq⟩] ≤ [k, h] and similarly [1, π_{B}][kp, ⟨hp, jq⟩] ≤ [l, j]. Finally, it is easy to see that [kp, ⟨hp, jq⟩] is unique with these properties.

Since any restriction functor preserves partial isomorphisms, it now follows that the diagonals in R_{d}(C) are partial isomorphisms as well, so that R_{d}(C) is discrete.

What is more, the BCC holds: given a pullback square of projections in R_{d}(C):

\xymatrix{C × B \ar[r]^{[k,h]×B} \ar[d]_{π_{C}} & A × B \ar[d]^{π_{A}} \\ C \ar[r]_{[k,h]} & A}

and a restriction idempotent [m, m] on C (where m : D → C), we consider the pullback

\xymatrix{P \ar[d]_{p} \ar[r]^{q} & C′ \ar[d]_{k} \\ D \ar[r]_{m} & C.}

We then have

π_{A}^{∗}∃_{[k,h]}[m, m] = π_{A}^{∗}[hq, hq] = [hq × B, hq × B].

However, the functor − × B preserves latent pullbacks (Lemma 2.6), which means that we also have a pullback diagram

\xymatrix{P × B \ar[d]_{p×B} \ar[r]^{q×B} & C′ × B \ar[d]_{k×B} \\ D × B \ar[r]_{m×B} & C × B.}

Therefore also

∃_{[k,h]×B}π_{C}^{∗}[m, m] = ∃_{k,h]×B}[m×B, m×B] = [(h×B)(q×B), (h×B)(q×B)] = [hq×B, hq×B].

The result is then:

3.27. Theorem. For a discrete cartesian restriction category C, the category R_{d}(C) is a discrete cartesian range category. The functor η : C → R_{d}(C) preserves the discrete structure, is faithful and is universal amongst product-preserving functors from C to discrete cartesian range categories.

Proof. What remains is to establish the universal property. Given a discrete cartesian range category D and product-preserving functor F : C → D, we define an extension F̃ : R_{d}(C) → D, which on objects is given by F̃C = F C, and which sends a map [k, h] in R_{d}(C) to F fF̂ k, where f is such that fk = h. We must first show that this is well-defined.

Suppose that fk = h = f′k. Then also F fF k = F f′F k, and hence by [RR.5] it follows that F fF̂ k = F f′F̂ k. Therefore F̃[k, h] does not depend on the choice of f.

Second, suppose that [k, h] = [km, hm] via diagram (3). We must then show that F fF̂ k = F f{ \atop F kF m}. Note first that it suffices to show that F̂ k = { \atop F kF m}, which in turn

follows from the inequality \overline{F k} ≤ F̂ m, since that gives F̂ k = { \atop F k\overline{F k}} ≤ { \atop F kF̂ m} = { \atop F kF m}, while obviously also { \atop F kF m} ≤ F̂ k.

We have \overline{F k} ≤ \overline{F bF a}, since

\overline{F k} = \overline{F v} = \overline{F (gv)} = \overline{F (cba)} ≤ \overline{F (ba)}

(where we have assumed that \overline{v} = \overline{k}, see Lemma 3.22). It remains to be shown that \overline{F (ba)} ≤ F̂ m. This follows from

\overline{F (ba)} = \overline{F a\overline{F b}}
= (F a)^{∗}(\overline{F b})
= F a^{∗}F b^{∗}∃_{F b}(\overline{F b})  since F b^{∗}∃_{F b}(\overline{F b}) = \overline{F b}
= ∃_{F m}(F b′F a′)^{∗}(\overline{F b}) by the BCC
≤ ∃_{F m}(1)
= F̂ m

This shows that F̃ is well-defined. To show that it preserves composition, consider again diagram (4). We need to show that F gF̂ lF fF̂ k = F (gf){ \atop F (l′k)}. First note that F (f)F (k)F (l′) = F (h)F (l′) = F (l)F (h′) = F̂ (l)F (l)F (h′) = F̂ (l)F (k)F (l′), so that

F (g)F (f){ \atop F (kl′)} = F (g)F̂ (l)F (f){ \atop F (kl′)}.

It therefore suffices to show that F̂ (l)F (f){ \atop F (k)} = F̂ (l)F (f){ \atop F (kl′)}. We prove that these two maps have the same domain. But this follows from

\overline{F̂ lF (f){ \atop F (k)}} = { \atop F (k)} ∧ F (f)^{∗}(F̂ (l))
= ∃_{F (k)}F (k)^{∗}F (f)^{∗}(F̂ (l))
= ∃_{F (k)}F (h)^{∗}(F̂ (l))
= ∃_{F (k)}({ \atop F (l′)}) by the BCC
= { \atop F (kl′)}.

It is also readily seen to preserve restriction, range and products. Finally, it is clear that up to isomorphism it is unique with these properties.

Thus we have proved that the forgetful 2-functor from discrete cartesian range categories to discrete cartesian restriction categories has a left adjoint. (An alternative proof based on logical methods will be given in the next section.) After splitting idempotents in R_{d}(C), the objects look very much the same as those of the usual regular completion. However, in the usual regular completion the objects f : A → B and Ker(f) → B are isomorphic but not equal, while in R_{d}(C) these maps represent identical idempotents.

Second, R_{d}(C) is of course not regular, since not every partial monic is a partial isomorphism. This manifests itself as a difference between the arrows in the (total maps of the) idempotent splitting of this category and in the regular completion: in the latter an arrow [k] : f → g is represented by a morphism k : dom(f) → dom(g), while in our case a morphism is represented by an arrow dom(f) → cod(g), for which there exists a factorization through cod(f). When every partial monic is a partial isomorphism one can transform the former into the latter.

4. Logic

In this section we present a term logic for cartesian range categories. The starting point is the term logic for cartesian restriction categories, which has been worked out in [Cockett & Hofstra 2010]. We will briefly review the rules for term formation and equational reasoning in this logic. Then we show how to add equality predicates to the logic; this results in a term logic for discrete cartesian categories. Finally, we add the existential quantifier, giving a term logic for discrete cartesian range categories. (As we saw in the previous section, every cartesian range category satisfying [RR.5] automatically is discrete.)

4.1. Term logic for cartesian restriction categories Our basic term logic starts with a signature Σ, consisting of a collection of basic sorts and function symbols. From these, and a countable stock of fresh variables for each basic sort, we generate a collection of partial terms. Formally, we consider term judgements Γ ⊢ t : T, where Γ is a variable context, t a term and T a type. The rules are displayed in Table 2. Note that we generate product types, including a terminal type, and that we suppress the associativity and unit isomorphisms for these.

The only rule which makes this different from the term logic for ordinary categories with finite products is the Restriction rule, which forms a term t restricted to the domain of s. Sometimes, typographical considerations will force us to write t|s instead of t_{|s}. We also simplify (t_{|s})_{|r} to t_{|s,r} or t_{|s∩r}, and use alpha-conversion whenever necessary. We use t[s/x] for the result of replacing all occurrences of x in t by s, and call this syntactical, or standard substitution. However, in the restriction setting there is another substitution operation t{s/x}, which agrees with t[s/x] except for in the case when x does not occur in t; then we have t{s/x} = t_{|s}.

[x^{1} : A^{1}, …, x^{n} : A^{n}] ⊢ x^{i} : A^{i} Projection

Γ ⊢ () : 1 Unit

\begin{matrix}\{Γ ⊢ t_{i} : T_{i}\}_{i=1,...,n} & f ∈ Ω([T_{1}, .., T_{n}], T_{0}) \\ Γ ⊢ f(t_{1}, ..., t_{n}) : T_{0} \end{matrix} Function application

\begin{matrix}\{Γ ⊢ t_{i} : T_{i}\} & i=1,...,n \\ Γ ⊢ (t_{1}, ..., t_{n}) : T_{1} × ⋯ × T_{n} \end{matrix} Tupling

\begin{matrix}Γ ⊢ t : T & Γ ⊢ s : S \\ Γ ⊢ t_{|s} : T \end{matrix} Restriction

{Γ ⊢ t : A \atop Γ, Δ ⊢ t : A} Weakening {Γ ⊢ t : A \atop σ(Γ) ⊢ t : A} Exchange(σ ∈ S_{n})

Table 2: Judgements for partial terms

Next, we list the rules for equational reasoning (Table 3). Note that the substitution rule uses the non-standard substitution operation.

We recall from [Cockett & Hofstra 2010] that terms in the logic have a normal form: each term is provably equal to a term of the form t_{|s_{1},...,s_{k}}, where neither t nor the s_{i} contain any restrictions, and where the s_{i} are also terms of basic type. If we wish, we may further assume that the terms s_{i} are pairwise incomparable in the subterm ordering.

It is often the case that a (large part of a) derivation in the logic consists only of manipulating the terms in the restriction. In such cases, it is inconvenient to keep the leading term in the notation. To make reasoning about domains easier, we introduce the following notation: by the sequent

Γ ⊢_{R} t_{1} ∩ ⋯ ∩ t_{k} = s_{1} ∩ ⋯ ∩ s_{l}

we mean

Γ ⊢ x⃗_{|t_{1},...,t_{k}} = x⃗_{|s_{1},...,s_{l}}

4.2. Term logic for discrete cartesian restriction categories As an intermediate step towards the logic for cartesian range categories, we first add equality predicates to our logic. This is done by adding a new term constructor

\begin{matrix}Γ ⊢ t : T & Γ ⊢ f, g : A \\ Γ ⊢ t_{|Eq(f,g)} : T \end{matrix} Equality  (5)

[eR.1]  t_{|t} = t
[eR.2]  t_{|s,s′} = t_{|s′,s}
[eR.3]  t_{|s′_{|s}} = t_{|s,s′}
[eR.4]  t_{|x} = t
[eR.5] (t_{1}, .., (t_{k})_{|s}, .., t_{n}) = (t_{1}, .., t_{k}, .., t_{n})_{|s}
[eR.6] f(t_{1}, .., (t_{k})_{|s}, .., t_{n}) = f(t_{1}, .., t_{k}, .., t_{n})_{|s}
[eR.7]  t_{|(t_{1},..,t_{k})} = t_{|t_{1},..,t_{k}}

\begin{matrix}x : S, Γ ⊢ t = t′ : T & Γ ⊢ s = s′ : S \\ Γ ⊢ t\{s/x\} = t′\{s′/x\} \end{matrix} Substitution

Table 3: Equational Logic for Partial Terms

[Eq.1]  {Γ ⊢ t : T \atop Γ ⊢ t_{|Eq(t,t)} = t : T} Eq1

[Eq.2] {Γ ⊢ t, s : T \atop Γ ⊢ t_{|Eq(t,s)} = s_{|Eq(t,s)} : T} Eq2 x ∉ F V (r)

Table 4: Logic of Equality

Here, the type of f and g need not be the same as that of the leading term t. Of course, the term t_{|Eq(f,g)} is thought of as t restricted to the subobject where f and g agree. The rule only allows the equality predicate to appear in restrictions.

We impose two obvious axioms for this new predicate; see Table 4. The side condition x ∉ F V (r) means that we require that x is not a free variable in r.

While the above formulation is convenient in practice, it is perhaps slightly unsatisfactory that the expressions Eq(f, g) are not terms in their own right and may only appear in restrictions. If we wish to be purist, we should instead define terms x, y : A ⊢ Eq′(x, y) : A × A, and impose the axioms (x, y)_{|Eq′(x,y)} = Eq′(x, y), Eq′(x, x) = (x, x), and x_{|Eq′(x,y)} = y_{|Eq′(x,y)}. Clearly this formulation is equivalent to the original one.

The following technical lemma lays out the basic facts concerning the interaction between equality, substitution and pairing.

4.3. Lemma. The following judgements are derivable:

(i) Γ ⊢ t_{|Eq(x,x)} = t

RANGE CATEGORIES II: TOWARDS REGULARITY  493

(ii) ⊢_{R} Eq(t, s) ∩ r[t/x] = Eq(t, s) ∩ r[s/x] (iii) ⊢_{R} Eq(t, y) ∩ Eq(s(y), r) ≤ Eq(s(t), r) (iv) ⊢_{R} Eq(t, s) ∩ r(t) ≤ Eq(r(t), r(s))

(v) ⊢_{R} Eq(t, s) ≤ Eq(r(t), r(s)) when r is total, i.e. x_{|r} = x.

(vi)

Γ ⊢ f, f′ : A Γ ⊢ g, g′ : B

Γ ⊢_{R} Eq(⟨f, g⟩, ⟨f′, g′⟩) = Eq(f, f′) ∩ Eq(g, g′) Proof.

(i) Γ ⊢ t_{|Eq(x,x)} = t_{|x∩Eq(x,x)} = t_{|x} = t where the second last step uses [Eq.1]. (ii) Substituting the equation from [Eq.2] into the term r(x) gives the result. (iii) By the previous item we have Eq(s(y), r)_{|Eq(t,y)} = Eq(s(t), r)_{|Eq(t,y)} ≤ Eq(s(t), r). (iv) Calculate

Γ ⊢_{R} Eq(t, s) ∩ Eq(r(t), r(s)) = Eq(t, s) ∩ Eq(r(t), r(t))
= Eq(t, s) ∩ r(t)

(v) Immediate from the previous item. (vi) Since projections are provably total, we have

⊢_{R} Eq(⟨f, g⟩, ⟨f′, g′⟩) ≤ Eq(π_{0}⟨f, g⟩, π_{0}⟨f′, g′⟩)
= Eq(f, f′).

Similarly, we find Eq(⟨f, g⟩, ⟨f′, g′⟩) ≤ Eq(g, g′). On the other hand, we have

⊢_{R} Eq(⟨f, g⟩, ⟨f′, g′⟩) ∩ Eq(f, f′) ∩ Eq(g, g′) = Eq(⟨f_{|Eq(f,f′)}, g_{|Eq(g,g′)}⟩, ⟨f′_{|Eq(f,f′)}, g′_{|Eq(g,g′)}⟩)
= ⟨f_{|Eq(f,f′)}, g_{|Eq(g,g′)}⟩
= f_{|Eq(f,f′)} ∩ g_{|Eq(g,g′)}
= Eq(f, f′) ∩ Eq(g, g′).

Thus ⊢_{R} Eq(⟨f, g⟩, ⟨f′, g′⟩) ≤ Eq(f, f′) ∩ Eq(g, g′) and the result is proved.

We may introduce a definitional extension of the logic by letting

t ∧ s := t_{|Eq(t,s)}.

It is straightforward to show that this syntactical meet operation behaves as expected, e.g. that it is associative, commutative and idempotent.

Now suppose that C is a discrete cartesian restriction category together with an interpretation of all basic types and function symbols. We now extend the interpretation for partial terms from [Cockett & Hofstra 2010] to include the equality predicates: given interpretations

\xymatrix{[[Γ]] \ar[r]^{[[t]]} & [[T]] & and & [[Γ]] \ar[r]^{[[f]]} \ar[r]_{[[g]]} & [[T]]}

we set [[t_{|Eq(f,g)}]] to be

\xymatrix{[[Γ]] \ar[r]^{\overline{[[f]]∧[[g]]}} & [[Γ]] \ar[r]^{[[t]]} & [[T]]}

In other words, we first form the meet of (the interpretations of) f and g (which is possible since any discrete cartesian category has meets), take the domain of this meet and then restrict t to it.

Next, we show that this interpretation is sound. For the axiom [Eq.1], this amounts

to showing that the composite \xymatrix{[[Γ]] \ar[r]^{\overline{[[t]]∧[[t]]}} & [[Γ]] \ar[r]^{[[t]]} & [[T]]} equals [[t]]. However, this is immediate from the fact that for any map h we have \overline{h ∧ h} = \overline{h}.

For axiom [Eq.2], we must show that the composites

\xymatrix{[[Γ]] \ar[r]^{\overline{[[t]]∧[[s]]}} & [[Γ]] \ar[r]^{[[t]]} & [[T]] & and & [[Γ]] \ar[r]^{\overline{[[t]]∧[[s]]}} & [[Γ]] \ar[r]^{[[s]]} & [[T]]}

are equal. This is immediate from Lemma 2.11, since both arrows equal [[t]] ∧ [[s]].

For completeness, we show that when 𝕋 is a theory in the given term logic (i.e. a specification of non-logical equational judgments over a given signature), then the classifying category C[𝕋] is discrete. Since it was already shown in [Cockett & Hofstra 2010] that the classifying category is a cartesian restriction category, it only remains to be shown that its diagonals are restriction monics.

To this end, consider a basic type A and the diagonal map Δ_{A} : A → A × A in C[𝕋]. The diagonal is the 𝕋-provable equality class of the term judgment x : A ⊢ (x, x) : A × A. Of course, we let its partial inverse be the equality class of the judgment x : A, y : A ⊢ x ∧ y : A. Axiom [Eq.1] says that precomposing this term with the diagonal gives x : A ⊢ x ∧ x = x : A, so that it is a retraction of the diagonal. Moreover, postcomposing with the diagonal gives

x : A, y : A ⊢ (x ∧ y, x ∧ y) : A × A.

But we have x_{|x∧y} = x ∧ y = y_{|x∧y}, so that (x ∧ y, x ∧ y) = (x, y)_{|x∧y}, which shows that this composite is a restriction idempotent. We have shown:

4.4. Theorem. [Completeness] For any theory 𝕋 (in the language of cartesian restriction categories with equality) the classifying category C[𝕋] is discrete.

Thus, the term logic is precisely the internal language for the class of discrete cartesian categories. In particular, we may, given a discrete cartesian category C, consider the theory of C, which has the objects of C for its sorts, the arrows of C for its function symbols and the commutative diagrams of C for its axioms. (In this case, the basic types are already closed under products, so we do not have to introduce new types.) We shall write T h(C) for this theory. We now use this to show to construct the free discrete cartesian category on a cartesian one.

As before, write ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱 for the sub-2-category of of ℜ𝔠𝔞𝔱 on the cartesian restriction categories and restriction functors which preserve restriction products. Similarly, denote by 𝔇𝔦𝔰𝔠ℜ𝔠𝔞𝔱 the sub-2-category on the discrete cartesian restriction categories and restriction functors which preserve restriction products.

4.5. Theorem. The forgetful 2-functor 𝔇𝔦𝔰𝔠ℜ𝔠𝔞𝔱 → ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱 has a left biadjoint.

Proof. Consider a cartesian category D. We may form its theory T h(D) in the cartesian fragment of the logic, and then form the classifying category C[T h(D)] w.r.t. the discrete logic. Clearly there is an embedding D → C[T h(D)] which preserves the restriction and the products. It is now easy to see that this embedding is universal w.r.t. product-preserving functors from D to discrete cartesian categories.

Taken together with Proposition 2.25, this means that all of the forgetful functors in the pullback diagram

\xymatrix{𝔇𝔦𝔰𝔠ℜ𝔠𝔞𝔱 \ar[r] \ar[d] & ℭ𝔞𝔯𝔱ℜ𝔠𝔞𝔱 \ar[d] \\ 𝔐𝔢𝔢𝔱ℜ𝔠𝔞𝔱 \ar[r] & ℜ𝔠𝔞𝔱}

have left biadjoints.

4.6. Term logic for discrete range categories We now add the existential quantifier to our logic. This will be done via a new term constructor which allows us to build terms of the form t_{|∃x.s(x)}, to be thought of as t restricted to the image of s along the projection onto the domain of t. Explicitly, we introduce a term formation rule

\begin{matrix}Γ, x : A ⊢ t_{|s(x)} : B & x ∉ F V (t) \\ Γ ⊢ t_{|∃x.s(x)} : B \end{matrix} ∃

in which the side condition that the variable x does not occur freely in t is essential. The intended interpretation of a judgement Γ ⊢ t_{|∃x.s(x)} : B is given by the following diagram:

\xymatrix{Γ × A \ar[r]^{\overline{s}} \ar[d]_{π_{Γ}} & Γ × A \ar[d]_{π_{Γ}} \ar[dr]^{[[t_{|s}]]} \\ Γ \ar[r]^{π̂_{Γ}\overline{s}} \ar[rr]_{[[t_{|∃x.s(x)}]]} & Γ \ar[r]^{t} & B}

[eRR.1] ⊢_{R} ∃x.∃y.s(x, y) = ∃y.∃x.s(x, y)
[eRR.2] ⊢_{R} ∃x.(r ∩ s(x)) = r ∩ ∃x.s(x) x ∉ F V (r)
[eRR.3]  ⊢_{R} s[r/x] ≤ ∃x.s(x)

[eRR.4]  {⊢_{R} s = s′ \atop ⊢_{R} ∃x.s(x) = ∃x.s′(x)}

Table 5: Range Equality Axioms

The rules governing the equational reasoning about such terms are given in Table 5. (We recall that we use the notation ⊢_{R} t = s to indicate that the domains of t and of s are provably equal.)

The first rule is obvious: we may permute quantifiers. Note that, because we suppress permutations of context variables from the notation, we have two judgements, x : A, y : B ⊢ s(x, y) and y : A, x : B ⊢ s(x, y), so both terms are well-defined. The second rule is the Frobenius condition. For the third, keep in mind that an inequality f ≤ g really is an equality f = g_{|f} in disguise; as such, it plays the role of the counit of the adjunction ∃_{X} ⊣ π_{X}^{∗}. Finally, the last rule simply ensures that the new term formation rule preserves provable equality.

4.7. Remark. Just as for equality, the axiomatization given has the disadvantage that the new expressions ∃x.s(x) are not first-class citizens. Again, this could be overcome using a formulation which takes ∃x.s(x) to be a genuine term, and then to stipulate that this term represents an idempotent.

In our axiomatization, the range of a term x : A ⊢ t : B may be defined as follows:

\begin{matrix}x : A, y : B ⊢ y_{|y} : B & x : A, y : B ⊢ y_{|t(x)} : B \\ x : A, y : B ⊢ y_{|Eq(t(x),y)} : B \end{matrix} ; y : B ⊢ y_{|∃x.Eq(t(x),y)} : B

When the domain of t is not a basic type, we quantify away the variables one by one. (The order doesn’t matter.) More generally, we define the direct image along t to be

∃_{t} : O(A) → O(B); [x : A ⊢_{R} s(x)] ↦ [y : B ⊢_{R} ∃x.Eq(t(x)_{|s(x)}, y)].

The following lemma collects some basic results.

4.8. Lemma. The following equational judgements are derivable:

(i) ⊢_{R} ∃y.s ≤ s when y ∉ F V (s)

RANGE CATEGORIES II: TOWARDS REGULARITY  497

(ii) x : A ⊢ t = t_{|∃x.Eq(x,x)} (iii) ⊢_{R} ∃y.[Eq(t, y) ∩ Eq(s(y), r)] ≤ Eq(s(t), r) when y ∉ F V (t) ∪ F V (r) Proof.

(i) We have ⊢_{R} ∃y.s = ∃y.(s ∩ Eq(y, y)) = s ∩ ∃y.Eq(y, y) ≤ s. (ii) Assume that x ∉ F V (t). Then y : A ⊢ t = t_{|Eq(y,y)} ≤ t_{|∃x.Eq(x,x)} by [eRR.3]. (iii) This follows from item (i) and Lemma 4.3.

We now establish soundness. We need to show that the rules [eRR.1] - [eRR.4] hold under the interpretation. [eRR.1] First, note that the interpretations of Γ, x : A, y : B ⊢ s(x, y) : S and Γ, y : B, x : A ⊢ s(x, y) : S fit into a commutative diagram

\xymatrix{A × B \ar[d]^{τ} \ar[dr]^{[[Γ,x,y⊢s(x,y)]]} \\ B × A \ar[r]_{[[Γ,y,x⊢s(x,y)]]} & S}

where τ is the canonical isomorphism. As a consequence, we have that

∃_{τ}(\overline{[[Γ, x, y ⊢ s(x, y)]]}) = \overline{[[Γ, y, x ⊢ s(x, y)]]}.

Now the diagram

\xymatrix{Γ × A × B \ar[rr]^{π_{Γ×A}} \ar[d]_{τ} &  & Γ × A \ar[d]^{π_{Γ}} \\ Γ × B × A \ar[r]_{π_{Γ×B}} & Γ × B \ar[r]_{π_{Γ}} & Γ}

commutes, hence

[[Γ ⊢_{R} ∃x∃y.s(x, y)]] = ∃_{π_{Γ}}∃_{π_{Γ×A}}(\overline{[[Γ, x, y ⊢ s(x, y)]]})
= ∃_{π_{Γ}}∃_{π_{Γ×B}}∃_{τ}(\overline{[[Γ, x, y ⊢ s(x, y)]]})
= ∃_{π_{Γ}}∃_{π_{Γ×B}}(\overline{[[Γ, y, x ⊢ s(x, y)]]})
= [[Γ ⊢_{R} ∃y∃x.s(x, y)]])

[eRR.2] This is simply the statement that the map ∃_{X} has the Frobenius property. [eRR.3] It suffices to show that Γ, x : A ⊢_{R} s(x) ≤ ∃x.s(x) is soundly interpreted. But this inequality is simply the counit of the adjunction ∃_{π_{Γ}} ⊣ π_{Γ}^{∗}.

[eRR.4] Obvious.

4.9. Completeness Next, we prove that the classifying category associated to a theory 𝕋 in the language of cartesian range categories is indeed a cartesian range category.

As explained above, we define the range of the morphism represented by a judgement Γ ⊢ t : T to be y : T ⊢ y_{|∃x⃗.Eq(t(x⃗),y)} : T. We need to verify the four range axioms.

[RR.1] Given t, we get that t̂t is represented by

y_{|∃x.t(x)=y}[t(z)/y] = t(z)_{|∃x.t(x)=t(z)}.

Now because t(z) = t(z)_{|t(z)=t(z)} ≤ t(z)_{|∃x.t(x)=t(z)} the result follows.

[RR.2] This is clear; given a term t we get

y_{|y|∃x.t(x)=y} = y_{|y,∃x.t(x)=y} = y_{|∃x.t(x)=y}

The first of these represents \overline{t̂}, the last t̂.

[RR.3] Consider \xymatrix{A \ar[r]^{s} & B \ar[r]^{t} & C} . On the one hand, \overline{t}ŝ is represented by

x : B ⊢_{R} t(x) ∩ ∃y.Eq(s(y), x) = ∃y.(t(x) ∩ Eq(s(y), x)) = ∃y.(t(s(y)) ∩ Eq(s(y), x)).

On the other hand, \overline{t}s is represented by y : A ⊢ s(y)_{|t(s(y))}, so that ˆ \overline{t}s is represented by

x : A ⊢_{R} ∃y.Eq(x, s(y)_{|t(s(y))}) = ∃y.(Eq(x, s(y)) ∩ t(s(y))).

[RR.4] Consider \xymatrix{A \ar[r]^{s} & B \ar[r]^{t} & C} . On the one hand, t̂s is represented by

z : C ⊢_{R} ∃x.Eq(z, t(s(x))).

On the other hand, tŝ is represented by y : B ⊢ t(y)_{|∃x.Eq(s(x),y)}, so that t̂ŝ is represented by

z : C ⊢_{R} ∃y.Eq(z, t(y)_{|∃x.Eq(s(x),y)}) = ∃y.[Eq(z, t(y)) ∩ ∃x.Eq(s(x), y)]
= ∃y∃x.[Eq(z, t(y)) ∩ Eq(s(x), y)]
≤ ∃y∃x.Eq(z, t(s(x)))
≤ ∃x.Eq(z, t(s(x))),

where the first two inequalities come from Lemma 4.8.

This shows that C[𝕋] is a cartesian restriction category with ranges. It remains to be shown that the Beck-Chevalley Condition holds. To this end, consider a term judgement x : A ⊢ t(x) : B, representing a morphism A → B, and a sort C. Then the pullback of [[t(x)]] : A → B along the projection B × C → B is represented by the tuple term x : A, z : C ⊢ ⟨t(x), z⟩ : B × C.

\xymatrix{A × C \ar[r]^{[[x,z⊢⟨t(x),z⟩]]} \ar[d] & B × C \ar[d] \\ A \ar[r]_{[[x⊢t(x)]]} & B}

Consider a restriction idempotent on A, represented by a term x : A ⊢_{R} s(x). First taking the direct image of this idempotent along t(x) and then pulling back yields the restriction idempotent represented by the term

y : B, z : C ⊢_{R} ∃x.Eq(y, t(x)_{|s(x)}).

First pulling back along the projection and then taking the direct image gives

y : B, z : C ⊢_{R} ∃x∃w.Eq(⟨t(x)_{|s(x)}, w⟩, ⟨y, z⟩)

However, using Lemma 4.8 we may calculate

y : B, z : C ⊢_{R} ∃x∃w.Eq(⟨t(x)_{|s(x)}, w⟩, ⟨y, z⟩) = ∃x∃w.(Eq(t(x)_{|s(x)}, y) ∩ Eq(w, z))
= ∃x.Eq(t(x)_{|s(x)}, y) ∩ ∃w.Eq(w, z)
= ∃x.Eq(t(x)_{|s(x)}, y)

where the last step uses z : C ⊢_{R} z = Eq(z, z) = ∃w.Eq(z, w).

The term logic for discrete cartesian range categories again provides us with left biadjoints to the forgetful functors from the 2-categories of discrete cartesian restriction categories, of cartesian restriction categories and of range categories satisfying [RR.5].

References

[Adamek et al. 1990] J. Adamek, H. Herrlich, and G. Strecker. Abstract and Concrete Categories: The Joy of Cats, volume 17. TAC Reprints, 2006. Originally published by John Wiley and Sons, New York, 1990.

[Barr et al. 1971] M. Barr, P.A. Grillet, and D.H. van Osdol. Exact categories and categories of sheaves,

volume 263 of Lecture Notes in Mathematics. Springer, 1971. [Butz 1998] C. Butz. Regular categories and regular logic, 1998. BRICS Lecture Series LS-98-2. [Carboni & Vitale 1998] A. Carboni and E.M. Vitale. Regular and exact completions. Journal of Pure

and Applied Algebra, (125):79–116, 1998. [Cockett & Hofstra 2010] J. R. B. Cockett and P. J. W. Hofstra. Unitary theories, unitary categories.

Electronic Notes in Theoretical Computer Science, 2010. [Cockett & Lack 2002] J.R.B Cockett and S. Lack. Restriction categories I. Theoretical Computer Sci-

ence, 270:223–259, 2002.

500  J.R.B. COCKETT, XIUZHAN GUO AND PIETER HOFSTRA

[Cockett & Lack 2007] J.R.B Cockett and S. Lack. Restriction categories III: colimits, partial limits, and extensivity. Mathematical Structures in Computer Science, 17:775–817, 2007.

[Hughes & Jacobs 2002] J. Hughes and B. Jacobs. Factorization systems and fibrations: Toward a fibred Birkhoff variety theorem. Electr. Notes in Theor. Comp. Sci., 69, 2002.

[Jackson & Stokes 2003] M. Jackson and T. Stokes. Agreeable semigroups. Journal of Algebra, 266(2):393 – 417, 2003.

[Jacobs 1999] B. Jacobs. Categorical logic and type theory. Elsevier Science, 1999.

[Johnstone 2002] P. T. Johnstone. Sketches of an elephant: a topos theory compendium. Oxford University Press, 2002.

[Kelly 1991] G.M. Kelly. A note on relations relative to a factorization system. In Category Theory, volume 1488 of Lecture Notes in Mathematics, 1991.

[Lawson 1998] M.V. Lawson. Inverse Semigroups. World Scientific, 1998.

[Di Paola & Heller 1987] R. Di Paola and A. Heller. Dominical categories: recursion theory without elements. Journal of Symbolic Logic, 52:595–635, 1987.

[Rosolini 1998] G. Rosolini. Representation theorems for p-categories. In F. Borceux, editor, Categorical Algebra and its Applications, volume 1348 of Lecture Notes in Mathematics, pages 307–315. Springer Verlag, 1988.

Department of Computer Science, University of Calgary 2500 University Dr. NW, Calgary, Alberta Canada T2N 1N4, Canada

Department of Mathematics and Statistics, University of Ottawa 585 King Edward Avenue, Ottawa, ON, K1N 6N5, Canada

Email: robin@ucalgary.ca
      guox@cpsc.ucalgary.ca
      phofstra@uottawa.ca

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/26/18/26-18.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne : kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Glasgow, Tom.Leinster@glasgow.ac.uk Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca