Joyal’s arithmetic universe as list-arithmetic pretopos

Maria Emilia Maietti Dipartimento di Matematica Pura ed Applicata University of Padova via Belzoni n.7, 35100 Padova, Italy maietti@math.unipd.it

January 26, 2004

Abstract

Andrè Joyal constructed arithmetic universes to provide a categorical proof of Gödel incompleteness results. He built them in three stages: he first took a Skolem theory, then the category of its predicates and finally he made the exact completion out of the latter.

Here, we prove that the construction of an initial arithmetic universe is equivalent to that of an initial list-arithmetic pretopos and also of an initial arithmetic pretopos. The initial list-arithmetic pretopos is built out of its internal language formulated as a dependent typed calculus in the style of Martin-Löf’s extensional type theory. Analogously, we prove that the second stage of Joyal’s construction is equivalent to taking an initial arithmetic lextensive category or an initial regular locos.

Finally, we show the existence of free internal categories and diagrams in any list-arithmetic pretopos as in any of Joyal’s arithmetic universes.

All these results motivate us to propose the notion of list-arithmetic pretopos as the general definition of arithmetic universe.

keywords: Dependent type theory, pretopoi, categorical logic.

1 Introduction

In category theory some kinds of category like topoi and pretopoi can be thought of as universes in which to develop mathematics (see [Joh77, JM95, MM92]). Arithmetic universes provide further examples of such universes.

The notion of arithmetic universe was introduced by Andrè Joyal in some lectures given in the seventies, all still unpublished. The main purpose was to provide a categorical proof of Gödel incompleteness theorems based on the fact that any arithmetic universe contains an initial one. Arithmetic universes are built in three stages: first, take a Skolem theory, namely a cartesian category with a parameterized natural numbers object where all the objects are finite products of the natural numbers object, then take the category of its predicates and finally add quotients by doing its exact completion. The outcome gives in particular a pretopos with parameterized list objects, here called list-arithmetic pretopos. An initial arithmetic universe is obtained by performing the described construction starting from an initial Skolem theory.

Now a question arises: what is the general categorical definition of arithmetic universe such that we can build free internal categories and diagrams as in any of Joyal’s arithmetic universes? In [Mor96] and [Wra85] it is more or less said that it 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, for at least two reasons. First, we prove that the construction of an initial arithmetic universe amounts to be equivalent to that of an initial list-arithmetic pretopos. Second, we show that free internal categories and diagrams exist in any list-arithmetic pretopos as Joyal proved for any of his arithmetic universes. Actually, since we prove that the construction of an initial arithmetic universe is equivalent to that of an initial arithmetic pretopos as well, we could also choose the notion of arithmetic pretopos as the general definition of arithmetic universe. But, we do not do that since we think that list constructors are essential to build free internal categories and diagrams.

All these results are obtained by employing internal languages of the considered categories. In particular that of list-arithmetic pretopoi, already introduced in [Mai99, Mai01], turns out to be an internal language for any initial arithmetic universe. Knowing an internal language for a category means that we can treat the category as a syntactic one built out of its internal language. This link between a calculus and a class of categories is a stronger than that established by a soundness and completeness theorem.

The internal type theory of list-arithmetic pretopoi, and hence of general arithmetic universes as defined here, is based on the dependent typed calculus Au formulated in the style of extensional Martin-Löf’s type theory [Mar84]. In designing the internal language of a category (at least lex) we are led to produce an extensional type theory since we view the equality between morphisms of the category as the definitional equality between terms. Extensional Martin-Löf’s type theory differs from the intensional Martin-Löf’s Constructive Type Theory [NPS90] for what regards its computational contents: while in the former the definitional equality between terms is in general undecidable, in the latter it is decidable and it enjoys all the computational properties good enough to reckon it as a paradigm of a functional programming language. Anyway, providing an internal dependent type theory, even if extensional, for an initial arithmetic universe is important to investigate its computational properties like, for example, the validity of a canonical normal form theorem for closed terms, which is the best one can hope for extensional dependent type theories and from which we can get a syntactic consistency proof of the theory.

Since the correspondence between type constructors and categorical properties is modular [Mai01], we can easily recognize internal type theories both of arithmetic lextensive categories and of regular locoi as fragments of the calculus Au. The novelty of the formulation of internal languages for categorical universes in terms of a dependent type theory, in contrast to traditional formulations in terms of a many sorted logic, is that they reveal that propositions interpreted as subobjects correspond to mono types, that is types with at most one proof. Hence, in designing an internal dependent type theory we do not need to add a new syntactic entity representing propositions with corresponding rules of formation, but we just consider dependent types. Thinking of the interpretation of a dependent typed calculus via fibrations [Ben85, Jac99], all this corresponds categorically to regain the properties of the subobject fibration of a category only by means of its codomain fibration [Mai01].

Here, by making use of the internal languages of the considered categories, we prove not only that the third stage in the construction of an initial arithmetic universe amounts to be equivalent to the construction of an initial list-arithmetic pretopos or even of an initial arithmetic pretopos, but also that the second stage is equivalent to the construction of an initial arithmetic lextensive category or of an initial regular locos.

The advantage of having an internal type theory available for the various categorical structures allows us to restore the set-theoretic reasoning in a categorical setting.

In the future we aim to employ the internal type theory of an arithmetic universe to translate Joyal’s categorical proof of Gödel incompleteness result into a type-theoretic one. Moreover, we intend to use the internal language to proceed in the constructions of theories generated from finite decidable sketches internally to a generic arithmetic universe as started in [Mai00].

This paper extends and provides more detailed proofs of the results reported in [Mai02].

2 The categorical definition of list-arithmetic pretopos

We recall the definitions of the categories we are going to use in the sequel. When we speak of functor preserving some categorical structure we mean preservation up to isomorphism.

Def. 2.1 A lextensive category is a finitely complete category with stable finite disjoint coproducts [CLW93].

Note that a lextensive category amounts to be a locally distributive lex category^{1}.

Def. 2.2 A parameterized natural numbers object in a category with finite 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 an unique rec(b, g) making the following diagrams commute

[figure: B; <id,0·!_{B}>; b; B×N; rec(b,g); B×N; id×s; rec(b,g); Y; Y; g]

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

It is worth to recall here that in the presence of function spaces, like in a cartesian closed category, this parameterized version of natural numbers object is equivalent to the usual natural numbers object.

Def. 2.3 An arithmetic lextensive category is a lextensive category with a parameterized natural numbers object.

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

[figure: B; <id,r_{o}^{A}·!_{B}>; b; B×List(A); rec(b,g); B×(List(A)×A); id×r_{1}^{A}; (rec(b,g)×id_{A})·σ; Y; Y ×A; g]

where σ : B×(List(A)×A) → (B×List(A))×A is the associative isomorphism << π_{1}, π_{1}·π_{2} >, π_{2}·π_{2} >.

In [Coc90] there is an equivalent definition of list-arithmetic finitely complete categories 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.

Def. 2.5 A locos is a lextensive category with parameterized list objects.

Def. 2.6 A regular locos is a locos which is also a regular category, namely it has stable images.

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

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

Def. 2.8 A list-arithmetic pretopos is a pretopos with parameterized list objects.

Some general categorical properties are needed in order to extract the internal dependent type theory of a category, for example of a list-arithmetic pretopos. To start with, we need a list-arithmetic pretopos to be locally a list-arithmetic pretopos (proved in [Mai01]):

Proposition 2.9 For every object A ∈ ObU of a list-arithmetic pretopos U the slice category U/A is still a list-arithmetic pretopos, i.e. the notion of list-arithmetic pretopos is local.

Supposing that a dependent type is modelled in a slice category, having a local structure means that the type-theoretic constructor corresponding to the categorical property that is localized can be modelled even when applied to dependent types. But this is not enough to interpret a dependent type theory. Indeed, since substitution for dependent types and terms is interpreted via the pullback functor, we also need that:

1In [Mai01] we used the term “distributive” as in [Coc90] for what most of the authors call “lextensive” to reserve the word “distributive” for a more general concept (see [CLW93]).

Proposition 2.10 For every morphism f : A → B of a list-arithmetic pretopos U the pullback functor f^{∗} : U/B → U/A preserves the list-arithmetic pretopos structure of the corresponding slice categories.

Proof. For what concerns the structure of a pretopos these propositions follow easily. The key point is then to prove that parameterized list objects exist in the slice categories and they are stable under pullbacks. The proof of these propositions for the list-arithmetic structure, stated also in [Coc90] about locoi, can be done by means of an internal language for a locos. Indeed, a locos has an internal language given by that for Heyting pretopoi in [Mai98] without forall types and quotient types but with list types restricted to closed types. Then, by means of this internal language, we can build list types on arbitrary dependent types, corresponding to list objects in a slice category, and prove that they are stable under pullbacks [Mai]. Analogously, in [Mai01] we prove that

Proposition 2.11 Arithmetic lextensive categories, regular locoi and arithmetic pretopoi are local in the sense of prop. 2.9 and the pullback functors preserve their structure in the sense of prop. 2.10.

Remark 2.12 Note that to interpret the type theory using the codomain fibration, that is dependent types into suitable slice categories, and substitution via pullback, we need to face some coherence problems that we can fix by using the split fibration [Ben85, Hof94, Jac99] associated to the codomain fibration (see [Mai99, Mai01] and subsection 3.1).

Remark 2.13 Note also that, for what just said about locoi in the proof of prop. 2.10, we can immediately deduce that an internal type theory for a list-arithmetic pretopos is that one in [Mai98] without forall type and natural numbers type, - corresponding to the internal language of a pretopos -, together with lists restricted to closed types - corresponding to parameterized list objects -. However, since we can prove that lists on arbitrary dependent types are definable, in the next section we will present the version of the calculus with them included.

3 An internal language for list-arithmetic pretopoi

In a few words the internal language of a list-arithmetic pretopos corresponds to predicative coherent logic equipped with the set-theoretic constructions of lists and quotients. We recall that with respect to intuitionistic logic, predicative coherent logic lacks implication and universal quantification, namely it has only conjunction, falsum, disjunction and existential quantification. Hence negation as A → ⊥ is not definable in general, but we can have proofs from A to falsum at the metalanguage level of an inference rule. For example, we can not prove the proposition 0 ≠ s(0) because we can not even express it as a proposition, but we can prove that from 0 = s(0) we get a contradiction. Now, we recall the rules of the typed calculus Au for arithmetic universes introduced in [Mai99]. The typed calculus Au is equipped with types, which should be thought of as sets or data types, and with typed terms which represent proofs of the types to which they belong. 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 following set equality rule and assumption of typed variables

set rule) \frac{a ∈ A [Γ] A = B [Γ]}{a ∈ B [Γ]} var) \frac{Γ, x ∈ A, Δ cont}{x ∈ A [Γ, x ∈ A, Δ]}

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 Au with the corresponding introduction, elimination and conversion rules of their terms. We omit the equality rules of all the type and term constructors that are necessary to derive the substitution rules. 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 A_{u}’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. A type is called mono if it is inhabitated by at most one proof. 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 Au dependent typed calculus

Terminal type

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

False type

Fs) ⊥ type E-Fs) \frac{a ∈ ⊥ B type}{r_{o}(a) ∈ B}

Indexed Sum type

Σ) \frac{C(x) type [x ∈ B]}{Σ_{x∈B}C(x) type} I-Σ) \frac{b ∈ B c ∈ C(b)}{< 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 >)}

Equality type

Eq) \frac{C type c ∈ C d ∈ C}{Eq(C, c, d) type}  I-Eq) \frac{c ∈ C}{eq_{C}(c) ∈ 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_{C}(c) ∈ Eq(C, c, d)}

Disjoint Sum type

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

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

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

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

Disjointness

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

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{p ∈ A/R l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A, d ∈ R(x, y)]}{El_{Q}(l, p) ∈ L(p)}
C-Q) \frac{a ∈ A l(x) ∈ L([x]) [x ∈ A] l(x) = l(y) ∈ L([x]) [x ∈ A, y ∈ A, d ∈ R(x, y)]}{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) ϵ ∈ List(C)  I_{2}-list) \frac{s ∈ List(C) c ∈ C}{cons(s, c) ∈ List(C)}
E-list) \frac{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{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, ϵ) = a ∈ L(ϵ)}
C_{2}-list) \frac{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 List(⊤) corresponds to the type of natural numbers represented as lists on a singleton. Hence, we put N ≡ List(⊤) with 0 ≡ ϵ and s(n) ≡ cons(n, ∗) for n ∈ List(⊤). Note also that the elimination rule of the Indexed Sum type can be equivalently replaced by the following projections

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

and corresponding β and η conversion rules (see [Mar84, Mai01]). In the following we will often use the more familiar notation a =_{A} b for Eq(A, a, b).

3.1 The interpretation of the calculus

In this subsection we briefly recall the definition of the interpretation of the calculus A_{u} in a listarithmetic pretopos U as in [Mai99, Mai01].

The general idea is to interpret a dependent type under a context as a sequence of morphisms of U ending with the terminal object 1, where the last morphism interprets the type and the rest its context. Instead a term is interpreted as a section of the last morphism of the type to which it belongs.

To this purpose we use the category P gr(U).

Def. 3.1 The objects of the category P gr(U) are finite sequences a_{1}, a_{2}, ..., a_{n} of morphisms of U

[figure: A_{n}; a_{n}; A_{2}; a_{2}; A_{1}; a_{1}; 1] and a morphism from a_{1}, a_{2}, ..., a_{n} to b_{1}, b_{2}, ..., b_{m} is a morphism b of U

[figure: A_{n}; b; a_{n}; B_{n}; b_{n}; 1; A_{1}; !_{A_{1}}; A_{n−1}; a_{n−1}] such that b_{n} · b = a_{n} provided n = m and a_{i} = b_{i} for i = 1, ..., n − 1.

But, since we want to interpret the substitution of a term in a type or in a term via the pullback operation, to overcome the coherence problems of finding a functorial choice of pullbacks, as in [Hof94] we choose to first define a preinterpretation of types and terms by means of the notion of fibred functor with the idea that the preinterpretation expresses the interpretation of a type and of a term with all its possible substitutions.

Before giving the definition of fibred functor, we recall the definition of the arrow category U^{→} of

a given a category U: the objects of U^{→} are the U-morphisms [figure: X; ϕ; A] and the morphisms are pairs of

morphisms of U, f : X → Y and u : A → B such that the following diagram commutes: [figure: X; ϕ; f; Y; ψ; A; u; B]

Then, we define the category of fibred functors related to an object of U.

Def. 3.2 For every object A in U, F ib(U/A, U^{→}) is the category of fibred functors σ : U/A → U^{→}, from the fibration dom_{U} to the fibration cod_{U} (they send cartesian morphisms of dom_{U} to cartesian morphisms of cod_{U}, see [Jac99] for corresponding definitions). A fibred functor σ : U/A → U^{→} associates to every

triangle [figure: C; t; b′; B; b; A] a pullback diagram [figure: C′; q(t,σ(b)); σ(b·t); B′; σ(b); C; t; B] . The morphisms of F ib(U/A, U^{→}) are

natural transformations ρ such that for every b : B → A the second member of ρ(b) is the identity (recall

that ρ(b) is a morphism of U^{→}), that is the triangle [figure: ρ_{1}(b); σ(b); τ(b); B] commutes.

To relate fibred functors to P gr(U), observe that the category of fibred functors F ib(U/A, U^{→}) is equivalent to the slice category U/A. The functor

ˆ(−) : U/A → F ib(U/A, U^{→})

establishes one side of the equivalence. This associates to an object b : B → A of U/A the fibred functor

b̂, defined as b̂(t) ≡ t^{∗}(b), namely the first projection of the pullback of b along t [figure: B_{Σ}; b^{∗}(t); t^{∗}(b); B; b; D; t; A] for every

t : D → A. Then, ˆ(−) is extended to morphisms by the universal property of pullback. For every

a : C → A and b : B → A, the morphism part of ˆ(−) associates to every [figure: C; g; a; B; b; A] the natural

transformation \overline{g} : â → b̂ defined in this way: for every t : D → A, we put \overline{g}(t) ≡< â(t),_{A} g · a^{∗}(t) >), where < â(t),_{A} g · a^{∗}(t) > is the unique morphism to the pullback of b along t induced by â(t) and g · a^{∗}(t).

The other side of the equivalence is established by the functor

(−)(id) : F ib(U/A, U^{→}) → U/A

The object part and morphism part of (−)(id) are defined exactly as the valuation of a fibred functor and of a natural transformation on the identity on A.

Since our idea is to preinterpret a type under context into a sequence of fibred functors and a term into a natural transformation, then, we will use the valuation functor (−)(id) to pass from the preinterpretation of types and terms to their interpretation in P gr(U). Moreover, in defining the preinterpretation we will use the functor ˆ(−) to preinterpret basic types: for example, we will preinterpret the False type into the fibred functor ˆ(!_{0}) where !_{0} : 0 → 1 is the unique morphism from the initial object 0 of U to the terminal object 1.

More in detail, in the next we will define a preinterpretation Ĩ_{U}_{|} : Au ⟶ P gf(U) of the calculus Au into the category P gf(U) of sequence of fibred functors defined as follows:

Def. 3.3 The objects of the category P gf(U) are finite sequences σ_{1}, σ_{2}, ..., σ_{n} of fibred functors σ_{i} : ObF ib(C/A_{i}, C^{→}) for i = 1, ..., n such that σ_{1}(id_{A_{1}}), σ_{2}(id_{A_{2}}), ..., σ_{n}(id_{A_{n}}) is an object of P gr(U). The morphisms of P gf(U) from σ_{1}, σ_{2}, ..., σ_{n} to τ_{1}, τ_{2}, ..., τ_{m} are defined only if n = m and σ_{i} = τ_{i} for i = 1, ..., n−1 and σ_{n}, τ_{n} ∈ ObF ib(U/A_{n}, U^{→}) and they are natural transformations ρ in F ib(U/A_{n}, U^{→}) from σ_{n} to τ_{n}.

Then, we will use a valuation functor V : P gf(U) ⟶ P gr(U) defined in this manner: for every object σ_{1}, σ_{2}, ..., σ_{n} of P gf(U) and for every morphism ρ of P gf(U) we put

V(σ_{1}, σ_{2}, ..., σ_{n}) ≡ σ_{1}(id_{A_{1}}), σ_{2}(id_{A_{2}}), ..., σ_{n}(id_{A_{n}}) V(ρ) ≡ ρ(id_{A_{n}})

by which we will define the interpretation I_{U} : Au ⟶ P gr(U) as I_{U} ≡ V · Ĩ_{U}_{|} [figure: Au; I_{U}; _{Ĩ_{U}_{|}}; P gr(U); P gf(U); V]

The preinterpretation Ĩ_{U}_{|} will be defined as a restriction of an a priori partial interpretation Ĩ_{U} from the pseudo-judgements of Au, which are expressions in the form of a judgement with the signature of Au, but not necessarily derivable in Au, by induction on the complexity of pseudo-judgements.

The reason for using a partial interpretation is that we can not define an interpretation by induction on the derivation of type and term judgements because a type or term judgement may be derived also from equality judgements like in the set equality rule conv. Hence, we opt for a partial interpretation on the pseudo-judgements pseudo(Au) of Au.

Def. 3.4 A dependent type judgement B(x_{1}, ..., x_{n}) [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n−1}(x_{1}, ..., x_{n−1})] will be preinterpreted as an object of P gf(U)

α_{1}, α_{2}, ..., α_{n}, β

and hence interpreted as

α_{1}(id), α_{2}(id), ..., α_{n}(id), β(id)

The equality between types will be preinterpreted as equality between objects of P gf(U) and hence interpreted as the equality between objects of P gr(U). A typed term judgement will be interpreted as a morphism of P gr(U): given the type judgement B(x_{1}, ..., x_{n}) [Γ_{n}] interpreted as α_{1}(id), α_{2}(id), ..., α_{n}(id), β(id) then the term judgement b ∈ B(x_{1}, ..., x_{n}) [Γ_{n}] will be preinterpreted as a natural transformation b^{I} from α_{1}, α_{2}, ..., α_{n}, i_{A_{Σn}} to α_{1}, α_{2}, ..., α_{n}, β, and interpreted as b^{I}(id), where the fibred functor i_{A_{Σn}} is defined as follows: it associates to every triangle

[figure: C; t; b′; B; b; A_{Σn}] the pullback diagram [figure: C; t; id; B; id; C; t; B] .

The equality between terms will be preinterpreted as equality between natural transformations and hence interpreted as the equality between morphisms of P gr(U).

Warning Note that to specify a fibred functor it is enough to specify its action on objects since its action on morphisms is determined by the pullback property, once we know that the defined object part fits well into a pullback. Therefore, in the following we will specify the interpretation of type judgements giving enough details to deduce the preinterpretation.

Note also that any component of a P gf(U)-morphism ρ is determined by the component ρ(id) by the properties of pullback. Therefore, in the next we will specify only the interpretation of a term into a morphism of P gr(U) since its preinterpretation into a morphism of P gf(U) can be uniquely deduced.

Moreover, note that to interpret weakening and substitution we make use of the following definition of fibred functor: given a morphism a : B → A and a fibred functor α we define α[a] as a fibred functor

in F ib(U/B, U^{→}) that associates to a triangle [figure: C; t; b′; D; b; B] the pullback [figure: C′; q(t,α(a·b)); α((a·b)·t); D′; α(a·b); C; t; D]

The (pre)interpretation on type and term constructors specific to Au is defined as follows: note that we use the following abbreviations Γ ≡ x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1}) and α⃗(id) ≡ α_{1}(id), α_{2}(id), ..., α_{n}(id) and we suppose that cod(α_{n}(id)) = A_{Σn} Assumption of variable: I_{U}(x ∈ B(x_{1}, ..., x_{n})[Γ, x ∈ B(x_{1}, ..., x_{n}), y ∈ C(x_{1}, ..., x_{n}, x)])(id) ≡ γ(id)^{∗}(△_{B_{Σ}}) where △_{B_{Σ}} is the diagonal with respect to β(id) in U/A_{Σn} provided that I_{U}(B(x_{1}, ..., x_{n})[Γ, x ∈ B(x_{1}, ..., x_{n}), y ∈ C(x_{1}, ..., x_{n}, x)]) ≡ α⃗(id), β(id), γ(id), β[γ(id) · β(id)](id) and that I_{U}(C(x_{1}, ..., x_{n}, x) [Γ_{n}, x ∈ B(x_{1}, ..., x_{n})]) ≡ α⃗(id), β(id), γ(id) The assumption of variable, when the context Δ is made of more than one typed variable, is interpreted by repeating the semantic operation of weakening of lemma 3.5; Terminal type: I_{U}(⊤ [ ]) ≡ îd_{1}(id) and I_{U}(⊤ [Γ_{n}]) ≡ α⃗(id), îd_{1}(!_{A_{Σn}}) I_{U}(⋆ ∈ ⊤ [Γ_{n}]) ≡< id_{A_{Σn}},_{1} !_{A_{Σn}} > which is a pairing map towards A_{Σn} × 1 False type: I_{U}(⊥ [Γ_{n}]) ≡ α⃗(id), ˆ!_{0}(!_{A_{Σn}}) where 0 is the initial object in U I_{U}(r_{o}(a) ∈ B [Γ_{n}]) ≡?_{B_{Σ}} · (a^{I}(id)) where ?_{B_{Σ}} is the unique morphism from A_{Σn} × 0 to B_{Σ} ≡ dom(β(id)) provided that I_{U}(B [Γ_{n}]) ≡ α⃗(id), β(id) Indexed Sum type: (we interpret the projections instead of the elimination rule shown at the beginning of section 3) I_{U}(Σ_{y∈B}C(y) [Γ_{n}]) ≡ α⃗(id), Σ_{β}(γ)(id) where Σ_{β}(γ)(t) ≡ β(t) · γ(q(t, β(id))) for any t : D → A_{Σn} provided that I_{U}(B [Γ_{n}]) ≡ α⃗(id), β(id) and I_{U}(C [Γ_{n}, z ∈ B]]) ≡ α⃗(id), β(id), γ(id) I_{U}(< b, c >∈ Σ_{y∈B}C(y)) [Γ_{n}]) ≡ q(b^{I}(id), γ(id)) · (c^{I}(id)) I_{U}(π_{1}(d) ∈ B [Γ_{n}]) ≡ γ(id) · (d^{I}(id)) I_{U}(π_{2}(d) ∈ C(π_{1}(d)) [Γ_{n}]) ≡< id,_{B_{Σ}} d^{I}(id) > which is the unique morphism to the pullback between γ(id) and γ(id) · (d^{I}(id)) Extensional Propositional Equality type: I_{U}(Eq(C, c, d) [Γ_{n}]) ≡ α⃗(id), Eq(c^{I}, d^{I})(id) where Eq(c^{I}, d^{I})(t) ≡ (< c^{I}(t),_{D} d^{I}(t) >)^{∗}(△_{D×C_{Σ}}) for t : D → A_{Σn} and △_{D×C_{Σ}} ≡< id_{D×C_{Σ}},_{D} id_{D×C_{Σ}} > is the diagonal in U/A_{Σn} with respect to γ(t) and D × C_{Σ} ≡ dom(γ(t)) provided that I_{U}(C [Γ_{n}]) ≡ α⃗(id), γ(id) I_{U}(eq_{U}(c) ∈ Eq(C, c, c) [Γ_{n}]) ≡< id_{A_{Σn}}, c^{I}(id) > which is the unique morphism in U/A_{Σn} to the pullback that defines the equalizer Eq(c^{I}, c^{I})(id) induced by id_{A_{Σn}} and c^{I}(id) Disjoint Sum type: I_{U}(C + D [Γ_{n}]) ≡ α⃗(id), (γ ⊕ δ)(id), where (γ ⊕ δ)(t) ≡ γ(t) ⊕ δ(t), which is the coproduct in U/A_{Σn}, for t : D → A_{Σn} provided that I_{U}(C [Γ_{n}]) ≡ α⃗(id), γ(id) and I_{U}(D [Γ_{n}]) ≡ α⃗(id), δ(id) I_{U}(inl(c) ∈ C + D [Γ_{n}]) ≡ ϵ_{1}(c^{I}) and I_{U}(inr(d) ∈ C + D [Γ_{n}]) ≡ ϵ_{2}(d^{I}) where ϵ_{1}, ϵ_{2} are the injections of the coproduct C_{Σ} ⊕ D_{Σ} and C_{Σ} ≡ dom(γ(id)) and D_{Σ} ≡ dom(δ(id)) I_{U}(El_{+}(w, a_{C}, a_{D}) ∈ A(w) [Γ_{n}, w ∈ C + D]) ≡ (q(ϵ_{1}, α(id)) · a_{C}^{I}(id)) ⊕ (q(ϵ_{2}, α(id)) · a_{D}^{I}(id)) which is the codiagonal morphism of q(ϵ_{1}, α(id)) · a_{C}^{I}(id) and q(ϵ_{2}, α(id)) · a_{D}^{I}(id) in U I_{U}(dsj(c, d) ∈ ⊥ [Γ_{n}]) ≡< id,_{1} t > where < id,_{1} t > is the unique morphism to the pullback of !_{0} and !_{A_{Σn}} and t is defined by the disjointness property of coproducts provided that ϵ_{1}(c^{I}(id)) = ϵ_{2}(d^{I}(id)). Quotient type: I_{U}(A/R [Γ_{n}]) ≡ Q(α)(id) where Q(α)(t) ≡ Q(α(t)) which is the unique morphism such that α(t) = Q(α(t)) · c(t) and c(t) is the quotient map of the equivalence relation ρ(q(q(t, α(id)), π_{1})) with π_{1} ≡ α(α(id)) provided that I_{U}(A [Γ_{n}]) ≡ α⃗(id), α(id) and I_{U}(R(x, y) type [x ∈ A, y ∈ A]) ≡ α⃗(id), α(id), α[α(id)](id), ρ(id) where ρ(id) is an equivalence relation in U/A_{Σn} I_{U}([a] ∈ A/R [Γ_{n}]) ≡ c(id) · (a^{I}(id)) I_{U}(El_{Q}(m, z) ∈ M [Γ_{n}, z ∈ A/R]) ≡< id, q > where q is the unique morphism such that q · c(id) = q(α(id), μ(id)) · m^{I}(id) provided that I_{U}(M [Γ_{n}]) ≡ α⃗(id), μ(id) and m^{I}(id) · (π_{1} · ρ(id)) = m^{I}(id) · (π_{2} · ρ(id)) (here we only interpret the elimination rule in the case the type M does not depend on the quotient type since this is enough (for a proof see [Mai99, Mai01])) I_{U}(eff(a, b) ∈ R(a, b) [Γ_{n}]) ≡< id, t > where t is the unique morphism such that (π_{1} · ρ(id)) · t = a^{I}(id) and (π_{2} · ρ(id)) · t = b^{I}(id) provided that c(id) · a^{I}(id) = c(id) · b^{I}(id) List type: I_{U}(List(C) [Γ_{n}]) ≡ α⃗(id), List(γ)(id) where List(γ)(t) ≡ List(γ(t)), which is the list object on γ(t) in U/D for t : D → A_{Σn} I_{U}(ϵ ∈ List(C) [Γ_{n}]) ≡ r_{o}^{γ} that is the empty map for List(γ)(id) in U/A_{Σn} I_{U}(cons(x, y) ∈ List(C) [Γ_{n}, x ∈ List(C), y ∈ C]) ≡< id, r_{1}^{γ} > where r_{1}^{γ} : List(γ)(id) × γ(id) → List(γ)(id) is the list-constructor map in U/A_{Σn} I_{U}(El_{List}(a, l, y) ∈ L [Γ_{n}, y ∈ List(C)]) ≡< id,_{A_{Σn}} r > where r is the unique morphism such that r · r_{o}^{γ} = a^{I} and (π_{2}^{L} · l^{I}(id)) · (r × id) = r · r_{1}^{γ} by the property of list object in U/A_{Σn} with π_{2}^{L} ≡ q(ξ(id) · γ(ξ(id)), ξ(id)) provided that I_{U}(L [Γ_{n}]) ≡ α⃗(id), ξ(id) (here we only interpret the elimination rule in the case the type L does not depend on the list type since this is enough (for a proof see [Mai99, Mai01])).

Lemma 3.5 The weakening of a variable in type and term judgements is interpreted as follows: if I_{U}(B(x_{1}, ..., x_{n}) [Γ_{n}]) ≡ α_{1}(id), α_{2}(id), ..., α_{n}(id), β(id), I_{U}(b ∈ B(x_{1}, ..., x_{n}) [Γ_{n}]) ≡ b^{I}(id) and I_{U}(D(x_{1}, ..., x_{j}) [Γ_{j}]) ≡ α_{1}(id), α_{2}(id), ..., α_{j}(id), δ(id) with n ≥ j, then I_{U}(B(x_{1}, ..., x_{n}) [Γ_{j}, y ∈ D, x_{j+1} ∈ A_{j+1}, ..., x_{n} ∈ A_{n}]) ≡ α_{1}(id), ..., δ(id), α_{j+1}[t_{j}](id), ..., α_{n}[t_{n−1}](id), β[t_{n}](id) and I_{U}(b ∈ B(x_{1}, ..., x_{n}) [Γ_{j}, y ∈ D, x_{j+1} ∈ A_{j+1}, ..., x_{n} ∈ A_{n}]) ≡ b^{I}[t_{n}](id) where t_{j} ≡ δ(id) and t_{i} ≡ q(t_{i−1}, α_{i}(id)) for i = j + 1, ..., n.

Lemma 3.6 The substitution of variables in type and term judgements is interpreted as follows: if I_{U}(B(x_{1}, ..., x_{n}) [Γ_{n}]) ≡ α_{1}(id), α_{2}(id), ..., α_{n}(id), β(id), I_{U}(a_{j} ∈ A_{j} [Γ_{j−1}]) ≡ a_{j}^{I}(id) and I_{U}(b ∈ B(x_{1}, ..., x_{n})[Γ_{n}]) ≡ b^{I}(id) where n ≥ j, then I_{U}(B(x_{1}, ..., x_{j−1}, a_{j}, x′_{j+1}, ..., x′_{n})[Γ_{j−1}, x′_{j+1} ∈ A′_{j+1}, ..., x′_{n} ∈ A′_{n}]) ≡ α_{1}(id), ..., α_{j+1}[q_{j}](id), ..., α_{n}[q_{n−1}](id), β[q_{n}](id) and I_{U}(b[x_{j}/a_{j}][x_{i}/x′_{i}]_{i=j,...,n} ∈ B(x_{1}, ..., x_{j−1}, a_{j}, x′_{j+1}, ..., x′_{n}) [Γ_{j−1}, x′_{j+1} ∈ A′_{j+1}, ..., x′_{n} ∈ A′_{n}]) ≡ b^{I}(q_{n}) where if n ≥ j + 1, A′_{j+k} ≡ A_{j+k}[x_{j}/a_{j}][x_{i}/x′_{i}]_{i=j+1,...,j+k−1} for k = 1, ...n − j and q_{j} ≡ a_{j}^{I}(id) and q_{i} ≡ q(q_{i−1}, α_{i}(id)) for i = j + 1, ..., n.

Now, we state the validity and completeness for list-arithmetic pretopoi with respect to Au:

Theorem 3.7 • (validity) If A type [Γ_{n}] is derivable in A_{u} then I_{U}(A type [Γ_{n}]) is well defined for any list-arithmetic pretopos U. If a ∈ A [Γ_{n}] is derivable in A_{u}, then I_{U}(a ∈ A [Γ_{n}]) is well defined for every list-arithmetic pretopos U. Suppose that A type [Γ_{n}] and B type [Γ_{n}] are derivable in A_{u}, if A = B [Γ_{n}] is derivable in A_{u}, then we have I_{U}(A type [Γ_{n}]) = I_{U}(B type [Γ_{n}]) for every list-arithmetic pretopos U. Suppose that a ∈ A [Γ_{n}] and b ∈ A [Γ_{n}] are derivable in A_{u}, if a = b ∈ A [Γ_{n}] is derivable in A_{u}, then we have I_{U}(a ∈ A [Γ_{n}]) = I_{U}(b ∈ A [Γ_{n}]) for every list-arithmetic pretopos U.

• (completeness) Suppose that A type [Γ_{n}] and B type [Γ_{n}] are derivable in A_{u}, if for every listarithmetic pretopos U we have I_{U}(A type [Γ_{n}]) = I_{U}(B type [Γ_{n}]), then A = B [Γ_{n}] is derivable in A_{u}. Suppose that a ∈ A [Γ_{n}] and b ∈ A [Γ_{n}] are derivable in A_{u}, if for every list-arithmetic pretopos U we have I_{U}(a ∈ A [Γ_{n}]) = I_{U}(b ∈ A [Γ_{n}]), then a = b ∈ A [Γ_{n}] is derivable in A_{u}

The proof of this theorem can be found in [Mai99, Mai01]. As already said, in [Mai99, Mai01] we proved even more, namely that:

Theorem 3.8 Au provides an internal type theory for list-arithmetic pretopoi.

Proof. The proof of this theorem consists in providing a sort of bi-equivalence between the category of list-arithmetic pretopoi with a fixed choice of their structure and equipped with strict functors, i.e. functors preserving the considered categorical structure strictly, and the category of theories based on Au.

Moreover, we can built out of Au an initial list-arithmetic pretopos:

Def. 3.9 U_{Au} is the syntactic category having the closed types of Au as objects and the proof-terms b(x) ∈ B [x ∈ A] derivable in Au in section 3 as morphisms.

With the technique used to prove the completeness theorem we can show:

Theorem 3.10 U_{Au} is an initial (up to iso) list-arithmetic pretopos in the sense that for any listarithmetic pretopos P there is a functor from U_{Au} to P preserving the list-arithmetic structure up to isomorphism and which is unique up to a natural isomorphism.

Proof. We define a list-arithmetic functor J_{P} : U_{Au} → P as follows:

\begin{matrix}J_{P}(A) ≡ dom(I_{P}(A[ ])) \\ J_{P}(b(x) ∈ B [x ∈ A]) ≡ q(I_{P}(A[ ]), I_{P}(B[ ])) · I_{P}(b ∈ B[x ∈ A]) \end{matrix}

where I_{P} is the interpretation of Au in P gr(P) and we recall that q(I_{P}(A[ ]), I_{P}(B[ ])) is the second projection of the pullback of I_{P}(B[ ])) along I_{P}(A[ ]). To show that this is unique up to a natural isomorphism, we prove that any other list-arithmetic functor preserving the structure up to isomorphism is obtained analogously to J_{P} from another valid interpretation of Au into P gr(P) that turns out to be naturally isomorphic to I_{P} in a suitable sense. The technique to show this is analogous to the one used in [Mai99, Mai01] to prove the completeness theorem of Au with respect to list-arithmetic pretopoi.

3.2 Internal type theories for other categorical structures

Here, we briefly describe internal type theories and corresponding initial categories for other categorical structures we will use in the rest of the paper.

By an initial (up to iso) category, for example among arithmetic lextensive categories, we mean that from this category to any other arithmetic lextensive category there is a functor preserving the arithmetic lextensive structure up to isomorphism and that is naturally isomorphic to any other such a functor. We start with a typed calculus that provides an internal language for arithmetic lextensive categories.

Def. 3.11 T_{ad} is the dependent type theory equipped with the terminal type, extensional equality types, indexed sum types, disjoint sum types and the natural numbers type List(⊤) as those present in the calculus Au at the beginning of section 3.

Then, we define a syntactic category out of this calculus:

Def. 3.12 U_{ad} is the syntactic category having the closed types of T_{ad} as objects and the proof-terms b(x) ∈ B [x ∈ A] derivable in T_{ad} as morphisms.

We prove then:

Theorem 3.13 T_{ad} provides an internal type theory for arithmetic lextensive categories and U_{ad} is an initial (up to iso) arithmetic lextensive category.

Proof. The proofs of these results are completely analogous to those for Au, being T_{ad} a fragment of Au.

Then, we describe a typed calculus that provides an internal language for regular locoi.

Def. 3.14 T_{rl} is the dependent type theory obtained by extending T_{ad} with quotient types of the kind A/⊤^{2} and list types as those present in the calculus Au in section 3.

Then, we define a syntactic category out of this calculus:

Def. 3.15 U_{rl} is the syntactic category having the closed types of T_{rl} as objects and the proof-terms b(x) ∈ B [x ∈ A] derivable in T_{rl} as morphisms.

We prove then:

Theorem 3.16 T_{rl} provides an internal type theory for regular locoi and U_{rl} is an initial (up to iso) regular locos.

Proof. The proofs of these results are completely analogous to those for Au, being T_{rl} a fragment of Au. Finally, we describe a typed calculus that provides an internal language for arithmetic pretopoi.

Def. 3.17 T_{pn} is the fragment of the dependent type theory Au in section 3 without list types but with the natural numbers type List(⊤).

2After Steve Awodey’s talk (presenting a joint work with Andrej Bauer) at the Mittag-Leffler Institute I realized that in my formulation of the internal type theory of regular categories A/Ker(f) for a term f can be derived from A/⊤.

Then, we define a syntactic category out of this calculus:

Def. 3.18 U_{pn} is the syntactic category having the closed types of T_{pn} as objects and the proof-terms b(x) ∈ B [x ∈ A] derivable in T_{pn} as morphisms.

We prove then:

Theorem 3.19 T_{pn} provides an internal type theory for arithmetic pretopoi and U_{pn} is an initial (also up to iso) arithmetic pretopos.

Proof. The proofs of these results are completely analogous to those for Au, being T_{pn} a fragment of Au.

4 Joyal’s arithmetic universes

What we describe in this section can be read in unpublished notes by Gavin Wraith [Wra85] and also in [Mor96] and it is due to Andrè Joyal. Joyal built arithmetic universes in three stages:

1. consider a Skolem theory S;

2. take the category P red(S) of predicates in S;

3. make the exact completion (P red(S))_{ex} on regular categories;

Then, he proved Gödel incompleteness theorems based on the fact that any arithmetic universe contains an initial one obtained by performing the above construction starting from an initial Skolem theory. Here, we describe Joyal’s construction in more detail.

Def. 4.1 A Skolem category is a cartesian category (i.e. a category with terminal object 1 and binary products) with a parameterized natural numbers object.

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

In [Wra85] an initial Skolem category is built and used to model a programming language which represents exactly primitive recursive functions. Using type theory we can also build an initial Skolem category as follows.

Def. 4.3 Let T_{sk} be the fragment of the type theory Au in section 3 with terminal type, natural numbers type (namely List(⊤)) and finite products (namely Σ_{x∈A}B with the two projections in section 3).

Def. 4.4 Let S_{in} be the category having the types of T_{sk} as objects and the proof-terms b(x) ∈ B [x ∈ A] derivable in T_{sk} as morphisms between types A and B.

Then, in an analogous way to Au for list-arithmetic pretopoi we can prove that

Proposition 4.5 T_{sk} provides an internal language for Skolem categories and S_{in} is an initial (also up to iso) Skolem category (and theory).

Here is an useful property of the natural numbers object in a Skolem theory:

Proposition 4.6 In any Skolem theory S the natural numbers object N is equipped with a structure of parameterized list object over itself.

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

To understand what is the list structure of N, first observe that, after extending any theory of T_{sk} with List(N), by a particular encoding trick based on the binary representation of natural numbers we can prove that the natural numbers type N is isomorphic to List(N). Indeed, we can define a morphism enc : List(N) → N by list recursion as follows:

1. enc(ϵ) ≡ 0

2. enc(cons(s, n) ≡ 2^{c} · 2^{n} + enc(s) where c ≡ min{ x : N | x ≥ enc(s) }.

We can then prove the existence of an inverse since any natural number can be uniquely represented in binary digits.

Logically, this means that the extension of any theory of T_{sk} with the type List(N) is equivalent to the starting theory.

We can then conclude that N is equipped with the following categorical list structure: r_{o}^{List(N)} : ⊤ → N is the constant morphism to zero where ⊤ is the terminal object, and r_{1}^{List(N)} : N × N → N is given by r_{1}^{ListN}(m, n) ≡ 2^{c} · 2^{n} + m where c ≡ min{ x : N | x ≥ m }.

Then, we are ready to define the category of predicates on a Skolem theory. First notice that we define f ≤ g ≡ f · − g = 0 between morphisms in the Skolem category, where · − is the usual truncated subtraction on natural numbers.

Def. 4.7 Given a Skolem theory S the category P red(S) of predicates has as

• Ob(P red(S)): S-morphisms P : N → N such that P ∗ P = P (where ∗ is the usual multiplication between natural numbers);

• Hom(P, Q): S-morphisms f : N → N such that P ≤ Q · f and two such S-morphisms f : N → N and g : N → N are equal iff P ∗ f = P ∗ g.

Note that, if P red(S) is embedded in the usual category Sets of classical ZFC-sets, then we get a category having subsets of the set of natural numbers as objects, because a subset is characterized by the elements with value 1 through a predicate P (that is its characteristic function), and equivalence classes of functions mapping a subset to the codomain subset as morphisms. Finally, two maps are considered equal if they are equal on the domain subset. This category of predicates has nice properties as Joyal proved:

Proposition 4.8 The category P red(S) of a Skolem theory S is regular with parameterized list objects and stable disjoint coproducts. Moreover, there is an epi-mono factorization where epimorphisms split.

Proof. We describe the claimed structure of P red(S). The terminal object is given by the predicate ⊤_{P red} : N → N defined as ⊤_{P red}(0) ≡ 1 and ⊤_{P red}(n) ≡ 0 for all n ≥ 1. The binary product of two predicates P and Q is given by (P ×Q)(n) ≡ P (π_{1}(ϕ(n)))·Q(π_{1}(ϕ(n))) where ϕ is a bijection from N to N × N and π_{i} : N × N → N for i = 1, 2 are the two projections of the cartesian product N × N. The two projections of P × Q are π_{P} : P × Q → P and π_{Q} : P × Q → Q defined as: π_{P} (n) ≡ π_{1}(ϕ(n)) and π_{Q}(n) ≡ π_{2}(ϕ(n)) for all n ∈ N. The equalizer of two morphisms f, g : P → Q is Eq(f, g)(n) ≡ P (n) · (eq(f(n), g(n))) for all n ∈ N where eq(n, m) is the equality relation defined as eq(n, m) ≡ 1 if n = m and 0 otherwise; the equalizer injection e : Eq → P is defined as e(n) ≡ n for all n ∈ N. The initial object is given by the predicate ⊥ : N → N defined as ⊥(n) ≡ 0 for all n.

The binary coproduct of two predicates P and Q is given by (P + Q)(n) ≡ \{ \begin{matrix}P (m) & if n = 2m \\ Q(m) & if n = 2m + 1 \end{matrix}

and 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 all n ∈ N. It follows easily that such binary coproducts are stable under pullbacks. The image object of a morphism f : P → Q is defined as

(Imf)(n) ≡ \{ \begin{matrix}0 & if P (n) = 0 \\ eq(n, m) & where m ≡ min\{ x : N | f(x) = f(n) \} if P (n) = 1 \end{matrix}

Its image morphism ι_{f} : Imf → Q is defined as ι_{f}(n) ≡ f(n) for all n ∈ N. The morphism f factorizes through ι_{f} and p : P → Imf where

p(n) ≡ \{ \begin{matrix}0 & if P (n) = 0 \\ m & where m ≡ min\{ x : N | (f(x) = f(n) \} if P (n) = 1 \end{matrix}

that is f = ι · p. Clearly, p has a section p^{−1} : Imf → P defined as p^{−1}(n) ≡ n, that is p · p^{−1} = id in P red(S). Since the epimorphism of the image factorization splits then images are stable under pullbacks.

By lemma 4.6 we know that in a Skolem theory there exists the list object List(N). Hence, we can easily prove that a parameterized list object of a predicate P is List(P)(n) ≡ \overline{P} · enc^{−1}(n) where \overline{P} : List(N) → N is the morphism induced by P on List(N) as follows:

\overline{P} (ϵ) ≡ ϵ \overline{P} (cons_{List(N)}(s, a) ≡ \overline{P} (s) · P (a)

The list structure of List(P) is the following: r_{0}^{List(P)}(n) ≡ \{ \begin{matrix}1 & if n = 0 \\ 0 & otherwise \end{matrix} defines r_{0}^{List(P)} : ⊤ →

List(P) and r_{1}^{List(P)} : List(P) × P → List(P) is defined as r_{1}^{List(P)}(n) ≡ cons_{List(N)}(n_{1}, n_{2}) for all n ∈ N, where n_{1} ≡ π_{1}(ϕ(n)) and n_{2} ≡ π_{2}(ϕ(n)) with ϕ the bijection from N to N × N.

Now, we are ready to perform the last step, namely we apply the exact completion construction on a regular category (see for example [CV98] and loc. cit.) to P red(S) and we call it (P red(S))_{ex}. Note that thanks to the epi-mono factorization where epimorphisms split we can define the morphisms in (P red(S))_{ex} as morphisms of P red(S) preserving the equivalence relations. Therefore, we put:

Def. 4.9 The Joyal-arithmetic universe (P red(S))_{ex} is a category having

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

• Hom((X, R), (Y, S)): P red(S)-morphisms preserving the equivalence relations.

Finally, we get

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

Proof. In [Wra85, Mor96] it is shown that (P red(S))_{ex} is a pretopos with list objects but we can show that list objects are also parameterized. With respect to the exact structure already presented in [CC82] we describe the finite coproducts and the list objects.

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. Moreover, given any type-theoretic relation R̃(z, z′) [z ∈ X, z′ ∈ X] we can turn it into a mono relation R(z, z′) ≡ R̃(z, z′)/top by quotienting R̃ under the total relation. The initial object of (P red(S))_{ex} is (⊥, x =_{⊥} x) with ⊥ is the initial object of P red(S) and x =_{⊥} x 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 P red(S) and R + S ≡ { \atop R + S}/⊤ and { \atop R + S} is defined as follows:

({ \atop 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} 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_{R} : (X, R) → (X+Y, R+S) and i_{S} : (X, R) → (X+Y, R+S) defined as i_{R}(x) ≡ i_{X}(x) for x ∈ X and i_{S}(y) ≡ i_{Y} (y) for y ∈ Y.

The list object of (X, R) is (List(X), List(R)) where List(X) is the list object of X in P red(S) and List(R) ≡ { \atop List(R)}/⊤ where { \atop List(R)} is defined as follows:

{ \atop 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 (see Def. 7.1) and \overline{π_{i}} ≡ List(π_{i}) for i = 1, 2 are obtained by lifting the first and second projections on the lists (see Def. 7.2). List(R) can be proved to be an equivalence relation since in T_{rl} given two lists 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, r_{o}^{(X,R)} : (⊤, x =_{⊤} x) → (List(X), List(R)) and r_{1}^{(X,R)} : (List(X), List(R)) × (X, R) → (List(X), List(R)) are defined as r_{o}^{X} and r_{1}^{X} respectively.

The list object is parameterized. Indeed, given g : (Z, H) → (C, M) and f : (C, M) × (X, R) → (C, M), using the property of the list object List(X) in P red(S) we get a P red(S)-morphism r : Z × List(X) → C such that r· < id, r_{o}^{X} >= g and r · (id × r_{1}^{X}) = (f · (r × id)) · σ. We can prove that r is a morphism in (P red(S))_{ex} from (Z, H) × (List(X), List(R)) to (C, M) satisfying r· < id, r_{o}^{(X,R)} >= g and r · (id × r_{1}^{(X,R)}) = (f · (r × id)) · σ in (P red(S))_{ex}. 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(r(< z, s >), r(< z′, s′ >)) holds by showing by induction on n ∈ N the validity of

M(r(< z, part_{n}(s) >), r(< z′, part_{n}(s′) >))

where part_{n}(s) is a list operation defined as part_{n}(s) ≡ \{ \begin{matrix}ϵ & if n = 0 \\ part_{n}(s) · p_{n+1}(s) & if n ≥ 1 \end{matrix} by induction

on n ∈ N and p_{n+1}(s) is the projection of the n + 1-th element of the list if n + 1 ≤ lh(s), otherwise it is the projection of the last element of the list (see Def. 7.5). This lets us prove what wanted since we can show that part_{k}(s) = s if k ≥ lh(s).

In an analogous way, by using induction on natural numbers via part_{n}(s) of a list s, we can prove the uniqueness of r.

Def. 4.11 We call A_{in} the initial arithmetic universe (P red(S_{in}))_{ex} where S_{in} is the initial Skolem category defined above.

Indeed, it can be easily shown that A_{in} is an initial (up to iso) arithmetic universe in the category of Joyal-arithmetic universes and functors induced from functors between Skolem theories, with a fixed choice of their structure, preserving such a structure strictly (up to iso). Note that P red(S_{in}) turns out to be the category of primitive recursive predicates.

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 U_{ad} and also to the initial regular locos U_{rl}. To this purpose, we define two embeddings E_{ad} : P red(S_{in}) ⟶ U_{ad} and E_{rl} : P red(S_{in}) ⟶ U_{rl} both as follows:

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

• E_{ad}(f) ≡ < f(π_{1}(z)), eq >∈ Σ_{x∈N}Q(x) =_{N} 1 [z ∈ Σ_{x∈N}P (x) =_{N} 1] for f : P → Q in P red(S_{in}). The definition of E_{rl} is analogous.

Then, we can prove that these embeddings have nice properties:

Lemma 5.1 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. E_{ad} preserves the terminal object, namely Σ_{x∈N}⊤_{P red}(x) =_{N} 1 is isomorphic to the terminal object of U_{ad}, defined as the terminal type ⊤, since in T_{ad} from a proof of 0 =_{N} 1 we conclude a proof of falsum because of coproduct disjointness.

E_{ad} preserves binary products since in U_{ad} we can define the bijection ϕ : N → N × N. Indeed, given two predicates P and Q, the binary product of E_{ad}(P) and E_{ad}(Q) in U_{ad} is defined as Σ_{x∈N}P (x) =_{N} 1 × Σ_{x∈N}Q(x) =_{N} 1. The first and second projections are defined by the terms π_{1}(z) ∈ E_{ad}(P) and π_{2}(z) ∈ E_{ad}(Q) for z ∈ E_{ad}(P) × E_{ad}(Q) respectively.

E_{ad} preserves equalizers thanks to the fact that we can prove that 0 =_{N} 1 is not valid in T_{ad}. The equalizer of E_{ad}(f) and E_{ad}(g) in U_{ad} is defined as Σ_{z∈E_{ad}(P)} E_{ad}(f)(z) =_{E_{ad}(Q)} E_{ad}(g)(z) and the equalizer map as e(z) ≡ π_{1}(z) ∈ E_{ad}(P) for z ∈ Σ_{z∈E_{ad}(P)} E_{ad}(f)(z) =_{E_{ad}(Q)} E_{ad}(g)(z).

E_{ad} preserves the initial object, which is the type ⊥ in U_{ad}, since 0 =_{N} 1 is not provable in T_{ad}. E_{ad} preserves binary coproducts since in T_{ad} we can prove that N is the union of even numbers and

of odd numbers. Given two predicates P and Q, the binary coproduct of E_{ad}(P) and E_{ad}(Q) in U_{ad} is given by E_{ad}(P) + E_{ad}(Q) and the 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).

E_{ad} preserves list objects since in U_{ad} we can define the bijection enc : N → List(N). The list object of a given a predicate P in U_{ad} is List(E_{ad}(P)), and the list maps are defined as r_{o}^{E_{ad}(P)}(z) ≡ ϵ ∈ List(E_{ad}(P)) for z ∈ ⊤ and r_{1}^{E_{ad}(P)}(z) ≡ cons(π_{1}(z), π_{2}(z)) for z ∈ List(E_{ad}(P)) × E_{ad}(P). We define a morphism σ : List(E_{ad}(P)) → E_{ad}(List(P)) by induction on the list z ∈ List(E_{ad}(P)) as follows:

σ(z) ≡ \{ \begin{matrix}< 0, eq > & if z = ϵ \\ < 2^{c} · 2^{π_{1}(a)} + σ(s), eq > & if z = cons(s, a) \end{matrix}

where c ≡ min{ x : N | x ≥ σ(s) }.

The inverse morphism σ^{−1} : E_{ad}(List(P)) → List(E_{ad}(P)) is defined for z ∈ E_{ad}(List(P)) as σ^{−1}(z) ≡ ρ(z, lh(enc^{−1}(π_{1}(z)))) ∈ List(E_{ad}(P)) where in turn ρ(z, n) ∈ List(E_{ad}(P)) is defined by induction on the natural number n as follows:

ρ(z, n) ≡ \{ \begin{matrix}ϵ & if n = 0 \\ cons(ρ(z, n − 1), < p_{n}(enc^{−1}(π_{1}(z))), eq >) & if 1 ≤ n ≤ lh(enc^{−1}(π_{1}(z))) \\ ρ(z, lh(enc^{−1}(π_{1}(z)))) & if n ≥ lh(enc^{−1}(π_{1}(z))) + 1 \end{matrix}

About E_{rl}, it remains to show that it preserves images, which follows since the bounded minimum of a primitive recursive subset can be defined in T_{rl}. The image object of a morphism E_{ad}(f) : E_{ad}(P) → E_{ad}(Q) in U_{ad} is defined as Im(E_{ad}(f)) ≡ Σ_{w∈E_{ad}(Q)} (Σ_{z∈E_{ad}(P)}E_{ad}(f)(z) =_{E_{ad}(Q)} w)/⊤, the image morphism ι : Im(E_{ad}(f)) → E_{ad}(Q) as ι(z) ≡ π_{1}(z) ∈ E_{ad}(Q) for z ∈ Im(E_{ad}(f)), and the projection morphism p : E_{ad}(P) → Im(E_{ad}(f) is p(z) ≡< E_{ad}(f)(z), [< z, eq >] >∈ Im(E_{ad}(f)) for z ∈ E_{ad}(P).

Thanks to this lemma we are ready to prove that:

Theorem 5.2 The syntactic categories U_{ad} and U_{rl} are equivalent to P red(S_{in}).

Proof. Since by proposition 4.8 we know that P red(S_{in}) is a regular locos, then thanks to theorem 3.13 and theorem 3.16 there exist an arithmetic lextensive functor and a regular locos functor, respectively J_{P red}^{ad} : U_{ad} ⟶ P red(S_{in}) and J_{P red}^{rl} : U_{rl} ⟶ P red(S_{in}) defined through the corresponding interpretations of T_{ad} and T_{rl} in P red(S_{in}), in turn defined as in subsection 3.1, analogously to the functor defined in the proof of theorem 3.10, being T_{ad} and T_{rl} fragments of Au.

It turns out that both J_{P red}^{ad} · E_{ad} and J_{P red}^{rl} · E_{rl} are naturally isomorphic to the identity functor after inspecting their actions on objects and morphisms.

Moreover, being U_{ad} and U_{rl} an initial up to iso arithmetic lextensive category and an initial up to iso regular locos respectively, E_{ad} · J_{P red}^{ad} : U_{ad} ⟶ U_{ad} and E_{rl} · J_{P red}^{rl} : U_{rl} ⟶ U_{rl} are naturally isomorphic to the corresponding identity functors and hence we conclude.

Corollary 5.3 The initial arithmetic lextensive category U_{ad} is equivalent to the initial regular locos U_{rl}.

From this corollary we conclude that in an initial arithmetic lextensive category pullback stable images and lists are definable. But, since the equivalence is built through the interpretation functors, defined in turn by induction on type and term constructors, we can not say to be able to construct images and lists internally to any arithmetic lextensive category.

Remark 5.4 At a first glance, we could have thought of P red(S_{in}) as an initial Skolem category closed under equalizers. But, we are not able to prove this, since, for example, the embedding of P red(S_{in}) in an initial finitely complete category does not preserve the terminal object of P red(S_{in}) unless we know that natural numbers can be decomposed disjointly in zero plus strictly positive numbers, namely unless we have finite disjoint coproducts.

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 list-arithmetic pretopos U_{Au} and also to the initial arithmetic pretopos U_{pn}.

To this purpose, analogously to the embeddings in theorem 5.2 we define E_{au} : P red(S_{in}) ⟶ U_{Au} as follows:

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

• E_{au}(f) ≡ < f(π_{1}(z)), eq >∈ Σ_{x∈N}Q(x) =_{N} 1 [z ∈ Σ_{x∈N}P (x) =_{N} 1]

for f : P → Q in P red(S_{in}).

Then, we can prove in the same way as in lemma 5.1 for E_{rl}:

Lemma 6.1 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 P red(S_{in}), by its universal property there exists a functor Ê_{au} : A_{in} ⟶ U_{Au} [CV98] defined as Ê_{au}((X, R)) ≡ X/R and Ê_{au}(f) ≡ Q(f) for f : (X, R) → (Y, S), where Q(f) is the unique map from the quotient X/R to Y/S such that Q(f)([x]_{X/R}) = [f(x)]_{Y/S} for x ∈ X.

Moreover, Ê_{au} preserves all the list-arithmetic pretopos structure since it is an exact functor by the property of exact completion and also:

Lemma 6.2 The functor Ê_{au} : A_{in} ⟶ U_{Au} preserves finite disjoint coproducts and list objects.

Proof. Clearly, Ê_{au} preserves the initial object. Indeed, Ê_{au}((⊥, x =_{⊥} x)) = ⊥/(x =_{⊥} x) which is isomorphic to ⊥.

We prove that Ê_{au} preserves the binary coproduct structure. The binary coproduct of Ê_{au}((X, R)) and Ê_{au}((Y, S)) is X/R + Y/S with the coproduct structure as described in 5.1 for U_{ad}. Then, we show how to build a bijection γ : Ê_{au}((X + Y, R + S)) → Ê_{au}((X, R)) + Ê_{au}((Y, S)) that is defined as the unique map induced on the quotient by a map σ : X + Y → X/R + Y/S defined by induction on the coproduct as follows: for w ∈ X + Y

σ(w) ≡ \{ \begin{matrix}inl([x]_{X/R}) & if w = inl(x) \\ inl([y]_{Y/R}) & if w = inr(y) \end{matrix}

The inverse map γ^{−1} : Ê_{au}((X, R)) + Ê_{au}((Y, S)) → Ê_{au}((X + Y, R + S)) is defined by induction on the coproduct as follows:

γ^{−1}(w) ≡ \{ \begin{matrix}ĩnl(z_{1}) & if w = inl(z_{1}) \\ ĩnr(z_{2}) & if w = inr(z_{2}) \end{matrix}

where ĩnl : X/R → X + Y/R + S is the unique induced on the quotient X/R from the map σ : X → X + Y/R + S defined as σ(x) ≡ [inl(x)]_{X+Y/R+S} for x ∈ X and preserving the relation R by definition of R + S, while analogously ĩnr : Y/S → X + Y/R + S is the unique induced on the quotient Y/S from the map σ : Y → X + Y/R + S defined as σ′(y) ≡ [inr(y)]_{X+Y/R+S} for y ∈ Y and preserving the relation S by definition of R + S.

We prove that Ê_{au} preserves the list object structure. The list object on Ê_{au}(X, R) = X/R is List(X/R) with the already defined list structure as described in 5.1 for U_{ad}. Then, we show how to build a bijection γ : Ê_{au}((List(X), List(R)) → List(Ê_{au}(X, R)) that is defined as the unique map induced on the quotient by a map σ : List(X) → List(X/R) preserving the relation List(R) and defined by induction on List(X) as follows:

σ(w) ≡ \{ \begin{matrix}ϵ & if w = ϵ \\ cons(σ(s), [a]_{X/R}) & if w = cons(s, a) \end{matrix}

To prove that σ preserves the relation List(R), namely that if List(R)(w, w′) holds then σ(w) =_{List(X/R)} σ(w′) holds, we prove by induction on natural numbers that σ(part_{n}(w)) =_{List(X/R)} σ(part_{n}(w′)).

The inverse map γ^{−1} : List(Ê_{au}(X, R)) → Ê_{au}((List(X), List(R)) is defined by induction on List(X/R) as follows:

δ(z) ≡ \{ \begin{matrix}[ϵ]_{List(X)/List(R)} & if z = ϵ \\ c̃ons(δ(l), c) & if w = cons(l, c) \end{matrix}

where in turn c̃ons : List(X)/List(R)×X/R → List(X)/List(R) is the unique map induced on the quotients List(X)/List(R) and X/R such that c̃ons([l]_{List(X)/List(R)}, [a]_{X/R}) ≡ [cons(l, a)]_{List(X)/List(R)}.

Now, we are ready to prove:

Theorem 6.3 The syntactic category U_{Au} is equivalent to A_{in}.

Proof. Since by proposition 4.10 we know that A_{in} is a list-arithmetic pretopos, there exists a listarithmetic functor J_{au} : U_{Au} ⟶ A_{in} defined on objects and morphisms of U_{Au} through the interpretation I_{A_{in}} of Au in P gr(A_{in}) as in theorem 3.10.

Then, note that J_{A_{in}} · E_{au} is naturally isomorphic to Y, by inspecting its action on objects and morphisms, from which we get Y ≃ J_{A_{in}} · E_{au} ≃ J_{A_{in}} · (Ê_{au} · Y) ≃ (J_{A_{in}} · Ê_{au}) · Y and by the uniqueness property of the exact completion we conclude that J_{A_{in}} · Ê_{au} is naturally isomorphic to the identity functor.

Moreover, being U_{Au} an initial up to iso list-arithmetic pretopos we also get that Ê_{au}·J_{A_{in}} is naturally isomorphic to the identity functor.

Therefore, we conclude that U_{Au} is equivalent to A_{in}.

From the equivalence between the initial arithmetic universe A_{in} and the initial list-arithmetic pretopos U_{Au} we deduce that an internal language for the initial arithmetic universe A_{in} is the typed calculus Au. Analogously, we can prove that

Theorem 6.4 The syntactic category U_{pn} is equivalent to A_{in}.

and hence we deduce

Corollary 6.5 The initial list-arithmetic pretopos U_{Au} is equivalent to the initial arithmetic pretopos U_{pn}.

In other words, we can prove that parameterized list objects are definable in an initial arithmetic pretopos. But it is worth noticing also here, as after corollary 5.3, that because of the nature of the above equivalence, where one of the functors is defined by induction on type and term constructors, we can not directly deduce that any arithmetic pretopos is list-arithmetic.

7 Free internal categories and diagrams

In this section we show how to define free internal categories and diagrams within a list-arithmetic pretopos by means of its internal language. The key difficulty when performing these constructions is the lack of a recursion principle available on a proper subtype of a list type to define operations that can not be defined on the whole list type. We overcome this difficulty by defining such operations by recursion on natural numbers through iteration of suitable operations. In doing our constructions we will often make use of the fact that a list-arithmetic pretopos has got coequalizers.

7.1 Useful operations on list types

We describe some useful operations on list types that we are using in the following. Given s, s′ ∈ List(A) we abbreviate s · s′ for Rec(s, cons, s′) which is the operation appending a list to another one. Hence, for s ∈ List(A) and a ∈ A we will write s · a instead of s · cons(ϵ, a) and simply a for cons(ϵ, a). Moreover, in defining an operation by the elimination rule of the list type instead of writing the resulting proof-term we simply write the base and inductive steps necessary to define it.

Def. 7.1 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

Def. 7.2 Given a term ϕ(x) ∈ B [x ∈ A] we lift this term on the lists defining List(ϕ)(s) ∈ List(B) [s ∈ List(A)] by the elimination rule on the list type as follows

List(ϕ)(ϵ) ≡ ϵ List(ϕ)(s · a) ≡ List(ϕ)(s) · ϕ(a)

Def. 7.3 The type of non-empty lists is defined as

List^{∗}(A) ≡ Σ_{t∈List(A)} (Σ_{x∈A} Σ_{s∈List(A)} t =_{List(A)} cons(ϵ, x) · s)

We will often need to define operations on the type List^{∗}(A) of non-empty lists. In the next proposition we prove that we can define such operations by using an elimination rule analogous to that one for List(A) by defining the operation first on the lists of one element and then on the extension with a new element of a list on which the operation is supposed to be already defined.

Proposition 7.4 Given the type B(s) [s ∈ List^{∗}(A)] and the following terms

\begin{matrix}h_{1}(x) ∈ B(\overline{x}) [x ∈ A] \\ h_{2}(x, s, y, w) ∈ B( \overline{x · (s · y)} ) [x ∈ A, s ∈ List^{∗}(A), y ∈ A, w ∈ B( \overline{x · s} )] \end{matrix}

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

\begin{matrix}h^{∗}(\overline{x}) = h_{1}(x) \\ h^{∗}( \overline{x · (s · y)} ) = h_{2}(x, s, y, h^{∗}( \overline{x · s} ) ) \end{matrix}

where we use the following abbreviations: \overline{x · s} ≡< x·s, < x, < s, eq >>> \overline{x} ≡< x, < x, < ϵ, eq >>>.

In the next when we define the operations on List^{∗}(A) we will simply write a non-empty list s instead of < s, < x, < s′, eq >>> for some x ∈ A and s′ ∈ List(A). Analogously, to facilitate the reading, given an operation t(s) ∈ B [s ∈ List(A)] we simply write t(z) instead of t(π_{1}(z)) for z ∈ List^{∗}(A).

Def. 7.5 On List^{∗}(A), we define the operation front(s) ∈ List(A) [s ∈ List^{∗}(A)] taking the front of a non-empty list:

front(a) ≡ ϵ front(s · a) ≡ front(s) · a

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

back(a) ≡ ϵ back(s · a) ≡ s

Moreover, we define the projections first(s) ∈ A [s ∈ List^{∗}(A)] and last(s) ∈ A [s ∈ List^{∗}(A)] of the first and last element of a list:

first(a) ≡ a first(s · a) ≡ first(s) last(a) ≡ a last(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 the positive natural numbers as follows

p_{1}(s) ≡ first(s) p_{n}(s) ≡ \begin{cases}p_{n−1}(front(s)) & if 2 ≤ n ≤ lh(s) \\ p_{n−1}(s) & if 1 ≤ lh(s) ≤ n − 1 \end{cases}

Finally, we use projections to define the n-th part of a list part(s, n) List(A) [s ∈ List(A), n ∈ N] by induction on natural numbers as follows: given a list s ∈ List(A)

part(s, 0) ≡ ϵ part(s, n + 1) ≡ \begin{cases}part(s, n) · p_{n+1}(s) & if lh(s) ≥ 1 and n ≤ lh(s) − 1 \\ part(s, n) & if lh(s) ≥ 1 and n ≥ lh(s) \\ ϵ & if lh(s) = 0 \end{cases}

7.2 A list-arithmetic pretopos has got coequalizers

Now we are going to prove that any list-arithmetic pretopos U has got coequalizers, by using its internal language. Indeed, we show how by using the list type we can make the natural relation relating elements that coequalize two given maps into an equivalence relation.

Proposition 7.6 In any list-arithmetic pretopos U there exists the coequalizer of any two given morphisms

[figure: C; a; b; A]

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

R(z, z′) ≡ z =_{A⊕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: to express that an element z ∈ A is connect to w ∈ 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}, w)

it is enough to require a list < z, x_{1} >, < x_{1}, x_{2} >, < x_{2}, x_{3} >, < x_{3}, w > characterized by the fact that each element of the list x_{1}, x_{2}, x_{3} obtained by making the second projection of each element of the back list < z, x_{1} >, < x_{1}, x_{2} >, < x_{2}, x_{3} > is equal to the list obtained by making the first projection of the front list < x_{1}, x_{2} >, < x_{2}, x_{3} >, < x_{3}, w >.

Hence, we define:

\begin{aligned}R_{t}(z, z′) ≡ & Σ_{s∈List^{∗}(Σ_{w∈A×A}R(π_{1}(w),π_{2}(w)))} \overline{π_{2}}(back(s)) =_{List(A)} \overline{π_{1}}(front(s)) \\ & × z =_{A} π_{1}(π_{1}(first(s))) × z′ =_{A} π_{2}(π_{1}(last(s))) \end{aligned}

where \overline{π_{i}} ≡ List(π_{i}) for i = 1, 2. It follows easily that R_{t} is an equivalence relation and that [−] : C → C/R_{t}, that is the map assigning to every c ∈ C its equivalence class in C/R_{t}, is the coequalizer of a and b.

7.3 Free internal categories

Given a graph internal to an arithmetic universe U

[figure: G_{1}; δ_{o}; δ_{1}; G_{0}]

we build the free internal category generated by it (we refer to [Joh77] or [MM92] for a general account on these concepts about internal category theory) as follows.

Def. 7.7 Given the above graph in U we define the objects of the category C as C_{0} ≡ G_{0} and the morphisms as

C_{1} ≡ G_{0} ⊕ Ĉ_{1}

where G_{0} stands for the identity morphisms and

Ĉ_{1} ≡ Σ_{w∈List^{∗}(G_{1})} front · \overline{δ_{0}}(w) =_{List(G_{0})} back · \overline{δ_{1}}(w)

is the equalizer of the following maps:

[figure: List^{∗}(G_{1}); front·\overline{δ_{0}}; back·\overline{δ_{1}}; List(G_{0})]

where \overline{δ_{0}}(s) ≡ List(δ_{0}) · π_{1} and \overline{δ_{1}}(s) ≡ List(δ_{1}) · π_{1}.

The domain morphism δ′_{0} : C_{1} → G_{0} and the codomain morphism δ′_{1} : C_{1} → G_{0} are defined as the following codiagonal morphisms:

δ′_{0} ≡ id ⊕ (δ_{0} · (first · π_{1})) δ′_{1} ≡ id ⊕ (δ_{1} · (last · π_{1}))

The unit e_{C} : G_{0} → C_{1} is defined for x ∈ G_{0} as

e_{C}(x) ≡ inl(x)

It follows immediately that

δ′_{0} · e_{C} = id δ′_{1} · e_{C} = id

The composition of morphisms

Comp_{C_{1}}(w) ∈ C_{1} [w ∈ C_{1} ×_{G_{0}} C_{1}]

where C_{1} ×_{G_{0}} C_{1} ≡ Σ_{f∈C_{1}} Σ_{g∈C_{1}} δ′_{1}(f) =_{G_{0}} δ′_{0}(g) is the vertex of the pullback of δ′_{0} along δ′_{1}, is basically defined as a restriction of the list composition of lists on C_{1} ×_{G_{0}} C_{1} because by distributivity of sum with respect to pullbacks we have

(G_{0} ⊕ Ĉ_{1}) ×_{G_{0}} (G_{0} ⊕ Ĉ_{1}) ≅ (G_{0} ×_{G_{0}} G_{0}) ⊕ (G_{0} ×_{G_{0}} Ĉ_{1}) ⊕ (Ĉ_{1} ×_{G_{0}} G_{0}) ⊕ (Ĉ_{1} ×_{G_{0}} Ĉ_{1})

and on the members with factor G_{0} we just project the list. In detail the composition is defined by double elimination on the sum type as follows: for z ∈ C_{1}, z′ ∈ C_{1} such that < z, < z′, eq >>∈ C_{1} ×_{G_{0}} C_{1}

Comp_{C_{1}}(< z, < z′, eq >>) ≡ \begin{cases}inl(x) & if z = inl(x) = z′ for x ∈ G_{0} \\ inr(s′) & if z = inl(x) for x ∈ G_{0} and z′ = inr(s′) for s′ ∈ Ĉ_{1} \\ inr(s) & if z′ = inl(y) for y ∈ G_{0} and z = inr(s) for s ∈ Ĉ_{1} \\ inr(< π_{1}(s) · π_{1}(s′), eq > & if z = inr(s) for s ∈ Ĉ_{1} and z′ = inr(s′) for s′ ∈ Ĉ_{1} \end{cases}

For short we simply write comp_{C_{1}}(z, z′) instead of Comp_{C_{1}}(< z, < z′, eq >>).

It is easy to check that this is actually a composition, that is well defined with respect to the domain and the codomain

δ′_{0} · π′_{1} = δ′_{0} · Comp_{C_{1}} δ′_{1} · π′_{2} = δ′_{1} · Comp_{C_{1}}

where π′_{1} and π′_{2} are the first and second projections of the pullback of δ′_{0} along δ′_{1}, and that is associative

Comp_{C_{1}} · (Comp_{C_{1}} × id) = Comp_{C_{1}} · (id × Comp_{C_{1}})

by using double elimination on

(G_{0} ×_{G_{0}} G_{0}) ⊕ (G_{0} ×_{G_{0}} Ĉ_{1}) ⊕ (Ĉ_{1} ×_{G_{0}} G_{0}) ⊕ (Ĉ_{1} ×_{G_{0}} Ĉ_{1})

In an analogous way, it is straightforward to prove that this composition admits the above define e_{C} as unit map, that is

Comp_{C_{1}} · (e_{C} × id) = π′_{2} Comp_{C_{1}} · (id × e_{C}) = π′_{1}

Then, we prove

Proposition 7.8 Internally to any list-arithmetic pretopos, given the graph

[figure: G_{1}; δ_{0}; δ_{1}; G_{0}]

then the category defined above in 7.7 as

\xymatrix{C_{1} \ar[r]^{δ′_{0}} \ar[r]_{δ′_{1}} & G_{0} \ar[l]|{e_{C}}} Comp_{C_{1}} : C_{1} ×_{G_{0}} C_{1} → C_{1}

is the free internal category generated by it.

Proof. Let C_{0} and C_{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_{0} is the identity map and j_{1} : G_{1} → C_{1} is defined as i_{1}(f) ≡ inr(< \overline{f}, eq >) for f ∈ G_{1}. Now, we prove the universal property. Given another internal category with the corresponding composition map

\xymatrix{D_{1} \ar[r]^{ϕ_{0}} \ar[r]_{ϕ_{1}} & D_{0} \ar[l]|{e_{D}}} Comp_{D_{1}} : D_{1} ×_{D_{0}} D_{1} → D_{1}

such that ψ_{0} : G_{0} → D_{0} and ψ_{1} : G_{1} → D_{1} are graph morphisms, we need to define an internal functor given by

ψ̂_{0} : C_{0} → D_{0}  ψ̂_{1} : C_{1} → D_{1}

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

ψ̂_{0} ≡ ψ_{0}

Then, in order to define ψ̂_{1}, we first define a map

m : Ĉ_{1} → D̂_{1}

as the unique map towards the equalizer D̂_{1} of front · \overline{ϕ_{0}} and back · \overline{ϕ_{1}} with respect to the map

List^{∗}(ψ_{1}) · p : Ĉ_{1} → List^{∗}(G_{1}) → List^{∗}(D_{1})

where List^{∗}(ψ_{1}) is the map induced from ψ_{1} on the corresponding non-empty list types by considering the internal category (D_{0}, D_{1}, ϕ_{0}, ϕ_{1}, e_{D}) simply as a graph and p : Ĉ_{1} → List^{∗}(G_{1}) is defined as p(z) ≡ π_{1}(z) for z ∈ Ĉ_{1}. Indeed, the map List^{∗}(ψ_{1}) · j equalizes front · \overline{ϕ_{0}} and back · \overline{ϕ_{1}} by the property of graph morphism

ϕ_{0} · ψ_{1} = ψ_{0} · δ_{0} ϕ_{1} · ψ_{1} = ψ_{0} · δ_{1}

Then, to reach D_{1} we define a map app : D̂_{1} → D_{1} by observing that we can not use an inductive elimination rule on D̂_{1} as we did with List^{∗}(G_{1}) thanks to proposition 7.4. Hence, we define app by fixing a list s obtained by projection from D̂_{1} and we compose the first element of the list with the second and so on, namely we iterate this operation for a number of times equal to the length of s. In essence we define app by using an operation ϕ(s, n) defined in turn by induction on natural numbers.

Def. 7.9 The operation

ϕ(s, n) ∈ D_{1} [s ∈ D̂_{1}, n ∈ N]

is defined in a way as

ϕ(s, 0) ≡ p_{1}(π_{1}(s)) ϕ(s, n + 1) ≡ \begin{cases}comp_{D_{1}}(ϕ(s, n), p_{n+2}(π_{1}(s))) & if n ≤ lh(s) − 2 \\ ϕ(s, n) & if n ≥ lh(s) − 1 \end{cases}

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

(Σ_{x∈D_{1}} δ_{1}(x) =_{G_{0}} δ_{0}(p_{n+2}(π_{1}(s))) × n ≤ lh(π_{1}(s)) − 2) + (Σ_{x∈D_{1}} n ≥ lh(π_{1}(s)) − 1) [s ∈ D̂_{1}, n ∈ N]

defined by induction on natural numbers essentially as ϕ together with a proof of the needed extra information. Finally, we put

app(s) ≡ ϕ(s, lh(π_{1}(s)) − 1)

and by means of app and m we define

ψ̂_{1} ≡ (e_{D} · ψ_{0}) ⊕ (app · m)

Clearly, it follows that ψ̂_{1} · j_{1} = ψ_{1}. In order to prove that ψ̂_{1} is functorial we need some lemmas.

Lemma 7.10 For every z_{1} ∈ D̂_{1}, z_{2} ∈ D̂_{1} such that δ′_{1}(inr(z_{1})) = δ′_{0}(inr(z_{2})) then if n ≤ lh(π_{1}(z_{1})) − 1

ϕ(comp_{D_{1}}(z_{1}, z_{2}), n) =_{D_{1}} ϕ(z_{1}, n)

Proof. By induction on n ∈ N.

Note that for s ∈ D̂_{1} by induction on the length of s we can prove that

ϕ_{0} · app(s) =_{D_{0}} ϕ_{0}(p_{1}(π_{1}(s))) = ϕ′_{0}(inr(s)) ϕ_{1} · app(s) =_{D_{0}} ϕ_{1}(last(π_{1}(s))) = ϕ′_{1}(inr(s))

considering that, when proving the second equation, p_{lh(s)}(s) =_{A} last(s) is derivable. Hence, the terms in the next lemma are well defined.

Lemma 7.11 Given z_{1} ∈ D̂_{1}, z_{2} ∈ D̂_{1} such that δ′_{1}(inr(z_{1})) = δ′_{0}(inr(z_{2})) and n ∈ N we derive

comp_{D_{1}}(ϕ(z_{1}, l_{1}), ϕ(z_{2}, n)) =_{D_{1}} ϕ(comp_{D_{1}}(z_{1}, z_{2}), l_{1} + n)

where l_{1} = lh(π_{1}(z_{1})) − 1.

Proof. By induction on n ∈ N.

Thanks to the above lemmas it is easy to check that

ϕ_{0} · ψ̂_{1} = ψ̂_{0} · δ′_{0}  ϕ_{1} · ψ̂_{1} = ψ̂_{0} · δ′_{1}  ψ̂_{1} · e_{C} = e_{D} · ψ̂_{0}
Comp_{D_{1}} · (ψ̂_{1} × ψ̂_{1}) = ψ̂_{1} · Comp_{C_{1}}

Now we prove the uniqueness of (ψ̂_{0}, ψ̂_{1}). Suppose that there exists an internal functor given by ρ_{0} : C_{0} → D_{0} and ρ_{1} : C_{1} → D_{1} such that ρ_{0} · j_{0} = ψ_{0} and ρ_{1} · j_{1} = ψ_{1}. Then, since j_{0} = id obviously ρ_{0} = ψ̂_{0} and it remains to prove that also ρ_{1} = ψ̂_{1}. To this purpose we prove the following lemma.

Lemma 7.12 Given an internal functor ρ_{0} : C_{0} → D_{0} and ρ_{1} : C_{1} → D_{1} such that ρ_{0} · j_{0} = ψ_{0} and ρ_{1} · j_{1} = ψ_{1} we derive: for z ∈ Ĉ_{1} and n ∈ N

ρ_{1}(inr(< part(π_{1}(z), n), eq >)) =_{D_{1}} ψ̂_{1}(inr(< part(π_{1}(z), n), eq >))

Proof. By induction on n ∈ N.

Then, by the elimination rule on the sum type C_{1} and knowing that part(s, lh(s)) =_{List(A)} s holds by lemma 7.12 we can derive ψ̂_{1}(z) =_{D_{1}} ρ_{1}(z) for z ∈ C_{1}. Therefore, we conclude that the claimed construction is the free category internally to a list-arithmetic pretopos. (of proposition 7.8)

7.4 Free internal diagrams

Applying the same technique adopted for the construction of a free category, we can also lift diagrams on a graph internal to a list-arithmetic pretopos to internal diagrams on the free category generated by the graph. Also here, when proving the universal property of a free internal diagram we need to define an operation on a proper subtype of a list type that can not be defined on the whole list type. Since no induction is available on this subtype, we define our operation by means of suitable operations defined by induction on natural numbers as we did when defining the map app in the previous subsection.

Proposition 7.13 Internally to any list-arithmetic pretopos, given the internal graph

[figure: G_{1}; δ_{o}; δ_{1}; G_{0}]

and the following internal diagram π_{0} : F → G_{0} with the action μ : F ×_{G_{0}} G_{1} → F - where F ×_{G_{0}} G_{1} is the vertex of the pullback of δ_{o} along π_{0} - such that the following diagram commutes

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

we can lift μ to an unique action on C_{1}

μ̃ : F ×_{G_{0}} C_{1} → F

where F ×_{G_{0}} C_{1} ≡ Σ_{f∈F} Σ_{z∈C_{1}} π_{0}(f) =_{G_{0}} δ′_{0}(z) is the vertex of the pullback of δ′_{o} along π_{0}, that is μ̃ is an internal diagram on the underlying graph of the free category C ≡ (C_{0}, C_{1}, δ′_{o}, δ′_{1}, e_{C}, Comp_{C_{1}}) such that

π_{0} · μ̃ = δ′_{1} · π′_{2}

where π′_{1} and π′_{2} are respectively the first and the second projection of the pullback of δ′_{0} along π_{0}, and the following diagrams commute

\xymatrix{F ×_{C_{0}} C_{0} \ar[r]^{id×e} \ar[dr]_{π′_{1}} & F ×_{C_{0}} C_{1} \ar[d]_{μ̃} & F ×_{C_{0}} C_{1} ×_{C_{0}} C_{1} \ar[r]^{μ̃×id} \ar[d]_{id×Comp_{C_{1}}} & F ×_{C_{0}} C_{1} \ar[d]^{μ̃} \\  & F & F ×_{C_{0}} C_{1} \ar[r]_{μ̃} & F}

where F ×_{C_{0}} C_{1} ×_{C_{0}} C_{1} ≡ Σ_{f∈F} Σ_{z_{1}∈C_{1}} Σ_{z_{2}∈C_{1}} π_{0}(f) =_{G_{0}} δ′_{o}(z_{1}) × δ′_{1}(z_{1}) =_{G_{0}} δ′_{o}(z_{2}) is the vertex of the pullback along π′_{2} of the first projection of the pullback of δ′_{o} along δ′_{1}.

Proof. In order to define the action μ̃, note that by distributivity of sums with respect to pullbacks we get

F ×_{G_{0}} C_{1} = F ×_{G_{0}} (G_{0} ⊕ Ĉ_{1}) ≃ (F ×_{G_{0}} G_{0}) ⊕ (F ×_{G_{0}} Ĉ_{1})

Hence, by the elimination rule on the sum type we define μ̃ : F ×_{G_{0}} C_{1} → F as follows: for f ∈ F, z ∈ C_{1} such that < f, < z, eq >>∈ F ×_{G_{0}} C_{1}

μ̃(< f, < z, eq >>) ≡ \begin{cases}f & if z = inl(x) for x ∈ G_{0} \\ μ̂(f, s) & if z = inr(s) for s ∈ Ĉ_{1} such that π_{0}(f) = δ′_{0}(inr(s)) \end{cases}

where μ̂(f, s) ≡ ν(f, s, lh(π_{1}(s)) − 1) and ν(f, s, n) ∈ F [f ∈ F, s ∈ Ĉ_{1}, d ∈ π_{0}(f) =_{G_{0}} δ′_{0}(inr(s))] is defined as follows:

ν(f, s, 0) = μ(f, p_{1}(π_{1}(s))) ν(f, s, n+1) = \begin{cases}μ(ν(f, s, n), p_{n+2}(π_{1}(s))) & if n ≤ lh(π_{1}(s)) − 2 \\ ν(f, s, n) & if n ≥ lh(π_{1}(s)) − 1 \end{cases}

But in order to assure the well definedness of the above definition we need to know that π_{0}(ν(f, s, n)) = δ′_{0}(p_{n+2}(π_{1}(s))). Therefore, ν is formally obtained by applying the first projection on the corresponding term of type

( Σ_{x∈F} π_{0}(x) =_{G_{0}} δ_{0}(p_{n+2}(π_{1}(s))) × n ≤ lh(π_{1}(s))−2 ) + ( Σ_{x∈F} n ≥ lh(π_{1}(s))−1 ) [s ∈ Ĉ_{1}, n ∈ N]

defined by induction on natural numbers essentially as ν together with a proof of the needed extra information. It follows that μ̃ is an internal diagram, namely that

π_{0} · μ̃ = δ′_{1} · π′_{2}  μ̃ · id × e_{C} = π′_{1}  μ̃ · (μ̃ × id) = μ̃ · (id × Comp_{C_{1}})

and that μ̃ is unique by proving similar lemmas to those regarding ψ̂_{1} of theorem 7.8 in the previous subsection.

8 Conclusions.

As the initial arithmetic universe A_{in} is equivalent to the initial list-arithmetic pretopos U_{Au}, we propose the notion of list-arithmetic pretopos as the general definition of arithmetic universe. Of course, being A_{in} equivalent to an initial arithmetic pretopos as well, we could also choose the notion of arithmetic pretopos for that. But we do not make this choice because, while we are able to define free internal categories and diagrams in any list-arithmetic pretopos, as Joyal did in any of his arithmetic universes, we doubt that this is possible in any arithmetic pretopos.

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]. Finally, I wish to thank Pino Rosolini and Silvio Valentini for their generous promptness in discussing my research work and surely Andrè Joyal for his interest in this work.

References

[Ben85] J. Benabou. Fibred categories and the foundations of naive category theory. Journal of Symbolic Logic, 50:10–37, 1985.

[CC82] A. Carboni and R. Celia Magno. The free exact category on a left exact one. Journal of Australian Math. Soc., 33:295–301, 1982.

[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.

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

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

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

[Hof94] M. Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Proceedings of CSL’94, September 1994.

[Jac99] B. Jacobs. Categorical Logic and Type Theory., volume 141 of Studies in Logic. Elsevier, 1999.

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

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

[Mai] M.E. Maietti. Locality of list objects via internal language. Manuscript, 2001.

[Mai98] M.E. Maietti. The internal type theory of an Heyting Pretopos. In C.Paulin-Mohring E. Gimenez, editor, Types for Proofs and Programs. Selected papers of International Workshop Types ’96, Aussois, volume 1512 of LNCS, pages 216–235. Springer Verlag, 1998.

[Mai99] 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.

[Mai00] M.E. Maietti. Theories generated by finite lex decidable sketches in an arithmetic universe. Technical report, University of Padova, n.9, December 2000.

[Mai01] M.E. Maietti. Modular correspondence between dependent type theories and categorical universes. Mittag-Leffler Preprint Series, 44, 2001.

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

[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.

[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.

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

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

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