Theory and Applications of Categories, Vol. 27, No. 17, 2013, pp. 445–463.

ELEMENTARY QUOTIENT COMPLETION

MARIA EMILIA MAIETTI AND GIUSEPPE ROSOLINI

Abstract. We extend the notion of exact completion on a category with weak finite limits to Lawvere’s elementary doctrines. We show how any such doctrine admits an elementary quotient completion, which is the universal solution to adding certain quotients. We note that the elementary quotient completion can be obtained as the composite of two other universal constructions: one adds effective quotients, the other forces extensionality of morphisms. We also prove that each construction preserves comprehension.

1. Introduction

Constructions for completing a category by quotients have been widely studied in category theory. The main instance is the so-called exact completion, see [Carboni and Celia Magno, 1982; Carboni and Vitale, 1998], which is the universal construction of an exact category over a category with finite limits; it formally adds quotients of (pseudo-)equiv-alence relations. In general, the category-theoretic analysis of the properties of quotients provides a very robust, mathematically structured theory which can be applied in various situations: the contents of the present paper offers precisely this with respect to the study of foundational theories for constructive mathematics.

Indeed, the use of quotients is pervasive in interactive theorem proving where proofs are performed in appropriate systems of formalized mathematics in a computer-assisted way. Indeed some kind of quotient completion is compulsory when mathematics is formalized within an intensional type theory, such as the Calculus of (Co)Inductive Constructions [Coquand, 1990; Coquand and Paulin-Mohring, 1990] or Martin-Löf’s type theory [Nordström et al., 1990]. In such a context, an abstract, finitary construction of quotient completion provides a formal framework where to combine the usual practice of (extensional) mathematics, with the need of formalizing it in an intensional theory with strong decidable properties (such as decidable type-checking) on which to perform the extraction of algorithmic contents from proofs.

To make explicit the use of quotient completion in the formalization of constructive mathematics, the paper [Maietti, 2009] included such notion as part of the very definition of constructive foundation which refines that originally given in [Maietti and Sambin, 2005] in terms of a two-level theory. According to [Maietti, 2009], a constructive foundation must be equipped with an intensional level, which can be represented by a suitable starting category C, and an extensional level that can be seen as (a fragment of) the internal language of a suitable quotient completion of C. As investigated in [Maietti and Rosolini, 2013a], some examples of quotient completion performed on intensional theories, such as the intensional level of the minimalist foundation in [Maietti, 2009], or the Calculus of Constructions, do not fall under the known constructions of exact completion given that the corresponding type theoretic categories closed under quotients are not exact.

Received by the editors 2012-03-31 and, in revised form, 2013-09-01.

Published on 2013-09-08 in the volume of articles from CT2011.

2010 Mathematics Subject Classification: 03G30 03B15 18C50 03B20 03F55.

Key words and phrases: quotient completion, split fibration, universal construction.

\begin{matrix}c \\ ◯ \end{matrix} Maria Emilia Maietti and Giuseppe Rosolini, 2013. Permission to copy for private use granted.

In [Maietti and Rosolini, 2013a] we studied the abstract category-theoretical structure behind such quotient completions. To this purpose we introduced the notion of equivalence relation and quotient relative to a suitable fibered poset and produced a universal construction adding effective quotients—hence the name elementary quotient completion—to elementary doctrines.

In the present paper we isolate the basic components of the universal constructions in [Maietti and Rosolini, 2013a]. After recalling the basic notions required in the sequel, we show how to add effective quotients universally to an elementary doctrine in the sense of [Lawvere, 1970], a fibered inf-semilattice on a category with finite products, endowed with equality. Separately, we describe how to force extensional equality of morphisms to (the base of) an elementary doctrine. Then we prove that the two constructions can be combined to give the elementary quotient completion. Finally we check that the exact completion of a category with products and weak equalizers is an instance of the elementary quotient completion while the regular completion of a category is an instance of a rather different construction.

2. Doctrines

We analyse quotients within the general theory of fibrations, in particular, the basic fibrational concept that we shall employ is that of a doctrine. It was introduced, in a series of seminal papers, by F.W. Lawvere to synthesize the structural properties of logical systems, see [Lawvere, 1969a; Lawvere, 1969b; Lawvere, 1970], see also [Lawvere and Rosebrugh, 2003] for a unified survey. Lawvere’s crucial intuition was to consider logical languages and theories as fibrations to study their 2-categorical properties, e.g. connectives and quantifiers are determined by structural adjunctions. That approach proved extremely fruitful, see [Makkai and Reyes, 1977; Carboni, 1982; Lambek and Scott, 1986; Jacobs, 1999; Taylor, 1999; van Oosten, 2008] and references therein.

Taking advantage of the category-theoretical presentation of logic by fibrations, we first introduce a general notion of elementary doctrine which we found appropriate to study the notion of quotient of an equivalence relation, see [Maietti and Rosolini, 2013a; Maietti and Rosolini, 2013b].

Denote by InfSL the category of inf-semilattice, i.e. posets with finite infima, and functions between them which preserves finite infima.

2.1. Definition. Let C be a category with binary products. An elementary doctrine (on C) is an indexed inf-semilattice P: C^{op} ⟶ InfSLsuch that, for every object A in C, there is an object δ_{A} in P (A × A) such that (i) the assignment

E_{⟨id_{A},id_{A}⟩}(α) := P_{pr_{1}}(α) ∧_{A×A} δ_{A}

for α in P (A) determines a left adjoint to P_{⟨id_{A},id_{A}⟩}: P (A × A) → P (A)—here and below we write P_{f} for the value of the indexing functor P on a morphism f;

(ii) for every morphism e of the form ⟨pr_{1}, pr_{2}, pr_{2}⟩: X × A → X × A × A in C, the

assignment

E_{e}(α) := P_{⟨pr_{1},pr_{2}⟩}(α) ∧_{X×A×A} P_{⟨pr_{2},pr_{3}⟩}(δ_{A})

for α in P (X × A) determines a left adjoint to P_{e}: P (X × A × A) → P (X × A).

2.2. Remark. (a) Condition (i) determines δ_{A} uniquely for every object A in C.

(b) Since ⟨pr_{2}, pr_{1}⟩ ∘ ⟨id_{A}, id_{A}⟩ = ⟨id_{A}, id_{A}⟩, from (a) it follows that

E_{⟨id_{A},id_{A}⟩}(α) = P_{pr_{2}}(α) ∧_{A×A} δ_{A}

for every α in P (A).

(c) In case C has a terminal object, conditions (ii) entails condition (i).

(d) One has that ⊤_{A} ≤_{A} P_{⟨id_{A},id_{A}⟩}(δ_{A}) and δ_{A} ≤_{A×A} P_{f×f}(δ_{B}) when f: A → B.

2.3. Remark. For α_{1} in P (X_{1} × Y_{1}) and α_{2} in P (X_{2} × Y_{2}), it is useful to introduce a notation like α_{1} ⊠ α_{2} for the object

P_{⟨pr_{1},pr_{3}⟩}(α_{1}) ∧ P_{⟨pr_{2},pr_{4}⟩}(α_{2})

in P (X_{1} ×X_{2} ×Y_{1} ×Y_{2}) where pr_{i}, i = 1, 2, 3, 4, are the projections from X_{1} ×X_{2} ×Y_{1} ×Y_{2} to each of the four factors—like we did above, we shall often drop the index in an infimum on in an inequality when it is clear in which fiber it is. Then condition 2.1(ii) is equivalent to the requirement that, for every pair of objects A and B in C, one has δ_{A×B} = δ_{A} ⊠ δ_{B}. We refer the reader to [Jacobs, 1999; Maietti and Rosolini, 2013a] for further details.

2.4. Examples. (a) The standard example of an indexed poset is the fibration of subobjects. Consider a category C with products and pullbacks. The functor S: C^{op} ⟶ InfSL assigns to any object A in C the poset S(A) of subobjects of A in C. For a morphism f: B → A, the assignment that maps a subobject in S(A) to that represented by the left-hand morphism in any pullback along f of its produces a functor S_{f}: S(A) → S(B) that preserves products.

The elementary structure is provided by the diagonal morphisms.

(b) (For logicians) The Lindenbaum-Tarski algebras of well-formed formulas of a theory 𝒯 with equality in the first order language ℒ provide another instance of elementary doctrine, in fact we believe it shows how elementary doctrines provide the appropriate abstract mathematical structure for that construction. The domain category is the category V of lists of variables and term substitutions:

object of V are lists of distinct variables x⃗ = (x_{1}, …, x_{n}); morphisms are lists of substitutions^{1} for variables [t⃗/y⃗]: x⃗ → y⃗ where each term t_{j} in t⃗

is built in ℒ on the variables x_{1}, …, x_{n};

composition \xymatrix{x⃗ \ar[r]^{[t⃗/y⃗]} & y⃗ \ar[r]^{[s⃗/z⃗]} & z⃗} is given by simultaneous substitutions

\xymatrix{x⃗ \ar[r]^{[s_{1}[t⃗/y⃗]/z_{1},...,s_{k}[t⃗/y⃗]/z_{k}]} & z⃗} .

The product of two objects x⃗ and y⃗ is given by a(ny) list w⃗ of as many distinct variables as the sum of the number of variables in x⃗ and of that in y⃗. Projections are given by substitution of the variables in x⃗ with the first in w⃗ and of the variables in y⃗ with the last in w⃗.

The elementary doctrine LT: V^{op} ⟶ InfSL on V is given as follows: for a list of distinct variables x⃗, the inf-semilattice LT (x⃗) has

objects equivalence classes of well-formed formulas of ℒ with no more free variables than x_{1},…,x_{n} with respect to provable reciprocal consequence W ⊣⊢_{𝒯} W′ in 𝒯 ;

morphisms [W] → [V ] are the provable consequences W ⊢_{𝒯} V in 𝒯 for some pair of representatives (hence for any pair);

composition is given by the cut rule in the logical calculus;

identities [W] → [W] are given by the logical rules W ⊢_{𝒯} W.

For a list of distinct variables x⃗, the poset LT (x⃗) has finite infima: the top element is x⃗ = x⃗ and the infimum of a pair of formulas is obtained by conjunction.

(c) Consider a category S with binary products and weak pullbacks. Another example of elementary doctrine which appears prima facie very similar to previous example (a) is given by the functor of weak subobjects Ψ: S^{op} ⟶ InfSL which evaluates as the poset reflection of each comma category S/A at each object A of S, introduced in [Grandis, 2000].

The apparently minor difference between the present example and example (a) depends though on the possibility of factoring an arbitrary morphism as a retraction followed by a monomorphism: for instance this can be achieved in the category Setof sets and functions thanks to the Axiom of Choice, see loc.cit.

It is possible to express precisely how the examples are related once we consider the 2-category ED of elementary doctrines: the 1-morphisms are pairs (F, b) where F: C → D is a functor and b: P →^{.} R ∘ F^{op} is a

1We shall employ a vector notation for lists of terms in the language as well as for simultaneous substitutions such as [t⃗/y⃗] in place of [t_{1}/y_{1}, …, t_{m}/y_{m}].

natural transformation as in the diagram

[figure: C^{op}; P; F^{op}; InfSL; D^{op}; R; b; ·]

where the functor F preserves products and, for every object A in C, the functor b_{A}: P (A) → R(F (A)) preserves all the structure. More explicitly, for every object A in C, the function b_{A} preserves finite infima and

b_{A×A}(δ_{A}) = R_{⟨F (pr_{1}),F (pr_{2})⟩}(δ_{F (A)});  (1)

the 2-morphisms are natural transformations θ: F →^{.} G such that

[figure: C^{op}; P; F^{op}; G^{op}; InfSL; D^{op}; R; b ·; · c; .; θ^{op}; ≤]

so that, for every A in C and every α in P (A), one has b_{A}(α) ≤_{F (A)} R_{θ_{A}}(c_{A}(α)).

2.5. Examples. (a) Given a theory 𝒯 with equality in a first order language ℒ (say with a single sort), a 1-morphism (F, b): LT → S from the elementary doctrine LT: V^{op} ⟶ InfSL as in 2.4(b) into S: Set^{op} ⟶ InfSL, the elementary doctrine in 2.4(a) with C = Set, determines a model 𝔐 of 𝒯 where the set underlying the interpretation is F (x). In fact, there is an equivalence between the category ED(LT, S) and the category of models of 𝒯 and ℒ -homomorphisms.

(b) Given a category C with products and pullbacks, one can consider the two indexed posets: that of subobjects S: C^{op} ⟶ InfSL, and the other Ψ: C^{op} ⟶ InfSL, obtained by the poset reflection of each comma category C/A, for A in C. The inclusions of the poset S(A) of subobjects over A into the poset reflection of C/A extend to a 1-morphism from S to Ψ which is an equivalence exactly when every morphism in C can be factored as a retraction followed by a monic.

3. Quotients in an elementary doctrine

The structure of elementary doctrine is suitable to describe the notions of an equivalence relation and of a quotient for such a relation.

3.1. Definition. Given an elementary doctrine P: C^{op} ⟶ InfSL, an object A in C and an object ρ in P (A × A), we say that ρ is a P -equivalence relation on A if it satisfies

reflexivity: δ_{A} ≤ ρ;

symmetry: ρ ≤ P_{⟨pr_{2},pr_{1}⟩}(ρ), for pr_{1}, pr_{2}: A × A → A the first and second projection, respectively;

transitivity: P_{⟨pr_{1},pr_{2}⟩}(ρ) ∧ P_{⟨pr_{2},pr_{3}⟩}(ρ) ≤ P_{⟨pr_{1},pr_{3}⟩}(ρ), for pr_{1}, pr_{2}, pr_{3}: A × A × A → A the projections to the first, second and third factor, respectively.

In elementary doctrines as those presented in 2.4, P -equivalence relations coincide with the usual notion for those of the form (a) or (b); more interestingly, in cases like (c) a Ψ-equivalence relation is a pseudo-equivalence relation in S in the sense of [Carboni and Celia Magno, 1982].

For P: C^{op} ⟶ InfSLan elementary doctrine, the object δ_{A} is a P -equivalence relation on A. And for a morphism f: A → B in C, the functor P_{f×f}: P (B ×B) → P (A×A) takes a P -equivalence relation σ on B to a P -equivalence relation on A. Hence, the P -kernel equivalence of f: A → B, the object P_{f×f}(δ_{B}) of P_{A×A} is a P -equivalence relation on A. In such a case, one speaks of P_{f×f}(δ_{B}) as an effective P -equivalence relation.

3.2. Remark. A 1-morphism (F, b): P → R in ED takes a P -equivalence relation on A to an R-equivalence relation on F A.

3.3. Remark. The notion of P -equivalence relation can be stated in any indexed infsemilattice P: C^{op} ⟶ InfSLreplacing the condition of reflexivity by

⊤_{A} ≤ P_{⟨id_{A},id_{A}⟩}ρ.

We refer the interested reader to [Pasquali, 2013].

3.4. Definition. Let P: C^{op} ⟶ InfSL be an elementary doctrine. Let ρ be a P - equivalence relation on A. A P -quotient of ρ (or simply a quotient when the doctrine is clear from the context) is a morphism q: A → C in C such that ρ ≤ P_{q×q}(δ_{C}) and, for every morphism g: A → Z such that ρ ≤ P_{g×g}(δ_{Z}), there is a unique morphism h: C → Z such that g = h ∘ q.

We say that such a P -quotient is stable if, in every pullback

\xymatrix{A′ \ar[d]_{f′} \ar[r]^{q′} & C′ \ar[d]^{f} \\ A \ar[r]_{q} & C}

in C, the morphism q′: A′ → C′ is a P -quotient.

Note that the inequality ρ ≤ P_{q×q}(δ_{C}) in 3.4 becomes an equality exactly when ρ is effective.

3.5. Remark. We should pause briefly to point out that the previous requirement of stability differs slightly from the usual one, see [Janelidze and Tholen, 1994; Janelidze et al., 2004; Joyal and Moerdijk, 1995; Hyland et al., 1990], where existence of any pullback of a quotient would be enforced in order to declare it stable. But we must recall that the main intention of the present paper is to adopt the point of view of category theory to analyse foundational theories. All examples in that area suggest to look at indexed categories—as their syntactic presentation yields directly that structure and the induced fibration of points has a cleavage—, and very rarely the base category of indices has pullbacks. Also, the universal solution will appear only if one states stability as in 3.4.

In the elementary doctrine S: C^{op} ⟶ InfSLobtained from a category C with products and pullbacks as in 2.4(a), a quotient of the S-equivalence relation [[figure: r: R; A × A]] is precisely a coequalizer of the pair of

\xymatrix{R \ar[r]^{pr_{1}∘r} \ar[r]_{pr_{2}∘r} & A}

In particular, all S-equivalence relations have stable, effective quotients if and only if the category C is exact.

Similarly, in the elementary doctrine Ψ: S^{op} ⟶ InfSL obtained from a category C with binary products and weak pullbacks as in 2.4(c), a quotient of the Ψ-equivalence relation [\xymatrix{r: R \ar[r] & A × A}] is precisely a coequalizer of the pair of

\xymatrix{R \ar[r]^{pr_{1}∘r} \ar[r]_{pr_{2}∘r} & A}

In particular, all Ψ-equivalence relations have quotients which are stable if and only if the category C is exact.

The abstract theory that captures the essential action of a quotient is that of descent. We recall some basic concepts from that in our particular case of interest of an elementary doctrine P: C^{op} ⟶ InfSL, see [Janelidze et al., 2004; Janelidze and Tholen, 1994; Janelidze and Tholen, 1997] for an excellent survey on descent theory.

For a P -equivalence relation ρ on an object A in C, the poset of descent data Des_{ρ} is the sub-poset of P (A) on those α such that

P_{pr_{1}}(α) ∧_{A×A} ρ ≤ P_{pr_{2}}(α),

where pr_{1}, pr_{2}: A × A → A are the projections. It is easy to see that Des_{ρ} ⊆ P (A) is closed under infima.

It follows immediately from 2.2(b) that, for any object A in C, one has that

Des_{δ_{A}} = P (A).

For f: A → B in C, write ϕ for the P -kernel equivalence P_{f×f}(δ_{B}). The functor P_{f}: P (B) → P (A) maps P (B) into Des_{ϕ}—it is the usual comparison functor. The morphism f is descent if the (obviously faithful) functor P_{f}: P (B) → Des_{ϕ} is also full. The morphism f is effective descent if the functor P_{f}: P (B) → Des_{ϕ} is an equivalence.

Consider the 2-full 2-subcategory QED of ED whose objects are elementary doctrines P: C^{op} ⟶ InfSLin which every P -equivalence relation has a P -quotient that is a descent morphism.

The 1-morphisms are those pairs (F, b) in ED

[figure: C^{op}; P; F; InfSL; D^{op}; R; b; ·]

such that F preserves quotients in the sense that, if q: A → C is a quotient of a P - equivalence relation ρ on A, then F q: F A → F C is a quotient of the R-equivalence relation R_{⟨F (pr_{1}),F (pr_{2})⟩}(b_{A×A}(ρ)) on F A.

4. Completing with quotients as a universal construction

It is a simple construction that produces an elementary doctrine with quotients. We shall present it below and prove that it satisfies a suitable universal property.

Let P: C^{op} ⟶ InfSLdenote an elementary doctrine for the rest of the section. Consider the category R_{P} of “equivalence relations of P ”:

an object of R_{P} is a pair (A, ρ) such that ρ is a P -equivalence relation on A;

a morphism f: (A, ρ) → (B, σ) is a morphism f: A → B in C such that ρ ≤_{A×A} P_{f×f}(σ) in P (A × A).

Composition is given by that of C, and identities are the identities of C.

The indexed poset (P)_{q}: R_{P}^{op} ⟶ InfSLon R_{P} will be given by categories of descent data: on an object (A, ρ) it is defined as

(P)_{q}(A, ρ) := Des_{ρ}

and the following lemma is instrumental to give the assignment on morphisms using the action of P on morphisms.

4.1. Lemma. With the notation used above, let (A, ρ) and (B, σ) be objects in R_{P}, and let β be in Des_{σ}. If f: (A, ρ) → (B, σ) is a morphism in R_{P}, then P_{f}(β) is in Des_{ρ}.

Proof. Let pr_{1}, pr_{2}: A × A → A and pr′_{1}, pr′_{2}: B × B → B be the product projections. Since β is in Des_{σ}, it is

P_{pr}′_{1}(β) ∧ σ ≤_{B×B} P_{pr}′_{2}(β).

Hence

P_{f×f}(P_{pr_{1}}(β)) ∧ P_{f×f}(σ) ≤_{A×A} P_{f×f}(P_{pr_{2}}(β))

as P_{f×f} preserves the structure. Since ρ ≤_{A×A} P_{f×f}(σ), we have

P_{pr_{1}}(P_{f}(β)) ∧ ρ ≤_{A×A} P_{pr_{2}}(P_{f}(β)).

4.2. Lemma. With the notation used above, the functor (P)_{q}: R_{P}^{op} ⟶ InfSL is an elementary doctrine.

Proof. For (A, ρ) and (B, σ) in R_{P} let pr_{1}, pr_{3}: A × B × A × B → A and pr_{2}, pr_{4}: A × B × A × B → B be the four projections. As an infimum of two P -equivalence relations on A × B, the P -equivalence relation

ρ ⊠ σ := P_{⟨pr_{1},pr_{3}⟩}(ρ) ∧_{A×B×A×B} P_{⟨pr_{2},pr_{4}⟩}(σ)

provides an object (A × B, ρ ⊠ σ) in R_{P} which, together with the morphisms determined by the two projections from A × B, is a product of (A, ρ) and (B, σ) in R_{P}. For an object (A, ρ) in R_{P}, one sees that ρ ∈ P (A × A) is in Des_{ρ⊠ρ} using symmetry and transitivity. We check that the assignment (( E )_{q})_{⟨id_{A},id_{A}⟩}(α) := P_{pr_{1}}(α) ∧_{A×A} ρ, for α in Des_{ρ}, gives the left adjoint (( E )_{q})_{⟨id_{A},id_{A}⟩} for ((P)_{q})_{⟨id_{A},id_{A}⟩} and leave the proof of 2.1(ii) to the reader. Consider β in Des_{ρ⊠ρ} such that α ≤_{(A,ρ)} ((P)_{q})_{⟨id_{A},id_{A}⟩}(β), i.e. α ≤_{A} P_{⟨id_{A},id_{A}⟩}(β). Therefore E_{⟨id_{A},id_{A}⟩}(α) ≤_{A×A} β, which is the same as P_{pr_{1}}(α) ∧ δ_{A} ≤_{A×A} β by 2.1(i). It follows that

P_{pr}′_{1}(α) ∧ P_{⟨pr′_{1},pr′_{2}⟩}(δ_{A}) ∧ P_{⟨pr′_{2},pr′_{3}⟩}(ρ) ≤_{A×A×A} P_{⟨pr′_{1},pr′_{2}⟩}(β) ∧ P_{⟨pr′_{2},pr′_{3}⟩}(ρ)
≤_{A×A×A} P_{⟨pr′_{1},pr′_{3}⟩}(β)

for pr′_{i}: A × A × A → A, i = 1, 2, 3, the projections. Reindexing the inequality along the morphism ⟨pr_{1}, pr_{2}, pr_{2}⟩: A × A → A × A × A, one obtains that P_{pr_{1}}(α) ∧ ρ ≤_{A×A} β, i.e.

(( E )_{q})_{⟨id_{A},id_{A}⟩}(α) ≤_{(A×A,ρ⊠ρ)} β.

The reverse implication that α ≤ ((P)_{q})_{⟨id_{A},id_{A}⟩}(β) when (( E )_{q})_{⟨id_{A},id_{A}⟩}(α) ≤ β follows immediately by reflexivity of ρ.

There is an obvious 1-morphism (J, j): P → (P)_{q} in ED, where J: C^{op} ⟶ R_{P} sends an object A in C to (A, δ_{A}) and a morphism f: A → B to f: (A, δ_{A}) → (B, δ_{B}) since δ_{A} ≤_{A×A} P_{f×f}(δ_{B}), and j_{A}: P (A) → (P)_{q}(A, δ_{A}) is the identity since

(P)_{q}(A, δ_{A}) = Des_{δ_{A}} = P (A).

It is immediate to see that J is full and faithful and that (J, j) is a change of base.

4.3. Remark. Note that an object of the form (A, δ_{A}) in R_{P} is projective with respect to quotients of (P)_{q}-equivalence relation, and that every object in R_{P} is a quotient of a (P)_{q}-equivalence relation on such a projective.

4.4. Lemma. With the notation used above, (P)_{q}: R_{P}^{op} ⟶ InfSL has descent quotients of (P)_{q}-equivalence relations. Moreover, quotients are stable and effective descent, and P -equivalence relations are effective.

Proof. Since the sub-poset Des_{ρ} ⊆ P (A) is closed under finite infima, a (P)_{q}-equivalence relation τ on (A, ρ) is also a P -equivalence relation on A. It is easy to see that id_{A}: (A, ρ) → (A, τ) is a descent quotient since ρ ≤_{A×A} τ—actually, effectively so. It follows immediately that τ is the P -kernel equivalence of the quotient id_{A}: (A, ρ) → (A, τ). To see that it is also stable, suppose

\xymatrix{(B, υ) \ar[r]_{f′} \ar[d]^{g} & (A, ρ) \ar[d]_{_{id_{A}}} \\ (C, σ) \ar[r]^{f} & (A, τ)}

is a pullback in R_{P}. So in the commutative diagram

\xymatrix{(C, δ_{C}) \ar[dr]_{_{id_{C}}} \ar[rr]^{f} & (B, υ) \ar[r]_{f′} \ar[d]^{g} & (A, ρ) \ar[d]_{_{id_{A}}} \\  & (C, σ) \ar[r]^{f} & (A, τ)}

there is a fill-in morphism h: (C, δ_{C}) → (B, υ). It is now easy to see that g: (B, υ) → (C, σ) is a quotient.

We can now prove that there is a left biadjoint to the forgetful 2-functor U: QED → ED.

4.5. Theorem. For every elementary doctrine P: C^{op} ⟶ InfSL, pre-composition with the 1-morphism

[figure: C^{op}; P; J; InfSL; R_{P}^{op}; (P)_{q}; j; ·]

in ED induces an essential equivalence of categories

− ∘ (J, j): QED((P)_{q}, Z) ≡ ED(P, Z)  (2)

for every Z in QED.

Proof. Suppose Z is a doctrine in QED. As to full faithfulness of the functor in (2), consider two pairs (F, b) and (G, c) of 1-morphisms from (P)_{q} to Z. By 4.3, the natural transformation θ: F →^{.} G in a 2-morphism from (F, b) to (G, c) in QED is completely determined by its action on objects in the image of J and (P)_{q}-equivalence relations on these. And, since a quotient q: U → V of an Z-equivalence relation r on U is descent, Z(V) is a full sub-poset of Z(U). Thus essential surjectivity of the functor in (2) follows from 4.3.

Recall that, for an elementary doctrine P: C^{op} ⟶ InfSL, and for an object α in some P (A), a comprehension of α is a morphism {|α|}: X → A in C such that P_{{|α|}}(α) = ⊤_{X} and, for every f: Z → A such that P_{f}(α) = ⊤_{Z} there is a unique morphism g: Z → X such that f = {|α|} ∘ g. Hence a comprehension is necessarily monic.

One says that P has comprehensions if every α has a comprehension, and that P has full comprehensions if, moreover, α ≤ β in P (A) whenever {|α|} factors through {|β|}.

4.6. Lemma. Let P: C^{op} ⟶ InfSLbe an elementary doctrine. If P has comprehensions, then (P)_{q} has comprehensions. Moreover, given a comprehension {|α|}: X → A of α in P (A), the morphism J({|α|}): JX → JA is a comprehension of j_{A}(α) if and only if δ_{X} = P_{{|α|}×{|α|}}(δ_{A}).

Proof. Suppose (A, ρ) is in R_{P} and α in (P)_{q}(A, ρ) = Des_{ρ} ⊆ P (A). Let {|α|}: X → A be a comprehension in C of α as an object of P (A) and consider the object (X, P_{{|α|}×{|α|}}(ρ)) in R_{P}. Clearly {|α|} determines a morphism (X, P_{{|α|}×{|α|}}(ρ)) → (A, ρ) in R_{P}; we intend to show that that morphism is a comprehension of α as an object in (P)_{q}(A, ρ). The following is a trivial computation in Des_{P_{{|α|}×{|α|}}(ρ)} ⊆ P (X):

⊤_{X} = P_{{|α|}}(α) = (P)_{q}_{{|α|}}(α).

Suppose now that f: (Z, σ) → (A, ρ) is such that ⊤_{Z} = (P)_{q}_{f}(α). Since {|α|} is a comprehension in C, there is a unique morphism g: Z → X such that f = {|α|} ∘ g. To conclude, it is enough to show that g determines a morphism (Z, σ) → (X, P_{{|α|}×{|α|}}(ρ)) in R_{P}, but

σ ≤_{Z×Z} P_{f×f}(ρ) = P_{g×g}(P_{{|α|}×{|α|}}(ρ)).

As for the second part of the statement, let α be in P (A) and let {|α|}: X → A be a comprehension of α in C. Suppose, first, that δ_{X} = P_{{|α|}×{|α|}}(δ_{A}), and consider a morphism f: (Z, σ) → (A, δ_{A}) such that ((P)_{q})_{f}(α) = ⊤_{Z}. By definition of (P)_{q}, there is a unique morphism g: Z → X such f = {|α|} ∘ g in C. Thus

σ ≤_{Z×Z} P_{f×f}(δ_{A}) = P_{g×g}P_{{|α|}×{|α|}}(δ_{A}) = P_{g×g}(δ_{X}).

Conversely, suppose {|α|}: (X, δ_{X}) → (A, δ_{A}) in R_{P} is a (necessarily monic) comprehension of α in (P)_{q}. Consider {|α|}: (X, P_{{|α|}×{|α|}}(δ_{A})) → (A, δ_{A}). Since ((P)_{q})_{{|α|}}(α) = P_{{|α|}}(α) = ⊤_{X}, the morphism must factor through {|α|}: (X, δ_{X}) → (A, δ_{A}), necessarily with the identity morphism. Hence the conclusion follows.

4.7. Remark. When P has full comprehensions, the condition δ_{X} = P_{{|α|}×{|α|}}(δ_{A}) is ensured for all A and α.

Recall that the fibration of vertical morphisms on the category G_{P} of points universally adds comprehensions to a given fibration producing an indexed poset in case the given fibration is such, see [Jacobs, 1999]. In our case of interest, for a doctrine P: C^{op} ⟶ InfSL, the indexed poset consists of the base category G_{P} where

an object is a pair (A, α) where A is in C and α is in P (A);

a morphism f: (A, α) → (B, β) is a morphism f: A → B in C such that α ≤ P_{f}(β).

The category G_{P} has products and there is a natural embedding I: C → G_{P} which maps A to (A, ⊤_{A}). The indexed functor extends to (P)_{c}: G_{P}^{op} ⟶ InfSL along I by setting (P)_{c}(A, α) := {γ ∈ P (A) | γ ≤ α}. Moreover, the comprehensions in (P)_{c} are full. As an immediate corollary, we have the following.

4.8. Theorem. There is a left biadjoint to the forgetful 2-functor from the full 2-category of QED on elementary doctrines with comprehensions and descent quotients into the 2category ED of elementary doctrines.

Proof. The left biadjoint sends an elementary doctrine P: C^{op} ⟶ InfSLto the elementary doctrine ((P)_{c})_{q}: R_{(P)c}^{op} ⟶ InfSL.

5. Extensional equality

In [Maietti and Rosolini, 2013a], “extensional” models of constructive theories, presented as doctrines P: C^{op} ⟶ InfSL, were obtained by forcing the equality of morphisms f, g: A → B in the base category C to correspond to the “provable” equality ⊤_{A} = P_{⟨f,g⟩}(δ_{B}) in the fibre P (A). We recall from [Jacobs, 1999] the basic property that supports a stronger notion of equality for the case of an elementary doctrine.

5.1. Proposition. Let P: C^{op} ⟶ InfSL be an elementary doctrine and let A be an object in C. The diagonal ⟨id_{A}, id_{A}⟩: A → A × A is a comprehension if and only if it is the comprehension of δ_{A}.

5.2. Definition. Given an elementary doctrine P: C^{op} ⟶ InfSL we say that it has comprehensive diagonals if every diagonal morphism ⟨id_{A}, id_{A}⟩: A → A × A is a comprehension.

5.3. Remark. In case C has equalizers, one finds that P has comprehensive diagonals in the sense of [Maietti and Rosolini, 2013a].

Let P: C^{op} ⟶ InfSLbe an elementary doctrine for the rest of the section. Consider the category X_{P}, the “extensional collapse” of P:

the objects of X_{P} are the objects of C; a morphism [f] : A → B is an equivalence class of morphisms f: A → B in C such that

δ_{A} ≤_{A×A} P_{f×f}(δ_{B}) in P (A × A) with respect to the equivalence which relates f and

f′ when δ_{A} ≤_{A×A} P_{f×f′}(δ_{B}).

Composition is given by that of C on representatives, and identities are represented by identities of C.

5.4. Lemma. The quotient functor C ⟶ X_{P} preserves finite products.

Proof. Given a product diagram \xymatrix{A & A × B \ar[l]_{^{pr^{1}}} \ar[r]^{^{pr^{2}}} & B} in C, the diagram

\xymatrix{A & A × B \ar[l]_{[^{pr^{1}}]} \ar[r]^{[^{pr^{2}}]} & B}

in X_{P} is clearly a weak product. To check that it is strong, suppose that f, g: X → A × B are such that δ_{X} ≤_{X×X} P_{(pr_{1}f)×(pr_{1}g)}(δ_{A}) and δ_{X} ≤_{X×X} P_{(pr_{2}f)×(pr_{2}g)}(δ_{B}). Recall from 2.3 that

δ_{A×B} = δ_{A} ⊠ δ_{B} = P_{⟨pr_{1},pr_{3}⟩}(δ_{A}) ∧ P_{⟨pr_{2},pr_{4}⟩}(δ_{B})

where pr_{i}, i = 1, 2, 3, 4, are the projections from A × B × A × B. So

P_{f×g}(δ_{A×B}) = P_{(pr_{1}f)×(pr_{1}g)}(δ_{A}) ∧ P_{(pr_{2}f)×(pr_{2}g)}(δ_{B}).

Hence the hypothesis on f and g ensures that δ_{X} ≤_{X×X} P_{f×g}(δ_{A×B}) which yields the conclusion.

The indexed inf-semilattice (P)_{x}: X_{P}^{op} ⟶ InfSL on X_{P} will be given essentially by P itself; the following lemma is instrumental to give the assignment on morphisms using the action of P on morphisms.

5.5. Lemma. With the notation used above, let f, g: A → B be morphisms in C and β an object in P (B). If δ_{A} ≤_{A×A} P_{f×g}(δ_{B}), then P_{f}(β) = P_{g}(β).

Proof. Suppose that δ_{A} ≤_{A×A} P_{f×g}(δ_{B}). Write pr_{1}, pr_{2}: A × A → A for the two projections and, similarly, pr′_{1}, pr′_{2}: B × B → B. By 2.2(b) one has P_{pr}′_{1}(β) ∧ δ_{B} ≤_{B×B} P_{pr}′_{2}(β). Thus

P_{f×g}(P_{pr}′_{1}(β)) ∧ P_{f×g}(δ_{B}) ≤_{A×A} P_{f×g}(P_{pr}′_{2}(β)).

From the hypothesis it follows that

P_{f∘pr_{1}}(β) ∧ δ_{A} ≤_{A×A} P_{g∘pr_{2}}(β).

Taking P_{⟨id_{A},id_{A}⟩} of both sides,

P_{f}(β) = P_{f}(β) ∧ ⊤_{A} = P_{⟨id_{A},id_{A}⟩}(P_{f∘pr_{1}}(β)) ∧ P_{⟨id_{A},id_{A}⟩}(δ_{A}) ≤ P_{⟨id_{A},id_{A}⟩}(P_{g∘pr_{2}}(β)) = P_{g}(β).

The other direction follows by symmetry.

In other words, the elementary doctrine P: C^{op} ⟶ InfSLfactors through the quotient functor K: C^{op} ⟶ X_{P}. That induces a 1-morphism (K, k): P → (P)_{x} in ED, where k_{A} is the identity for A in C.

Consider the full 2-subcategory CED of ED whose objects are elementary doctrines P: C^{op} ⟶ InfSLwith comprehensive diagonals.

The following result is now obvious.

5.6. Lemma. With the notation used above, (P)_{x}: X_{P}^{op} ⟶ InfSLis an elementary doctrine with comprehensive diagonals.

Also the following is easy.

5.7. Theorem. For every elementary doctrine P: C^{op} ⟶ InfSL, pre-composition with the 1-morphism

[figure: C^{op}; P; K; InfSL; X_{P}^{op}; (P)_{x}; k; ·]

in ED induces an essential equivalence of categories

− ∘ (K, k): CED((P)_{x}, Z) ≡ ED(P, Z)  (3)

for every Z in CED.

We can now mention the explicit connection between the two universal constructions we have considered. For that it is useful to prove the following two lemmas.

5.8. Lemma. Let P: C^{op} ⟶ InfSLbe an elementary doctrine. The morphism (K, k): P → (P)_{x} preserves quotients. Therefore, if P has descent quotients of P -equivalence relations, then (P)_{x} has descent quotients of (P)_{x}-equivalence relations.

Proof. It is easy to check that K preserves quotients of P -equivalence relations. Since the k-components of (K, k): P → (P)_{x} are identity functions, a (P)_{x}-equivalence relation τ on A is also a P -equivalence relation in P (A × A).

5.9. Lemma. Let P: C^{op} ⟶ InfSLbe an elementary doctrine. If P has comprehensions, then (P)_{x} has comprehensions. Moreover (K, k): P → (P)_{x} preserves comprehensions, in the sense that if {|α|}: X → A is a comprehension of α in P (A), then K({|α|}): KX → KA is a comprehension of k_{A}(α).

Proof. Since P = (P)_{x}K^{op} and k has identity components, (K, k) preserves comprehensions. The rest follows immediately.

The results of this section, together with 4.5, produce an extension of the quotient completion of [Maietti and Rosolini, 2013a].

5.10. Theorem. There is a left biadjoint to the forgetful 2-functor from the full 2category of QED on elementary doctrines with comprehensions, descent quotients and comprehensive diagonals into the 2-category ED of elementary doctrines.

Proof. The left biadjoint sends an elementary doctrine P: C^{op} ⟶ InfSLto the elementary quotient completion (((P)_{c})_{q})_{x}: X_{((P)c)q}^{op} ⟶ InfSL.

5.11. Corollary. For P: C^{op} ⟶ InfSL an elementary doctrine, the elementary quotient completion \overline{P}: Q_{P}^{op} ⟶ InfSL in [Maietti and Rosolini, 2013a] coincides with the doctrine ((P)_{q})_{x}: X_{(P)q}^{op} ⟶ InfSL.

5.12. Remark. Because of the logical setup in [Maietti and Rosolini, 2013a], only a particular case of 5.10 was proved, namely the left biadjoint was restricted to the full sub-2-category of ED of elementary doctrines with full comprehensions and comprehensive diagonals, see 5.3. On those doctrines P: C^{op} ⟶ InfSL, the action of the left biadjoint was simply ((P)_{q})_{x}: X_{(P)q}^{op} ⟶ InfSL.

6. Comparing some universal constructions

The elementary quotient completion resembles very closely that of exact completion. In fact, one has the following results.

6.1. Theorem. Given a category S with finite products and weak pullbacks, let Ψ: S^{op} ⟶ InfSLbe the elementary doctrine of weak subobjects. Then the doctrine ((Ψ)_{q})_{x}: X_{(Ψ)q}^{op} ⟶ InfSL, is equivalent to the doctrine S: S_{ex}^{op} ⟶ InfSLof subobjects on the exact completion S_{ex} of S.

Proof. It follows from 4.3 and the characterization of the embedding of S into S_{ex} in [Carboni and Vitale, 1998].

Though an elementary quotient completion with full comprehension is regular, see [Maietti and Rosolini, 2013a], the regular completion is an instance of a completion of a doctrine which is radically different from the elementary quotient completion in 5.10.

6.2. Remark. For an elementary doctrine P: C^{op} ⟶ InfSL, a weak comprehension of α is a morphism {|α|}: X → A in C such that ⊤_{X} ≤ P_{{|α|}}(α) and, for every morphism g: Y → A such that ⊤_{Y} ≤ P_{g}(α) there is a (not necessarily unique) h: Y → X such that g = {|α|} ∘ h, see [Maietti and Rosolini, 2013a].

For an elementary doctrine P: C^{op} ⟶ InfSLwith weak comprehensions, it is possible to add (strong) comprehensions to its extensional collapse as formal retracts of weak comprehensions: consider the category D_{P} determined by the following data objects of D_{P} are triples (A, α, c) such that A is an object in C, α is an object in P (A),

and c: X → A is a weak comprehension α;

a morphism [f] : (A, α, c) → (B, β, d) is an equivalence class of morphisms f: X → Y in C such that P_{c×c}(δ_{A}) ≤ P_{f×f}(P_{d×d}(δ_{B})) with respect to the relation f ∼ f′

determined by P_{c×c}(δ_{A}) ≤ P_{f×f′}(P_{d×d}(δ_{B}));

composition of [f] : (A, α, c) → (B, β, d) and [g] : (B, β, d) → (C, γ, e) is [g ∘ f].

There is a full functor K: C → D_{P} defined on objects A as K(A) := (A, ⊤_{A}, id_{A})—it factors through X_{P}. It preserves products and there is an extension (P)_{r}: D_{P}^{op} ⟶ InfSL of P: C^{op} ⟶ InfSL defined on objects as (P)_{r}(A, α, c) := Des_{(P_{c×c}(δ_{A}))}. The doctrine (P)_{r}: D_{P}^{op} ⟶ InfSL is elementary with comprehensions and K preserves all existing comprehensions.

Given a category S with finite products and weak pullbacks, let Ψ: S^{op} ⟶ InfSLbe the elementary doctrine of weak subobjects. Then the doctrine (Ψ)_{r}: D_{Ψ}^{op} ⟶ InfSLis equivalent to the doctrine S: S_{reg}^{op} ⟶ InfSL of subobjects on the regular completion S_{reg} of S.

The proof is similar to that of 6.1 since, in the regular completion S_{reg} of S, every object is covered by a regular projective and a subobject of a regular projective, see [Carboni and Vitale, 1998].

Since the construction given in 6.1 factors through that in 6.2 via the exact completion of a regular category, see [Freyd and Scedrov, 1991], and the exact completion of a weakly finitely complete category may appear very similar to the category X_{((P)q)x}, it is appropriate to mention an example of an elementary quotient completion which is not exact.

For that, consider the indexed poset on the monoid of partial recursive functions F: N^{op} ⟶ InfSL whose value on the single object of N is the powerset of the natural numbers and, for any φ partial recursive function, F_{φ} := φ^{−1}, the inverse image of a subset along the partial function. It is clearly an elementary doctrine, and the doctrine ((F)_{c})_{x}: X_{(F)c}^{op} ⟶ InfSL is equivalent to the subobject doctrine S: PR^{op} ⟶ InfSL on the category PR of subsets of natural numbers and (restrictions of) partial recursive functions between them, see [Carboni, 1995] for properties of that category, in particular its exact completion (as a weakly finitely complete category) is the category D of discrete objects of the effective topos.

Now, if one considers the elementary doctrine ((S)_{q})_{x}: X_{(S)q}^{op} ⟶ InfSL, the category X_{(S)q} is equivalent to the category PER of partial equivalence relations on the natural numbers, and the indexed poset ((S)_{q})_{x} is equivalent to that of subobjects on that category. The category PER is not exact because there are equivalence relations which are not kernel equivalences. In fact, the exact completion PER_{ex/reg} of PER as a regular category is the category D of discrete objects.

Similar examples can be produced using topological categories such as those in the papers [Birkedal et al., 1998; Carboni and Rosolini, 2000]. Other examples of elementary quotient completions that are not exact are given in the paper [Maietti and Rosolini, 2013a]: one is applied to the doctrine of the Calculus of Constructions [Coquand, 1990; Streicher, 1992] and the other to the doctrine of the intensional level of the minimalist foundation in [Maietti, 2009].

References

[Birkedal et al., 1998] Birkedal, L., Carboni, A., Rosolini, G., and Scott, D. (1998). Type theory via exact categories. In Pratt, V., editor, Proc. 13th Symposium in Logic in Computer Science, pages 188–198, Indianapolis. I.E.E.E. Computer Society.

[Carboni, 1982] Carboni, A. (1982). Analysis non-standard e topos. Rend. Istit. Mat. Univ. Trieste, 14(1-2):1–16.

[Carboni, 1995] Carboni, A. (1995). Some free constructions in realizability and proof theory. J. Pure Appl. Algebra, 103:117–148.

[Carboni and Celia Magno, 1982] Carboni, A. and Celia Magno, R. (1982). The free exact category on a left exact one. J. Aust. Math. Soc., 33(A):295–301.

[Carboni and Rosolini, 2000] Carboni, A. and Rosolini, G. (2000). Locally cartesian closed exact completions. J. Pure Appl. Algebra, 154:103–116.

[Carboni and Vitale, 1998] Carboni, A. and Vitale, E. (1998). Regular and exact completions. J. Pure Appl. Algebra, 125:79–117.

[Coquand, 1990] Coquand, T. (1990). Metamathematical investigation of a calculus of constructions. In Odifreddi, P., editor, Logic in Computer Science, pages 91–122. Academic Press.

[Coquand and Paulin-Mohring, 1990] Coquand, T. and Paulin-Mohring, C. (1990). Inductively defined types. In Martin-Löf, P. and Mints, G., editors, Proceedings of the International Conference on Computer Logic (Colog ’88), volume 417 of Lecture Notes in Computer Science, pages 50–66, Berlin, Germany. Springer.

[Freyd and Scedrov, 1991] Freyd, P. and Scedrov, A. (1991). Categories Allegories. North Holland Publishing Company.

[Grandis, 2000] Grandis, M. (2000). Weak subobjects and the epi-monic completion of a category. J. Pure Appl. Algebra, 154(1-3):193–212.

[Hyland et al., 1990] Hyland, J. M. E., Robinson, E. P., and Rosolini, G. (1990). The discrete objects in the effective topos. Proc. Lond. Math. Soc., 60:1–36.

[Jacobs, 1999] Jacobs, B. (1999). Categorical Logic and Type Theory. North Holland Publishing Company.

[Janelidze et al., 2004] Janelidze, G., Sobral, M., and Tholen, W. (2004). Beyond Barr exactness: effective descent morphisms. In Categorical foundations, volume 97 of Encyclopedia Math. Appl., pages 359–405. Cambridge University Press, Cambridge.

[Janelidze and Tholen, 1994] Janelidze, G. and Tholen, W. (1994). Facets of descent. I. Appl. Categ. Structures, 2(3):245–281.

[Janelidze and Tholen, 1997] Janelidze, G. and Tholen, W. (1997). Facets of descent. II. Appl. Categ. Structures, 5(3):229–248.

[Joyal and Moerdijk, 1995] Joyal, A. and Moerdijk, I. (1995). Algebraic Set Theory, volume 220 of London Math. Soc. Lecture Note Ser. Cambridge University Press.

[Lambek and Scott, 1986] Lambek, J. and Scott, P. (1986). Introduction to Higher Order Categorical Logic. Cambridge University Press.

[Lawvere, 1969a] Lawvere, F. W. (1969a). Adjointness in foundations. Dialectica, 23:281– 296.

[Lawvere, 1969b] Lawvere, F. W. (1969b). Diagonal arguments and cartesian closed categories. In Category Theory, Homology Theory and their Applications, II (Battelle Institute Conference, Seattle, Wash., 1968, Vol. Two), pages 134–145. Springer.

[Lawvere, 1970] Lawvere, F. W. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Heller, A., editor, Proc. New York Symposium on Application of Categorical Algebra, pages 1–14. Amer.Math.Soc.

[Lawvere and Rosebrugh, 2003] Lawvere, F. W. and Rosebrugh, R. (2003). Sets for Mathematics. Cambridge University Press.

[Maietti, 2009] Maietti, M. (2009). A minimalist two-level foundation for constructive mathematics. Ann. Pure Appl. Logic, 160(3):319–354.

[Maietti and Rosolini, 2013a] Maietti, M. and Rosolini, G. (2013a). Quotient completion for the foundation of constructive mathematics. To appear in Log. Univers.

[Maietti and Rosolini, 2013b] Maietti, M. and Rosolini, G. (2013b). Unifying exact completions. To appear in Appl. Categ. Structures.

[Maietti and Sambin, 2005] Maietti, M. and Sambin, G. (2005). Toward a minimalist foundation for constructive mathematics. In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91–114. Oxford University Press.

[Makkai and Reyes, 1977] Makkai, M. and Reyes, G. (1977). First Order Categorical Logic, volume 611 of Lecture Notes in Math. Springer-Verlag.

[Nordström et al., 1990] Nordström, B., Petersson, K., and Smith, J. (1990). Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford.

[Pasquali, 2013] Pasquali, F. (2013). A co-free construction for elementary doctrines. To appear in Appl. Categ. Structures.

[Streicher, 1992] Streicher, T. (1992). Independence of the induction principle and the axiom of choice in the pure calculus of constructions. Theoret. Comput. Sci., 103(2):395– 408.

[Taylor, 1999] Taylor, P. (1999). Practical Foundations of Mathematics. Cambridge University Press.

[van Oosten, 2008] van Oosten, J. (2008). Realizability: An Introduction to its Categorical Side, volume 152. North Holland Publishing Company.

Dipartimento di Matematica Pura ed Applicata, Università degli Studi di Padova via Trieste 63, 35121 Padova, Italy

Dipartimento di Matematica, Università degli Studi di Genova via Dodecaneso 35, 16146 Genova, Italy

Email: maietti@math.unipd.it
      rosolini@unige.it

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/27/17/27-17.{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 Edinburgh: Tom.Leinster@ed.ac.uk Ieke Moerdijk, Radboud University Nijmegen: i.moerdijk@math.ru.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