Theory and Applications of Categories, Vol. 24, No. 3, 2010, pp. 39–83.

JOYAL’S ARITHMETIC UNIVERSE AS LIST-ARITHMETIC PRETOPOS

MARIA EMILIA MAIETTI

Abstract. We explain in detail why the notion of list-arithmetic pretopos should be taken as the general categorical definition for the construction of arithmetic universes introduced by André Joyal to give a categorical proof of Gödel’s incompleteness results. We motivate this definition for three reasons: first, Joyal’s arithmetic universes are listarithmetic pretopoi; second, the initial arithmetic universe among Joyal’s constructions is equivalent to the initial list-arithmetic pretopos; third, any list-arithmetic pretopos enjoys the existence of free internal categories and diagrams as required to prove Gödel’s incompleteness. In doing our proofs we make an extensive use of the internal type theory of the categorical structures involved in Joyal’s constructions. The definition of list-arithmetic pretopos is equivalent to the general one that I came to know in a recent talk by André Joyal.

1. Introduction

The categories of topoi and pretopoi can be viewed as universes of abstract sets in which to develop mathematics (see [LR03, Joh77, JM95, MM92, Hyl82]). Joyal’s arithmetic universes provide further examples of such universes.

André Joyal introduced arithmetic universes in some lectures given in the seventies, all still unpublished, to provide a categorical proof of Gödel’s incompleteness theorems. He defined arithmetic universes by giving a general construction of examples including the free initial one. He then intended to prove incompleteness by mimicking the diagonal argument of Cantor’s theorem within the initial arithmetic universe [Joy05]. Indeed, the initial arithmetic universe supports the amount of self-reference needed to perform the mentioned argument because it contains an internal copy of itself.

At that time it was not clear what to take as the most general categorical structure behind the construction of arithmetic universes by Joyal. It was only clear that the desired categorical structure should support the construction of free internal categories and diagrams generated from graphs. In [Mor96, Wra85, Tay05] it is more or less said that the general definition of an arithmetic universe should be a pretopos with free internal categories and diagrams. Here we propose the notion of list-arithmetic pretopos as the general notion of arithmetic universe, as first announced in [Mai03] and used in [Mai05b].

Received by the editors 2009-06-15 and, in revised form, 2010-02-16.

Transmitted by Martin Hyland. Published on 2010-02-20.

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

Key words and phrases: Pretopoi, dependent type theory, categorical logic.

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

We think that our proposal is justified by the following reasons:

1) all the examples of arithmetic universe built by Joyal are list-arithmetic pretopoi;

2) the construction of the initial arithmetic universe by Joyal is equivalent to the initial list-arithmetic pretopos;

3) list-arithmetic pretopoi enjoy free internal categories and diagrams as Joyal proved for any of his arithmetic universes.

In order to prove 1) and 2) we briefly describe how Joyal built his arithmetic universes. An arithmetic universe à la Joyal is a category of the form (Pred(S))_{ex} built in 3 steps

as follows:

• take a Skolem theory S, namely a cartesian category with a parameterized natural numbers object where all the objects are finite products of the natural numbers object;

• take the category Pred(S) of predicates in S, which gives a regular category;

• make its exact completion (Pred(S))_{ex} on a regular category (see [CV98]).

Now, given that the category of predicates Pred(S) is not only regular but also enjoys stable finite disjoint coproducts and parameterized list objects, as shown by Joyal and in [Rol76, Mor96, Wra85], then its exact completion (Pred(S))_{ex} inherits stable finite disjoint coproducts and parameterized list objects, and hence it turns out to be a list-arithmetic pretopos, namely fact 1) holds.

To prove fact 2), we first observe that the category of predicates of the initial Skolem theory S_{in} is equivalent to the initial regular locos. From this we derive that the initial arithmetic universe, which is (Pred(S_{in}))_{ex} built on the initial Skolem theory, is equivalent to the initial list-arithmetic pretopos.

Finally, to prove fact 3), namely that free internal categories and diagrams exist in any list-arithmetic pretopos, we employ list objects. In particular, to prove the universal properties of the free constructions we build the needed morphisms by iteration on natural numbers.

It is worth mentioning that, when proving fact 2) above, we notice that the category of predicates of the initial Skolem category is also equivalent to the construction of the initial arithmetic lextensive category. This implies that the initial arithmetic universe is also equivalent to the construction of the initial pretopos with a parameterized natural numbers object. All this says that the notion of pretopos with a parameterized natural numbers object, called arithmetic pretopos, surely satisfies corresponding facts 1) and 2). But we are not able to prove the corresponding fact 3), namely that any arithmetic pretopos supports free internal categories and diagrams or it is list-arithmetic. We leave this as an open problem.

In showing our results we employ internal languages of the categorical structures involved and these are taken from [Mai05a]. Also in [Rol76] and in [Mor96, Wra85] a term language is presented to reason within a Skolem theory and to build the category of predicates on it.

Here we reason within all the three stages of Joyal’s constructions by adopting internal languages that are defined in a modular way as dependent type theories in the style of Martin-Löf’s extensional type theory in [Mar84]. These languages are obtained by combining type constructors corresponding to properties defining the various categorical structures thanks to the modular correspondence between them described in [Mai05a].

Finally, we want to remark that the notion of list-arithmetic pretopos as a general definition of arithmetic universe is equivalent to the one that I came to know in a recent talk [Joy05] by André Joyal as a pretopos with free monoid actions (the notion of free monoid actions can be found in [Rol76]).

2. The definition of list-arithmetic pretopos and related categorical structures

Here we recall the definition of list-arithmetic pretopos and of some weaker categorical structures that we will use in the next. We also remind readers of a key preservation property that such structures have in order to enjoy an internal language as a dependent type theory according to [Mai05a].

Note that when we speak of functor preserving some categorical structure we mean preservation up to isomorphism.

Among the basic concepts to build an arithmetic universe there are the notions of Skolem category and Skolem theory. A Skolem category is equipped with the minimum structure needed to interpret primitive recursion on natural numbers. We start by reminding the notion of parameterized natural numbers object:

2.1. Definition. A parameterized natural numbers object in a category with finite products (i.e. a category with terminal object 1 and binary products) is an object N together with maps 0 : 1 → N , s : N → N such that for every b : B → Y and g : Y → Y there is a unique rec(b, g) making the following diagrams commute

\xymatrix{B \ar[r]^{⟨id,0·!_{B}⟩} \ar[dr]_{b} & B × N \ar[d]^{rec(b,g)} & B × N \ar[l]_{id×s} \ar[d]^{rec(b,g)} \\  & Y & Y \ar[l]^{g}}

with !_{B} : B → 1 the unique map towards the terminal object.

It is worth recalling here that in the presence of function spaces, as in a cartesian closed category, this parameterized version of natural numbers object is equivalent to the usual natural numbers object [Joh02a].

2.2. Definition. A Skolem category is a category with finite products and a parameterized natural numbers object.

A Skolem theory is a Skolem category whose objects are finite products of the natural numbers object.

Next, we consider more complex categorical structures that enables one to interpret primitive recursion:

2.3. Definition. A lextensive category is a finitely complete category, that is a category with a terminal object and pullbacks, equipped with stable finite disjoint coproducts [CLW93].

If a lextensive category has a parameterized natural numbers object it is said to be arithmetic lextensive.

2.4. Definition. A finitely complete category U has parameterized list objects if for any object A ∈ Ob U, there is an object List(A) with morphisms r_{o}^{A} : 1 → List(A) and r_{1}^{A} : List(A) × A → List(A) such that for every b : B → Y and g : Y × A → Y there is a unique rec(b, g) making the following diagrams commute

\xymatrix{B \ar[r]^{⟨id,r_{o}^{A}·!_{B}⟩} \ar[dr]_{b} & B × List(A) \ar[d]^{rec(b,g)} & B × (List(A) × A) \ar[l]_{id×r_{1}^{A}} \ar[d]^{(rec(b,g)×id_{A})·σ} \\  & Y & Y × A \ar[l]^{g}}

where σ : B × (List(A) × A) → (B × List(A)) × A is the associative isomorphism defined in detail as ⟨⟨π_{1}, π_{1} · π_{2}⟩, π_{2} · π_{2}⟩.

In [Coc90] there is an equivalent definition of parameterized list objects in terms of recursive objects and preservation of recursive objects by the pullback functor !_{D}^{∗} : U → U/D sending an object B to π_{1} : D × B → D.

2.5. Definition. A locos is a lextensive category with parameterized list objects. If a locos is also a regular category it is called a regular locos.

Finally, we recall the categorical definition of pretopos [MR77], [JM95].

2.6. Definition. A pretopos is a category equipped with finite limits, stable finite disjoint coproducts and stable effective quotients of monic equivalence relations.

If a pretopos has a parameterized natural numbers object it is said to be an arithmetic pretopos.

If a pretopos has parameterized list objects it is called a list-arithmetic pretopos.

Note that a list-arithmetic pretopos is an arithmetic pretopos since the parameterized list object of the terminal object gives a parameterized natural numbers object.

An important property that all these categorical structures enjoy is that their structure is local.

We say that a structure on a finitely complete category U is local when it satisfies the following:

1) If U has the considered structure then so does the slice category U/A for every object A ∈ Ob U.

2) for every morphism f : A → B in U the pullback functor f^{∗} : U/B → U/A preserves the considered structure of the corresponding slice categories.

We recall that all the above mentioned categorical structures are local (see [Mai05a] for a proof):

2.7. Proposition. The structural properties of being

• arithmetic lextensive

• a regular locos

• an arithmetic pretopos

• a list-arithmetic pretopos

are all local.

The property of being local for a categorical structure is a prerequisite in order to enjoy an internal dependent type theory as described in [Mai05a]. In particular property 1) of a local structure is needed to model types with dependencies. Indeed a dependent type is modelled in a slice category and hence any slice category has to be equipped with all the structure of the starting category. Instead property 2) is needed to make valid the interpretation of substitution via pullback. Indeed, given that substitution of terms both in types and in terms is interpreted via a functor isomorphic to the pullback pseudofunctor, then all the structure used to interpret types and terms has to be preserved under the interpretation of substitution, and hence under pullbacks.

3. An internal language for list-arithmetic pretopoi and related structures

Here we describe internal languages of the categorical structures presented in the previous section in terms of a dependent type theory in the style of Martin-Löf’s extensional type theory in [Mar84].

What is an internal language? When we say that a calculus T provides an internal language of some categorical structures we mean not only that T is valid and complete with respect to the considered categorical structures, but also that the category of the theories associated to T is in a sort of equivalence with the category of the considered categorical structures. Usually such an equivalence is shown on one hand by mapping a category to its internal language, which is obtained by augmenting T with some specific axioms, and on the other hand by mapping a theory of T to the syntactic category built out of the theory (the one built to prove completeness!). For more details and examples see [Mai05a].

The fact that the described correspondence gives rise to a sort of equivalence means in particular that any categorical structure is equivalent to the syntactic category built out of its internal language. Therefore, we can perform categorical constructions inside any categorical structure by using its internal language.

Note that the link between a typed calculus and a class of categorical structures in terms of the internal language theorem is much stronger than the link established by a soundness and completeness theorem. Indeed, a simple validity and completeness theorem between a calculus and a class of categorical structures does not generally guarantee that the calculus provides the internal language of the considered categories (for an example of this see [MMdPR05]).

Modular correspondence type constructors/categorical properties. In order to single out the dependent typed theories of the categorical structures mentioned in the previous section we will make use of the modular correspondence between type constructors and categorical properties described in [Mai05a]. We just recall here the correspondence for the categorical properties of our interest:

Type constructors  Categorical properties
terminal type  finite limits

+ indexed sum types

+ extensional equality types

quotient types on  stable images

the total equivalence relation

quotient types on  stable quotients on
mono equivalence relations  monic equivalence relations
+ effectiveness axiom  + effectiveness of quotients
false type  stable initial object
+ disjoint sum types  stable binary coproducts
+ disjointness axiom  + disjointness of coproducts
natural numbers type  parameterized natural numbers object
list types  parameterized list objects

We also recall that, to interpret the above type constructors in a finitely complete category with the corresponding categorical properties, in [Mai05a] we made use of a split fibration associated to the codomain one following [Hof95]. This makes the original naive interpretation in [See84] (see also [Joh02b]) correct when interpreting substitution.

3.1. The typed calculus for list-arithmetic pretopoi. Now we describe in detail the rules of the dependent typed calculus that provides an internal language for listarithmetic pretopoi (it was first introduced in [Mai99b] and reported in [Mai03, Mai05a]). We call such a calculus T_{au} because we will identify the general notion of arithmetic universe with that of list-arithmetic pretopos. Moreover, we will use the pure calculus T_{au} to build the initial list-arithmetic pretopos that will be shown to be equivalent to the initial arithmetic universe among Joyal’s constructions.

The calculus T_{au} is equipped with types, which should be thought of as sets or data types, and with typed terms which represent elements of the types to which they belong. In addition types may depend on typed terms. Hence, dependent types should be better thought of set families.

In the style of Martin-Löf’s type theory, we have four kinds of judgements [NPS90]:

A type [Γ] A = B [Γ] a ∈ A [Γ] a = b ∈ A [Γ]

that is the type judgement, the equality between types, the term judgement and the equality between terms of the same type. The contexts Γ of these judgements are telescopic [dB91], since types are allowed to depend on variables of other types. The contexts are generated by the following rules

1C) ∅ cont 2C) \frac{Γ cont A type [Γ]}{Γ, x ∈ A cont} (x ∈ A ∉ Γ)

plus the rules of equality between contexts [Str91], [Pit00].

In the following, we present the inference rules to construct type judgements and term judgements with their equality judgements by recursion. One should also add all the inference rules that express reflexivity, symmetry and transitivity of the equality between types and terms together with the type equality rules conv) and conv-eq) and the assumption of variables:

{a ∈ A [Γ] A = B [Γ] \atop a ∈ B [Γ]} conv) {a = b ∈ A [Γ] A = B [Γ] \atop a = b ∈ B [Γ]} conv-eq)

Γ, x ∈ A, Δ cont

x ∈ A [Γ, x ∈ A, Δ] var)

We can derive then the structural rules of weakening and of a suitable exchange.

In the following we give the formation rules for types specific to T_{au} with the corresponding introduction, elimination and conversion rules of their terms. But we omit the equality rules expressing that all the type and term constructors preserve equality as in [Mar84] and that are necessary to derive the substitution rules. Moreover, we adopt the usual definitions of bound and free occurrences of variables and we identify two terms under α-conversion. Note that the context common to all judgements involved in a rule will be omitted. The typed variable appearing in a context is meant to be added to the implicit context as the last one.

The rules to generate T_{au}’s types and terms are all present in the extensional version of Martin-Löf’s type theory [Mar84] except for the disjointness axiom, the rules about quotients types restricted to mono equivalence relations and the effectiveness axiom.

Supposing A type and R(x, y) type [x, y ∈ A], we will write Equiv(R) to mean the following three judgements:

refl(x) ∈ R(x, x) [x ∈ A]
sym(x, y, z) ∈ R(y, x) [x ∈ A, y ∈ A, z ∈ R(x, y)]
trans(x, y, z, u, v) ∈ R(x, z) [x ∈ A, y ∈ A, z ∈ A, u ∈ R(x, y), v ∈ R(y, z)]

Moreover, we will write Mono(R) to mean

z = w ∈ R(x, y) [x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)]

The T^{au} dependent typed calculus

Terminal type

Tr) ⊤ type  I-Tr) ⋆ ∈ ⊤  C-Tr) \frac{t ∈ ⊤}{t = ⋆ ∈ ⊤}

False type

Indexed Sum type

Σ) \frac{C(x) type [x ∈ B]}{Σ_{x∈B}C(x) type} I-Σ) \frac{b ∈ B c ∈ C(b) Σ_{x∈B}C(x) type}{⟨b, c⟩ ∈ Σ_{x∈B}C(x)}

E-Σ) \frac{d ∈ Σ_{x∈B}C(x) m(x, y) ∈ M(⟨x, y⟩) [x ∈ B, y ∈ C(x)]}{El_{Σ}(d, m) ∈ M(d)}

C-Σ) \frac{b ∈ B c ∈ C(b) m(x, y) ∈ M(⟨x, y⟩) [x ∈ B, y ∈ C(x)]}{El_{Σ}(⟨b, c⟩, m) = m(b, c) ∈ M(⟨b, c⟩)}

Eq) \frac{C type c ∈ C d ∈ C}{Eq(C, c, d) type}  I-Eq) \frac{c ∈ C}{eq ∈ Eq(C, c, c)}
E-Eq) \frac{p ∈ Eq(C, c, d)}{c = d ∈ C}  C-Eq) \frac{p ∈ Eq(C, c, d)}{p = eq ∈ Eq(C, c, d)}

Fs) ⊥ type E-Fs) \frac{a ∈ ⊥ B type}{r_{⊥}(a) ∈ B} Equality type Disjoint Sum type

+) \frac{B type C type}{B + C type} I_{1}-+) \frac{b ∈ B B + C type}{inl(b) ∈ B + C} I_{2}-+) \frac{c ∈ C B + C type}{inr(c) ∈ B + C}

JOYAL’S ARITHMETIC UNIVERSE AS LIST-ARITHMETIC PRETOPOS  47

E-+) \frac{\begin{matrix}A(z) [z ∈ B + C] \\ w ∈ B + C a_{B}(x) ∈ A(inl(x)) [x ∈ B] a_{C}(y) ∈ A(inr(y)) [y ∈ C] \end{matrix}}{El_{+}(w, a_{B}, a_{C}) ∈ A(w)}

C_{1}-+) \frac{\begin{matrix}A(z) [z ∈ B + C] \\ b ∈ B a_{B}(x) ∈ A(inl(x)) [x ∈ B] a_{C}(y) ∈ A(inr(y)) [y ∈ C] \end{matrix}}{El_{+}(inl(b), a_{B}, a_{C}) = a_{B}(b) ∈ A(inl(b))}

C_{2}-+) \frac{\begin{matrix}A(z) [z ∈ B + C] \\ c ∈ C a_{B}(x) ∈ A(inl(x)) [x ∈ B] a_{C}(y) ∈ A(inr(y)) [y ∈ C] \end{matrix}}{El_{+}(inr(c), a_{B}, a_{C}) = a_{C}(c) ∈ A(inr(c))}

Disjointness

dis-+) \frac{b ∈ B c ∈ C inl(b) = inr(c) ∈ B + C}{dsj(b, c) ∈ ⊥}

Quotient type

Q) \frac{R(x, y) type [x ∈ A, y ∈ A] Mono(R) Equiv(R)}{A/R type}

I-Q) \frac{a ∈ A A/R type}{[a] ∈ A/R} eq-Q) \frac{a ∈ A b ∈ A d ∈ R(a, b) A/R type}{[a] = [b] ∈ A/R}

E-Q) \frac{\begin{matrix}L(z) [z ∈ A/R] \\ p ∈ A/R l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A, d ∈ R(x, y)] \end{matrix}}{El_{Q}(l, p) ∈ L(p)}

C-Q) \frac{\begin{matrix}L(z) [z ∈ A/R] \\ a ∈ A l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A, d ∈ R(x, y)] \end{matrix}}{El_{Q}(l, [a]) = l(a) ∈ L([a])}

Effectiveness

\frac{a ∈ A b ∈ A [a] = [b] ∈ A/R}{eff(a, b) ∈ R(a, b)}

List type

list) \frac{C type}{List(C) type}  I_{1}-list) \frac{List(C) type}{ϵ ∈ List(C)}  I_{2}-list) \frac{s ∈ List(C) c ∈ C}{cons(s, c) ∈ List(C)}

E-list) \frac{L(z) [z ∈ List(C)] s ∈ List(C) a ∈ L(ϵ) l(x, y, z) ∈ L(cons(x, y)) [x ∈ List(C), y ∈ C, z ∈ L(x)]}{El_{List}(a, l, s) ∈ L(s)}

C_{1}-list) \frac{L(z) [z ∈ List(C)] a ∈ L(ϵ) l(x, y, z) ∈ L(cons(x, y)) [x ∈ List(C), y ∈ C, z ∈ L(x)]}{El_{List}(a, l, ϵ) = a ∈ L(ϵ)}

C_{2}-list) \frac{L(z) [z ∈ List(C)] s ∈ List(C) c ∈ C a ∈ L(ϵ) l(x, y, z) ∈ L(cons(x, y)) [x ∈ List(C), y ∈ C, z ∈ L(x)]}{El_{List}(a, l, cons(s, c)) = l(s, c, El_{List}(a, l, s)) ∈ L(cons(s, c))}

Note that we can represent the type of natural numbers N as lists of the terminal type since this represents a chosen singleton. Therefore, we define N ≡ List(⊤) with 0 ≡ ϵ and successor s(n) ≡ cons(n, ∗) for n ∈ List(⊤).

3.2. Remark. Note also that the elimination rule of the Indexed Sum type can be equivalently replaced by the following projections

\frac{d ∈ Σ_{x∈B}C(x)}{π_{1}(d) ∈ B} E_{1}-Σ  \frac{d ∈ Σ_{x∈B}C(x)}{π_{2}(d) ∈ C(π_{1}(d))} E_{2}-Σ

and corresponding β and η conversion rules

{b ∈ B c ∈ C(b) \atop π_{1}(⟨b, c⟩) = b ∈ B} β_{1} C-Σ  {b ∈ B c ∈ C(b) \atop π_{2}(⟨b, c⟩) = c ∈ C(b)} β_{2} C-Σ
{d ∈ Σ_{x∈B}C(x) \atop ⟨π_{1}(d), π_{2}(d)⟩ = d ∈ Σ_{x∈B}C(x)} η C-Σ

3.3. Remark. [Notation on lists] Given s, s′ ∈ List(A) we abbreviate

⌊s, s′⌋ for Rec(s, cons, s′) ∈ List(A)

which is the operation appending a list to another one.

Moreover, for s ∈ List(A) and a ∈ A we will write

⌊s, a⌋ for cons(s, a)  and  ⌊a⌋ for cons(ϵ, a)

Mono types and quotients. In [Mai05a] we introduced the notion of mono type, namely a type B [Γ] for which

w = z ∈ B [Γ, w ∈ B, z ∈ B]

is derivable. Since the interpretation of a mono type as given in [Mai05a] turns out to be a monomorphism, we can then represent the quotient of a monic equivalence relation in the internal language of a pretopos as the quotient type of a mono equivalence relation. Then, effectiveness of quotients is represented by adding a specific axiom. Note that the fact that effectiveness holds for mono equivalence relations is crucial. Indeed effectiveness of quotients on generic relations may lead to classical logic [Mai99a].

Finally we anticipate here that in T_{au} we can define quotients on arbitrary relations that are not necessarily equivalences. Categorically this corresponds to the fact that in any list-arithmetic pretopos arbitrary coequalizers exist (see next section).

Coproducts. Coproducts are represented by disjoint sums as in [Mar84] and to represent disjointness we need to add a specific axiom. Indeed, disjointness is not generally derivable by using the same argument in [Smi88] for Peano’s fourth axiom.

Coherent logic in a pretopos. Mono types in T_{au} inherit enough structure to validate coherent logic by interpreting falsum, equality, conjunction, disjunction and existential quantification on a type as follows: for ϕ, ψ mono types

Interpretation of connectives

falsum ≡ ⊥  s =_{A} t ≡ Eq(A, s, t)
ϕ ∧ ψ ≡ ϕ × ψ  ϕ ∨ ψ ≡ (ϕ ⊕ ψ)/⊤

∃_{x∈A}ϕ(x) ≡ (Σ_{x∈A}ϕ(x))/⊤

Thanks to the way connectives are interpreted, they inherit elimination rules that are stronger than the usual ones in intuitionistic logic (see the discussion on the calculus of regular categories on page 22 in [Mai05a]).

Now we describe the internal languages of the categorical structures defined in section 2 and weaker than that of list-arithmetic pretopos. These can be deduced from the table previously described.

The typed calculus of Skolem categories T_{sk}. The calculus T_{sk} is a type theory with no dependent types including the following type constructors: terminal type, product types and the natural numbers type with the rules of List(⊤) in T_{au} restricted to nondependent types that is:

Product type

\frac{B type C type}{B × C type} ×) \frac{b ∈ B c ∈ C}{⟨b, c⟩ ∈ B × C} I-×)

\frac{d ∈ B × C}{π_{1}(d) ∈ B} E_{1}-×) \frac{d ∈ B × C}{π_{2}(d) ∈ C} E_{2}-×)

\frac{b ∈ B c ∈ C}{π_{1}(⟨b, c⟩) = b ∈ B} C_{1}-Σ) \frac{b ∈ B c ∈ C}{π_{2}(⟨b, c⟩) = c ∈ C} C_{2}-×)

\frac{d ∈ B × C}{⟨π_{1}(d), π_{2}(d)⟩ = d ∈ B × C} η-×)

N type nat  ^{0 ∈ N I_{1}-nat}  ^{{n ∈ N \atop s(n) ∈ N} I_{2}-nat}

Natural Numbers type

\begin{matrix}L type \\ n ∈ N a ∈ L l(y) ∈ L [y ∈ L] \end{matrix} ; El_{N}(a, l, n) ∈ L E-nat

\begin{matrix}L type \\ a ∈ L l(y) ∈ L [y ∈ L] \end{matrix} ; El_{N}(a, l, 0) = a ∈ L C_{1}-nat  ^{\begin{matrix}L type \\ n ∈ N a ∈ L l(y) ∈ L [y ∈ L] \end{matrix} El_{N}(a, l, s(n)) = l(El_{N}(a, l, n)) ∈ L C_{2}-nat}

The typed calculus of arithmetic lextensive categories T_{alxt}. The calculus T_{alxt} includes the following type constructors: terminal type, indexed sum types, extensional equality types, false type, disjoint sum types, disjointness axiom, the natural numbers type having the rules of List(⊤) in T_{au} that is:

Natural Numbers type

N type nat  ^{0 ∈ N I_{1}-nat}  ^{{n ∈ N \atop s(n) ∈ N} I_{2}-nat}

\begin{matrix}L(z) type [z ∈ N] \\ n ∈ N a ∈ L(0) l(x, y) ∈ L(s(x)) [x ∈ N, y ∈ L(x)] \end{matrix} ; El_{N}(a, l, n) ∈ L(n) E-nat

\begin{matrix}L(z) type [z ∈ N] \\ a ∈ L(0) l(x, y) ∈ L(s(x)) [x ∈ N, y ∈ L(x)] \end{matrix} ; El_{N}(a, l, 0) = a ∈ L(0) C_{1}-nat

\begin{matrix}L(z) type [z ∈ N] \\ n ∈ N a ∈ L(0) l(x, y) ∈ L(s(x)) [x ∈ N, y ∈ L(x)] \end{matrix}

El_{N}(a, l, s(n)) = l(n, El_{N}(a, l, n)) ∈ L(s(n))

C_{2}-nat

The typed calculus of locoi T_{l}. The calculus T_{l} is obtained by extending T_{alxt} with list types. Hence it includes the following type constructors: terminal type, indexed sum types, extensional equality types, false type, disjoint sum types, disjointness axiom, list types.

The typed calculus of regular locoi T_{rl}. The calculus T_{rl} is obtained by extending T_{l} with quotient types on the total relation namely:

Quotient types on the total relation

A type ; A/⊤ type Qtr  ^{{a ∈ A \atop [a] ∈ A/⊤} I-Qtr}  ^{{a ∈ A b ∈ A \atop [a] = [b] ∈ A/⊤} eq-Qtr}

\begin{matrix}L(z) type [z ∈ A/⊤] \\ p ∈ A/⊤ l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A] \end{matrix} ; El_{Q}(l, p) ∈ L(p) E-Qtr

\begin{matrix}L(z) type [z ∈ A/⊤] \\ a ∈ A l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A] \end{matrix} ; El_{Q}(l, [a]) = l(a) ∈ L([a]) C-Qtr

Hence T_{rl} includes the following type constructors: terminal type, indexed sum types, extensional equality types, false type, disjoint sum types, disjointness axiom, list types and quotient types of the kind A/⊤.

The typed calculus of arithmetic pretopoi T_{pn}. The calculus T_{pn} includes the following type constructors: terminal type, indexed sum types, extensional equality types, false type, disjoint sum types, disjointness axiom, quotient types on mono equivalence relations with the effectiveness axiom and the natural numbers type.

In other words T_{pn} is the fragment of the dependent type theory T_{au} in section 3 without list types but with the natural numbers type N ≡ List(⊤).

By using the typed calculi mentioned so far we can build the initial structures among the categorical structures they describe.

From [Mai05a] we recall that given a typed calculus T for a certain kind of categorical structures, let us say S-structures, the initial S-structure amounts to the category C_{T} defined as follows:

3.4. Definition. The objects of C_{T} are the closed types A, B, C … of T modulo their equality, and the morphisms between two types, A and B, are the expressions (x) b(x) (see [NPS90]) corresponding to the judgement b(x) ∈ B [x ∈ A] — where the type B does not depend on A — modulo their definitional equality, that is we state that (x) b(x) ∈ C_{T} (A, B) and (x) b′(x) ∈ C_{T} (A, B) are equal if and only if we can derive in T the judgement b(x) = b′(x) ∈ B [x ∈ A]. The composition in C_{T} is defined by substitution, that is given (x) b(x) ∈ C_{T} (A, B) and (y) c(y) ∈ C_{T} (B, C) their composition is (x) c(b(x)). The identity is (x) x ∈ C_{T} (A, A) obtained from x ∈ A [x ∈ A].

Then by following the technique used in [Mai05a] we can prove that the above calculi provide internal languages of the corresponding structures and give rise to the initial structures in a modular way:

3.5. Theorem. The following hold:

• T_{sk} provides an internal language for Skolem categories and C_{T_{sk}}, also called S_{in}, is the initial Skolem category, and it is also the initial Skolem theory.

• T_{alxt} provides an internal language for arithmetic lextensive categories and C_{T_{alxt}} is the initial arithmetic lextensive category.

• T_{rl} provides an internal language for regular locoi and C_{T_{rl}} is the initial regular locos.

• T_{pn} provides an internal language for arithmetic pretopoi and C_{T_{pn}} is the initial arithmetic pretopos.

• T_{au} provides an internal language for list-arithmetic pretopoi and C_{T_{au}} is the initial list-arithmetic pretopos.

3.6. Remark. It is worth mentioning that in [Wra85, Mor96] an initial Skolem category is built and used to model a programming language representing primitive recursive functions. Also in [Rol76] a term language including a primitive recursive operator is presented to reason within a Skolem theory.

3.7. First applications of our internal languages. Before entering into the main topic of our paper we give two applications regarding the use of internal languages of the mentioned categorical structures to prove some of their categorical properties.

The first application is a simple proof that parameterized list objects are local in a locos as first proved in [Coc90]. The second application is the proof that list-arithmetic pretopoi are closed under coequalizers.

3.8. Locality of locoi. Here we apply the internal type theory of a locos to show that its structure is local with a simple proof alternative to that in [Coc90]. First of all, note that the difficulty in proving that a locos C is local relies in proving that parameterized list objects are local. Indeed, the structure of lextensive category is local because the forgetful functor from C/A to C creates finite limits and stable finite disjoint coproducts.

To prove that C/A enjoys parameterized list objects we use the internal language of a locos and we anticipate a technique to define operations by iteration that we will also use to build free internal categories and diagrams in a list-arithmetic pretopos.

First note that the notion of parameterized list object corresponds in type theory to the notion of list type of a closed type. Hence, we can easily prove that the typed calculus for locoi can be taken to be a fragment T_{l}^{∗} of the typed calculus T_{l} already presented. The fragment T_{l}^{∗} is obtained from T_{l} by allowing list types List(A) only if A is a closed type. List objects are needed to interpret such list types, while their parameterization is needed to interpret the structural rule of weakening applied to such list types with their terms.

Now, we prove that in T_{l}^{∗} we can represent list types List(B(x)) [x ∈ A] of types B(x) type [x ∈ A] depending on at most one type. This is enough to deduce categorically that any slice category of a locos C is equipped with list objects. Indeed, for any object A in C and for any C/A-object b : B → A, thought of as a term b(y) ∈ A [y ∈ B], we can form the list object List(b) as the interpretation of the list type of the dependent type Σ_{y∈B} b(y) =_{A} x for x ∈ A. In T_{l}^{∗} the type of lists of a dependent type B(x) [x ∈ A] with A closed type can be defined by using the indexed sum type as follows: for x ∈ A

List(B(x)) ≡ Σ_{w∈List(Σ_{x∈A}B(x))} \overline{π_{1}}(w) =_{List(A)} mult(x, lh(w))

where \overline{π_{1}} ≡ Lst(π_{1}) is the lifting on lists of the first projection, lh(w) is the length of the list w (see the appendix for related definitions) and mult(x, lh(w)) ≡ \underbrace{⌊x, x, …, x⌋}_{n-times} is

the list with n-times x, formally defined by induction on natural numbers as follows: for x ∈ A and n ∈ N

mult(x, n) ≡ \begin{cases}ϵ & if n = 0 \\ ⌊mult(x, m), x⌋ & if n = m + 1 \end{cases}

Then, the list constructors are the following: for x ∈ A

ϵ^{B(x)} ≡ ⟨ϵ^{Σ}, eq⟩
cons^{B(x)}(s, b) ≡ ⟨⌊π_{1}(s), ⟨x, b⟩⌋, eq ⟩ for s ∈ List(B(x)), b ∈ B(x)

where ϵ^{Σ} is the empty list in List(Σ_{x∈A}B(x)).

Finally, in order to prove the validity of the elimination rule on List(B(x)) in the context of an extensional type theory, as described in [Mai05a], it is sufficient to prove the validity of the elimination rule towards types not depending on List(B(x)) for x ∈ A

E-list) \frac{C type s ∈ List(B(x)) c ∈ C l(y, z) ∈ C [y ∈ C, z ∈ B(x)]}{El_{List}(c, l, s) ∈ C}

with corresponding β and η conversion rules. However, since we can not use the full elimination on List(Σ_{x∈A}B(x)), given that List(B(x)) is defined as a proper subtype of List(Σ_{x∈A}B(x)), we define the elimination constructor by iteration, i.e. by induction on natural numbers.

Therefore, given a type C [x ∈ A] — not depending on List(B(x)) — together with a term c ∈ C [x ∈ A, w ∈ Γ] (representing the value on the empty list, that is the base step) and l(y, z) ∈ C [x ∈ A, w ∈ Γ, y ∈ C, z ∈ B(x)] (representing the inductive step) we define

El_{list}(c, l, z) ≡ Itr(c, l, z, lh(z_{1})) ∈ C [x ∈ A, w ∈ Γ, z ∈ List(B(x))]

where in turn

Itr(c, l, z, n) ∈ C [x ∈ A, w ∈ Γ, z ∈ List(B(x)), n ∈ N]

is defined as follows

Itr(c, l, z, 0) ≡ c
Itr(c, l, z, n + 1) ≡ \begin{cases}l(Itr(c, l, z, n), p_{n+1}(z_{1})) & if n + 1 ≤ lh(z_{1}) \\ Itr(c, l, z, n) & if n + 1 > lh(z_{1}) \end{cases}

where z_{1} ≡ π_{1}(z) and p_{n}(z_{1}) is the nth element of the list z_{1} (see the appendix). Then, we can easily prove that this elimination constructor enjoys the corresponding β and η conversions.

Moreover, we can show that such list objects in C/A are preserved by pullbacks. In particular the pullback of the interpretation of List(B(x)) [x ∈ A] in C/A along f : C → A, thought of as a term f(y) ∈ A [y ∈ C], turns out to be isomorphic to the interpretation of

List(B(x))[x/f] ≡ Σ_{w∈List(Σ_{x∈A}B(x))} \overline{π_{1}}(w) =_{List(A)} mult(f(y), lh(w))

obtained by substituting x with f(y) for y ∈ C. Analogously the pullback of the interpretation of B(x) [x ∈ A] in C/A along f : C → A turns out to be isomorphic to the interpretation of B(f(y)) [y ∈ C] and then, its list object turns out to be the interpretation of

List(B(x)[x/f]) ≡ Σ_{z∈List(Σ_{y∈C}B(f(y))} \overline{π_{1}}(w) =_{List(C)} mult(y, lh(w))

for y ∈ C. Now we show that List(B(x))[x/f] is isomorphic to List(B(x)[x/f]) by just defining a morphism in the slice category over C

ϕ : List(B(x))[x/f] → List(B(x)[x/f])

as ϕ(w) ≡ ϕ̃(w, lh(w_{1})) where ϕ̃(w, n) is in turn defined by iteration on natural numbers as follows: for y ∈ C, w ∈ List(B(x))[x/f]

ϕ̃(w, 0) ≡ ⟨ϵ^{Σ}, eq⟩

ϕ̃(w, n + 1) ≡ \begin{cases}⟨⌊π_{1}(ϕ̃(w, n)), ⟨y, p_{n+1}(w_{1})⟩⌋, eq⟩ & if n + 1 ≤ lh(w_{1}) \\ ϕ̃(w, n) & if n + 1 > lh(w_{1}) \end{cases}

where w_{1} ≡ π_{1}(w).

ϕ is an isomorphism whose inverse can be defined in an analogous way by iteration on natural numbers.

3.9. A list-arithmetic pretopos has coequalizers. Now we are going to prove that any list-arithmetic pretopos U has coequalizers by using its internal language. The key point is to show how to make the relation needed to coequalize two given maps into an equivalence relation. To do this we use lists in a crucial way.

3.10. Proposition. In any list-arithmetic pretopos U the coequalizer of any two given morphisms

\xymatrix{C \ar[r]^{a} \ar[r]_{b} & A}

exists.

Proof. First, we consider the following reflexive and symmetric relation on A: for elements z, z′ ∈ A

R(z, z′) ≡ z =_{A} z′
∨ ∃_{c∈C} (a(c) =_{A} z ∧ b(c) =_{A} z′)
∨ ∃_{c∈C} (b(c) =_{A} z ∧ a(c) =_{A} z′)

Then, to define its transitive closure the idea is the following: in order to express that an element z ∈ A is connected to z′ ∈ A through a finite list of elements x_{1}, x_{2}, x_{3} such that

R(z, x_{1}) ∧ R(x_{1}, x_{2}) ∧ R(x_{2}, x_{3}) ∧ R(x_{3}, z′)

we require the existence of a list s ≡ ⌊⟨z, x_{1}⟩, ⟨x_{1}, x_{2}⟩, ⟨x_{2}, x_{3}⟩, ⟨x_{3}, z′⟩⌋ of pairs related by R with the property that the list ⌊x_{1}, x_{2}, x_{3}⌋, containing the second components of elements in the back list ⌊⟨z, x_{1}⟩, ⟨x_{1}, x_{2}⟩, ⟨x_{2}, x_{3}⟩⌋, is equal to the list with the first components of elements in the front list ⌊⟨x_{1}, x_{2}⟩, ⟨x_{2}, x_{3}⟩, ⟨x_{3}, z′⟩⌋. Moreover, z must be the first component of the first element in s, while z′ must be the second component of the last element in s.

Hence, we define:

R_{t}(z, z′) ≡ ∃_{s∈List^{∗}(Q)} (Lst(π̃_{2})(bck(s)) =_{List(A)} Lst(π̃_{1})(frt(s)) ∧ z =_{A} π̃_{1}(fst(s)) ∧ z′ =_{A} π̃_{2}(las(s)))

where Q ≡ Σ_{w∈A×A}R(π_{1}(w), π_{2}(w)) and π̃_{1} ≡ π_{1} · π_{1} and π̃_{2} ≡ π_{2} · π_{1} (see the appendix for precise definitions of non-empty lists List^{∗}(Q) and operations Lst(−), fst, las, bck and frt).

It follows easily that R_{t} is an equivalence relation and that [−] : A → A/R_{t}, that is the map assigning to every x ∈ A its equivalence class in A/R_{t}, is the coequalizer of a and b.

4. Joyal’s arithmetic universes

In this section we describe the construction of arithmetic universes given by André Joyal in the seventies. The construction can be read in unpublished notes by Joyal himself, Gavin Wraith [Wra85], in [Mor96] and partly in [Rol76].

Joyal built examples of arithmetic universes by taking the exact completion of the category of predicates built out of a Skolem theory.

Before giving the definition of predicate we define some primitive recursive operations and review some key properties of the natural numbers object in a Skolem category.

4.1. Definition. Given a Skolem category S, the predecessor, truncated subtraction, order, equality are defined as follows

x · − 1 ≡ \begin{cases}0 · − 1 ≡ 0 \\ (n + 1) · − 1 ≡ n \end{cases} x · − y ≡ \begin{cases}x · − 0 ≡ x \\ x · − (n + 1) ≡ (x · − n) · − 1 \end{cases}

x ∨ y ≡ x + (y · − x) x ∧ y ≡ x · − (x · − y) eq(x, y) ≡ 1 · − ((x · − y) ∨ (y · − x))

4.2. Definition. [Wra85, Mor96] A predicate in a Skolem category S is an S-morphism P : N → N between natural numbers satisfying P ∗ P =_{S} P where ∗ : N × N → N is the multiplication morphism of natural numbers.

In essence a predicate is an S-morphism with values 0, 1. It defines a decidable subobject of N whose elements can be thought of those with value 1. By using the above definitions as proved in classical recursion (for example see [Odi89]) we can show:

4.3. Proposition. In any Skolem category S the collection of predicates forms a boolean algebra with bounded existential and universal quantifications where the order is defined as follows

P ≤ Q ≡ P · − Q =_{S} 0

namely the truncated subtraction of them is the zero constant morphism in S.

In particular, the equality induced by the order is the equality predicate above defined and it amounts to the equality of S-morphisms, i.e. we have

P ≤ Q and Q ≤ P iff eq(P, Q) =_{S} 1 iff P =_{S} Q

Moreover, the conjunction is the multiplication, i.e. P ∧ Q =_{S} P ∗ Q, and the complement of P is 1 · − P.

4.4. Proposition. In any Skolem category S the following hold:

• the natural numbers object N is isomorphic to the binary product of itself N × N, namely there exist S-morphisms

pair : N × N → N  pr_{1} : N → N  pr_{2} : N → N
such that ⟨pr_{1} · pair, pr_{2} · pair⟩ =_{S} id pair · ⟨pr_{1}, pr_{2}⟩ =_{S} id

• in S the natural numbers object N is a parameterized list object over itself.

Proof. We employ the internal language of a Skolem theory.

By following standard ideas in recursion theory (see for example [Odi89]) we define the pairing map as follows

pair(x, y) ≡ 2^{x} ∗ (2 ∗ y + 1) · − 1

which provides the required isomorphism with the following projections

pr_{1}(z) ≡ min{ x ≤ z | ∃y ≤ z z =_{S} pair(x, y) }
pr_{2}(z) ≡ min{ y ≤ z | ∃x ≤ z z =_{S} pair(x, y) }

N turns out to be a list object over itself by using the binary representation of natural numbers. The idea is to represent the empty list as zero, and a list like ⌊n_{1}, n_{2}, …, n_{m}⌋ as the number represented in binary digits as the list starting with 1 followed by a number of zeros equal to the last element n_{m} of the list, and then again 1 followed by a number of zeros equal to the last but one element n_{m−1} of the list and so on. For example:

ϵ ⟼ 0
⌊0⌋ ⟼ 1
⌊3⌋ ⟼ 1000 = 2^{3}
⌊0, 1, 3⌋ ⟼ 1000101 = 2^{6} + 2^{2} + 1

Conversely any natural number in binary digits represents a list where each nth element counts the nested zeros after the nth-1 counted from the right.

More formally, the list constructors are defined as follows: for s, n ∈ N

1) ϵ ≡_{List(N)} 0

2) cons_{List(N)}(s, n) ≡ 2^{c} · 2^{n} + s where c ≡ min{ x ≤ s | 2^{x} > s }.

After defined the nth-projection of any natural number thought of as a list, we define the list elimination constructor rec_{List(N)}(b, g, z) by induction on natural numbers, by starting from b and then iterating the application of g up to the length of z, if this is not zero. This construction is analogous to the corresponding one for list objects in a slice category of a locos in section 3.8.

4.5. Remark. In [Rol76] and in a draft by Joyal, a predicate is defined as an S-morphi-sm P : N^{k} → N from a finite product of N to N satisfying P ∧ 1 =_{S} P. If S is a Skolem theory, then these predicates represent the decidable subobjects of S-objects, given that objects in S are only finite products of N. However thanks to proposition 4.4, predicates on N^{k} with k ≥ 1 are in bijective correspondence with predicates on N by precomposing with the isomorphism between N^{k} and N. Hence, without loss of generality, we can restrict to predicates from N to N. In this case definition 4.7 is equivalent to that by Joyal since P ∗ P =_{S} P iff P ∧ 1 =_{S} P.

Now, we are ready to define the category of predicates in a Skolem theory S:

4.6. Definition. [Mor96, Wra85] Given a Skolem theory S the category Pred(S) of predicates in S is defined as follows:

• Ob(Pred(S)): predicates in S, namely morphisms P : N → N such that P ∗P =_{S} P;

• Hom(P, Q): S-morphisms f : N → N such that P ≤ Q · f (where Q · f is the composition of Q with f) and two such S-morphisms f : N → N and g : N → N are equal iff P ∗ f =_{S} P ∗ g.

Note that, if the Skolem theory is the full subcategory S_{ZF C} of the usual category of classical ZFC-sets with only finite products of natural numbers as objects, then Pred(S_{ZF C}) is the category having subsets of natural numbers as objects. Indeed a subset is characterized by the elements with value 1 through a predicate P that is its characteristic function. Moreover, morphisms of Pred(S_{ZF C}) turn out to be functions mapping the domain subset to the codomain subset. Finally, two maps are considered equal if they are equal on the domain subset.

Joyal proved that the category of predicates Pred(S) is a regular locos:

4.7. Proposition. [Wra85, Mor96, Rol76] The category Pred(S) of a Skolem theory S is regular with stable finite disjoint coproducts and parameterized list objects. Moreover, epimorphisms of image factorizations split.

Proof. We describe the claimed structure of Pred(S).

The terminal object is given by the predicate ⊤_{Pred} : N → N defined as the singleton zero for n ∈ N

⊤_{Pred}(n) ≡ 1 · − n

The binary product of two predicates P and Q is given by

(P × Q)(n) ≡ P (pr_{1}(n)) ∗ Q(pr_{2}(n)) for n ∈ N

The two projections of P × Q are π_{P} : P × Q → P and π_{Q} : P × Q → Q defined as: π_{P} (n) ≡ pr_{1}(n) and π_{Q}(n) ≡ pr_{2}(n) for n ∈ N.

The pairing morphism of f : C → P and g : C → Q is defined as ⟨f, g⟩_{Pred}(n) ≡ pair(f(n), g(n)) for n ∈ N.

The equalizer of two morphisms f, g : P → Q is

Eq(f, g)(n) ≡ P (n) ∗ eq(f(n), g(n)) for n ∈ N

and the equalizer injection e : Eq(f, g) → P is defined as e(n) ≡ n for all n ∈ N. Obviously, the morphism factoring any h : C → P equalizing f and g is h itself but with Eq(f, g) as codomain.

The initial object is given by the predicate ⊥_{Pred} : N → N defined as

⊥_{Pred}(n) ≡ 0 for n ∈ N

The binary coproduct of two predicates P and Q is defined as follows: for n ∈ N

(P + Q)(n) ≡ even(n) ∗ P (n/2) + odd(n) ∗ Q(n · − 1/2)

where n/2 is the quotient of the division by 2 and the operations even, odd are defined as follows:

even(n) ≡ \begin{cases}even(0) ≡ 1 \\ even(n + 1) ≡ 1 · − even(n) \end{cases} odd(n) ≡ \begin{cases}odd(0) ≡ 0 \\ odd(n + 1) ≡ 1 · − odd(n) \end{cases}

The injections i_{P} : P → P + Q and i_{Q} : Q → P + Q are defined as i_{P} (n) ≡ 2 ∗ n and i_{Q}(n) ≡ 2 ∗ n + 1 for n ∈ N. Given f : P → C and g : Q → C their coproduct morphism f + g : P + Q → C is defined as follows: for n ∈ N

(f + g)(n) ≡ even(n) ∗ f(n/2) + odd(n) ∗ g(n · − 1/2)

It follows easily that such binary coproducts are stable under pullbacks.

The image object of a morphism f : P → Q is defined as follows: for n ∈ N

(Imf)(n) ≡ P (n) ∗ eq(n, p(n))

where

p(n) ≡ min{ x ≤ n | P (x) ∗ eq(f(x), f(n)) =_{S} 1 }

Its image morphism ι_{f} : Imf → Q is defined as ι_{f}(n) ≡ f(n) for n ∈ N and this factors f through p : P → Imf defined as the above p(n) for n ∈ N, i.e. f = ι_{f} · p in Pred(S). Moreover, p has a section p^{−1} : Imf → P defined as p^{−1}(n) ≡ n, that is p · p^{−1} = id in Pred(S). Since epimorphisms of image factorizations split then images are stable under pullbacks.

The parameterized list object of a predicate is defined by using the fact that N is isomorphic to List(N) by prop 4.4. Hence, given a predicate P its parameterized list object is

List(P)(n) ≡ \begin{cases}1 & if n ≡ 0 \\ List(P)(m) ∗ P (k) & if n ≡ cons_{List(N)}(m, k) \end{cases}

The list structure of List(P) is induced by that of List(N) as follows:

r_{0}^{List(P)} : ⊤ → List(P) is defined for n ∈ N as

r_{0}^{List(P)}(n) ≡ 0

and r_{1}^{List(P)} : List(P) × P → List(P) is defined for n ∈ N as

r_{1}^{List(P)}(n) ≡ cons_{List(N)}(pr_{1}(n), pr_{2}(n))

Then, given b : C → Q and g : Q × P → Q we put rec_{List(P)}(b, g)(n) ≡ rec_{List(N)}(b, g, n) for n ∈ N.

Now, we are finally ready to give Joyal’s definition of arithmetic universe. It amounts to the exact completion (Pred(S))_{ex} of the category of predicates built out of a Skolem theory S. Given that the category of predicates in a Skolem theory is regular as proved in proposition 4.7, then we can use the exact completion performed on a regular category (see [CV98] and loc. cit.). However, since in Pred(S) epimorphisms of image factorizations split, then we can define the morphisms in such exact completions (Pred(S))_{ex} just as Pred(S)-morphisms preserving the equivalence relations. Therefore, we put:

4.8. Definition. A Joyal-arithmetic universe is the category (Pred(S))_{ex} built out of a Skolem theory S as follows:

• Ob(Pred(S))_{ex}: (X, R) where X is an object of Pred(S) and R : dom(R) → X × X is a monic categorical equivalence relation on X;

• Hom((X, R), (Y, S)): Pred(S)-morphisms f : X → Y preserving the equivalence relations, that is R ≤ (f × f)^{∗}(S) as subobjects where (f × f)^{∗}(S) is the first projection of the pullback of S along f × f. Moreover, two arrows f, g : (X, R) → (Y, S) in Hom((X, R), (Y, S)) are equal iff R ≤ (f × g)^{∗}(S).

We also recall the definition of the embedding of Pred(S) into (Pred(S))_{ex}:

4.9. Definition. The embedding functor

Y : Pred(S) ⟶ (Pred(S))_{ex}

is defined as follows:

Y(P) ≡ (P, x =_{P} y) Y(f) ≡ f

where x =_{P} y ≡ Eq(π_{1}, π_{2}) is the identity relation on P, that is the equalizer of the projections π_{1}, π_{2} from P × P in Pred(S) (categorically Eq(π_{1}, π_{2}) is isomorphic to the diagonal ⟨id, id⟩ : P → P × P).

We now give the main result of this section:

4.10. Proposition. (Pred(S))_{ex} is a list-arithmetic pretopos.

Proof. In [Wra85, Mor96] it is shown that (Pred(S))_{ex} is a pretopos with list objects but we can show that list objects are also parameterized. We know from [CV98] that this category is exact and hence we just describe finite coproducts and list objects (see [Car95, BCRS98]).

Note that in doing this we employ the internal language of a regular locos provided by T_{rl} according to which we can consider the equivalence relation R as a type-theoretic equivalence relation.

The initial object of (Pred(S))_{ex} is (⊥_{Pred}, x =_{⊥_{Pred}} x) where x =_{⊥_{Pred}} x is the identity relation.

The binary coproduct of two objects (X, R) and (Y, S) is (X + Y, R + S) where X + Y is the coproduct in Pred(S) and R + S is defined as follows: for z, z′ ∈ X + Y

(R + S)(z, z′) ≡ \{ \begin{matrix}∃_{x∈X} ∃_{x′∈X} (z =_{X} i_{X}(x)) ∧ (z′ =_{X} i_{X}(x′)) ∧ R(x, x′) \\ ∨ \\ ∃_{y∈Y} ∃_{y′∈Y} (z = i_{Y} (y)) ∧ (z′ =_{Y} i_{Y} (y′)) ∧ S(y, y′) \\ ∨ \\ ⊥ ∧ ∃_{x∈X} ∃_{y∈Y} ((z =_{X} i_{X}(x) ∧ z′ = i_{Y} (y)) \\ ∨ (z′ =_{X} i_{X}(x) ∧ z = i_{Y} (y))) \end{matrix}

R + S can be proved to be an equivalence relation since in T_{rl}, as proved in [Mai05a], given an element z ∈ X + Y we can derive a proof of

(∃_{x∈X} inl(x) =_{X} z) ∨ (∃_{y∈Y} inr(y) =_{Y} z)

The injections are i_{(X,R)} : (X, R) → (X +Y, R+S) and i_{(Y,S)} : (Y, S) → (X +Y, R+S) defined as i_{(X,R)}(x) ≡ i_{X}(x) for x ∈ X and i_{(Y,S)}(y) ≡ i_{Y} (y) for y ∈ Y.

The list object on (X, R) is (List(X), List(R)) where List(X) is the list object on X in Pred(S) and List(R) is defined as follows:

List(R)(s, s′) ≡ \{ \begin{matrix}∃_{t∈List(Σ_{x∈X}Σ_{x′∈X}R(x,x′))} (\overline{π_{1}}(t) =_{List(X)} s ∧ \overline{π_{2}}(t) =_{List(X)} s′ \\ ∧ lh(s) =_{List(X)} lh(s′)) \\ ∨ \\ ⊥ ∧ (lh(s) < lh(s′) ∨ lh(s′) < lh(s)) \end{matrix}

where lh(l) is the length of the list l and \overline{π_{1}} ≡ Lst(π_{1}) and \overline{π_{2}} ≡ Lst(π_{1} · π_{2}) are obtained by lifting the first and second projections on lists (see the appendix) and for x, x′ ∈ N we put x < x′ ≡ ∃_{y∈N} x′ =_{N} x + (y + 1) for x, x′ ∈ N.

List(R) can be proved to be an equivalence relation since in T_{rl}, given s, s′ ∈ List(X), we can derive a proof of

lh(s) =_{List(X)} lh(s′) ∨ lh(s) < lh(s′) ∨ lh(s′) < lh(s)

Moreover, the list structure on (List(X), List(R)) is defined as follows:

r_{o}^{(X,R)} : (⊤, x =_{⊤} x) → (List(X), List(R))  as r_{o}^{(X,R)}(x) ≡ r_{o}^{X}(x)
for x ∈ X
r_{1}^{(X,R)} : (List(X), List(R)) × (X, R) → (List(X), List(R)) as r_{1}^{(X,R)}(s, x) ≡ r_{1}^{X}(s, x)

for s ∈ List(X), x ∈ X

The list object is parameterized. Indeed, given the morphisms f : (Z, H) → (C, M) and g : (C, M)×(X, R) → (C, M), by using the property of the list object List(X) in Pred(S) we obtain a Pred(S)-morphism

rec(f, g) : Z × List(X) ⟶ C

satisfying rec(f, g) · ⟨id, r_{o}^{X}·!_{Z}⟩ = f and rec(f, g) · (id × r_{1}^{X}) = (g · (rec(f, g) × id)) · σ in Pred(S) and hence in (Pred(S))_{ex} if rec(f, g) is a (Pred(S))_{ex}-morphism.

We can prove that rec(f, g) is a morphism in (Pred(S))_{ex} from (Z, H)×(List(X), List(R)) to (C, M). Indeed, given z, z′ ∈ Z for which H(z, z′) holds and s, s′ ∈ List(X) for which List(R)(s, s′) holds, we prove that M( rec(f, g)(⟨z, s⟩) , rec(f, g)(⟨z′, s′⟩) ) holds by showing by induction on n ∈ N the validity of

M( rec(f, g)(⟨z, part_{n}(s)⟩) , rec(f, g)(⟨z′, part_{n}(s′)⟩) )

where part_{n}(s) is a list operation defined in the appendix. This lets us prove what wanted since part_{k}(s) =_{List(X)} s holds for k ≥ lh(s).

Finally, we can show uniqueness of rec(f, g) in an analogous way. Indeed, for any morphism h with the same domain and codomain of rec(f, g) satisfying

\begin{matrix}h · ⟨id, r_{o}^{(X,R)}·!_{(Z,H)}⟩ = f \\ h · (id × r_{1}^{(X,R)}) = (g · (h × id)) · σ \end{matrix}

in (Pred(S))_{ex}, we can then prove by induction on n ∈ N the validity of

M( rec(f, g)(⟨z, part_{n}(s)⟩) , h(⟨z′, part_{n}(s′)⟩) )

from which rec(f, g) =_{(Pred(S))_{ex}} h follows.

Observe that (Pred(S_{in}))_{ex} built out of the initial Skolem category S_{in} amounts to the initial arithmetic universe (Pred(S_{in}))_{ex} in the category of Joyal-arithmetic universes and functors induced from functors between Skolem theories, with a fixed choice of their structure, preserving the Skolem structure. Note that Pred(S_{in}) turns out to be the category of primitive recursive predicates.

In the following we simply call A_{in} the initial arithmetic universe (Pred(S_{in}))_{ex}.

5. The category of primitive recursive predicates via type theory

Here we outline how the category of primitive recursive predicates is equivalent to the initial arithmetic lextensive category C_{T_{ad}} and also to the initial regular locos C_{T_{rl}}.

To this purpose, we define two embeddings

E_{ad} : Pred(S_{in}) ⟶ C_{T_{ad}} E_{rl} : Pred(S_{in}) ⟶ C_{T_{rl}}

where E_{ad} is defined as follows:

• E_{ad}(P) ≡ Σ_{x∈N}P (x) =_{N} 1

for any predicate P in Ob Pred(S_{in}).

• E_{ad}(f)(z) ≡ ⟨f(π_{1}(z)), eq⟩ ∈ Σ_{x∈N}Q(x) =_{N} 1 [z ∈ Σ_{x∈N}P (x) =_{N} 1]

for f : P → Q in Pred(S_{in}), that is E_{ad}(f) is the function associating f(x) satisfying Q(f(x)) =_{N} 1 to any x ∈ N such that P (x) =_{N} 1 holds.

The functor E_{rl} can be defined essentially in the same way. Indeed observe that the calculus T_{ad} is a fragment of T_{rl} after recalling to represent the natural numbers object as the list type of the terminal type. This means that the category C_{T_{ad}} is a subcategory of C_{T_{rl}}

and that the embedding \xymatrix{C_{T_{ad}} \ar@{^{(}->}[r]^{i_{ad}^{rl}} & C_{T_{rl}}} , which is the identity on objects and morphisms, preserves the arithmetic lextensive structure. Then, we define E_{rl} as the composition of the embedding i_{ad}^{rl} with E_{ad}

E_{rl} ≡ i_{ad}^{rl} · E_{ad}

In the next we prove that the embeddings E_{ad} and E_{rl} preserve the relevant structure of their domain categories. To prove this we will make use of the fact that 0 =_{N} n + 1 is false:

5.1. Lemma. In the typed calculus T_{ad} from a proof of 0 =_{N} n + 1 for n ∈ N, we can derive a proof of falsum ⊥. Therefore, also in any arithmetic lextensive category we can prove that 0 =_{N} n + 1 is false for n ∈ N.

Proof. By the elimination rule on the natural numbers n ∈ N we can define the term

(tt ⊕ ff) (n) ∈ ⊤ ⊕ ⊤

as follows

(tt ⊕ ff) (n) ≡ \begin{cases}tt & if n ≡ 0 \\ ff & if n ≡ m + 1 \end{cases}

where tt ≡ inl(⋆) and ff ≡ inr(⋆).

Hence, if there existed a proof of 0 =_{N} n+1, then by the rule E-Eq) of the extensional propositional equality we would get 0 = n + 1 ∈ N. Hence, by equality preservation of tt ⊕ ff we would obtain that (tt ⊕ ff)(0) = (tt ⊕ ff)(n + 1) ∈ ⊤ ⊕ ⊤. Now, after recalling that (tt ⊕ ff)(0) = tt and (tt ⊕ ff)(n + 1) = ff, we would also get

ff = tt ∈ ⊤ ⊕ ⊤

By disjointness of sum, namely by rule dis-+), we would conclude a proof of ⊥ as claimed.

Now, we are ready to prove that the embeddings E_{ad} and E_{rl} have the following preservation properties:

5.2. Lemma. The embedding E_{ad} is an arithmetic lextensive functor and E_{rl} is a regular locos functor.

Proof. We first show that E_{ad} preserves the arithmetic lextensive structure. The structure of C_{T_{ad}} is described in [Mai05a].

E_{ad} preserves the terminal object because, thanks to lemma 5.1, Σ_{x∈N}⊤_{Pred}(x) =_{N} 1 is isomorphic to ⊤ which can be chosen as a terminal object in C_{T_{ad}}. Indeed, the key point is to prove that from ⟨x, eq⟩ ∈ Σ_{x∈N}⊤_{Pred}(x) =_{N} 1 we obtain ⟨x, eq⟩ =_{E_{ad}(⊤_{Pred})} ⟨0, eq⟩. This follows by elimination of disjunction from

x =_{N} 0 ∨ ∃_{y∈N}x =_{N} y + 1

that can be proved by induction on natural numbers. In the case x =_{N} 0 we conclude trivially, and in the case x =_{N} y + 1 for some y ∈ N we conclude by lemma 5.1.

E_{ad} preserves binary products. Recall from [Mai05a] that the indexed sum type allows to define the binary product E_{ad}(P) × E_{ad}(Q) in C_{T_{ad}}, for P, Q predicates, with projections π_{1}(z) ∈ E_{ad}(P) and π_{2}(z) ∈ E_{ad}(Q), respectively, for z ∈ E_{ad}(P) × E_{ad}(Q).

Then, observe that the morphism induced by the product projections in Pred(S_{in})

⟨E_{ad}(π_{P}), E_{ad}(π_{Q})⟩ : E_{ad}(P × Q) ⟶ E_{ad}(P) × E_{ad}(Q)

has an inverse defined as follows: for z ∈ E_{ad}(P) × E_{ad}(Q)

In_{×}(z) ≡ ⟨pair(π_{1}(z_{1}), π_{1}(z_{2})), eq⟩

where z_{1} ≡ π_{1}(z) and z_{2} ≡ π_{2}(z).

E_{ad} preserves equalizers. Recall that the equalizer of E_{ad}(f) and E_{ad}(g) in C_{T_{ad}}, for f, g : P → Q in Pred(S_{in}), is defined as

Eq_{C_{T_{ad}}}(E_{ad}(f), E_{ad}(g)) ≡ Σ_{z∈E_{ad}(P)} E_{ad}(f)(z) =_{E_{ad}(Q)} E_{ad}(g)(z)

and the equalizer map is π_{1} : Eq_{C_{T_{ad}}}(E_{ad}(f), E_{ad}(g)) ⟶ E_{ad}(P). Since the equalizer embedding e : Eq(f, g) → P gives E_{ad}(f) · E_{ad}(e) = E_{ad}(g) · E_{ad}(e) in C_{T_{ad}}, it induces a morphism

Un_{eq} : E_{ad}(Eq(f, g)) ⟶ Eq_{C_{T_{ad}}}(E_{ad}(f), E_{ad}(g))

defined as Un_{eq}(z) ≡ ⟨E_{ad}(e)(z), eq⟩ for z ∈ E_{ad}(Eq(f, g)), which is indeed an isomorphism with inverse In_{eq} defined as In_{eq}(z) ≡ ⟨π_{1}(π_{1}(z)), eq⟩ for z ∈ Eq_{C_{T_{ad}}}(E_{ad}(f), E_{ad}(g)).

E_{ad} preserves the initial object, since ⊥, which can be chosen as the initial object in C_{T_{ad}}, is isomorphic to Σ_{x∈N}0 =_{N} 1 thanks to lemma 5.1.

E_{ad} preserves binary coproducts since in T_{ad} we can prove that N is isomorphic to the coproduct of even numbers with odd ones. To prove this more in detail, recall that the type E_{ad}(P) + E_{ad}(Q) is a binary coproduct of E_{ad}(P) and E_{ad}(Q) for given predicates P and Q, and its injections are the terms inl(z) ∈ E_{ad}(P) + E_{ad}(Q) for z ∈ E_{ad}(P) and inr(w) ∈ E_{ad}(P) + E_{ad}(Q) for w ∈ E_{ad}(Q).

Now, the coproduct morphism induced by the injections in Pred(S_{in})

E_{ad}(j_{P}) ⊕ E_{ad}(j_{Q}) : E_{ad}(P) + E_{ad}(Q) ⟶ E_{ad}(P + Q)

is an isomorphism with inverse In_{⊕} defined as follows: for z ∈ E_{ad}(P + Q)

In_{⊕}(z) ≡ \begin{cases}inl(⟨z_{1}/2, eq⟩) & if even(z_{1}) = 1 \\ inr(⟨(z_{1} · − 1)/2, eq⟩) & if odd(z_{1}) = 1 \end{cases}

where z_{1} ≡ π_{1}(z).

E_{rl} is a lextensive functor being the composition of E_{ad} with an embedding preserving such a structure.

In order to prove that E_{rl} is a regular locos functor, we need to show that it preserves images and list objects.

We start by showing that E_{rl} preserves images. We recall from [Mai05a] that the image object of a morphism E_{rl}(f) : E_{rl}(P) → E_{rl}(Q) in C_{T_{rl}} is defined as

Im(E_{rl}(f)) ≡ Σ_{w∈E_{rl}(Q)} ∃_{z∈E_{rl}(P)} E_{rl}(f)(z) =_{E_{rl}(Q)} w

and the image morphism ι_{E(f)} : Im(E_{rl}(f)) ⟶ E_{rl}(Q) is defined as

ι_{E(f)}(z) ≡ π_{1}(z) ∈ E_{rl}(Q)

for z ∈ Im(E_{rl}(f)).

From the image factorization of f in Pred(S_{in}) it follows that E_{rl}(f) = E_{rl}(ι_{f})·E_{rl}(p) with E_{rl}(ι_{f}) monic since E_{rl} preserves pullbacks (recall that a monomorphism is characterized by the fact that the projections of its pullback along itself are isomorphic to the identities). Hence by the universal property of images there exists a morphism

Un_{im} : Im(E_{rl}(f)) ⟶ E_{rl}(Imf)

that is indeed an isomorphism with inverse In_{im} defined as follows: for z ∈ E_{rl}(Imf)

In_{im}(z) ≡ ⟨⟨f(z_{1}), eq⟩, [ ⟨z_{1}, eq⟩, eq⟩ ]⟩

where z_{1} ≡ π_{1}(z).

Finally, we show that E_{rl} preserves list objects. We recall that the list object of E_{rl}(P) in C_{T_{rl}} is List(E_{rl}(P)) with list constructors

r_{o}^{E_{rl}(P)}(z) ≡ ϵ ∈ List(E_{rl}(P))  for z ∈ ⊤
r_{1}^{E_{rl}(P)}(z) ≡ cons(π_{1}(z), π_{2}(z))  for z ∈ List(E_{rl}(P)) × E_{rl}(P)

By using the list structure of N as defined in proposition 4.4, we can easily define an isomorphism

Bin : List(E_{rl}(P)) ⟶ E_{rl}(List(P))

by induction on the list z ∈ List(E_{rl}(P)) as follows:

Bin(z) ≡ \{ \begin{matrix}⟨0, eq⟩ & if z ≡ ϵ \\ ⟨cons_{List(N)}(π_{1}(Bin(s)), π_{1}(a)), eq⟩ & if z ≡ cons(s, a) \\ & for s ∈ List(E_{rl}(P)), a ∈ E_{rl}(P) \end{matrix}

whose inverse In_{list} is defined by iteration on natural numbers as

In_{list}(z) ≡ Ĩn_{list}(z, lh(z_{1}))

for z ∈ E_{rl}(List(P)) where z_{1} ≡ π_{1}(z) and in turn Ĩn_{list}(z, lh(z_{1})) is defined as follows

Ĩn_{list}(z, 0) ≡ ϵ
Ĩn_{list}(z, n + 1) ≡ \begin{cases}cons(Ĩn_{list}(z, n), ⟨p_{n+1}(z_{1}), eq⟩) & if n + 1 ≤ lh(z_{1}) \\ Ĩn_{list}(z, n) & if n + 1 > lh(z_{1}) \end{cases}

where p_{n+1}(z_{1}) is the n + 1-th projection of the number z_{1} thought of as a list in List(N).

Thanks to this lemma we are ready to prove that:

5.3. Theorem. The syntactic categories C_{T_{ad}} and C_{T_{rl}} are equivalent to Pred(S_{in}).

Proof. Since by proposition 4.7 we know that Pred(S_{in}) is a regular locos, then by the initiality of C_{T_{ad}} and C_{T_{rl}}, as stated in theorem 3.5, there exist an arithmetic lextensive functor J_{ad} : C_{T_{ad}} ⟶ Pred(S_{in}) and a regular locos functor J_{rl} : C_{T_{rl}} ⟶ Pred(S_{in}), defined through the corresponding interpretations of T_{ad} and T_{rl} in Pred(S_{in}) as detailed in [Mai05a].

It turns out that both J_{ad} · E_{ad} and J_{rl} · E_{rl} are naturally isomorphic to the identity functor. This is because the interpretation of a predicate P turns out to be isomorphic to itself as a Pred(S_{in})-morphism and eq(P, 1) = P holds in S_{in}.

Moreover, being C_{T_{ad}} and C_{T_{rl}} respectively an initial up to iso arithmetic lextensive category and an initial up to iso regular locos, it follows that E_{ad} · J_{ad} : C_{T_{ad}} ⟶ C_{T_{ad}} and E_{rl} · J_{rl} : C_{T_{rl}} ⟶ C_{T_{rl}} are naturally isomorphic to the corresponding identity functors and hence we conclude.

5.4. Corollary. The initial arithmetic lextensive category C_{T_{ad}} is equivalent to the initial regular locos C_{T_{rl}}.

From this corollary we conclude that stable images and parameterized list objects are definable in the initial arithmetic lextensive category by translating back into C_{T_{ad}} the image and list structures of C_{T_{rl}} via the equivalences in theorem 5.3. But, since these equivalences are built through interpretation functors, defined in turn by induction on type and term constructors, we can not expect to be able to construct images and lists internally to any arithmetic lextensive category. Indeed the construction of images and list objects rely on the fact that every object can be considered a predicate on natural numbers as in Pred(S_{in}): this is an external property that does not seem necessarily valid internally in any arithmetic lextensive category. Logically it means that any type in the internal language of C_{T_{ad}}, which is the pure calculus T_{ad} without the addition of axioms, can be seen as an indexed sum of a predicate on natural numbers. But this property does not seem necessarily valid in any theory of T_{ad}.

6. The initial arithmetic universe via type theory

Here, we outline how the construction of the initial arithmetic universe A_{in} is equivalent to the initial arithmetic pretopos C_{T_{pn}} and also to the initial list-arithmetic pretopos C_{T_{au}}.

To this purpose, analogously to the embeddings of lemma 5.2 we define the embeddings

E_{pn} : Pred(S_{in}) ⟶ C_{T_{pn}} E_{au} : Pred(S_{in}) ⟶ C_{T_{au}}

They are essentially defined as E_{ad}. Indeed observe that the calculus T_{ad} is a fragment of T_{pn} and also of T_{au}, always after recalling to represent the natural numbers object as the list type of the terminal type. This means that the category C_{T_{ad}} is a subcategory of C_{T_{pn}} and also of C_{T_{au}}. Therefore the embeddings

\xymatrix{C_{T_{ad}} \ar@{^{(}->}[r]^{i_{ad}^{pn}} & C_{T_{pn}} & C_{T_{ad}} \ar@{^{(}->}[r]^{i_{ad}^{au}} & C_{T_{au}}}

which are the identity on objects and morphisms, preserve the arithmetic lextensive structure. Hence, we put

E_{pn} ≡ i_{ad}^{pn} · E_{ad} E_{au} ≡ i_{ad}^{au} · E_{ad}

Now note that E_{pn} and E_{au} enjoy the same preservation properties of E_{ad} and also of E_{rl} when applicable:

6.1. Lemma. The embedding E_{pn} is regular and preserves finite disjoint coproducts and the parameterized natural numbers object.

The embedding E_{au} is regular and preserves finite disjoint coproducts and parameterized list objects.

Therefore, by the above lemma, since A_{in} is the exact completion of Pred(S_{in}), by its universal property [CV98] there exist two exact functors

Ê_{pn} : A_{in} ⟶ C_{T_{pn}}  Ê_{au} : A_{in} ⟶ C_{T_{au}}

such that

Ê_{pn} · Y ≃ E_{pn}  Ê_{au} · Y ≃ E_{au}

Ê_{pn} can be explicitly defined as follows:

• Ê_{pn}((X, R)) ≡ E_{pn}(X)/E_{pn}(R),

• Ê_{pn}(f) ≡ Q(E_{pn}(f)) for f : (X, R) → (Y, S), where Q(E_{pn}(f)) is the unique map from the quotient E_{pn}(X)/E_{pn}(R) to E_{pn}(Y)/E_{pn}(S) such that Q(E_{pn}(f))([x]) ≡ [E_{pn}(f)(x)] for x ∈ E_{pn}(X).

The functor Ê_{au} is defined in the same way by using E_{au} in place of E_{pn}. However, since T_{pn} is a fragment of T_{au}, and hence the category C_{T_{pn}} is a subcategory of C_{T_{au}} with an embedding

\xymatrix{C_{T_{pn}} \ar@{^{(}->}[r]^{i_{pn}^{au}} & C_{T_{au}}}

preserving the arithmetic pretopos structure, it turns out that Ê_{au} satisfies

Ê_{au} = i_{pn}^{au} · Ê_{pn}

From [CV98] we know that Ê_{au} as well as Ê_{pn} are exact functors. Here we check that they preserve also finite coproducts and, respectively, list objects and the natural numbers object:

6.2. Lemma. The functor Ê_{pn} : A_{in} ⟶ C_{T_{pn}} preserves the arithmetic pretopos structure as well as the functor Ê_{au} : A_{in} ⟶ C_{T_{au}} preserves the list-arithmetic pretopos structure.

Proof. For simplicity, we just show that Ê_{au} preserves finite disjoint coproducts and list objects. The proof that Ê_{pn} is an arithmetic pretopos functor can be seen a special case of the above, given that these functors are defined in the same way and that natural numbers are lists of the terminal type.

Moreover we use the abbreviations X^{E} and R^{E} for E_{au}(X) and E_{au}(R) respectively. Clearly, Ê_{au} preserves the initial object. Indeed, given that E_{au} is regular and preserves

the initial object, then Ê_{au}((⊥_{Pred}, x =_{⊥_{Pred}} x)) ≃ ⊥/(x =_{⊥} x) which is in turn isomorphic to ⊥.

Now we prove that Ê_{au} preserves the binary coproduct structure. The binary coproduct of Ê_{au}((X, R)) and Ê_{au}((Y, S)) is X^{E}/R^{E} + Y^{E}/S^{E} with the coproduct structure described in lemma 5.2 for C_{T_{ad}}. Since E_{au} is regular and preserves coproducts, for simplicity we just suppose Ê_{au}((X + Y, R + S)) ≡ X^{E} + Y^{E}/R^{E} + S^{E}. Then, injections in (X + Y, R + S) induce an isomorphism

Ê_{au}(i_{(X,R)}) ⊕ Ê_{au}(i_{(Y,S)}) : Ê_{au}((X, R)) + Ê_{au}((Y, S)) ⟶ Ê_{au}((X + Y, R + S))

whose inverse Q(In_{cp}) is defined to be the unique morphism induced on the quotient (X^{E} +Y^{E})/(R^{E} +S^{E}) by a map In_{cp} : X^{E} +Y^{E} ⟶ X^{E}/R^{E} +Y^{E}/S^{E} defined by elimination on the sum as follows: for w ∈ X^{E} + Y^{E}

In_{cp}(w) ≡ \{ \begin{matrix}inl([x]_{X^{E}/R^{E}}) & if w = inl(x) for x ∈ X^{E} \\ inr([y]_{Y^{E}/R^{E}}) & if w = inr(y) for y ∈ Y^{E} \end{matrix}

Now we prove that Ê_{au} preserves the list object structure. The list object on Ê_{au}(X, R) = X^{E}/R^{E} is List(X^{E}/R^{E}) with the list structure described in lemma 5.2 for C_{T_{rl}}. Since E_{au} is regular and preserves list objects, for simplicity we suppose

Ê_{au}((List(X), List(R)) ≡ List(X^{E})/ List(R^{E}).

Now, by induction on the list structure of List(X^{E}/R^{E}) we can define an isomorphism

Un_{list} : List(Ê_{au}(X, R)) ⟶ Ê_{au}((List(X), List(R)))

as follows: for z ∈ List(X^{E}/R^{E})

Un_{list}(z) ≡ \{ \begin{matrix}[ϵ]_{L′} & if z = ϵ \\ Q(cons)(Un_{list}(l), c) & if w = cons(l, c) for l ∈ List(X^{E}/R^{E}), c ∈ X^{E}/R^{E} \end{matrix}

where L′ ≡ List(X^{E})/ List(R^{E}) and in turn

Q(cons) : List(X^{E})/ List(R^{E}) × X^{E}/R^{E} ⟶ List(X^{E})/ List(R^{E})

is the unique map induced on the quotients List(X^{E})/ List(R^{E}) and X^{E}/R^{E} such that

Q(cons)([s]_{L′}, [x]_{X^{E}/R^{E}}) ≡ [cons(s, x)]_{L′}

for s ∈ List(X^{E}) and x ∈ X^{E}.

The inverse of Un_{list}, called Q(In_{list}), can be defined as the unique map induced on the quotient List(X^{E})/ List(R^{E}) by a map In_{list} : List(X^{E}) ⟶ List(X^{E}/R^{E}) preserving the relation List(R^{E}) and defined by induction on List(X)^{E} as follows: for w ∈ List(X^{E})

In_{list}(w) ≡ \{ \begin{matrix}ϵ & if w = ϵ \\ cons(In_{list}(s), [x]_{X^{E}/R^{E}}) & if w = cons(s, x) for s ∈ List(X^{E}), x ∈ X^{E} \end{matrix}

In order to show that In_{list} preserves the relation List(R^{E}), namely that if List(R^{E})(w, w′) holds then In_{list}(w) =_{List(X^{E}/R^{E})} In_{list}(w′) holds, too, we prove by induction on natural numbers that In_{list}(part_{n}(w)) =_{List(X^{E}/R^{E})} In_{list}(part_{n}(w′)) holds.

Now, we are ready to prove:

6.3. Theorem. Both the syntactic categories C_{T_{pn}} and C_{T_{au}} are equivalent to A_{in}.

Proof. Since by proposition 4.10 we know that A_{in} is a list-arithmetic pretopos, by the initiality of C_{T_{pn}} and of C_{T_{au}}, as stated in theorem 3.5, there exist an arithmetic pretopos functor J_{pn} : C_{T_{pn}} ⟶ A_{in} and a list-arithmetic pretopos functor J_{au} : C_{T_{au}} ⟶ A_{in} defined on objects and morphisms through the interpretation of T_{pn} and of T_{au} in A_{in}, respectively, as described in [Mai05a].

Then, note that J_{pn} · E_{pn} and J_{au} · E_{au} are both naturally isomorphic to Y. Indeed, since the interpretation of a predicate P in the initial Skolem category turns out to be isomorphic to Y(P) thinking of P as a morphism, eq(P, 1) =_{S_{in}} P holds and Y preserves finite limits (see [CV98]), then the interpretation of E_{pn}(P) is still isomorphic to Y(P) and the same happens for morphisms.

Hence, we get Y ≃ J_{pn} · E_{pn} ≃ J_{pn} · (Ê_{pn} · Y) ≃ (J_{pn} · Ê_{pn}) · Y and by the uniqueness property of the exact completion we conclude that J_{pn} · Ê_{pn} is naturally isomorphic to the identity functor. The same argument lets us conclude that J_{au} · Ê_{au} is also isomorphic to the identity functor.

Moreover, being C_{T_{pn}} the initial up to iso arithmetic pretopos and C_{T_{au}} the initial up to iso list-arithmetic pretopos, thanks to theorem 3.5 we also get that Ê_{pn} · J_{pn} is naturally isomorphic to the identity functor and so is Ê_{au} · J_{au}. Therefore, we conclude that both C_{T_{pn}} and C_{T_{au}} are equivalent to A_{in}.

6.4. Corollary. The initial arithmetic pretopos C_{T_{pn}} is equivalent to the initial listarithmetic pretopos C_{T_{au}}.

From this corollary we deduce that parameterized list objects are definable in the initial arithmetic pretopos via the equivalences in theorem 6.3. But it is worth noticing also here, as after corollary 5.4, that, since such equivalences make use of interpretation functors defined by induction on type and term constructors, we can not directly deduce that any arithmetic pretopos is list-arithmetic.

This is not an exceptional fact: consider for example that the initial finite product category and the initial finite limit category coincide with the trivial category with one object and one arrow.

We end by leaving as an open problem whether a generic arithmetic pretopos is also list-arithmetic.

7. Free internal categories and diagrams in a list-arithmetic pretopos

In this section we show how to define free internal categories and diagrams within a listarithmetic pretopos by means of its internal language (first shown in [Mai99b]). Recall that any list-arithmetic pretopos U is equivalent to the syntactic category C_{T (U)} built out of its internal type theory T (U). This type theory is obtained from T_{au} by adding specific axioms regarding the proper dependent types and terms of U and their corresponding equalities valid in U, as described in [Mai05a].

The use of the internal language is helpful here to perform proofs by induction. In particular, in building free internal categories and diagrams a key difficulty is to define operations on proper subtypes of list types with no specific recursion principle available. We overcome this difficulty by defining such operations by recursion on natural numbers through iteration of suitable operations. And here the use of a logical/type theoretic language in which to perform inductions as usual is more helpful than the categorical reasoning via universal properties.

This technique has already been applied to prove that the slice categories of a locos enjoy list objects in section 3.8. Moreover, it is also the same technique that one can adopt to prove that in a Skolem category the natural numbers object N is a list object over itself as stated in proposition 4.4. Actually it is enough to work in a regular locos to build free internal categories and diagrams as shown here.

7.1. Free internal categories. Given a graph G ≡ (G_{0}, G_{1}, dm_{G}, cd_{G}) internal to a list-arithmetic pretopos U

\xymatrix{G_{1} \ar[r]^{^{dm^{G}}} \ar[r]_{_{cd_{G}}} & G_{0}}

we build the free internal category generated from it. For a general account on these concepts about internal category theory we refer to [Joh77] or [MM92] or [Joh02a].

7.2. Definition. Given a graph G ≡ (G_{0}, G_{1}, dm_{G}, cd_{G}) internal to U, we define the category C^{G} as a candidate to be the free internal category generated from G as follows.

The objects of C^{G} are defined as the graph objects C^{G}_{0} ≡ G_{0}.

The morphisms of C^{G} are defined as the coproduct of the graph objects G_{0} representing the identity maps with lists of composable graph arrows represented by Ĉ^{G}_{1}:

C^{G}_{1} ≡ G_{0} ⊕ Ĉ^{G}_{1}

where Ĉ^{G}_{1} is formally defined as the equalizer of the set of non-empty lists of composable arrows, namely lists of arrows ⌊f_{1}, …, f_{n}⌋ such that ⌊dm_{G}(f_{2}), …, dm_{G}(f_{n})⌋, that is frt · Lst(dm_{G})([f_{1}, …, f_{n}]), is equal to the list ⌊cd_{G}(f_{1}), …, cd_{G}(f_{n−1})⌋, that is bck · Lst(cd_{G})(⌊f_{1}, …, f_{n}⌋) (see the definition of such operations in the appendix):

\xymatrix{Ĉ^{G}_{1} \ar@{^{(}->}[r] & List^{∗}(G_{1}) \ar[r]^{frt·Lst(dm_{G})} \ar[r]_{bck·Lst(cd_{G})} & List(G_{0})}

where

Ĉ^{G}_{1} ≡ Σ_{w∈List^{∗}(G_{1})} frt · Lst(dm_{G})(w) =_{List(G_{0})} bck · Lst(cd_{G})(w)

The domain morphism dm_{C^{G}} : C^{G}_{1} ⟶ C^{G}_{0} is defined as the coproduct morphism of the identity with the domain of the first morphism of the list

dm_{C^{G}} ≡ id ⊕ (dm_{G} · (fst · π_{1}))

while the codomain morphism cd_{C^{G}} : C^{G}_{1} ⟶ C^{G}_{0} is defined as the coproduct morphism of the identity with the codomain of the last morphism of the list

cd_{C^{G}} ≡ id ⊕ (cd_{G} · (las · π_{1}))

The unit e_{C^{G}} : C^{G}_{0} → C^{G}_{1} is defined as the first injection

e_{C^{G}}(x) ≡ inl(x) for x ∈ C^{G}_{0}

It follows immediately that

dm_{C^{G}} · e_{C^{G}} = id cd_{C^{G}} · e_{C^{G}} = id

The composition of morphisms

Cmp_{C^{G}}(w) ∈ C^{G}_{1} [w ∈ C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1}]

where C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1} is the vertex of the pullback of dm_{C^{G}} along cd_{C^{G}}

C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1} ≡ Σ_{f∈C^{G}_{1}} Σ_{g∈C^{G}_{1}} cd_{C^{G}}(f) =_{C^{G}}_{0} dm_{C^{G}}(g)

is defined by cases after noting that by distributivity of coproducts with respect to pullbacks we have

\begin{matrix}(G_{0} ⊕ Ĉ^{G}_{1}) ×_{C^{G}}_{0} (G_{0} ⊕ Ĉ^{G}_{1}) \\ ≅ (G_{0} ×_{C^{G}}_{0} G_{0}) ⊕ (G_{0} ×_{C^{G}}_{0} Ĉ^{G}_{1}) ⊕ (Ĉ_{1}^{G} ×_{C^{G}}_{0} G_{0}) ⊕ (Ĉ^{G}_{1} ×_{C^{G}}_{0} Ĉ^{G}_{1}) \end{matrix}

In the next we simply write ⟨z_{1},_{C^{G}}_{0} z_{2}⟩ for ⟨z_{1}, ⟨z_{2}, eq⟩⟩ given z_{1}, z_{2} ∈ C^{G}_{1} such that cd_{C^{G}}(z_{1}) =_{C^{G}}_{0} dm_{C^{G}}(z_{2}) holds.

In detail the composition is defined by cases as follows

Cmp_{C^{G}}(⟨z_{1},_{C^{G}}_{0} z_{2}⟩) ≡ \begin{cases}inl(x) & if z_{1} = inl(x) = z_{2} \\ & for x ∈ G_{0} \\ inr(s) & if z_{1} = inl(x) and z_{2} = inr(s) \\ & for x ∈ G_{0} and s ∈ Ĉ^{G}_{1} \\ inr(s) & if z_{2} = inl(y) and z_{1} = inr(s) \\ & for y ∈ G_{0} and s ∈ Ĉ^{G}_{1} \\ inr(⟨⌊π_{1}(s_{1}), π_{1}(s_{2})⌋, eq⟩) & if z_{1} = inr(s_{1}) and z_{2} = inr(s_{2}) \\ & for s_{1} ∈ Ĉ^{G}_{1} and s_{2} ∈ Ĉ^{G}_{1} \end{cases}

It is easy to check that this is well defined and that the composed morphism has the right domain and codomain:

dm_{C^{G}} · π′_{1} = dm_{C^{G}} · Cmp_{C^{G}} cd_{C^{G}} · π′_{2} = cd_{C^{G}} · Cmp_{C^{G}}

where π′_{1} and π′_{2} are respectively the first and second projection of the pullback of dm_{C^{G}} along cd_{C^{G}}.

Moreover, given that the operation of appending a list to another is associative, it follows that the composition is associative, too

Cmp_{C^{G}} · (Cmp_{C^{G}} × id) · σ = Cmp_{C^{G}} · (id × Cmp_{C^{G}})

where σ is isomorphism from C^{G}_{1} ×_{C^{G}}_{0} (C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1}) to (C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1}) ×_{C^{G}}_{0} C^{G}_{1}.

Finally it is easy to show that the defined composition admits the morphism e_{C^{G}} as identity:

Cmp_{C^{G}} · (e_{C^{G}} × id) = π′_{2} Cmp_{C^{G}} · (id × e_{C^{G}}) = π′_{1}

Then, we are ready to prove:

7.3. Proposition. Internally to any list-arithmetic pretopos U, given a graph G ≡ (G_{0}, G_{1}, dm_{G}, cd_{G})

\xymatrix{G_{1} \ar[r]^{^{dm^{G}}} \ar[r]_{_{cd_{G}}} & G_{0}}

then the category C^{G} ≡ (C^{G}_{0}, C^{G}_{1}, dm_{C^{G}}, cd_{C^{G}}, e_{C^{G}}, Cmp_{C^{G}}) defined above in definition 7.2

\xymatrix{C^{G}_{1} \ar[r]^{^{dm^{C^{G}}}} \ar[r]_{_{cd_{C^{G}}}} & C^{G}_{0} \ar[l]|{e_{C^{G}}}} Cmp_{C^{G}} : C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1} ⟶ C^{G}_{1}

is the free internal category generated by it.

Proof. Let C^{G}_{0} and C^{G}_{1} be defined as above. Then we define the injection from the graph into its claimed free internal category as follows: j_{0} : G_{0} ⟶ C^{G}_{0} is the identity map, that is j_{0} ≡ id_{G_{0}} in U, and j_{1} : G_{1} → C^{G}_{1} is defined as j_{1}(f) ≡ inr(⟨⌊f⌋, eq⟩) for f ∈ G_{1}. Then, (j_{0}, j_{1}) is a graph morphism from G to C^{G} since it satisfies

dm_{C^{G}} · j_{1} = j_{0} · dm_{G} cd_{C^{G}} · j_{1} = j_{0} · cd_{G}

Now, we prove that (j_{0}, j_{1}) has the universal property of lifting a graph morphism (ψ_{0}, ψ_{1}) from G to an internal category D to a unique internal functor (ψ_{0}^{lf}, ψ_{1}^{lf}) from C^{G} to D such that ψ_{0}^{lf} · j_{0} = ψ_{0} and ψ_{1}^{lf} · j_{1} = ψ_{1}

\xymatrix{G \ar[r]^{(j_{0},j_{1})} \ar[dr]_{(ψ_{0},ψ_{1})} & C^{G} \ar[d]^{(ψ_{0}^{lf},ψ_{1}^{lf})} \\  & D}

Given an internal category D ≡ (D_{0}, D_{1}, dm_{D}, cd_{D}, e_{D}, Cmp_{D})

\xymatrix{D_{1} \ar[r]^{^{dm^{D}}} \ar[r]_{_{cd_{D}}} & D_{0} \ar[l]|{e_{D}}} Cmp_{D} : D_{1} ×_{D_{0}} D_{1} ⟶ D_{1}

and a graph morphism (ψ_{0}, ψ_{1}) where ψ_{0} : G_{0} → D_{0} and ψ_{1} : G_{1} → D_{1} are maps in U satisfying

dm_{D} · ψ_{1} = ψ_{0} · dm_{G} cd_{D} · ψ_{1} = ψ_{0} · cd_{G}

we define an internal functor

ψ_{0}^{lf} : C^{G}_{0} ⟶ D_{0} ψ_{1}^{lf} : C^{G}_{1} ⟶ D_{1}

such that ψ_{0}^{lf} · j_{0} = ψ_{0} and ψ_{1}^{lf} · j_{1} = ψ_{1} as follows. Being C_{0} = G_{0}, we obviously define

ψ_{0}^{lf} ≡ ψ_{0}

Then, in order to define ψ_{1}^{lf} : C^{G}_{1} → D_{1}, recall that C^{G}_{1} = G_{0} ⊕ Ĉ^{G}_{1}. Hence we define ψ_{1}^{lf} as a coproduct morphism of the action on identity morphisms and on lists of composable graph morphisms. To identity morphisms we associate the corresponding identity ones by using ψ_{0}. Instead to a list of composable G-graph morphisms we associate the composition of their values as D-morphisms via ψ_{1}. Hence, we define

ψ_{1}^{lf} ≡ (e_{D} · ψ_{0}) ⊕ (app · C(ψ_{1}))

where

C(ψ_{1}) : Ĉ^{G}_{1} ⟶ Ĉ^{D}_{1}

is just the lifting of ψ_{1} between the corresponding list parts defined as follows: for z ∈ Ĉ^{G}_{1}

C(ψ_{1})(z) ≡ ⟨Lst(ψ_{1})(z_{1}), eq⟩ ∈ Ĉ^{D}_{1}

where z_{1} ≡ π_{1}(z) and

app : Ĉ^{D}_{1} ⟶ D_{1}

is a map sending a list of composable morphisms of D_{1} into their composition. At this point note that we can not define app by using an inductive elimination rule on Ĉ^{D}_{1} as for List^{∗}(G_{1}) in proposition A.4 of the appendix. But we define app by iteration: we first fix a list s obtained by first projection from Ĉ^{D}_{1}, then we compose the first element of the list with the second and so on, namely to define the value of app(s) we iterate the described operation for a number of times equal to the length of s minus one (we start to apply from zero!). Formally, we define app as follows: for s ∈ Ĉ^{D}_{1}

app(s) ≡ ãpp(s, lh(s_{1}) − 1)

by using the operation

ãpp(s, n) ∈ D_{1} [s ∈ Ĉ^{D}_{1}, n ∈ N]

defined in turn by induction on natural numbers as follows:

ãpp(s, 0) ≡ p_{1}(s_{1})
ãpp(s, n + 1) ≡ \begin{cases}Cmp_{D}(⟨ãpp(s, n),_{D_{0}} p_{n+2}(s_{1})⟩) & if n + 2 ≤ lh(s_{1}) \\ ãpp(s, n) & if n + 2 > lh(s_{1}) \end{cases}

where s_{1} ≡ π_{1}(s).

Actually, in order to guarantee that ãpp is well-defined we need to know that ãpp(s, n) has the same codomain as the domain of p_{n+2}(s_{1}) and we have to add this information when defining it by induction. Therefore, formally ãpp is obtained by applying the first projection on the corresponding term of type

Σ_{x∈D_{1}} ((cd_{D}(x) =_{D_{0}} dm_{D}(p_{n+2}(s_{1})) ∧ n + 2 ≤ lh(s_{1})) ∨ n + 2 > lh(s_{1})) [s ∈ Ĉ^{D}_{1}, n ∈ N]

defined by induction on natural numbers essentially as ãpp together with a proof of the needed extra information.

Clearly, it follows that ψ_{1}^{lf} · j_{1} = ψ_{1}. Moreover, we can prove that ψ_{1}^{lf} is functorial, i.e. it satisfies the following equations:

dm_{D} · ψ_{1}^{lf} = ψ_{0}^{lf} · dm_{C^{G}} cd_{D} · ψ_{1}^{lf} = ψ_{0}^{lf} · cd_{C^{G}}
ψ_{1}^{lf} · e_{C^{G}} = e_{D} · ψ_{0}^{lf}
Cmp_{D} · (ψ_{1}^{lf} × ψ_{1}^{lf}) = ψ_{1}^{lf} · Cmp_{C^{G}}

In order to prove the first two equations, we show that the following equations hold, for s ∈ Ĉ^{D}_{1},

dm_{D}(ãpp(s, n)) =_{D_{0}} dm_{D}(p_{1}(s_{1})) cd_{D}(ãpp(s, n)) =_{D_{0}} cd_{D}(p_{n+1}(s_{1}))

by induction on n ∈ N.

The third equation follows easily. Instead in order to prove the last equation, for z ∈ Ĉ^{D}_{1} and w ∈ Ĉ^{D}_{1} such that cd_{C^{D}}(inr(z)) =_{D_{0}} dm_{C^{D}}(inr(w)) we derive the validity of the following: for n ≤ lh(z_{1}) − 1

ãpp(⟨⌊z_{1}, w_{1}⌋, eq⟩, n) =_{D_{1}} ãpp(z_{1}, n)

and for n ≤ lh(w_{1}) − 1

Cmp_{D}(ãpp(z, l_{1}),_{D_{0}} ãpp(w, n)) =_{D_{1}} ãpp(⟨⌊z_{1}, w_{1}⌋, eq⟩, l_{1} + n + 1)

where l_{1} = lh(z_{1}) − 1 and z_{1} ≡ π_{1}(z) and w_{1} ≡ π_{1}(w). The actual proof is derived by induction on n ∈ N towards the type obtained by enriching the above equations with the constrain on n in disjunctive form, as done to derive ãpp.

Now we end by proving the uniqueness of (ψ_{0}^{lf}, ψ_{1}^{lf}). Suppose that there exists an internal functor given by ρ_{0} : C^{G}_{0} → D_{0} and ρ_{1} : C^{G}_{1} → D_{1} such that ρ_{0} · j_{0} = ψ_{0} and ρ_{1} · j_{1} = ψ_{1}. Then, since j_{0} = id we get that ρ_{0} = ψ_{0}^{lf} follows trivially. It remains to prove that also ρ_{1} = ψ_{1}^{lf}. To this purpose we prove by induction on n ∈ N the following: for z ∈ Ĉ^{G}_{1} and n ≥ 1

ρ_{1}(inr({ \atop part_{n}}(z))) =_{D_{1}} ψ_{1}^{lf}(inr({ \atop part_{n}}(z)))

where { \atop part_{n}}(z) ≡ ⟨part_{n}(z_{1}), eq⟩ and z_{1} ≡ π_{1}(z).

Then, by elimination on the sum type C^{G}_{1} and knowing that part_{lh(s)}(s) =_{List^{∗}(G_{1})} s holds for s ∈ List^{∗}(G_{1}), we get that ψ_{1}^{lf}(z) =_{D_{1}} ρ_{1}(z) holds for z ∈ C^{G}_{1}.

Therefore, we conclude that (ψ_{0}^{lf}, ψ_{1}^{lf}) is the unique internal functor obtained by lifting (ψ_{0}, ψ_{1}). This ends the proof that C^{G} is the free category internally to a list-arithmetic pretopos.

7.4. Free internal diagrams. Applying the same technique adopted to build free internal categories, we can also prove that in any list-arithmetic pretopos free internal categorical diagrams exist. Also here, the key point is to show the universal property of the free internal diagram by defining an operation on a proper subtype of a list type by iteration on natural numbers.

7.5. Proposition. In any list-arithmetic pretopos U, given the internal graph G ≡ (G_{0}, G_{1}, dm_{G}, cd_{G})

\xymatrix{G_{1} \ar[r]^{^{dm^{G}}} \ar[r]_{_{cd_{G}}} & G_{0}}

and the internal diagram π_{0} : F ⟶ G_{0} with the action

μ : F ×_{G_{0}} G_{1} ⟶ F

such that the following diagram commutes

\xymatrix{F ×_{G_{0}} G_{1} \ar[r]^{π_{2}} \ar[d]^{μ} & G_{1} \ar[d]_{_{cd_{G}}} \\ F \ar[r]_{π_{0}} & G_{0}}

where F ×_{G_{0}} G_{1} is the vertex of the pullback of dm_{G} along π_{0}

F ×_{G_{0}} G_{1} ≡ Σ_{f∈F} Σ_{z∈G_{1}}π_{0}(f) =_{G_{0}} dm_{G}(z)

and π_{2} its second projection, we can lift μ to an unique action on C^{G}_{1}

μ^{lf} : F ×_{C^{G}}_{0} C^{G}_{1} ⟶ F

where F ×_{C^{G}}_{0} C^{G}_{1} is the vertex of the pullback of dm_{C^{G}} along π_{0}

F ×_{C^{G}}_{0} C^{G}_{1} ≡ Σ_{f∈F} Σ_{z∈C^{G}_{1}}π_{0}(f) =_{G_{0}} dm_{C^{G}}(z)

that is μ^{lf} is an internal diagram on the underlying graph of the free category C^{G} ≡ (C^{G}_{0}, C^{G}_{1}, dm_{C^{G}}, cd_{C^{G}}, e_{C^{G}}, Cmp_{C^{G}}) such that

\xymatrix{F ×_{G_{0}} C^{G}_{1} \ar[r]^{π′_{2}} \ar[d]^{μ^{lf}} & C^{G}_{1} \ar[d]_{_{cd_{C^{G}}}} \\ F \ar[r]_{π_{0}} & _{C^{G}_{0}}}

π_{0} · μ^{lf} = cd_{C^{G}} · π′_{2}

where π′_{1} and π′_{2} are respectively the first and the second projections of the pullback of dm_{C^{G}} along π_{0}, and in addition also the following diagrams commute

\xymatrix{F ×_{C^{G}}_{0} C^{G}_{0} \ar[r]^{id×e_{C^{G}}} \ar[dr]_{π′_{1}} & F ×_{C^{G}}_{0} C^{G}_{1} \ar[d]_{μ^{lf}} & F ×_{C^{G}}_{0} (C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1}) \ar[r]^{(μ^{lf}×id)·σ} \ar[d]_{id×Cmp_{C^{G}}} & F ×_{C^{G}}_{0} C^{G}_{1} \ar[d]^{μ^{lf}} \\  & F & F ×_{C^{G}}_{0} C^{G}_{1} \ar[r]_{μ^{lf}} & F}

where

F ×_{C^{G}}_{0} (C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1})
≡ Σ_{f∈F} Σ_{z_{1}∈C^{G}_{1}}Σ_{z_{2}∈C^{G}_{1}}π_{0}(f) =_{G_{0}} dm_{C^{G}}(z_{1}) ∧ cd_{C^{G}}(z_{1}) =_{G_{0}} dm_{C^{G}}(z_{2})

is the vertex of the pullback along π′_{2} of the first projection of the pullback of dm_{C^{G}} along cd_{C^{G}} and σ is the isomorphism from F ×_{C^{G}}_{0} (C^{G}_{1} ×_{C^{G}}_{0} C^{G}_{1}) to (F ×_{C^{G}}_{0} C^{G}_{1}) ×_{C^{G}}_{0} C^{G}_{1}.

Proof. In order to define the action μ^{lf}, note that by distributivity of coproducts with respect to pullbacks we get

F ×_{C^{G}}_{0} C^{G}_{1} = F ×_{C^{G}}_{0} (G_{0} ⊕ Ĉ^{G}_{1}) ≃ (F ×_{G_{0}} G_{0}) ⊕ (F ×_{G_{0}} Ĉ^{G}_{1})

Hence, by the elimination rule on the sum type we define μ^{lf} : F ×_{C^{G}}_{0} C^{G}_{1} ⟶ F as follows: for f ∈ F, z ∈ C^{G}_{1} such that ⟨f,_{C^{G}}_{0} z⟩ ∈ F ×_{C^{G}}_{0} C^{G}_{1}

μ̃^{lf}(⟨f,_{C^{G}}_{0} z⟩) ≡ \begin{cases}f & if z = inl(x) for x ∈ G_{0} \\ μ̃^{lf}(f, s, lh(s_{1}) − 1) & if z = inr(s) for s ∈ Ĉ^{G}_{1} \\ & such that π_{0}(f) =_{G_{0}} dm_{C^{G}}(inr(s)) \end{cases}

where s_{1} ≡ π_{1}(s) and in turn

μ̃^{lf}(f, s, n) ∈ F [f ∈ F, s ∈ Ĉ^{G}_{1}, d ∈ π_{0}(f) =_{G_{0}} dm_{C^{G}}(inr(s))]

is defined as follows:

μ̃^{lf}(f, s, 0) ≡ μ(⟨f,_{G_{0}} p_{1}(s_{1})⟩)
μ̃^{lf}(f, s, n + 1) ≡ \begin{cases}μ(⟨μ̃^{lf}(f, s, n),_{G_{0}} p_{n+2}(s_{1})⟩) & if n + 2 ≤ lh(s_{1}) \\ μ̃^{lf}(f, s, n) & if n + 2 > lh(s_{1}) \end{cases}

But in order to assure the well definedness of the above definition we need to know the validity of π_{0}(μ̃^{lf}(f, s, n)) =_{G_{0}} dm_{G}(p_{n+2}(s_{1})). Therefore, μ̃^{lf} is formally obtained by applying the first projection on the corresponding term of type

Σ_{x∈F} ((π_{0}(x) =_{G_{0}} dm_{G}(p_{n+2}(s_{1})) ∧ n + 2 ≤ lh(s_{1})) ∨ n + 2 > lh(s_{1})) [s ∈ Ĉ^{G}_{1}, n ∈ N]

defined by induction on natural numbers essentially as ãpp in the previous section together with a proof of the needed extra information.

It follows that μ^{lf} is an internal diagram, namely that

π_{0} · μ^{lf} = cd_{C^{G}} · π′_{2} μ^{lf} · (id × e_{C^{G}}) = π′_{1} μ^{lf} · (id × Cmp_{C^{G}}) = μ^{lf} · (μ^{lf} × id) · σ

and that μ^{lf} is unique with arguments similar to those used for ψ_{1}^{lf} in theorem 7.3.

8. Conclusions

As promised we have shown here the following facts:

• arithmetic universes built by Joyal are list-arithmetic pretopoi;

• the initial arithmetic universe among Joyal’s constructions is equivalent to the initial list-arithmetic pretopos;

• any list-arithmetic pretopos enjoys free categories and diagrams generated from

graphs. We think that these three facts provide the claimed justification for the identification of the general notion of arithmetic universe with that of list-arithmetic pretopos:

8.1. Definition. An arithmetic universe is a list-arithmetic pretopos.

We leave as an open problem whether the notion of arithmetic pretopos, namely a pretopos with a parameterized natural numbers object, can be taken as a notion of arithmetic universe. This suspicion is supported by the fact that the initial arithmetic pretopos is equivalent to the initial arithmetic universe built by Joyal. However we doubt that any arithmetic pretopos supports free internal categories and diagrams or is listarithmetic.

Finally, our general definition of arithmetic universe as list-arithmetic pretopos is equivalent to that used in a recent talk by André Joyal [Joy05].

Acknowledgements. My acknowledgements go first to Martin Hyland, who proposed me to work on arithmetic universes and helped me with many fruitful discussions during my staying in Cambridge. Many thanks also to Steve Vickers for providing me Gavin Wraith’s unpublished notes [Wra85] with the master’s thesis of his student [Mor96] and to Robin Cockett for sending Roland’s master’s thesis [Rol76]. Then, I wish also to thank Pino Rosolini, Giovanni Sambin, Paul Taylor and Silvio Valentini for their generous promptness in discussing my research work. Finally, I am very grateful to André Joyal for his interest in this work and for letting me know his draft about Gödel incompleteness.

A. Appendix: Useful operations on list types

Here, we describe some very useful operations on list types following the notation in remark 3.3.

We warn the reader that when defining an operation by elimination on the list type we simply write the base and inductive steps necessary to define it instead of writing the whole resulting proof-term.

A.1. Definition. We define the length of a list lh(s) ∈ List(A) [s ∈ List(A)] by the elimination rule on the list type as follows

lh(ϵ) ≡ 0 lh(⌊s, a⌋) ≡ lh(s) + 1

A.2. Definition. Given a term ϕ(x) ∈ B [x ∈ A] we lift this term on lists by defining

Lst(ϕ)(s) ∈ List(B) [s ∈ List(A)]

by elimination on the list type as follows

Lst(ϕ)(ϵ) ≡ ϵ Lst(ϕ)(⌊s, a⌋) ≡ ⌊Lst(ϕ)(s), ϕ(a)⌋

Now, we define the type of non-empty lists which also enjoys a specific induction.

A.3. Definition. The type of non-empty lists is defined as

List^{∗}(A) ≡ Σ_{t∈List(A)}lh(t) ≥ 1

where n ≥ m may be defined as ∃_{y∈N} n =_{N} m + y.

In the next, given a non-empty list l ∈ List(A) such that p ∈ lh(l) ≥ 1 we simply write

l^{∗} ∈ List^{∗}(A) instead of ⟨l, p⟩ ∈ List^{∗}(A)

Observe that we can think of List^{∗}(A) as the inductive type with the following constructors:

• the basic constructors of List^{∗}(A) are the one element lists of A: for a ∈ A

⌊a⌋^{∗} ∈ List^{∗}(A)

• the list constructor cons of List(A) produces a constructor

cons_{List}^{∗}(z, a) ∈ List^{∗}(A) [z ∈ List^{∗}(A), a ∈ A]

defined as cons_{List}^{∗}(z, a) ≡ cons(z_{1}, a)^{∗} where z_{1} ≡ π_{1}(z).

In order to define operations on the type List^{∗}(A) of non-empty lists, we can use an elimination rule analogous to that one for List(A). This elimination says that in order to define an operation on the type List^{∗}(A) we first define the operation on the one element lists, which is the base case, and then we specify how to define it on the lists obtained by adding a new element to a list on which the operation is supposed to be already defined, which is the inductive case.

A.4. Proposition. [Induction on non-empty lists] Given the type B(s) [s ∈ List^{∗}(A)] and the following terms

(base case)  d_{1}(x) ∈ B(⌊x⌋^{∗}) [x ∈ A]
(inductive case) d_{2}(s, y, w) ∈ B(cons_{List}^{∗}(s, y)) [s ∈ List^{∗}(A), y ∈ A, w ∈ B(s)]

there exists a term El_{List}^{∗}(z) ∈ B(z) [z ∈ List^{∗}(A)] such that for s ∈ List^{∗}(A), x ∈ A, y ∈ A

El_{List}^{∗}(⌊x⌋^{∗}) = d_{1}(x)
El_{List}^{∗}(cons_{List}^{∗}(s, y)) = d_{2}(s, y, El_{List}^{∗}(s))

Proof. By using the hypothesis of our statement we can derive a proof of the type

Σ_{z′∈List(A)^{∗}}(B(z′) × w =_{List(A)} π_{1}(z′)) + w =_{List(A)} ϵ

by induction on w ∈ List(A). Then, observe that for z ∈ List^{∗}(A), since π_{1}(z) =_{List(A)} ϵ is false by sum disjointness (with a proof similar to that of proposition 5.1), and since z = z′ ∈ List^{∗}(A) if π_{1}(z) =_{List(A)} π_{1}(z′) holds, we then conclude a proof of B(z) as claimed.

A.5. Remark. In order to facilitate the definition of operations on non-empty lists, here and in the main body of this paper we simply write

l ∈ List^{∗}(A) if l ∈ List(A) with a proof of lh(l) ≥ 1

and conversely also simply

l ∈ List(A) if l ∈ List^{∗}(A)

A.6. Definition. On List^{∗}(A) we define the operation frt(s) ∈ List(A) [s ∈ List^{∗}(A)] taking the front of a non-empty list: for s ∈ List^{∗}(A) and a ∈ A

frt(⌊a⌋) ≡ ϵ frt(⌊s, a⌋) ≡ ⌊frt(s), a⌋

and the operation bck(s) ∈ List(A) [s ∈ List^{∗}(A)] taking the back of a non-empty list: for s ∈ List^{∗}(A) and a ∈ A

bck(⌊a⌋) ≡ ϵ bck(⌊s, a⌋) ≡ s

Moreover, we define the operation fst(s) ∈ A [s ∈ List^{∗}(A)] selecting the first element of a list as follows: for s ∈ List^{∗}(A) and a ∈ A

fst(⌊a⌋) ≡ a fst(⌊s, a⌋) ≡ fst(s)

and the operation las(s) ∈ A [s ∈ List^{∗}(A)] selecting the last element of a list as follows: for s ∈ List^{∗}(A) and a ∈ A

las(⌊a⌋) ≡ a las(⌊s, a⌋) ≡ a

Then, we define projections on a non-empty list. For every n ∈ N we define the n-th projection p_{n}(s) ∈ A [s ∈ List^{∗}(A), n ∈ N] by the elimination rule on non-empty lists as follows

p_{n}(s) ≡ \begin{cases}a & if s ≡ ⌊a⌋ \\ p_{n}(s′) & if s ≡ ⌊s′, a⌋ and n ≤ lh(s′) \\ a & if s ≡ ⌊s′, a⌋ and n > lh(s′) \end{cases}

Finally, we use projections to define the n-th part of a list

part_{n}(s) ∈ List(A) [s ∈ List(A), n ∈ N]

by induction on natural numbers as follows: given a list s ∈ List(A)

part_{0}(s) ≡ ϵ
part_{n+1}(s) ≡ \begin{cases}⌊part_{n}(s), p_{n+1}(s)⌋ & if n + 1 ≤ lh(s) \\ part_{n}(s) & if n + 1 > lh(s) \end{cases}

References

[BCRS98] L. Birkedal, A. Carboni, G. Rosolini, and D. Scott. Type theory via exact categories (extended abstract). In Thirteenth Annual IEEE Symposium on Logic in Computer Science (Indianapolis, IN, 1998), IEEE Computer Soc., pages 188–198, 1998.

[Car95] A. Carboni. Some free constructions in realizability and proof theory. Journal of Pure and Applied Algebra, 103:117–148, 1995.

[CLW93] A. Carboni, S. Lack, and R.F.C. Walters. Introduction to extensive and distributive category. Journal of Pure and Applied Algebra, 84:145–158, 1993.

[CV98] A. Carboni and E.M. Vitale. Regular and exact completions. Journal of Pure and Applied Algebra, 125:79–116, 1998.

[Coc90] J.R.B. Cockett. List-arithmetic distributive categories: locoi. Journal of Pure and Applied Algebra, 66:1–29, 1990.

[dB91] N.G. de Bruijn. Telescopic mapping in typed lambda calculus. Information and Computation, 91:189–204, 1991.

[Hof95] M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Computer science logic (Kazimierz, 1994), volume 933 of Lecture Notes in Comput. Sci., pages 427–441, 1995.

[Hyl82] J.M.E. Hyland. The effective topos. In The L.E.J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), volume 110 of Stud. Logic Foundations Math., pages 165–216. North-Holland, Amsterdam-New York, 1982.

[JM95] A. Joyal and I. Moerdijk. Algebraic set theory, volume 220 of Lecture Note Series. Cambridge University Press, 1995.

[Joh77] P.T. Johnstone. Topos theory Academic Press, 1977.

[Joh02a] P.T. Johnstone. Sketches of an elephant: a topos theory compendium. Vol. 1, volume 43 of Oxford Logic Guides. The Clarendon Press, Oxford University Press, New York,, 2002.

[Joh02b] P. T. Johnstone. Sketches of an elephant: a topos theory compendium. Vol. ., volume 44 of Oxford Logic Guides. The Clarendon Press, Oxford University Press, New York,, 2002.

[Joy05] A. Joyal. The Gödel incompleteness theorem, a categorical approach. Cahiers de topologie et géometrie différentielle categoriques, 16(3), 2005. Short abstract of the talk given at the International conference Charles Ehresmann: 100 ans, Amiens, 7-9 October, 2005.

[LR03] F.W. Lawvere and R. Rosebrugh. Sets for mathematics. Cambridge University Press, 2003.

[Mai99a] M.E. Maietti. About effective quotients in constructive type theory. In W. Naraschewski T. Altenkirch and B. Reus, editors, Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31. 1999, volume 1657 of Lectures Notes in Computer Science, pages 164–178. Springer Verlag, 1999.

[Mai99b] M.E. Maietti. The typed calculus of arithmetic universes. Technical report, University of Birmingham, CSR-99-14, December 1999. Also Technical Report-University of Padova n.5 Dec. 1999.

[Mai03] M.E. Maietti. Joyal’s arithmetic universes via type theory. In Category Theory in Computer Science, 2002, volume 69 of Electronic Notes in Theoretical Computer Science. Elsevier, 2003.

[Mai05a] M.E. Maietti. Modular correspondence between dependent type theories and categories including pretopoi and topoi. Mathematical Structures in Computer Science, 15(6), 2005.

[Mai05b] M.E. Maietti. Reflection into models of finite decidable fp-sketches in an arithmetic universe. In Category Theory in Computer Science, 2004, volume 122 of Electronic Notes in Theoretical Computer Science, pages 105–126. Elsevier, 2005.

[Mar84] P. Martin-Löf. Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padua, June 1980. Bibliopolis, Naples, 1984.

[MM92] S. MacLane and I. Moerdijk. Sheaves in Geometry and Logic. A first introduction to Topos theory. Springer Verlag, 1992.

[MMdPR05] M.E. Maietti, P. Maneggia, V. de Paiva, and E. Ritter. Relating categorical semantics for intuitionistic linear logic. Applied Categorical Structures, 13(1):1–36, 2005.

[Mor96] A. Morrison. Reasoning in arithmetic universes. Master’s thesis, University of London - Imperial College of Science, Technology and Medicine, advisor: S. Vickers, September 1996.

[MR77] M. Makkai and G. Reyes. First order categorical logic, volume 611 of Lecture Notes in Mathematics. Springer Verlag, 1977.

[NPS90] B. Nordström, K. Peterson, and J. Smith. Programming in Martin-Löf’s Type Theory. Clarendon Press, Oxford, 1990.

[Odi89] P. Odifreddi. Classical recursion theory, volume 125 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., 1989.

[Pit00] A.M. Pitts. Categorical logic. In Oxford University Press, editor, Handbook of Logic in Computer Science, volume 5 of Oxford Sci. Publ., pages 39–128, 2000.

[Rol76] S. Roland. Essai sur les mathématiques algorithmiques. Master’s thesis, Université du Québec, Montréal - Maîtrise ès sciences (mathématiques), advisor: A. Joyal, January 1976.

[See84] R. Seely. Locally cartesian closed categories and type theory. Math. Proc. Cambr. Phyl. Soc., 95:33–48, 1984.

[Smi88] J. Smith. The independence of Peano’s fourth axiom from Martin Löf’s type theory without universes. Journal of Symbolic Logic, 53, 1988.

[Str91] Th. Streicher. Semantics of type theory. Birkhäuser, 1991.

[Tay05] P. Taylor. Inside every model of abstract Stone duality lies an arithmetic universe. In Category Theory in Computer Science, 2004, volume 122 of Electronic Notes in Theoretical Computer Science, pages 247–296. Elsevier, 2005.

[Wra85] G.C. Wraith. Notes on arithmetic universes and Gödel incompleteness theorems. Unpublished manuscript, 1985.

Dipartimento di Matematica Pura ed Applicata University of Padova via Belzoni n.7, 35100 Padova, Italy

Email: maietti@math.unipd.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/24/3/24-03.{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 Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Cuill Inc.: valeria@cuill.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Tom Leinster, University of Glasgow, T.Leinster@maths.gla.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr 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 Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.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