The typed calculus of arithmetic universes.

Maria Emilia Maietti

School of Computer Science University of Birmingham Edgbaston, Birmingham B15 2TT, United Kingdom mem@cs.bham.ac.uk

Abstract

The notion of arithmetic universe was introduced by A. Joyal to give a categorical proof of Gödel incompleteness theorems. To this purpose, through an exact completion process he built a category to be understood as the initial arithmetic universe.

Here, we consider a general definition of an arithmetic universe to be a pretopos with parameterized recursive objects. For such arithmetic universes we present a valid and complete typed calculus based on dependent types and proof-terms. This typed calculus is also shown to provide the internal type theory of an arithmetic universe. Then we prove that in any arithmetic universe we can build free categories and free internal diagrams as in Joyal’s construction.

Contents

1 Introduction 3

2 The typed calculus Au 4

3 The syntactic arithmetic universe 7 3.1 The disjoint coproduct . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.2 The quotient of an equivalence relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.3 The list object . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

4 The semantics in an arithmetic universe 13 4.1 The model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 The interpretation and validity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

4.2.1 The partial interpretation of the typed calculus Au . . . . . . . . . . . . . . . . . 19 4.2.2 The validity of the typed calculus Au . . . . . . . . . . . . . . . . . . . . . . . . 27

5 The completeness theorem 32

6 The internal type theory of a universe 36 6.1 The relation between the Au type theories and arithmetic universes . . . . . . . . . . . 38

7 The free arithmetic universe 40

8 Free internal categories and diagrams 42 8.1 Useful operations on list types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 8.2 An arithmetic universe has got coequalizers . . . . . . . . . . . . . . . . . . . . . . . . . 47 8.3 Free internal categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 8.4 Free internal diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

9 Conclusions 53

10 Acknowledgements 53

References 53

1 Introduction

Some categories like elementary toposes are said universes since they provide models for certain kinds of set theory or type theories that may be regarded as their internal languages.

The concept of arithmetic universe was invented by A. Joyal to prove Gödel incompleteness theorems in some lectures given in the seventies (see Wraith’s notes [Wra85]). He considered the initial Skolem category, that is the initial category with finite products and parameterized natural numbers object. Then he built the exact completion of its subcategory of recursive predicates to be considered as the initial arithmetic universe where to prove Gödel theorems.

Here we propose a general definition of an arithmetic universe to be a pretopos with parameterized recursive objects, whose Joyal’s categorical construction is an instance. In support of our definition we prove that the above categorical requirements are sufficient to allow such arithmetic universes to have free internal categories and free internal diagrams as in Joyal’s construction. This is proved contrary to what is claimed in [Mor96].

The proof is done by means of the internal language of an arithmetic universe, which is shown here to be a dependent typed calculus.

Indeed, following the style of Martin-Löf’s type theory [Mar84], we introduce a typed lambda calculus, called Au, which is valid and complete with respect to these arithmetic universes. The notion of categorical model and the technique to prove these results are the same to those used in [Mai98a] for the typed calculi of Heyting pretoposes and toposes.

The typed calculus Au is just the type theory of Heyting pretoposes [Mai98b] without the forall type, but with the list type in addition. More precisely the typed calculus Au consists of the terminal type, the indexed sum type, the extensional equality type - all these corresponding to finite limits -, the quotient type based only on mono equivalence relations - corresponding to the quotient of an equivalence relation -, the disjoint sum type together with the false type - corresponding to finite disjoint coproducts - and finally the list type for dependent types - corresponding to parameterized recursive objects -. We can also prove that the categories of this kind of dependent type theories is biequivalent to the categories of arithmetic universes, i.e. Au is the internal language of arithmetic universes. In order to interpret the dependent types, we use the fact that any arithmetic universe is locally an arithmetic universe, i.e. for every object A ∈ ObU of an arithmetic universe U, U/A is an arithmetic universe, which follows from the fact that a locos with parameterized recursive objects happens to be locally a locos as shown in [Coc90]. The categorical interpretation of a dependent typed calculus is more complex than that one of a simple typed calculus where types are interpreted as objects and terms as morphisms. Indeed, we interpret a dependent type under a context as a sequence of morphisms of the arithmetic universe and a dependent term as a morphism of a suitable comma category of the arithmetic universe. Substitution of a term in types and terms is dealt with pullback. But, since pullbacks are defined up to isomorphisms, to overcome coherence problems we use the split fibration [Ben85], [Jac91], [Hof94] associated to the codomain fibration of an arithmetic universe. Our notion of model combines that one given by display maps [HP89],

[See84] together with the tools provided by contextual categories to interpret substitution correctly [Car86].

One of the key point to get an internal typed calculus for arithmetic universes is the characterization of subobjects in terms of dependent types with at most one proof, called mono types. We say that a dependent type B(x)[x ∈ A] is mono, when

y = z ∈ B(x) [x ∈ A, y ∈ B(x), z ∈ B(x)]

is derivable. The name is justified by the fact that in the categorical semantics we adopt the interpretation of a mono type turns out to be in correspondence with a monomorphism. The mono type is the crucial concept for the proof-theoretical characterization of effective quotients based only mono equivalence relations.

According to the style of Martin-Löf’s type theory, for every type we give a formation rule and introduction, elimination and conversion rules for terms of the same type. However, to prove the completeness theorem of Au with respect to the class of arithmetic universes, we need two axioms out of this schema: effectiveness for quotients of mono equivalence relations and disjointness of sums.

By means of this typed calculus we can build free categories and free internal diagrams. The key point in doing these constructions is to define some operations on proper subsets of list types that can not be defined on the whole list type by the usual elimination rule on lists. We counter this difficulty by defining such operations by recursion on natural numbers, namely as the outcome of suitable iterations.

Our ultimate goal is to use such a typed calculus as a logical tool to explore what kind of free algebras can be build in an arithmetic universe.

2 The typed calculus Au

We start with the description of the dependent typed calculus Au, which we will prove to be valid and complete with respect to arithmetic universes in the next sections. This typed system 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 following we present the formation rules for types and the introduction and elimination rules for terms. 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], [Pit95]. 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 and the set equality rule

conv) \frac{a ∈ A [Γ] A = B [Γ]}{a ∈ B [Γ]}

Moreover, by the following rule we assume typed variables

var) \frac{Γ, x ∈ A, Δ cont}{x ∈ A [Γ, x ∈ A, Δ]}

We can derive then the structural rules of weakening and of a suitable exchange. Now, we give the formation rules for types specific to Au and then the introduction, elimination and conversion rules of its terms. We omit the corresponding equality rules for all type and term constructors, which are necessary to derive the various substitution rules. We adopt the usual definitions of bound and free occurrences of variables and we identify two terms under α-conversion.

Remark 2.1 In the following, 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 Au calculus

Terminal type

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

False type

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

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)]}{split(d, m) ∈ M(d)}

C-Σ) \frac{b ∈ B c ∈ C(b) m(x, y) ∈ M(⟨x, y⟩) [x ∈ B, y ∈ C(x)]}{split(⟨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} ∈ 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]}{D(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]}{D(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]}{D(inr(b), a_{C}, a_{B}) = a_{B}(b) ∈ A(inr(b))}

Disjointness

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

Quotient type

Q) \frac{\begin{matrix}R(x, y) type [x ∈ A, y ∈ A], & z = w ∈ R(x, y)[x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)] \\ c_{1} ∈ R(x, x)[x ∈ A], & c_{2} ∈ R(y, x)[x ∈ A, y ∈ A, z ∈ R(x, y)] \\ c_{3} ∈ R(x, z)[x ∈ A, y ∈ A, z ∈ A, w ∈ R(x, y), w′ ∈ R(y, z)] \end{matrix}}{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] = [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)]}{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)]}{Q(l, [a]) = l(a) ∈ L([a])}

Effectiveness

\frac{a ∈ A b ∈ A [a] = [b] ∈ A/R}{f(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)]}{Rec_{l}(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)]}{Rec_{l}(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)]}{Rec_{l}(a, l, cons(s, c)) = l(s, c, Rec_{l}(a, l, s)) ∈ L(cons(s, c))}

Thus, we have finished with the presentation of our calculus.

In the following we shall often omit the word type in the type judgements. Note that the disjointness axiom is not derivable from the other rules. Indeed, we can obtain a model for the calculus, which falsifies disjointness by using a domain with only one element (see [Smi88]), where the quotient type A/R is interpreted as A.

Actually, from now on, we will refer to an equivalent formulation of the calculus Au, where the elimination and conversion rules for the indexed sum type are replaced by the following rules:

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))}

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

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

We call mono every type for which we can prove

\frac{B(x) type [x ∈ A]}{y = z ∈ B(x) [x ∈ A, y ∈ B(x), z ∈ B(x)]}

also called proof-irrelevant, for example in [Hof97].

In the following, given a judgement b(x) ∈ B(x)[x ∈ A] by the expression

(x)b(x)

we mean the equivalence class of b(x) ∈ B(x)[x ∈ A] under the following relation:

b(x) ∈ B(x)[x ∈ A] ∼ b(y) ∈ B(y)[y ∈ A]

Moreover, we write b for (x)b(x). Actually, in order to have such expressions we should pass to the type theory with higher ariety [NPS90], with the warning that what it is a type here, it is a set in [NPS90]. By adding the so called function type given b(x) ∈ B(x)[x ∈ A] we have the abstraction, that is (x)b ∈ (x ∈ A)B(x), the application, the β-conversion and the η-conversion, that is (x)b(x) = b ∈ (x ∈ A)B(x).

Note that the E-quotient and C-quotient rules of the quotient type are derivable, by using the indexed sum type, from the following restricted elimination rule of the quotient type for types not depending on A/R E_{s}-quotient

\frac{M type m(x) ∈ M [x ∈ A] m(x) = m(y) ∈ M [x ∈ A, y ∈ A, d ∈ R(x, y)]}{Q_{s}(m, z) ∈ M [z ∈ A/R]}

together with the following two conversion rules, also derivable in Au: one is the β-conversion β_{s}C-quotient

\frac{a ∈ A m(x) ∈ M [x ∈ A] m(x) = m(y) ∈ M [x ∈ A, y ∈ A, d ∈ R(x, y)]}{Q_{s}(m, [a]) = m(a) ∈ M}

and the other one is the η-conversion stating the uniqueness of Q_{s} η_{s}C-quotient

\frac{t(z) ∈ M [z ∈ A/R]}{Q_{s}((x)t([x]), z) = t(z) ∈ M [z ∈ A/R]}

Also, the E-list rule and the conversion rules of the list type are derivable, by using the indexed sum type, from the following restricted elimination rule of the list type for types not depending on List(C) E_{s}-list

\frac{L type a ∈ L l(z, x) ∈ L [z ∈ L, x ∈ C]}{Rec_{s}(a, l, s) ∈ L [s ∈ List(C)]}

together with the following three conversion rules, also derivable in Au: two are the β-conversions β_{s}C_{1}-list

\frac{L type a ∈ L l(z, x) ∈ L [z ∈ L, x ∈ C]}{Rec_{s}(a, l, 0) = a ∈ L}

β_{s}C_{2}-list

\frac{L type a ∈ L l(z, y) ∈ L [z ∈ L, y ∈ C]}{Rec_{s}(a, l, cons(x, y)) = l(Rec_{s}(a, l, x), y) ∈ L [x ∈ List(C), y ∈ C]}

and the other one is the η-conversion stating the uniqueness of Rec_{s} η_{s}C-list

\frac{\begin{matrix}a ∈ L & l(z, y) ∈ L [z ∈ L, y ∈ C] & t(z) ∈ L [z ∈ List(C)] \\ t(ϵ) = a ∈ L & t(cons(x, y)) = l(t(x), y) ∈ L [x ∈ List(C), y ∈ C] \end{matrix}}{Rec_{s}(a, l, z) = t(z) ∈ L [z ∈ List(C)]}

Remark 2.2 Note that the extensional propositional equality type is crucial to derive the conversion rules stating the uniqueness of the elimination constants for the quotient type and the list type.

3 The syntactic arithmetic universe

We recall the categorical definition of a pretopos [MR77], [JM95] since the definition of an arithmetic universe is based on it.

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

Def. 3.2 An arithmetic universe is a list-arithmetic pretopos.

We recall that a category U with binary products is list-arithmetic if it has got parameterized recursive objects [Coc90]. We say that a category U has recursive objects if for all objects A, B ∈ ObU, there is an object rec(A, B) and morphisms r_{o}^{A,B} and r_{1}^{A,B} such that for every b : B → Y and g : Y × A → Y there is an unique rec(b, g) such that the following diagrams commute

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

A recursive object is parameterized if for every object A the pullback functor along !_{A} : A → 1 preserves recursive objects, where !_{A} is the unique morphism from A to a terminal object 1. From now on we call rec(A, 1) list-object on A. Note that to have parameterized recursive objects is sufficient to check that for all objects A, B the object rec(A, 1) × B is isomorphic to the recursive object rec(A, B). In order to understand how the calculus Au is related to this categorical notion of arithmetic universe, against to the usual practice, we proceed immediately to show how to build an arithmetic universe out of a Au dependent type theory, i.e. Au possibly with other dependent types and corresponding terms. This construction will be used to prove the completeness theorem of Au with respect to arithmetic universes. We define the syntactic category U_{Au} as follows.

Def. 3.3 The objects of U_{Au} are the closed types of Au, A, B, C … and the morphisms between two types, A and B, are the expressions (x)b(x) (see [NPS90]) corresponding to

b(x) ∈ B[x ∈ A]

where the type B does not depend on A. The composition in U_{Au} is defined by substitution, that is given (x)b(x) ∈ U_{Au}(A, B) and (y)c(y) ∈ U_{Au}(B, C) their composition is (x)c(b(x)). We state that (x)b(x) ∈ P (A, B) and (x)b′(x) ∈ P (A, B) are equal iff we can derive

b(x) = b′(x) ∈ B [x ∈ A]

The identity is (x)x ∈ P (A, A) obtained by x ∈ A [x ∈ A].

Now we are going to prove that

Proposition 3.4 The category U_{Au} is an arithmetic universe.

First of all we prove that U_{Au} has finite limits. The terminal object is ⊤ and from any object A the morphism towards ⊤ is

(x)⋆ ∈ U_{Au}(A, ⊤)

which is unique by the conversion rule for ⊤. Given c ∈ U_{Au}(A, C) and d ∈ U_{Au}(B, C) the pullback is given by

Σ_{x∈A}Σ_{y∈B}Eq(C, c(x), d(y))

where the first projection to A is

(z)π_{1}^{A}(z) ∈ U_{Au}(Σ_{x∈A}Σ_{y∈B}Eq(C, c(x), d(y)), A)

and the second projection to B is

(z)π_{1}^{B}(π_{2}^{A}(z)) ∈ U_{Au}(Σ_{x∈A}Σ_{y∈B}Eq(C, c(x), d(y)), B)

From now on, we simply write a =_{A} b to mean Eq(A, a, b) and often we will simply write eq_{C}, instead of eq_{C}(c). Moreover we will often omit the type annotation in the projections, i.e. for example we simply write π_{1} instead of π_{1}^{A}.

3.1 The disjoint coproduct

The coproduct of A and B is defined by A + B, where the injections are

(x) inl(x) ∈ U_{Au}(A, A + B) and (y) inr(y) ∈ U_{Au}(B, A + B)

Given c ∈ U_{Au}(A, C) and d ∈ U_{Au}(B, C) the mediating morphism c⊕d from A+B to C is (w)D(w, c, d). Coproducts are disjoint by the rule of disjointness. Moreover, coproducts are stable under pullback. To this purpose we first prove a very useful lemma.

Remark 3.5 In the next proofs we will not make use of disjointness axiom.

Lemma 3.6 A + B is isomorphic in U_{Au} to

Σ_{w∈A+B}(Σ_{x∈A} inl(x) =_{A+B} w) + (Σ_{y∈B} inr(y) =_{A+B} w)

Proof. We put the following abbreviations

A +_{P} B ≡ Σ_{w∈A+B}(Σ_{x∈A} inl(x) =_{A+B} w) + (Σ_{y∈B} inr(y) =_{A+B} w)

and for any w ∈ A + B

Ã(w) ≡ Σ_{x∈A} inl(x) =_{A+B} w  B̃(w) ≡ Σ_{y∈B} inr(y) =_{A+B} w

where the injections of Ã(w) + B̃(w) are called

inl^{P} (z) ∈ Ã(w) + B̃(w) [z ∈ Ã(w)] inr^{P} (z) ∈ Ã(w) + B̃(w) [z ∈ B̃(w)]

We consider (z)π_{1}(z) ∈ U_{Au}(A +_{P} B, A + B) and we define its inverse δ as

(w)⟨w, D(w, d_{1}, d_{2})⟩ ∈ U_{Au}(A + B, A +_{P} B)

where d_{1} corresponds to

inl^{P} (⟨x, eq_{A+B}⟩) ∈ Ã(inl(x)) + B̃(inl(x)) [x ∈ A]

and d_{2} corresponds to

inr^{P} (⟨y, eq_{A+B}⟩)Ã(inr(y)) + B̃(inr(y)) [y ∈ B]

We can easily see that π_{1} is the inverse morphism of δ. Indeed, π_{1} · δ = id follows from the elimination rule for the disjoint sum type. In order to prove that δ · π_{1} = id, that is to find a proof of

⟨π_{1}(z), D(π_{1}(z), d_{1}, d_{2})⟩ = z ∈ A +_{P} B [z ∈ A +_{P} B]

it is sufficient to derive a proof of

D(π_{1}(z), d_{1}, d_{2}) = π_{2}(z) ∈ Ã(π_{1}(z)) + B̃(π_{1}(z)) [z ∈ A +_{P} B]

To this purpose we show how by the elimination rule for the disjoint sum type we derive a proof of

D(π_{1}(z), d_{1}, d_{2}) =_{A+_{P} B} z_{2} [z ∈ A +_{P} B, z_{2} ∈ Ã(π_{1}(z)) + B̃(π_{1}(z))]

Indeed, given z ∈ A +_{P} B and w_{1} ∈ Ã(π_{1}(z)), we get inl(π_{1}^{A}(w_{1})) = π_{1}(z) ∈ A + B and then

D(π_{1}(z), d_{1}, d_{2}) = D(inl(π_{1}^{A}(w_{1})), d_{1}, d_{2}) = inl^{P} (⟨π_{1}^{A}(w_{1}), eq_{A+B}⟩) = inl^{P} (w_{1})

that is we get a proof of D(π_{1}(z), d_{1}, d_{2}) =_{A+_{P} B} inl^{P} (w_{1}) [z ∈ A +_{P} B, w_{1} ∈ Ã(π_{1}(z))]. Analogously, we derive a proof of D(π_{1}(z), d_{1}, d_{2}) =_{A+_{P} B} inr^{P} (w_{2}) [z ∈ A +_{P} B, w_{2} ∈ B̃(π_{1}(z))]. So, given z ∈ A +_{P} B, by elimination rule with respect to Ã(π_{1}(z)) + B̃(π_{1}(z)) we get a proof of

D(π_{1}(z), d_{1}, d_{2}) =_{A+_{P} B} z_{2} [z ∈ A +_{P} B, z_{2} ∈ Ã(π_{1}(z)) + B̃(π_{1}(z))]

Now, given z ∈ A +_{P} B, since π_{2}(z) ∈ Ã(π_{1}(z)) + B̃(π_{1}(z)) then by substitution and by elimination of the extensional equality type we conclude

D(π_{1}(z), d_{1}, d_{2}) = π_{2}(z) ∈ Ã(π_{1}(z)) + B̃(π_{1}(z))

Proposition 3.7 In U_{Au} coproducts are stable under pullbacks.

Proof. Given the following pullbacks

\xymatrix{P_{1} \ar[d]_{π_{1}^{1}} \ar[r]^{π_{2}^{1}} & A \ar[d]^{a} & P_{2} \ar[d]_{π_{1}^{2}} \ar[r]^{π_{2}^{2}} & B \ar[d]^{b} & P \ar[d]_{π_{1}^{P}} \ar[r]^{π_{2}^{P}} & A + B \ar[d]^{a⊕b} \\ D \ar[r]^{m} & C & D \ar[r]^{m} & C & D \ar[r]^{m} & C}

we have to show that in U_{Au}/D

π_{1}^{1} ⊕ π_{1}^{2} ≃ π_{1}^{P}

For this purpose we define

γ : P_{1} + P_{2} → P

as γ ≡ (w)D(w, d_{1}, d_{2}) where d_{1} corresponds to

⟨π_{1}(w_{1}), ⟨inl(π_{1}(π_{2}(w_{1}))), eq_{C}⟩⟩ ∈ P [w_{1} ∈ P_{1}]

and d_{2} corresponds to

⟨π_{1}(w_{2}), ⟨inr(π_{1}(π_{2}(w_{2}))), eq_{C}⟩⟩ ∈ P [w_{2} ∈ P_{2}]

We can notice that π_{1}^{P} · γ = π_{1}^{1} ⊕ π_{1}^{2} and that π_{2}^{P} · γ = (inl · π_{2}^{1}) ⊕ (inr · π_{2}^{2}). Moreover, we want to define

γ^{−1} : P → P_{1} + P_{2}

First of all, we consider that, given w ∈ P, we get π_{1}(π_{2}(w)) ∈ A + B, hence, by δ defined in the above lemma we deduce

π_{2}(δ(π_{1}(π_{2}(w)))) ∈ Ã(π_{1}(π_{2}(w))) + B̃(π_{1}(π_{2}(w)))

Now, we use the elimination rule with respect to Ã(π_{1}(π_{2}(w))) + B̃(π_{1}(π_{2}(w))) and we define

γ^{−1} ≡ (w)D(π_{2}(δ(π_{1}(π_{2}(w)))), d′_{1}, d′_{2})

where d′_{1} corresponds to

inl(⟨π_{1}(w), ⟨π_{1}(x′), eq_{C}⟩⟩) ∈ P_{1} + P_{2} [w ∈ P, x′ ∈ Ã(π_{1}(π_{2}(w)))]

Indeed, from w ∈ P and x′ ∈ Ã(π_{1}(π_{2}(w))) we get

m(π_{1}(w)) = (a ⊕ b)(π_{1}(π_{2}(w))) and π_{1}(π_{2}(w)) = inl(π_{1}(x′))

and hence m(π_{1}(w)) = a(π_{1}(x′)). In an analogous way, we define d′_{2} as

inr(⟨π_{1}(w), ⟨π_{1}(y′), eq_{C}⟩⟩) ∈ P_{1} + P_{2} [w ∈ P, y′ ∈ B̃(π_{1}(π_{2}(w)))]

We can prove that γ^{−1} is the inverse morphism of γ. In particular to prove that γ · γ^{−1} = id we derive by the elimination rule on the quotient type a proof-term for

γ(D(z, d′_{1}, d′_{2})) =_{P} w [w ∈ P, z ∈ Ã(π_{1}(π_{2}(w))) + B̃(π_{1}(π_{2}(w)))]

and substituting z with π_{2}(δ(π_{1}(π_{2}(w)))) we conclude that γ(γ^{−1}(w)) = w.

3.2 The quotient of an equivalence relation

Given an equivalence relation

[figure: R; g; A × A]

in the syntactic category U_{Au}, we consider the following mono type:

R(x, x′) ≡ Σ_{y∈R}g(y) =_{A×A} ⟨x, x′⟩[x ∈ A, x′ ∈ A]

It is easy to check that the categorical definition of equivalence relation implies that R(x, x′)[x ∈ A, x′ ∈ A] is an equivalence relation from the type-theoretical point of view. Let A/R be the quotient with respect to R(x, x′)[x ∈ A, x′ ∈ A]. We can prove that (z)[z] ∈ U_{Au}(A, A/R) is the coequalizer of π_{1} · g ∈ U_{Au}(R, A) and π_{2} · g ∈ U_{Au}(R, A) by the elimination and conversion rules of the quotient type. The uniqueness property of the coequalizer follows from the η_{s}C-quotient rule. In U_{Au} the categorical equivalence relations are effective, that is π_{1} · g and π_{2} · g are projections (or kernel pair) for the pullback of (z)[z] along itself. The existence of a morphism towards the pullback vertex is guaranteed by the effectiveness axiom and its uniqueness follows from the fact that equivalence relations are monic. Moreover, we prove stability of quotients for equivalence relations.

Proposition 3.8 In U_{Au} equivalence relations are stable effective.

Proof. In the following we write π_{i}^{A×D} for the i’th projection from the vertex of the pullback of suitable arrows A → · ← D. We will omit to label the projections when their domains and codomains are clear from the context. Given m ∈ U_{Au}(D, A/R) let us consider the following pullbacks:

\xymatrix{ &  & Q \ar[dd]_{π_{1}^{D×R}} \ar[r]^{π_{2}^{D×R}} & R \ar[d]_{π_{1}·g} \ar[d]^{π_{2}·g} \\ P \ar[r]^{π_{2}^{D×A}} \ar[d]_{π_{1}^{D×A}} & A \ar[d]^{(z)[z]} &  & A \ar[d]^{(z)[z]} \\ D \ar[r]^{m} & A/R & D \ar[r]^{m} & A/R}

where

P ≡ Σ_{w∈D}Σ_{x∈A}Eq(A/R, m(w), [x]) and Q ≡ Σ_{w∈D}Σ_{y∈R}Eq(A/R, m(w), [(π_{1} · g)(y)])

Moreover, let us consider these two pullbacks:

\xymatrix{Q \ar[d]_{(π_{2}^{D×A})^{∗}(π_{1}·g)} \ar[r]^{π_{2}^{D×R}} & R \ar[d]^{π_{1}·g} & Q \ar[d]_{(π_{2}^{D×A})^{∗}(π_{2}·g)} \ar[r]^{π_{2}^{D×R}} & R \ar[d]^{π_{2}·g} \\ P \ar[r]_{π_{2}^{D×A}} & A & P \ar[r]_{π_{2}^{D×A}} & A}

where

(π_{2}^{D×A})^{∗}(π_{1} · g) ≡ (w)⟨π_{1}(w), ⟨π_{1}(g(π_{1}(π_{2}(w)))), eq⟩⟩

and

(π_{2}^{D×A})^{∗}(π_{2} · g) ≡ (w)⟨π_{1}(w), ⟨π_{2}(g(π_{1}(π_{2}(w)))), eq⟩⟩

We must show that in P/U_{Au}

π_{1}^{D×A} ≃ coeq((π_{2}^{A})^{∗}(π_{1} · g), (π_{2}^{A})^{∗}(π_{2} · g))

We recall that the objects of the category P/U_{Au} are the morphisms b : P → B of U, and the morphisms of P/U_{Au} from b : P → B to b′ : P → B′ are the morphisms t : B → B′ of U such that t · b = b′. We can observe that the pullback given by the effectiveness

\xymatrix{R \ar[d]_{π_{1}·g} \ar[r]^{π_{2}·g} & A \ar[d]^{(z)[z]} \\ A \ar[r]^{(z)[z]} & A/R \\ D \ar[ur]_{m}}

can be completed in a cube of pullbacks and hence

[figure: Q; (π_{2}^{A})^{∗}(π_{1}·g); (π_{2}^{A})^{∗}(π_{2}·g); P; π_{1}^{D×A}; P; π_{1}^{D×A}; D]

is a pullback. Therefore ⟨π_{2}^{∗}(π_{1} · g), π_{2}^{∗}(π_{2} · g)⟩ is an equivalence relation as kernel pair of π_{1}^{D×A}. Then let us consider the coequalizer of π_{2}^{∗}(π_{1} · g) and π_{2}^{∗}(π_{2} · g)

[−]_{P} : P → P/m^{∗}(R)

where P/m^{∗}(R) is the quotient type with respect to the equivalence relation ⟨π_{2}^{∗}(π_{1} · g), π_{2}^{∗}(π_{2} · g)⟩. Since π_{1}^{D×A} · π_{2}^{∗}(π_{1} · g) = π_{1}^{D×A} · π_{2}^{∗}(π_{2} · g) there exists a map

Q^{P} : P/m^{∗}(R) → D

such that Q^{P} · [−]_{P} = π_{1}^{D×A}. Now we want to prove that Q^{P} is an isomorphism in P/U_{Au}. In order to define the inverse of Q^{P} we need the following lemma:

Lemma 3.9 For every equivalence relation R on A we prove that A/R is isomorphic to

Σ_{z∈A/R} (Σ_{x∈A}([x] =_{A/R} z))/⊤

Proof. We define in Au

ϕ : A/R → Σ_{z∈A/R} (Σ_{x∈A}([x] =_{A/R} z))/⊤

as ϕ(z) ≡ ⟨z, Q(z, (x)[⟨x, eq⟩])⟩ for z ∈ A/R and

ϕ^{−1} : Σ_{z∈A/R} (Σ_{x∈A}([x] =_{A/R} z))/⊤ → A/R

as ϕ^{−1}(z′) ≡ π_{1}(z′) for z′ ∈ Σ_{z∈A/R}Σ_{x∈A}([x] =_{A/R} z)/⊤. It is immediate to see ϕ^{−1} · ϕ = id and ϕ · ϕ^{−1} = id follows from the fact that Σ_{x∈A}([x] =_{A/R} z)/⊤ is a mono type for every fixed z ∈ A/R.

Remark 3.10 Note that the type A/⊤ can be proved to be mono because of the extensionality feature of our quotients types that is expressed by the fact that two equivalent terms belong to definitionally equal equivalent classes.

Now we go back to prove that Q^{P} is an isomorphism by finding its inverse. By means of ϕ defined in the above lemma we define: for d ∈ D

Q^{P}^{−1}(d) ≡ Q(π_{2}(ϕ(m(d))), (w)[⟨d, ⟨π_{1}w, eq⟩⟩])

where the elimination constant Q is referred to the type (Σ_{x∈A}([x] =_{A/R} m(d)))/⊤. This term is well typed by effectiveness. Then by the elimination rule on the quotient type P/m^{∗}(R) it is easy to prove that Q^{P}^{−1} · Q^{P} = id. Moreover, note that Q^{P}^{−1} is mono by the elimination rule on the quotient type and effectiveness. Hence Q^{P} · Q^{P}^{−1} = id also follows. This concludes the proof that π_{1}^{D} is a coequalizer of (π_{2}^{A})^{∗}(π_{1} · g) and (π_{2}^{A})^{∗}(π_{2} · g).

3.3 The list object

The syntactic arithmetic universe is equipped with recursive objects. To this purpose we prove that for every object A there exists a list object rec(A, 1) and that B ×rec(A, 1) is the recursive object rec(A, B) for every object B. For every closed type A, the list object rec(A, 1) is List(A). The empty map is

(x)ϵ ∈ U_{Au}(⊤, List(A))

and the list-constructor map corresponds to (z)cons(π_{1}(z), π_{2}(z)) ∈ U_{Au}(List(A) × A, List(A)). We proceed directly to show that B × List(A) is the recursive object rec(A, B), since it includes the case where B is the terminal object. Given a closed type Y and the morphisms f ∈ U_{Au}(B, Y) and g ∈ U_{Au}(Y × A, Y) we can prove that there exists a unique morphism t ∈ U_{Au}(B × List(A), Y) such that the following diagram commutes in all its parts:

[figure: B; id×((x)ϵ); f; B×List(A); t; (B×List(A))×A; cons; t×id; Y; Y ×A; g]

Indeed by the elimination rule of the list type we can define

t ≡ (z)Rec_{s}(f(π_{1}(z)), g, π_{2}(z)) ∈ U_{Au}(B × List(A), Y)

which is the unique map making the diagrams commute by β_{s} and η_{s} C-list conversion rules.

Remark 3.11 Note that the extensional propositional equality type is crucial to get an arithmetic universe out of the category U_{Au}, if we consider terms as morphisms and the definitional equality as the equality of morphisms. Indeed, we need the extensional equality type to get equalizers. We also used it to prove the uniqueness related to the universal properties for the various categorical constructors and their stability under pullback.

4 The semantics in an arithmetic universe

Our notion of model for the typed calculus Au described in the previous section combines the notion of model given by display maps [HP89], [See84] together with the tools provided by contextual categories to interpret substitution correctly [Car86]. This is the same notion used in in [Mai98a] to provide the semantics for the typed calculi of Heyting pretoposes and toposes. We shall emphasize context formation. Indeed, the judgement B [Γ], asserting that B is a dependent type under the context Γ, is interpreted as a suitable sequence of morphisms of U to the terminal object. Moreover, the judgement b ∈ B[Γ], asserting that b is a term of type B under the context Γ, is interpreted as a section of the last morphism of the sequence representing the dependent type B. Since we want to express substitution by means of pullback, which is determined up to isomorphisms, we use fibred functors, as in [Hof94], to interpret substitution correctly. But in our semantics, a type judgement corresponds to a sequence of fibred functors, which represents the type under a context with all its possible substitutions, and a term judgement corresponds to a natural transformation, which also represents the term under a context with all its possible substitutions.

Our model for Au corresponds to particular contextual categories, where the category of contexts is equivalent to the universe under consideration. Indeed, our model is given by an arithmetic universe, with a choice of its structure, where the interpretation of judgements is defined by taking the reindexing functor of the split fibration equivalent to the codomain fibration of the universe. It is worthwhile to say that it is enough to consider a split fibration of the codomain fibration in order to obtain a correct interpretation not only of substitution, but also of all the other constructors.

4.1 The model

Since we intend to model a typed calculus, we shall assume that with an arithmetic universe a given choice of its categorical constructors is made. More precisely with an arithmetic universe U we fix choices of

• finite limits: 1 is the terminal object and for every object A of U the unique morphism to the terminal object is !_{A} : A → 1; for all t : D → A and f : B → A the following diagram is a pullback

[figure: D_{Σ}; t^{∗}(f); f^{∗}(t); D; t; B; f; A], so that for every f : A → B we can define the pullback functor f^{∗} : U/B → U/A,

which associates f^{∗}(t) to every t : D → A and to every morphism b : t → s of U/B the unique morphism ⟨f^{∗}(t),_{B} b · t^{∗}(f)⟩ to the pullback of s along f; since we have defined pullback, the product of A and B is the vertex of the pullback of !_{A} and !_{B} and the two projections are π_{1}^{A} ≡ !_{A}^{∗}(!_{B}) : A × B → A and π_{2}^{B} ≡ !_{B}^{∗}(!_{A}) : A × B → B, and finally the equalizer of a : A → B and b : A → B is (⟨a, b⟩)^{∗}(⟨id_{B}, id_{B}⟩) : E → A, where ⟨a, b⟩ is the unique morphism to the product B × B such that π_{1}^{B} · ⟨a, b⟩ = a and π_{2}^{B} · ⟨a, b⟩ = b;

• finite coproducts: O is the initial object and, for every object A of U, the unique morphism from the initial object is ?_{A} : O → A; for all objects A and B in U, A ⊕ B is the coproduct together with the injections ϵ_{1} : A → A ⊕ B and ϵ_{2} : B → A ⊕ B and given a : A → C and b : B → C a ⊕ b : A ⊕ B → C is the unique morphism such that a ⊕ b · ϵ_{1} = a and a ⊕ b · ϵ_{2} = b;

• quotients of equivalence relations: for every equivalence relation ρ : R → A × A there is a quotient c = coeq(π_{1} · ρ, π_{2} · ρ), where π_{i} for i = 1, 2 are the two projections of the pullback of !_{A} : A → 1 along itself;

• for every object A in U, a recursive object rec(A, 1), with the empty map r_{o}^{A} : 1 → rec(A, 1) and the list-constructor map r_{1}^{A} : rec(A, 1) × A → rec(A, 1).

An essential feature for the interpretation of a dependent typed calculus is the local property of the universe under consideration. Indeed, for every object A of the arithmetic universe U, the comma category U/A is an arithmetic universe. This is a consequence of the fact shown in [Coc90] that a locos - i.e. a category with finite limits, stable disjoint coproducts and parameterized recursive objects - is local in the sense that any of its slice categories is a locos, too. Lastly note that in the slice category U/D for an object D of the arithmetic universe U given an equivalence relation

[figure: R; ρ; r; A×_{D}A; a·π_{1}; D]

⟨π_{1} · ρ, π_{2} · ρ⟩ : R → A × A is also an equivalence relation in U, where π_{i} : A ×_{D} A → A for i : 1, 2 are the projections of the pullback of a : A → D along itself in U. Indeed the functor Σ_{D} : U/D → U that sends an object b : B → D of U/D to B and a morphism t : b → b′ of U/D to t : B → B′ preserves coequalizers and equivalence relations in the above sense, i.e. if ρ = ⟨π_{1} · ρ,_{D} π_{2} · ρ⟩ is an equivalence relation in U/D then ⟨π_{1} · ρ, π_{2} · ρ⟩ is an equivalence relation in U. Therefore Σ_{D} preserves quotients of equivalence relations, since it has got a right adjoint !_{D}^{∗}. These observations let us conclude that being an arithmetic universe property is inherited by slice categories.

The reason to require the local property of the structure of a universe is that constructing a type depending on a context Γ from other types corresponds to a categorical property of U/A, where A is determined by Γ. Moreover, since substitution corresponds to pullback, the various categorical properties must be stable under pullback.

The idea is to interpret a dependent type as a sequence of morphisms of an arithmetic universe U ending with the terminal object 1, whereas the terms are sections of the last morphism of the type to which they belong. Thus, we consider the algebraic development of the fibration cod of U: it is the category P gr(U).

Def. 4.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 such that b_{n} · b = a_{n}

[figure: A_{n}; b; a_{n}; B_{n}; b_{n}; 1; A_{1}; !_{A_{1}}; A_{n−1}; a_{n−1}]

provided n = m and a_{i} = b_{i} for i = 1, ..., n − 1.

Remark 4.2 We recall that given a category U we can define the category U^{→}, whose objects are the morphisms of U

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

Besides, given an arithmetic universe U the following functors are fibrations (see [Ben85], [Jac91] for the definition):

• cod_{U} : U^{→} ⟶ U defined by:

( [figure: X; ϕ; A] ) ↦ A  and  (f, u)  ↦  u

• dom_{U} : U^{→} ⟶ U defined by:

( [figure: X; ϕ; A] ) ↦ X  and  (f, u)  ↦  f

Remark 4.3 We would like to interpret substitution by means of pullback, using the reindexing pseudofunctor F : U^{OP} ⟶ Cat with respect to the fibration cod_{U} defined as follows: F associates to every A ∈ ObU the category U/A and to every morphism f : B → A of U the pullback pseudofunctor f^{∗} : U/A → U/B. But, in general, for an arbitrary choice of pullbacks, F would not be a functor: for instance, even F (id) may not be an identity. Therefore, if substitution were interpreted by F then it would not be well defined. The solution is to replace F by an equivalent pseudofunctor S : U^{OP} ⟶ Cat, which is indeed a functor [Ben85], [Jac91]. S is defined as follows. For every object A in U, S(A) ≡ F ib(U/A, U^{→}), where 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}). 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. Moreover, for a morphism

f : B → A of U, the functor S(f) : F ib(U/A, U^{→}) → F ib(U/B, U^{→}) associates to every fibred functor σ a fibred functor σ[f]. σ[f] is defined as follows: for every t : C → B, σ[f](t) ≡ σ(f · t). Besides, for every natural transformation ρ, S(f)(ρ) ≡ ρ[f], where ρ[f](t) ≡ ρ(f · t) for every t : C → B. S is the reindexing functor with respect to the fibration p_{G(S)} : F ib(U/−, U^{→}) → U, which is the Grothendieck construction on the functor S defined as follows. The object of F ib(U/−, U^{→}) are (A, σ) such that σ ∈ ObF ib(U/A, U^{→}) and the morphisms from (A, σ) to (B, τ) are (f, ρ), where f ∈ U(A, B) and ρ : σ → S(f)(τ) is a morphism of F ib(U/A, U^{→}). The fibration G(S) is a projection: p_{G(S)}(A, σ) = A for every (A, σ) ∈ ObF ib(U/−, U^{→}) and p_{G(S)}((f, ρ)) = f for every (f, ρ) ∈ MorF ib(U/−, U^{→}). Note that the pseudofunctor F : U^{OP} ⟶ Cat is equivalent to the functor S in the appropriate 2-category of pseudofunctors, and also the codomain fibration cod_{U} is equivalent to p_{G(S)}. The functors establishing such an equivalence can be described as follows. We define a functor

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

which associates to every σ ∈ ObF ib(U/A, U^{→}) its evaluation σ(id) on the identity of the object A, and for every σ, τ ∈ ObF ib(U/A, U^{→}) the morphism part

(−)(id)_{σ,τ} : S(A)(σ, τ) → U/A(σ(id), τ(id))

associates to every ρ ∈ S(A)(σ, τ) the morphism [figure: D; ρ(id); σ(id); B; τ(id); A] . Moreover, we define the functor

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

establishing the equivalence with (−)(id). The object part of (−)(id) associates to every object b : B → A of U/A the fibred functor b̂, defined as b̂(t) ≡ t^{∗}(b) for every t : D → A and extended to morphisms by the universal property of pullback. For every a : C → A and b : B → A, the morphism part of (−)(id)

ˆ(−)_{â,b̂} : U/A(a, b) → S(A)(â, b̂)

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),_{B} g · a^{∗}(t)⟩), where ⟨â(t),_{B} g · a^{∗}(t)⟩ is the unique morphism to the pullback of b along t induced by â(t) and g · a^{∗}(t).

We use fibred functors to interpret the dependent types with all its possible substitutions, as in [Hof94]. Moreover, we use natural transformations to represent terms with all its possible substitutions. We call preinterpretation an assignment of fibred functors to type judgements and of natural transformations to term judgements. To this purpose, we consider the category P gf(U), where the judgements of the typed calculus Au are preinterpreted. We put I(σ) = A if σ ∈ [U/A, U^{→}].

Def. 4.4 The objects of the category P gf(U) are finite sequences σ_{1}, σ_{2}, ..., σ_{n} of fibred functors such that σ_{1}(id_{A_{1}}), σ_{2}(id_{A_{2}}), ..., σ_{n}(id_{A_{n}}) is an object of P gr(U), where A_{i} = I(σ_{i}) for i = 1, ..., n. 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 they are natural transformations from the functor σ_{n} to τ_{n} such that, if A_{n} = I(σ_{n}) = I(τ_{n}), then for every b : B → A_{n} the second member of ρ(b) is the identity (recall that ρ(b) is a

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

In the following, we simply write σ_{i} instead of σ_{i}(id_{A_{i}}). Moreover, since the second member of ρ(b) is always the identity, we confuse ρ(b) with the first member ρ_{1}(b).

Besides, notice that by naturality any component ρ(b) of a morphism ρ of P gf(U) is determined

by the properties of pullback from ρ(id_{A_{n}}). Indeed, if we consider [figure: B; b; b; A_{n}; id; A_{n}] , we get that ρ(b)

is equal to ⟨σ_{n}(b),_{B} ρ(id_{A_{n}}) · q(b, σ_{n}(id))⟩, from σ_{n}(b) to τ_{n}(b), and it is the unique morphism to the pullback of τ_{n}(id) along b, according to the functorial choice of pullbacks of τ, induced by σ_{n}(b) and ρ(id_{A_{n}}) · q(b, σ_{n}(id)) . We conclude that ρ ≡ (−)(id)_{σ,τ}^{−1}(ρ(id)).

Finally, for every A ∈ ObU, we define the fibred functor i_{A} : U/A → U^{→} associating to every triangle

[figure: C; t; b′; B; b; A] the following pullback diagram [figure: C; t; id; B; id; C; t; B] .

4.2 The interpretation and validity

Given an arithmetic universe U, before defining the interpretation, we define a preinterpretation Ĩ_{U}_{|} : Au ⟶ P gf(U) on the type and term judgements derivable in the typed calculus Au. Ĩ_{U}_{|} will turn out to 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.

The preinterpretation says how to interpret a dipendent type and a typed term after any possible substitution. The interpretation of type and term judgements corresponds to evaluate their preinterpretations on the identical substitution. Moreover, we define a valuation V : P gf(U) ⟶ P gr(U) in this manner: for every object of P gf(U) σ_{1}, σ_{2}, ..., σ_{n}

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

where A_{i} = I(σ_{i}) for i = 1, ..., n, and for every morphism ρ of P gf(U) between σ_{1}, σ_{2}, ..., σ_{n} and τ_{1}, τ_{2}, ..., τ_{n}

V(ρ) = ρ(id_{A_{n}})

Finally, the interpretation I_{U} : Au ⟶ P gr(U) is defined as I_{U} ≡ V · Ĩ_{U}_{|}

[figure: Au; I_{U}; _{Ĩ_{U}_{|}}; P gr(U); P gf(U); V]

So, a type judgement of Au will be preinterpreted as a sequence of fibred functors, since a fibred functor is used to represent the dependent type with all the possible substitutions in its free variables [Hof94], and it will turn out to be interpreted as an object of P gr(U), by the evaluation of the fibred functors on the identical substitution. Precisely, a type judgement with empty context, that is a closed type, will be simply interpreted as a sequence of only one arrow to the terminal object 1 of U: for example, every judgement of Au

A type [ ] will be preinterpreted as a fibred functor

α_{1} : U/1 → U^{→}

and interpreted as

[figure: A_{Σ}; !_{A_{Σ}}; 1]

since α_{1}(id_{1}) =!_{A_{Σ}} where A_{Σ} = dom(α_{1}(id_{1})). More generally, a dependent type judgement of Au

B(x_{1}, ..., x_{n}) [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n−1}(x_{1}, ..., x_{n−1})]

will be preinterpreted as the object of P gf(U)

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

and hence interpreted as

[figure: 1; A_{Σ1}; α_{1}(id); A_{Σn}; α_{n}(id); B_{Σ}; β(id)]

In the following, for short, we write Γ_{n} ≡ x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1}). 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). The typed term judgements will be interpreted as morphisms of P gr(U):

given the type judgement B(x_{1}, ..., x_{n}) [Γ_{n}] interpreted as [figure: 1; A_{Σ1}; α_{1}(id); A_{Σn}; α_{n}(id); B_{Σ}; β(id)] 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 it will be interpreted as b^{I}(id), that is a section of β(id)

[figure: A_{Σn}; b(id); id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

The equality between terms will be preinterpreted as equality between natural transformations and hence interpreted as the equality between morphisms of P gr(U). From now on, for short, we simply write b^{I} to mean b^{I}(id).

Essentially, we define the preinterpretation

Ĩ_{U} : pseudo(Au) ⟶ P gf(U)

as an a priori partial function on the pseudo-judgements of Au by induction on the complexity of their dependent types and terms (see, for example, [Pit95], [Str91]). Then we will show that the preinterpretation is well defined on the type and term judgements derivable in the calculus in the same time we prove the validity theorem by induction on the derivation of the judgement. Indeed we need the validity of some judgements about equality between types and terms in order to guarantee that the interpretation of some types and terms is well defined. With regard to this, consider for example the formation rule for quotient types where we require the equivalence relation to be a mono through a definitional equality judgement or even the set equality rule conv.

Remark 4.5 For a simple typed calculus we can give an interpretation of term judgements by induction on their derivations. Then we prove the validity theorem with respect to the equality judgements.

In a dependent typed calculus type or term judgements can be derived also from equality judgements and this is the case even with the only set equality rule conv. Hence, if the derivation of type and term judgements is not unique and requires certain conditions on equality judgements we can not define an interpretation for them by induction on the derivation and we opt for a partial interpretation.

4.2.1 The partial interpretation of the typed calculus Au

We define pseudo(Au) as the pseudo-judgements of Au, consisting of expressions of these four kinds

A(\underline{x}) type [Γ] A(\underline{x}) = B(\underline{x}) [Γ]
a(\underline{x}) ∈ A(\underline{x}) [Γ] a(\underline{x}) = b(\underline{x}) ∈ A(\underline{x}) [Γ]

where \underline{x} ≡ x_{1}, …, x_{n} and

• Γ ≡ [ ] or Γ ≡ x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1}) is a list of distinct typed variables, and A_{i}(x_{1}, ..., x_{i−1}) for i = 1, …, n is a raw type, that may depend on variables previously listed; we call this list a pseudo-context;

• A(\underline{x}) is a raw type, whose variables occur in the pseudo-context Γ;

• a(\underline{x}) is a raw term, whose variables occur in the pseudo-context Γ.

Remark 4.6 We will omit to write the type in the signature of a term. Indeed, we assume that whenever a new symbol is introduced in the introduction, elimination and conversion rules of the calculus about a term judgement a ∈ A [Γ], the types that should be appear in the signature of the term a are determined by A and by the types of the premisses.

We define an a priori partial preinterpretation Ĩ_{U} : pseudo(Au) ⟶ P gf(U) of the pseudo-judgements of the typed calculus Au

A type [Γ] a ∈ A [Γ]

by induction on the complexity of pseudo-judgements. The complexity of pseudo-judgements is defined by recursion, as in [Str91]. We assume to know the complexity of raw types and raw terms. We define the depth of a context. The depth of the empty context is 0. The depth of a pseudo-context Γ, x ∈ A is the complexity of the pseudo-judgement A type [Γ]. The complexity of a pseudo-judgement A type [Γ] is the sum of the complexity of the type-valued function symbol A with the depth of the pseudo-context Γ. The complexity of a pseudo-judgement a ∈ A [Γ] is the sum of the complexity of the term-valued function symbol a with the complexity of A type [Γ]. Moreover, we preinterpret the pseudo-contexts:

• for the empty context

Ĩ_{U}([ ]) ≡ 1

• for a generic pseudo-context

Ĩ_{U}(Γ, x ∈ A) ≡ Ĩ_{U}(A type [Γ])

As for the judgements, we define the partial preinterpretation of the pseudo-judgements of equality:

• Ĩ_{U}(A = B [Γ]) is preinterpreted as

Ĩ_{U}(A type [Γ]) = Ĩ_{U}(B type [Γ])

provided that Ĩ_{U}(A type [Γ]) and Ĩ_{U}(B type [Γ]) are defined;

• Ĩ_{U}(a = b ∈ A [Γ]) is preinterpreted as

Ĩ_{U}(a ∈ A [Γ]) = Ĩ_{U}(b ∈ A [Γ])

provided that Ĩ_{U}(a ∈ A [Γ]) and Ĩ_{U}(b ∈ A [Γ]) are defined.

Now, we proceed to define the partial preinterpretation Ĩ_{U} on the type and term pseudo-judgements of Au into P gf(U), and therefore the interpretation into P gr(U). In the inductive hypothesis, we will refer to the interpretation of a pseudo-judgement, assuming that also the preinterpretation is given. We recall that is sufficient to specify only the interpretation of a term, since its preinterpretation is the corresponding natural transformation of P gf(U) determined by its evaluation on the identity. The interpretation of the assumption of variable is the following: provided that the pseudo-judgement

C(x_{1}, ..., x_{n}, x) [Γ_{n}, x ∈ B(x_{1}, ..., x_{n})]

is interpreted as

!_{A_{σ1}}, α_{2}(id), ..., α_{n}(id), β(id), γ(id)

and the pseudo-judgement

B(x_{1}, ..., x_{n}) [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1}), x ∈ B(x_{1}, ..., x_{n}), y ∈ C(x_{1}, ..., x_{n}, x)]

as

!_{A_{σ1}}, α_{2}(id), ..., α_{n}(id), β(id), γ(id), β(γ(id) · β(id))

then

x ∈ B(x_{1}, ..., x_{n}) [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1}), x ∈ B(x_{1}, ..., x_{n}), y ∈ C(x_{1}, ..., x_{n}, x)]

is interpreted as

[figure: C_{Σ}; x^{I}; id; C_{Σ}×B_{Σ}^{2}; β(γ(id)·β(id)); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id); C_{Σ}; γ(id)]

where x^{I}(id) = γ(id)^{∗}(△_{B_{Σ}}) and △_{B_{Σ}} ≡ ⟨id_{B_{Σ}}, id_{B_{Σ}}⟩. In order to interpret the inference rule about the assumption of variable, when the context Δ is made of more than one typed variable, we repeat the semantic operation of weakening, interpreted as in the lemmas of weakening (we refer to section 4.2.2 for its interpretation). Now, we go on by defining the interpretation on the signature given by the formation, introduction and elimination rules for types and terms.

Remark 4.7 Note that we will write Â for the fibred functor ˆ !_{A} : U/1 → U^{→}.

1. The T erminal type pseudo-judgement as follows:

if the pseudo-context Γ_{n} is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

⊤ [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}×1_{Σ}; ˆ1(!_{A_{Σn}})]

where 1_{Σ} ≡ dom(id^{∗}(id_{1})), and we recall that the preinterpretation ˆ1 : U/1 → U^{→} is the functor

defined in the following manner: for every [figure: D; !_{D}; 1] we put ˆ1(!_{D}) = (!_{D})^{∗}(id_{1}) and on the morphisms it is defined through the pullback. Hence we get ˆ1(id_{1}) =!_{1_{Σ}}.

Moreover we interpret ⋆ ∈ ⊤ [Γ_{n}] as

[figure: A_{Σn}; ⋆^{I}(id); id; A_{Σn}×1_{Σ}; ˆ1(!_{A_{Σn}}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where ⋆^{I}(id) ≡ ⟨id_{A_{Σn}}, (!_{1Σ})^{−1}·!_{A_{Σn}}⟩.

2. The False type is interpreted by the initial object in a way analogous to the terminal type as follows. If the pseudo-context Γ_{n} is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

the F alse type pseudo-judgement

⊥ [Γ_{n}]

is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}×0_{Σ}; ˆ0(!_{A_{Σn}})]

where 0 is the initial object of U and 0_{Σ} ≡ dom((id_{1})^{∗}(!_{0})) and the preinterpretation ˆ0 : U/1 → U^{→} is the functor defined in the following manner: for every [figure: D; !_{D}; 1] we put ˆ0(!_{D}) = (!_{D})^{∗}(!_{0}). Therefore ˆ0(id_{1}) =!_{0_{Σ}}. On the morphisms it is defined through the pullback.

3. The Indexed Sum type.

Provided that the pseudo-judgement C(y) [Γ_{n}, y ∈ B] is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id); C_{Σ}; γ(id)]

we interpret

Σ_{y∈B}C(y) [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); C_{Σ}; Σ_{β}(γ)(id)]

where Σ_{β}(γ) : U/A_{Σn} → U^{→} is the functor defined in the following manner: for every [figure: D; t; A_{Σn}] we put Σ_{β}(γ)(t) = β(t) · γ(q(t, β(id))) and on the morphisms it is defined through the pullback. It is well defined, since the corresponding Beck-Chevalley conditions hold in any arithmetic universe. The pair term is interpreted in the following manner: provided that the pseudo-judgements b ∈ B [Γ_{n}] and c ∈ C(b) [Γ_{n}] are interpreted as

[figure: A_{Σn}; b^{I}; id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}; c^{I}; id; A_{Σn}×C_{Σ}; γ(b^{I}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

⟨b, c⟩ ∈ Σ_{y∈B}C(y) [Γ_{n}]

as

[figure: B_{Σ}; ⟨b,c⟩^{I}; id; C_{Σ}; Σ_{β}(γ)(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where ⟨b, c⟩^{I}(id) = q(b^{I}(id), γ(id)) · (c^{I}(id)). The first projection of the indexed sum type is interpreted in this manner: provided that the pseudo-judgement d ∈ Σ_{y∈B}C(y) [Γ_{n}] is interpreted as

[figure: A_{Σn}; d^{I}; id; C_{Σ}; Σ_{β}(γ)(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

π_{1}(d) ∈ B [Γ_{n}]

as

[figure: A_{Σn}; (π_{1}(d))^{I}; id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where (π_{1}(d))^{I}(id) ≡ γ(id) · (d^{I}(id)). The second projection of the indexed sum type is interpreted in this manner: provided that the pseudo-judgement d ∈ Σ_{y∈B}C(y) [Γ_{n}] is interpreted as

[figure: A_{Σn}; d^{I}; id; C_{Σ}; Σ_{β}(γ)(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

π_{2}(d) ∈ C(π_{1}(d)) [Γ_{n}]

as

[figure: A_{Σn}; (π_{2}(d))^{I}; id; A_{Σn}×C_{Σ}; γ(γ(id)·d^{I}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where (π_{2}(d))^{I}(id) ≡ ⟨id,_{B_{Σ}} d^{I}(id)⟩ is the unique morphism to the pullback between γ(id) and γ(id) · (d^{I}(id)).

4. The Equality type. Provided that the pseudo-judgements c ∈ C [Γ_{n}] and d ∈ C [Γ_{n}] are interpreted as

[figure: A_{Σn}; c^{I}; id; C_{Σ}; γ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}; d^{I}; id; C_{Σ}; γ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

Eq(C, c, d) [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); E_{Σ}; Eq(c^{I},d^{I})(id)]

where Eq(c^{I}, d^{I}) : U/A_{Σn} → U^{→} is the functor defined in the following manner: for every

\xymatrix{D \ar[r]^{t} & A_{Σn}} we put Eq(c^{I}, d^{I})(t) = (⟨c^{I}(t), d^{I}(t)⟩)^{∗}(△_{D×C_{Σ}}) with △_{D×C_{Σ}} ≡ ⟨id_{D×C_{Σ}}, id_{D×C_{Σ}}⟩.

It is well defined since each pullback functor preserves equalizers, as it enjoys a left adjoint. On the morphisms it is defined through the pullback.

The signature introduced in the introduction rule of the equality type is interpreted in the following manner:

provided that the pseudo-judgement c ∈ C [Γ_{n}] is interpreted as

[figure: A_{Σn}; c^{I}; id; C_{Σ}; γ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

eq_{C}(c) ∈ Eq(C, c, c) [Γ_{n}]

as

[figure: A_{Σn}; △_{C}(A_{Σn}); id; E_{Σ}; Eq(c^{I},c^{I})(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where △_{C}(A_{Σn}) ≡ ⟨id_{A_{Σn}},_{C} c^{I}(id)⟩ is the unique morphism to the pullback that defines the equalizer Eq(c^{I}, c^{I})(id) induced by id_{A_{Σn}} and c^{I}(id). Therefore, eq_{C}(c)^{I} ≡ { \atop △_{C}(A_{Σn})}.

5. The Disjoint Sum type.

Provided that the pseudo-judgements C [Γ_{n}] and B [Γ_{n}] are interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); C_{Σ}; γ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id)]

we interpret

C + B [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); C_{Σ}⊕B_{Σ}; γ⊕β(id)]

where γ ⊕ β : U/A_{Σn} → U^{→} is the functor defined in the following manner: for every [figure: D; t; A_{Σn}] we put γ ⊕ β(t) = γ(t) ⊕ β(t) and on the morphisms it is defined through the pullback. It is well defined, since coproducts are stable under pullback.

The first and second injections of the introduction rules of the disjoint sum type are interpreted in this manner:

provided that the pseudo-judgements c ∈ C [Γ_{n}] and b ∈ B [Γ_{n}] are interpreted as

[figure: A_{Σn}; c^{I}; id; C_{Σ}; γ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}; b^{I}; id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

inl(c) ∈ C + B [Γ_{n}] and inr(b) ∈ C + B [Γ_{n}]

as

[figure: A_{Σn}; ϵ_{1}(c^{I}); id; C_{Σ}⊕B_{Σ}; γ⊕β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}; ϵ_{2}(b^{I}); id; C_{Σ}⊕B_{Σ}; γ⊕β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where (inl(c))^{I}(id) ≡ ϵ_{1} · (c^{I}(id)), (inr(b))^{I}(id) ≡ ϵ_{2} · (b^{I}(id)) and ϵ_{1}, ϵ_{2} are the injections of the coproduct C_{Σ} ⊕ B_{Σ}.

The signature introduced in the elimination rule for the disjoint sum type is interpreted in this manner:

provided that the pseudo-judgements a_{C} ∈ A(inl(y)) [Γ_{n}, y ∈ C] and a_{B} ∈ A(inr(z)) [Γ_{n}, z ∈ B] are interpreted as

[figure: C_{Σ}; a_{C}^{I}; id; A_{Σ}×C_{Σ}; α(ϵ_{1}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); C_{Σ}; γ(id); B_{Σ}; a_{B}^{I}; id; A_{Σ}×B_{Σ}; α(ϵ_{2}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id)]

we interpret

D(w, a_{C}, a_{B}) ∈ A(w) [Γ_{n}, w ∈ C + B]

as

[figure: C_{Σ}⊕B_{Σ}; D^{I}; id; A_{Σ}; α(id); 1; A_{Σ1}; !_{A_{Σ1}}; C_{Σ}⊕B_{Σ}; γ⊕β(id)]

where D^{I}(id) ≡ (q(ϵ_{1}, α(id)) · a_{C}^{I}(id)) ⊕ (q(ϵ_{2}, α(id)) · a_{B}^{I}(id)). We prove that D^{I}(id) is a section of α(id). Indeed, we get α(id) · (D^{I}(id) · ϵ_{1}) = α(id) · (q(ϵ_{1}, α(id)) · a_{C}^{I}(id)) = (ϵ_{1} · α(ϵ_{1})) · a_{C}^{I}(id) = ϵ_{1}, by the definitions of D^{I} and α and by the hypothesis on a_{C}^{I}, and, hence, analogously α(id)·(D^{I}(id)· ϵ_{2}) = ϵ_{2}. Since ϵ_{1} ⊕ ϵ_{2} = id, we conclude that D^{I}(id) is a section of α(id).

Now, we interpret the signature introduced in the axiom of Disjointness

m(c, b) ∈ ⊥ [Γ_{n}] as [figure: A_{Σn}; ⟨id,t⟩; id; A_{Σn}×0_{Σ}; ˆ0(!_{A_{Σn}}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

provided that ϵ_{1}(c^{I}(id)) = ϵ_{2}(b^{I}(id)), where ⟨id, t⟩ is the unique morphism to the pullback of !_{0} and !_{A_{Σn}} and t is defined as follows. Since the coproduct is disjoint, the unique morphisms p_{1} : O → C_{Σ} and p_{2} : O → B_{Σ} are the projections of a pullback square between ϵ_{1} and ϵ_{2} (though this is not the specified one from the structure of U). So, by the hypothesis ϵ_{1}(c^{I}(id)) = ϵ_{2}(b^{I}(id)), there exists a unique t : A_{Σn} → 0 such that p_{1} · t = c^{I}(id) and p_{2} · t = b^{I}(id).

6. The Quotient type.

Suppose that the pseudo-judgement

R(x, y) type [x ∈ A, y ∈ A]

is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σ}×A_{Σ}; α(id)·π_{1}; R_{Σ}; ρ(id)]

where ρ(id) is an equivalence relation in U/A_{Σn} and

A [Γ_{n}]

is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σ}; α(id)]

with π_{1} ≡ α(α(id)) and π_{2} ≡ q(α(id), α(id)).

Since ρ(id) is an equivalence relation in U/A_{Σn}, there exists its quotient, that is the coequalizer c : A_{Σ} → A_{Σ}/R_{Σ} of π_{1} · ρ(id) and π_{2} · ρ(id), and we get Q(α(id)) such that the following triangle diagram commutes

\xymatrix{R_{Σ} \ar[r]_{π_{2}·ρ(id)} \ar[r]^{π_{1}·ρ(id)} & A_{Σ} \ar[rr]^{c} \ar[dr]_{α(id)} &  & A_{Σ}/R_{Σ} \ar[dl]^{Q(α(id))} \\  &  & A_{Σn}}

Therefore, we interpret

A/R [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σ}/R_{Σ}; Q(α)(id)]

where Q(α) : U/A_{Σn} → U^{→} is the functor defined in the following manner: for every [figure: D; t; A_{Σn}] we put Q(α)(t) ≡ Q(α(t)), where Q(α(t)) is the unique morphism such that α(t) = Q(α(t)) · c(t), c(t) is the quotient of the equivalence relation ρ(q(q(t, α(id)), π_{1})) in U/A_{Σn} and c(id) is the above coequalizer c. Q(α) is well defined because the quotient is stable under pullbacks. On the morphisms it is defined through the pullback. The signature of the introduction rule of the quotient type is interpreted in the following manner: provided that the pseudo-judgement a ∈ A [Γ_{n}] is interpreted as

[figure: A_{Σn}; a^{I}; id; A_{Σ}; α(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

we interpret

[a] ∈ A/R [Γ_{n}]

as

[figure: A_{Σn}; c·(a^{I}(id)); id; A_{Σ}/R_{Σ}; Q(α)(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

Now, we interpret the signature introduced in the restricted elimination rule, E_{s}-quotient. Suppose that the pseudo-judgement m(x) ∈ M [Γ_{n}, x ∈ A] is interpreted as

[figure: A_{Σ}; m^{I}; id; A_{Σ}×M_{Σ}; μ(α(id)); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σ}; α(id)]

and that m^{I}(id) · (π_{1} · ρ(id)) = m^{I}(id) · (π_{2} · ρ(id)). Therefore, as c is the coequalizer of π_{1} · ρ(id) and π_{2} · ρ(id), there exists a morphism q in U/A_{Σn} such that q · c = q(α(id), μ(id)) · m^{I}(id). Since by hypothesis μ(id) · (q(α(id), μ(id)) · m^{I}(id)) = α(id), recalling that c is epi or equivalently by the uniqueness for morphisms defined by the universal property of a quotient we conclude μ(id) · q = Q(α(id)). We finally define the interpretation of Q_{s}(m, z) ∈ M [Γ_{n}, z ∈ A/R] as

[figure: A_{Σ}/R_{Σ}; ⟨id,q⟩; id; A_{Σ}/R_{Σ}×M_{Σ}; μ(Q(α)(id)); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σ}/R_{Σ}; Q(α(id))]

Now, we interpret the signature introduced in the axiom of Effectiveness. Suppose that the pseudo-context Γ_{n} is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

We interpret

f(a, b) ∈ R(a, b) [Γ_{n}]

as

[figure: A_{Σn}; ⟨id,t⟩; id; R_{Σ}; ρ(⟨a^{I},b^{I}⟩); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

provided that c · a^{I}(id) = c · b^{I}(id), where t is defined as follows. Since the quotient is effective in U/A_{Σn}, then there exists a morphism t : A_{Σn} → R_{Σ} such that (π_{1} · ρ(id)) · t = a^{I}(id) and (π_{2} · ρ(id)) · t = b^{I}(id).

7. The List type.

Provided that the pseudo-judgement C [Γ_{n}] is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); C_{Σ}; γ(id)]

then we interpret

List(C) [Γ_{n}]

as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); rec(C_{Σ},1); rec(γ)(id)]

where rec(γ) : U/A_{Σn} → U^{→} is the functor defined in the following manner: for every [figure: D; t; A_{Σn}] we put rec(γ)(t) ≡ rec(γ(t), id_{D}), which is the list object on γ(t) in U/D. On the morphisms rec(γ) is defined through the pullback.

Moreover, under the same assumption about Γ_{n}, the empty list

ϵ ∈ List(C) [Γ_{n}]

is interpreted as

[figure: A_{Σn}; r_{o}^{γ}; id; rec(C_{Σ},1); rec(γ)(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

where r^{γ}_{o} : id_{A_{Σn}} → rec(γ)(id) is the empty map for rec(γ)(id) in U/A_{Σn};

and the list-constructor

cons(x, y) ∈ List(C) [Γ_{n}, x ∈ List(C), y ∈ C]

is interpreted as

[figure: rec(C_{Σ},1)×C_{Σ}; id; ⟨id,r_{1}^{γ}⟩; rec(C_{Σ},1)×C_{Σ}×rec(C_{Σ},1); π̄_{1}; 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); rec(C_{Σ},1); rec(γ)(id); rec(C_{Σ},1)×C_{Σ}; γ(rec(γ)(id))]

where r_{1}^{γ} : rec(γ)(id) × γ(id) → rec(γ)(id) is the list-constructor map in U/A_{Σn}, π̄_{1} ≡ rec(γ)(γ(rec(γ)(id))) and ⟨id, r_{1}^{γ}⟩ is the universal map towards the pullback of rec(γ)(id) along γ(rec(γ)(id)).

Now, we interpret the signature introduced in the weaker elimination rule E_{s}-List.

Provided that the pseudo-judgements a ∈ L [Γ_{n}] and l(y, z) ∈ L [Γ_{n}, y ∈ L, z ∈ C] are interpreted as

[figure: A_{Σn}; a^{I}; id; L_{Σ}; ξ(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); L_{Σ}×C_{Σ}; l^{I}; id; L_{Σ}×C_{Σ}×L_{Σ}; π_{1}^{L}; 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); L_{Σ}; ξ(id); L_{Σ}×C_{Σ}; γ(ξ(id))]

where π_{1}^{L} ≡ ξ(ξ(id) · γ(ξ(id))), then we interpret

Rec_{s}(a, l, y) ∈ L [Γ_{n}, y ∈ List(C)]

as

[figure: rec(C_{Σ},1); ⟨id,_{A_{Σn}} r⟩; id; rec(C_{Σ},1)×L_{Σ}; ξ(rec(γ)(id)); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); rec(C_{Σ},1); rec(γ)(id)]

where r is the unique morphism that makes the following diagram commute by the property of recursive object in U/A_{Σn}

[figure: id_{A_{Σ}}; ^{r_{o}^{γ}}; a^{I}; rec(γ(id),id); r; rec(γ(id),id)×γ(id); r×id; ^{r_{1}^{γ}}; ξ(id); ξ(id)×γ(id); π_{2}^{L}·l^{I}(id)]

with π_{2}^{L} ≡ q(ξ(id) · γ(ξ(id)), ξ(id)).

4.2.2 The validity of the typed calculus Au

In order to prove the validity theorem with respect to type and term judgements and their equality judgements we need to know how the rules for weakening and substitution are interpreted. Weakening and substitution of variables in types and terms are expressed by pullback:

Lemma 4.8 The weakening of a variable in type and term judgements is interpreted as follows: given the pseudo-judgements

B(x_{1}, ..., x_{n}) [Γ_{n}] and D(x_{1}, ..., x_{j}) [Γ_{j}]

where n ≥ j, interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj}; α_{j}(id); D_{Σ}; δ(id)]

then the pseudo-judgement

B(x_{1}, ..., x_{n}) [Γ_{j}, y ∈ D, x_{j+1} ∈ A_{j+1}, …, x_{n} ∈ A_{n}]

is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj}; D_{Σ}; δ(id); D_{Σ}×A_{Σj+1}; α_{j+1}(t_{j}); D_{Σ}×A_{Σn}; α_{n}(t_{n−1}); D_{Σ}×B_{Σ}; β(t_{n})]

where t_{j} ≡ δ(id) and if n ≥ j + 1, t_{i} ≡ q(t_{i−1}, α_{i}(id)) for i = j + 1, …, n and given the pseudo-judgement

b ∈ B(x_{1}, ..., x_{n}) [Γ_{n}] and D(x_{1}, ..., x_{j}) [Γ_{j}]

where n ≥ j, interpreted as

[figure: A_{Σn}; b^{I}(id); id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj}; α_{j}(id); D_{Σ}; δ(id)]

then

b ∈ B(x_{1}, ..., x_{n}) [Γ_{j}, y ∈ D, x_{j+1} ∈ A_{j+1}, …, x_{n} ∈ A_{n}]

is interpreted as

[figure: D_{Σ}×A_{Σn}; b^{I}(t_{n}); id; D_{Σ}×B_{Σ}; β(t_{n}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj}; D_{Σ}; ξ(id); D_{Σ}×A_{Σn}; α_{n}(t_{n−1})]

Lemma 4.9 The substitution of variables in type and term judgements is interpreted as follows: given the pseudo-judgements

B(x_{1}, ..., x_{n}) [Γ_{n}] and a_{j} ∈ A_{j} [Γ_{j−1}]

where n ≥ j, interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); B_{Σ}; β(id); A_{Σj−1}; a_{j}^{I}(id); id; A_{Σj}; α_{j}(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj−1}; α_{j−1}(id)]

then the pseudo-judgement

B(x_{1}, …, x_{j}, a_{j}, x′_{j+1}, …, x′_{n})[Γ_{j−1}, x′_{j+1} ∈ A′_{j+1}, …, x′_{n} ∈ A′_{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, is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj−1}; A′_{Σj+1}; α_{j+1}(q_{j}); A′_{Σn}; α_{n}(q_{n−1}); B′_{Σ}; β(q_{n})]

where q_{j} ≡ a_{j}^{I}(id) and if n ≥ j + 1, q_{i} ≡ q(q_{i−1}, α_{i}(id)) for i = j + 1, …, n and given a pseudo-term judgement

b ∈ B(x_{1}, ..., x_{n}) [Γ_{n}] and a_{j} ∈ A_{j} [Γ_{j−1}]

where n ≥ j, interpreted as

[figure: A_{Σn}; b^{I}(id); id; B_{Σ}; β(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σj−1}; a_{j}^{I}(id); id; A_{Σj}; α_{j}(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj−1}; α_{j−1}(id)]

then the pseudo-judgement

b[x_{j}/a_{j}][x_{i}/x′_{i}]_{i=j,...,n} ∈ B(x_{1}, …, x_{j}, a_{j}, x′_{j+1}, …, x′_{n}) [Γ_{j−1}, x′_{j+1} ∈ A′_{j+1}, …, x′_{n} ∈ A′_{n}] is interpreted as

[figure: A′_{Σn}; b^{I}(q_{n}); id; B′_{Σ}; β(q_{n}); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σj−1}; A′_{Σj+1}; α_{j+1}(q_{j}); A′_{Σn}; α_{n}(q_{n−1})]

The proofs can be done by induction on the signature of the judgements. For the assumption of variable, the lemma of weakening holds by definition and the lemma of substitution holds because terms are interpreted as sections. In the case of constant type, like ⊤ or N, we use the inductive hypothesis, since the preinterpretation of a context is reduced to that of a type pseudo-judgement. The definition of partial preinterpretation of type and term judgements assures that all these lemmas for weakening and substitution hold for the other type and term constructors. Now, we are ready to prove the validity theorem:

Theorem 4.10 (Validity) Given an arithmetic universe U, if A type [Γ_{n}] is derivable in Au then I_{U}(A type [Γ_{n}]) is well defined. If a ∈ A [Γ_{n}] is derivable then I_{U}(a ∈ A [Γ_{n}]) is well defined. Suppose that A type [Γ_{n}] and B type [Γ_{n}] are derivable in Au, if A = B [Γ_{n}] is derivable in Au then I_{U}(A type [Γ_{n}]) = I_{U}(B type [Γ_{n}]). Suppose that a ∈ A [Γ_{n}] and b ∈ A [Γ_{n}] are derivable in Au, if a = b ∈ A [Γ_{n}] is derivable in Au, then I_{U}(a ∈ A [Γ_{n}]) = I_{U}(b ∈ A [Γ_{n}]).

Proof. The proof can be done by induction on the derivation of the judgement.

Remark 4.11 A judgement is valid, if its interpretation is well-defined and hence, in particular an equality judgement for types or terms is valid, if the interpretations of the corresponding type or term judgements are well defined and equal. We say that an inference rule holds or is valid, if it preserves the validity of judgements.

Surely, the set rule conv) preserves validity of the judgements. Hence, we proceed by proving the validity of the formation, introduction and elimination and conversion rules for the various types with their terms. The lemma of weakening and substitution are crucial for the dependent types, whose rules refer to substitution or weakening such as, for example, the Indexed Sum type.

1. The formation, introduction and elimination and conversion rules for the Terminal type hold because for every object D in U, ˆ1(!_{D}) is a terminal object in U/D.

2. The formation and elimination rules of the False type are valid, since for every object D in U, ˆ0(!_{D}) is an initial object in U/D.

3. The formation, introduction and elimination rules of the Indexed Sum type are valid. Moreover, the β and η conversion rules for the indexed sum type hold by the properties of pullback. Indeed, the β_{1}-C conversion rule for the indexed sum type

\frac{b ∈ B c ∈ C(b)}{π_{1}(⟨b, c⟩) = b ∈ B}

holds because γ(id) · (q(b^{I}(id), γ(id)) · c^{I}(id)) = b^{I}(id) · γ(b^{I}(id)) · c^{I}(id), from which as c^{I}(id) is a section of γ(b^{I}(id)) we get γ(id) · (q(b^{I}(id), γ(id)) · c^{I}(id) = b^{I}(id). The β_{2}-C conversion rule for the indexed sum type

\frac{b ∈ B c ∈ C(b)}{π_{2}(⟨b, c⟩) = c ∈ C(b)}

holds because ⟨id, q(b^{I}(id), γ(id)) · c^{I}(id)⟩ = c^{I}(id), since c^{I}(id) is a section of γ(b^{I}(id)). Finally, the η-C conversion rule for the indexed sum type

\frac{d ∈ Σ_{x∈B}C(x)}{⟨π_{1}(d), π_{2}(d)⟩ = d ∈ Σ_{x∈B}C(x)}

holds since q(γ(id) · d^{I}(id), γ(id)) · ⟨id, d^{I}(id)⟩ = d^{I}(id).

4. The formation, introduction rules of the Equality type hold.

The E-equality elimination rule

\frac{p ∈ Eq(C, c, d)}{c = d ∈ C}

holds because for every t : D → A_{n}, p^{I}(t) is a section of Eq(c^{I}, d^{I})(t), which is the equalizer of c^{I}(t) and d^{I}(t), so we conclude that c^{I}(t) = d^{I}(t). Moreover, the C-equality conversion rule

\frac{p ∈ Eq(C, c, d)}{p = eq_{C} ∈ Eq(C, c, d)}

holds, because the equalizer is a monomorphism.

5. The formation, introduction and elimination rules of the Disjoint Sum type hold.

The C_{1} conversion rule for the disjoint sum type

\frac{a_{C}(x) ∈ A(inl(x)) [x ∈ C] a_{B}(y) ∈ A(inr(y)) [y ∈ B]}{D(inl(x), a_{C}, a_{B}) = a_{C}^{I}(x) ∈ A(inl(x)) [x ∈ C]}

holds since D(inl(x), a_{C}, a_{B})^{I}(id) = ⟨id ,_{C_{Σ}⊕B_{Σ}} (q(ϵ_{1}, α(id)) · a_{C}^{I}(id) ⊕ q(ϵ_{2}, α(id)) · a_{B}^{I}(id))) · ϵ_{1}⟩ and by uniqueness of the morphism to a pullback D(inl(x), a_{C}, a_{B})^{I}(id) = a_{C}^{I}(id).

The C_{2} conversion rule for the disjoint sum type holds for an analogous reason.

The axiom of Disjointness is valid, since by hypothesis ϵ_{1}(c^{I}(id)) = ϵ_{2}(b^{I}(id)).

6. The formation rule of the Quotient type holds.

Indeed, given the following judgements (we omit Γ_{n} in the context)

R(x, y) type [x ∈ A, y ∈ A], z = w ∈ R(x, y) [x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)],
c_{1} ∈ R(x, x)[x ∈ A],  c_{2} ∈ R(y, x)[x ∈ A, y ∈ A, z ∈ R(x, y)],
c_{3} ∈ R(x, z)[x ∈ A, y ∈ A, z ∈ A, w ∈ R(x, y), w′ ∈ R(y, z)]

suppose that R(x, y) type [Γ_{n}, x ∈ A, y ∈ A] is interpreted as

[figure: 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σ}×A_{Σ}; α(id)·π_{1}; R_{Σ}; ρ(id)]

with π_{1} ≡ α(α(id)) and π_{2} ≡ q(α(id), α(id)). From the validity of the judgement expressing that R(x, y) is a mono type, ρ(id) is a monomorphism as follows. In fact, the interpretations of z ∈ R(x, y) [Γ_{n}, x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)] and w ∈ R(x, y) [Γ_{n}, x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)] are isomorphic with the same isomorphism respectively to the first projection and to the second projection of the product ρ(id) × ρ(id). Therefore, by the interpretation of z = w ∈ R(x, y) [Γ_{n}, , x ∈ A, y ∈ A, z ∈ R(x, y), w ∈ R(x, y)], we get that the two projections of ρ(id), that are ρ(ρ(id)) and q(ρ(id), ρ(id)), are equal and we conclude that ρ(id) is a monomorphism in U/A_{Σn}.

The fact that ρ(id) is an equivalence relation in U/A_{Σn} easily follows by chasing diagrams.

The equality rule for the quotient type holds. Indeed, suppose that a ∈ A [Γ_{n}] and b ∈ A [Γ_{n}] are interpreted as

[figure: A_{Σn}; a^{I}; id; A_{Σ}; α(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id); A_{Σn}; b^{I}; id; A_{Σ}; α(id); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

and d ∈ R(a, b) [Γ_{n}] is interpreted as

[figure: A_{Σn}; d^{I}; id; R; ρ(⟨a^{I},b^{I}⟩); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σn}; α_{n}(id)]

Then we get that (π_{1}·ρ(id))·(q(⟨a^{I}, b^{I}⟩, ρ(id))·d^{I}) = a^{I}(id) and (π_{2}·ρ(id))·(q(⟨a^{I}, b^{I}⟩, ρ(id))·d^{I}) = b^{I}(id). We conclude that c · a^{I}(id) = c · b^{I}(id), that gives the validity of

[a] = [b] ∈ A/R [Γ_{n}]

The elimination rule for the quotient type holds, since given m(x) ∈ M [Γ_{n}, x ∈ A] interpreted as

[figure: A_{Σ}; m^{I}; id; A_{Σ}×M_{Σ}; μ(α(id)); 1; A_{Σ1}; !_{A_{Σ1}}; A_{Σ}; α(id)]

and given m(x) = m(y) ∈ M [Γ_{n}, x ∈ A, y ∈ A, d ∈ R(x, y)] interpreted as the equality between morphisms, we get that

⟨id, m^{I}(id) · (π_{1} · ρ(id))⟩ = ⟨id, m^{I}(id) · (π_{2} · ρ(id))⟩

(we recall that π_{1} ≡ α(α(id)) and π_{2} ≡ q(α(id), α(id))). From this, we obtain m^{I}(id)·(π_{1} ·ρ(id)) = m^{I}(id) · (π_{2} · ρ(id)), which is the required condition to get a well defined interpretation for the signature introduced in the elimination rule for the quotient type.

The β_{s}C-quotient conversion rule

\frac{a ∈ A m(x) ∈ M [x ∈ A] m(x) = m(y) ∈ M [x ∈ A, y ∈ A, d ∈ R(x, y)]}{Q_{s}(m, [a]) = m(a) ∈ M}

holds since

(Q_{s}(m, [a]))^{I}(id) = ⟨id ,_{A_{Σ}/R_{Σ}} ⟨id ,_{A_{Σn}} q⟩ · c · (a^{I}(id))⟩ = ⟨id ,_{A_{Σn}} q · (c · a^{I}(id))⟩ = = ⟨id,_{A_{Σn}} (q(α(id), μ(id)) · m^{I}(id)) · a^{I}(id)⟩ = ⟨id ,_{A_{Σ}} m^{I}(id) · a^{I}(id)⟩ = m(a)^{I}(id).

The η_{s}C-quotient conversion rule

\frac{t(z) ∈ M [z ∈ A/R]}{Q_{s}((x)t([x]), z) = t(z) ∈ M [z ∈ A/R]}

holds since

Q_{s}((x)t([x]), z)^{I}(id) = ⟨id ,_{A_{Σn}} q⟩, where q · c = q(Q(α)(id), μ(id)) · (t^{I}(id) · c). So by uniqueness of the morphism from a coequalizer we get q = q(Q(α)(id), μ(id))·t^{I}(id) and then ⟨id,_{A_{Σn}} q⟩ = t^{I}(id).

The axiom of Effectiveness holds

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

since the validity of the premisses c · a^{I}(id) = c · b^{I}(id).

7. The formation, introduction and elimination rule for the List type hold, since rec(γ)(id) is a list object of U/A_{Σn}.

The conversion rules for the list type follow from the properties of the recursive object. The β_{s}C_{1}-list conversion rule for the natural numbers type

\frac{a ∈ L l(y, z) ∈ L [y ∈ L, z ∈ C]}{Rec_{s}(a, l, ϵ) = a ∈ L}

holds since

Rec_{s}(a, l, ϵ)^{I}(id) = ⟨id ,_{A_{Σn}} r · r_{o}^{γ}⟩ = a^{I}(id) by definition of the recursive object rec(γ)(id) in U/A_{Σn}.

The β_{s}C_{2}-list conversion rule for the list type

\frac{a ∈ L l(y, z) ∈ L [y ∈ L, z ∈ C]}{Rec_{s}(a, l, cons(s, z)) = l(Rec_{s}(a, l, s), z) ∈ L [s ∈ List(C), z ∈ C]}

holds since

Rec_{s}(a, l, cons(s))^{I}(id) = ⟨id ,_{A_{Σn}} r · r_{1}^{γ}⟩ =

= ⟨id ,_{A_{Σn}} (q(ξ(id) · γ(ξ(id)), ξ(id)) · l^{I}(id)) · r × id⟩ = l(Rec_{s}(a, l, s), z)^{I}(id).

The η_{s}C-list conversion rule for the list type also holds by uniqueness of the morphism that makes the diagram of the recursive object rec(γ)(id) commute with respect to l^{I}.

5 The completeness theorem

In this section we show a completeness theorem for the typed calculus Au with respect to arithmetic universes. We are interested in completeness with respect to the equality judgements and the completeness with respect to provability of a type follows as well using the same technique. Our notion of model for Au within an arithmetic universe described in the previous section corresponds to a particular contextual category with attributes in [Pit95], [Hof94] or [Hof97], namely those related to the split fibration equivalent to the codomain fibration. We know that the completeness theorem with respect to general contextual categories with attributes is quite straightforward (see, for example, [Pit95], [Str91]). Indeed, the interpretation in the syntactic contextual category is faithful, since it turns out to correspond to an identity modulo provable equality between types and between terms. But, since our models are particular contextual categories with attributes, and the interpretation of the indexed sum type is the composition of fibred functors, the interpretation in the syntactic category is no longer exactly an identity modulo provable equality. However, this interpretation is isomorphic to a canonical comprehension structure, which does not require new data or choices, where we can easily interpret the calculus and prove completeness.

Having seen the validity of the typed calculus Au with respect to P gr(U) for every arithmetic universe U, we prove the completeness theorem with respect to the class of arithmetic universes with a fixed choice of their structure. For this purpose we introduce a new category where to define the above isomorphism.

Def. 5.1 Given an arithmetic universe U, we define the category U^{→^{n}} whose objects are the objects of P gr(U) and whose morphisms between α_{1}, α_{2}, ..., α_{n} and β_{1}, β_{2}, ..., β_{n} are sequences of morphisms of U ϕ_{1}, ..., ϕ_{n} such that all the following squares commute

[figure: A_{n}; ϕ_{n}; α_{n}; B_{n}; β_{n}; A_{n−1}; α_{n−1}; ϕ_{n−1}; B_{n−1}; β_{n−1}; A_{2}; α_{2}; ϕ_{2}; B_{2}; β_{2}; A_{1}; α_{1}; ϕ_{1}; B_{1}; β_{1}; 1; id_{1}; 1]

The proof of the completeness theorem with respect to the class of arithmetic universes is based on the investigation of the interpretation I_{U_{Au}}, defined in section 4, within the syntactic arithmetic universe U_{Au} defined in section 3. This interpretation does not resemble the identity interpretation. However, we will prove that there is a kind of isomorphism between the interpretation I_{U_{Au}} and another interpretation of judgements of Au, which we call J_{U_{Au}}. The interpretation J_{U_{Au}} resembles the identity interpretation modulo the equality and is faithful.

We define the interpretation

J_{U_{Au}} : Au → P gr(U_{Au})

by induction on the number of assumptions in the context in this manner: J_{U_{Au}}(B type [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1})]) is

[figure: Σ_{zn∈Ãn} \overline{B}; π_{1}^{B}; Σ_{z_{n−1}∈{ \atop A_{n−1}}} \overline{A_{n}}; π_{1}^{n}; Σ_{z∈⊤}\overline{A_{1}}; π_{1}^{1}; ⊤]

where Ã_{n} is the domain of the last morphism of J_{U_{Au}}(A_{n} type[x_{1} ∈ A_{1}, ..., x_{n−1} ∈ A_{n−1}(x_{1}, ..., x_{n−2})]) and

\overline{B} ≡ B[x_{1} := π_{2}^{1} · π_{1}^{2} ⋯ π_{1}^{n}(z_{n})] … [x_{n−1} := π_{2}^{n−1}(π_{1}^{n}(z_{n}))][x_{n} := π_{2}^{n}(z_{n})]

with π_{i}^{n} ≡ λx.π_{i}^{n}(x) for i = 1, 2, where π_{1}^{n}(x) and π_{2}^{n}(x) are the two projections of Σ_{z_{n−1}∈{ \atop A_{n−1}}} \overline{A_{n}} and

π_{1}^{B} and π_{2}^{B} are the two projections of Σ_{z_{n}∈Ã_{n}} \overline{B}. For i = 1, …, n \overline{A_{i}} is defined in the same manner as

\overline{B}, where Ã_{1} ≡ Σ_{z∈⊤}\overline{A_{1}} and \overline{A_{1}} ≡ A_{1}. If b ∈ B [Γ_{n}] is a judgement of Au, we put

\overline{b} ≡ b [x_{1} := π_{2}^{1} · π_{1}^{2} ⋯ π_{1}^{n}(z_{n})] … [x_{n−1} := π_{2}^{n−1}(π_{1}^{n}(z_{n}))][x_{n} := π_{2}^{n}(z_{n})]

and we can derive

\overline{b} ∈ \overline{B} [z_{n} ∈ Ã_{n}]

From now on, we call B^{I} = dom(I_{U_{Au}}(B type [Γ_{n}])). In order to prove the completeness theorem, we want to show that

Proposition 5.2 For every judgement

B type [Γ_{n}]

derivable in Au, (which we suppose to be interpreted as α_{1}(id), α_{2}(id), ..., α_{n}(id), β(id)) there is an isomorphism of U_{Au}^{→_{n}}

ϕ_{A_{1}}, ..., ϕ_{A_{n}}, ϕ_{B}

between I_{U_{Au}}(B type [Γ_{n}]) and J_{U_{Au}}(B type [Γ_{n}]) such that for every judgement b ∈ B [Γ_{n}]

ϕ_{B} · b^{I}(id) = ⟨id, \overline{b}⟩ · ϕ_{A_{n}}

and for weakening, for every judgement with n ≥ j

M type [Γ_{j}]

(which we suppose to be interpreted as α_{1}(id), α_{2}(id), ..., α_{j}(id), μ(id))

ϕ_{B} · t_{n} = p_{n} × id · ϕ_{M×B}

where ϕ_{M×B} : (M × B)^{I} → Σ_{x∈M̃}\overline{B}, t_{i} is defined as in the lemma of weakening, p_{j} ≡ π_{1}^{M} × id and if n ≥ j + 1, p_{i} ≡ p_{i−1} × id for i = j + 1, …, n, and for substitution, for every a_{j} ∈ A_{j} [Γ_{j−1}] with n ≥ j

ϕ_{B} · q_{n} = s_{n} × id · ϕ_{B(a_{n})}

where q_{i} is defined as in the lemma of substitution, s_{j} ≡ ⟨id, \overline{a_{n}}⟩ × id and if n ≥ j + 1, s_{i} ≡ s_{i−1} × id for i = j + 1, …, n.

Proof. The definition of the isomorphisms is given by induction on the derivation of type and term judgements of Au. In general, given a type judgement

B type [x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}(x_{1}, ..., x_{n−1})]

by inductive hypothesis we know that ϕ_{A_{1}}, ..., ϕ_{A_{n}} is an isomorphism in U_{Au}^{→_{n}} between I_{U_{Au}}(A_{n} type [x_{1} ∈ A_{1}, ..., x_{n−1} ∈ A_{n−1}(x_{1}, ..., x_{n−2})]) and J_{U_{Au}}(A_{n} type [x_{1} ∈ A_{1}, ..., x_{n−1} ∈ A_{n−1}(x_{1}, ..., x_{n−2})]), so we only define a U-isomorphism ϕ_{B} : B^{I} → Σ_{z_{n}∈Ã_{n}} \overline{B} in order to prove that ϕ_{A_{1}}, ..., ϕ_{A_{n}}, ϕ_{B} is an isomorphism in U_{Au}^{→_{n}} between I_{U_{Au}}(B type [Γ_{n}]) and J_{U_{Au}}(B type [Γ_{n}]). We can define the isomorphisms by induction on the derivation of type and term judgements, since by the validity theorem these are well defined. For the terms it is crucial that the U-isomorphisms commute with the second projections of pullbacks related to weakening and substitution. For example, we show the inductive steps for the terminal type and for the indexed sum type.

1. Given the T erminal type judgement ⊤ [Γ_{n}] we define

ϕ_{A_{n}×⊤} : ⊤^{I} → Σ_{z_{n}∈Ã_{n}}⊤

as ϕ_{A_{n}×⊤}(z) = ⟨ϕ_{A_{n}}(π_{1}^{⊤}(z)), π_{1}(π_{2}^{⊤}(z))⟩ for z ∈ ⊤^{I}, since by definition ⊤^{I} ≡ Σ_{z_{n}∈Ã_{n}}Σ_{y∈⊤} ⋆ =_{⊤} ⋆. We can easily prove that this isomorphism satisfies all the equations of the proposition.

2. Given the Indexed Sum type judgement Σ_{y∈B}C(x_{1}, ..., x_{n}, y)[Γ_{n}] we define

ϕ_{Σ_{y∈B}C} : (Σ_{y∈B}C)^{I} → Σ_{z_{n}∈Ã_{n}} \overline{Σ_{y∈B}C}

as ϕ_{Σ_{y∈B}C} ≡ ζ_{C} · ϕ_{C} where

ζ_{C} : Σ_{y∈B̃}\overline{C} → Σ_{z_{n}∈Ã_{n}} \overline{Σ_{y∈B}C}

is defined in this manner: for every z ∈ Σ_{y∈B̃}\overline{C}

ζ_{C}(z) = ⟨π_{1}^{B}(π_{1}^{C}(z)), ⟨π_{2}^{B}(π_{1}^{C}(z)), π_{2}^{C}(z)⟩⟩

For short we write Σ for Σ_{y∈B}C.

We can easily prove that ζ_{C} is an isomorphism.

To prove the weakening equation

ϕ_{Σ} · t_{n} = p_{n} × id · ϕ_{M×Σ}

is sufficient to show that

(p_{n} × id\overline{Σ_{y∈B}C}) · ζ_{M×C} = ζ_{C} · ((p_{n} × id\overline{B}) × id\overline{C})

Finally, in analogous way we can prove the substitution equations.

Given the pair term ⟨b, c⟩ ∈ Σ_{y∈B}C(x_{1}, ..., x_{n}, y)[Γ_{n}] we want to prove that

ϕ_{Σ_{y∈B}C} · (⟨b, c⟩)^{I} = ⟨id, \overline{⟨b, c⟩}⟩ · ϕ_{A_{n}}

Indeed by inductive hypotheses on substitution and on c^{I} (ζ_{C} · ϕ_{C})) · (q(b^{I}, γ(id)) · c^{I}) = = ζ_{C} · (⟨id, \overline{b}⟩ × id · ϕ_{C(b)}) · c^{I} = = (ζ_{C} · ⟨id, \overline{b}⟩ × id) · (⟨id, \overline{c}⟩ · ϕ_{A_{n}}) = ⟨id, \overline{⟨b, c⟩}⟩ · ϕ_{A_{n}}. Given the first projection π_{1}(d) ∈ B(x_{1}, ..., x_{n})[Γ_{n}] we want to prove that

ϕ_{B} · (π_{1}(d))^{I} = ⟨id, \overline{π_{1}(d)}⟩ · ϕ_{A_{n}}

Indeed, by inductive hypotheses on type judgements and on d^{I} ϕ_{B} · (γ(id) · d^{I}) = π_{1}^{Σ_{y∈B}C} · (ϕ_{C} · d^{I}) = = π_{1}^{Σ_{y∈B}C} · (ζ_{C}^{−1} · ⟨id, \overline{d}⟩ · ϕ_{A_{n}}) = ⟨id, \overline{π_{1}(d)}⟩ · ϕ_{A_{n}}. Given the second projection π_{2}(d) ∈ B(x_{1}, ..., x_{n})[Γ_{n}] we want to prove that

ϕ_{C(π_{1}(d))} · (π_{2}(d))^{I} = ⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}}

We start to consider ϕ_{C(π_{1}(d))}^{−1} · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}}) and note that by inductive hypotheses γ(π_{1}(d)^{I}) · ϕ_{C(π_{1}(d))}^{−1} · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}})) =

= (ϕ_{A_{n}}^{−1} · π_{1}^{C(b)}) · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}})) = = id and moreover, by inductive hypotheses on substitution and on d^{I} q(π_{1}(d)^{I}, γ(id)) · (ϕ_{C(π_{1}(d))}^{−1} · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}})) = = (ϕ_{C}^{−1} · ⟨id, \overline{π_{1}(d)}⟩ × id) · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}}) = = ϕ_{C}^{−1} · (ζ_{C}^{−1} · ⟨id, \overline{d}⟩) · ϕ_{A_{n}}) = = d^{I}. Therefore, by uniqueness of a morphism towards a pullback we conclude that

π_{2}(d)^{I} = ⟨id, d^{I}⟩ = ϕ_{C(π_{1}(d))}^{−1} · (⟨id, \overline{π_{2}(d)}⟩ · ϕ_{A_{n}})

For all the other types, we can go on defining the isomorphisms that satisfy the various equations by using their term constructors and the inductive hypotheses. For the equality type the equations follow directly from the inductive hypotheses, since the last morphism is a mono.

Now we are ready to prove: Theorem 5.3 (completeness) Suppose that a ∈ A [Γ_{n}] and b ∈ A [Γ_{n}] are derivable in Au, if for every arithmetic universe U we have I_{U}(a ∈ A [Γ_{n}]) = I_{U}(b ∈ A [Γ_{n}]) then a = b ∈ A [Γ_{n}] is derivable in Au. Suppose that A type [Γ_{n}] and B type [Γ_{n}] are derivable in Au, if for every arithmetic universe U I_{U}(A type [Γ_{n}]) = I_{U}(B type [Γ_{n}]) then A = B [Γ_{n}] is derivable in Au. Proof. If I_{U_{Au}}(a ∈ A [Γ_{n}]) = I_{U_{Au}}(b ∈ A [Γ_{n}]) then by the above proposition

ϕ_{B}^{−1} · ⟨id, \overline{a}⟩ · ϕ_{A_{n}} = a^{I} = b^{I} = ϕ_{B}^{−1} · ⟨id, \overline{b}⟩ · ϕ_{A_{n}}

from which we conclude a = b ∈ A [Γ_{n}]. The proof for the judgements about equality between types can be done by double induction on the derivation, considering the interpretation I_{U_{Au}} in the syntactic category U_{Au}. When the equality type step occurs in the induction, we can conclude by the completeness for judgements about equality between terms.

6 The internal type theory of a universe

In this section given an arithmetic universe U we want to describe its internal dependent type theory T (U). We apply the same technique developed in [Mai98b]. The type theory is based on the initial type theory Au for arithmetic universes, augmented with the specific type and term judgements of U. As in the non-dependent case, we give a dependent formulation of the internal language of a universe saying what a type judgement is, what a term judgement is, in a clear order, without considering first raw types and raw terms and then well-formed types and terms. As in the categorical semantics for the dependent typed calculi in section 4, the idea is to consider a dependent type as a sequence of morphisms of U, ending with the terminal object 1, whereas the terms are sections of the last morphism of the type to which they belong. Therefore, the type theory T (U) is formulated in the style of Martin-Löf’s type theory. We assume all the inference rules about the formation of contexts, declarations of typed variables, about reflexivity, symmetry and transitivity of the equality between types and terms and the set rule conv) as in section 2. As in the semantics in section 4, a type judgement arises from a object of P gf(U), which represents a dependent type with all its possible substitutions. More precisely, a type judgement corresponds to the evaluation of a finite sequence of fibred functors on the identity. Indeed, for a sequence of fibred functors α_{1}, α_{2}, ..., α_{n}, β of P gf(U), we define

β^{−1}(x_{1}, ..., x_{n})[x_{1} ∈ α_{1}^{−1}, ..., x_{n} ∈ α_{n}^{−1}(x_{1}, ..., x_{n−1})]

as the type judgement corresponding to

[figure: B; β(id); A_{n}; α_{n}(id); A_{1}; α_{1}(id); 1]

by thinking of the fibers of the morphism β(id). This notation turns out to be very clear when we look at the category of paths built on any syntactic arithmetic universe. The equality between types corresponds to the equality between objects of P gf(U), which implies the equality between objects of P gr(U). For short, we use the abbreviation Γ_{n} ≡ x_{1} ∈ α_{1}^{−1}, ..., x_{n} ∈ α_{n}^{−1}(x_{1}, ..., x_{n−1}) in the contexts. On the other hand, a term judgement arises from a morphism of P gf(U), which is a natural transformation representing a term with all its possible substitutions. The evaluation of a natural transformation on the identical substitution is a term judgement. Indeed, for a suitable morphism b of P gf(U) from α_{1}, α_{1}, ..., α_{n}, i_{A_{n}} to α_{1}, α_{2}, ..., α_{n}, β, the term judgement

b ∈ β^{−1}(x_{1}, ..., x_{n})[Γ_{n}]

corresponds to a section of β(id) [figure: A_{n}; b(id); id; B; β(id); 1; A_{1}; !_{A_{1}}; A_{n}; α_{n}] by choosing the identity as the terminal object

in U/A_{n}. The equality between terms corresponds to the equality between morphisms of P gf(U). So, we add as axioms all the equality judgements that correspond to actual equations holding in P gf(U). In the following, to make formulas more readable in type judgements, we will write β[Γ_{n}] instead of β^{−1}[Γ_{n}]. In the diagrams we will often write σ_{i} instead of σ_{i}(id_{A_{i}}) for fibred functors and b instead of b(id) for natural transformations.

Def. 6.1 The description of the internal language follows closely the interpretation of Au in an arithmetic universe for what regards the common core, namely the typed calculus Au. Then we add the types and terms specific to the arithmetic universe in consideration.

The rules for substitution of variables in a type and in a term and for weakening of a variable w.r.t type and term judgements are the usual ones and they are defined as their interpretation in the semantics in section 4. We only recall how they work in these particular cases:

sT \frac{γ[Γ_{n}, y ∈ β] b ∈ β[Γ_{n}]}{γ[b(id)][Γ_{n}]} is [figure: C; γ; B; β; A_{n}...; A_{n}; b; id; B; β; A_{n}; A_{n}×C; γ[b(id)]; A_{n}...]

where we put γ[b(id)](id) ≡ γ(b(id))

st \frac{c ∈ γ[Γ_{n}, y ∈ β] b ∈ β[Γ_{n}]}{c[b(id)] ∈ γ[b(id)][Γ_{n}]} is [figure: C; c; id; C; γ; A_{n}; B; β; A_{n}; b; id; B; β; A_{n}; A_{n}; c[b(id)]; A_{n}×C]

where we put c[b(id)](id) ≡ c(b(id))

wT \frac{β[Γ_{n}] δ[Γ_{n}]}{β[Γ_{n}, y ∈ δ]} is [figure: B; β; A_{n}...; D; δ; A_{n}...; D×B; β[δ(id)]; D; δ; A_{n}...]

where we put β[δ(id)](id) ≡ β(δ(id))

wt \frac{b ∈ β[Γ_{n}] ξ[Γ_{n}]}{b ∈ β[Γ_{n}, w ∈ ξ]} is [figure: A_{n}; b; id; B; β; A_{n}; E; ξ; A_{n}...; E; b[ξ(id)]; id; E×B; β[ξ(id)]; A_{n}; E; ξ]

where we put b[ξ(id)](id) ≡ (ξ(id))^{∗}(b(id)), that is the unique morphism of U/E from i_{A_{n}}(ξ(id)) to β(ξ(id)), obtained from b(id) by the properties of pullback.

The rule expressing the assumption of variable is the following:

var \frac{β [Γ_{n}]}{x ∈ β[Γ_{n}, x ∈ β]} is [figure: B; β; A_{n}...; B; △; id; B×B; β[β(id)]; A_{n}; B; β]

where x(id) ≡ △_{B} ≡ ⟨id_{B}, id_{B}⟩.

Now, we show the formation rules for types and then the introduction, elimination and conversion rules for their terms.

The proper types and terms of T (U) are described as follows. Proper type judgements arise from objects of P gr(U) and proper term judgements arise from morphisms of P gr(U). For every object of P gr(U) a_{1}, a_{2}, ..., a_{n}, t we consider the sequence obtained by making the pullback of a_{1} along the identity, then by making the pullback of a_{2} along the second projection p_{1} of the previous pullback, and so on, that is we obtain the following sequence of pullbacks:

[figure: B_{Σ}; p_{n}^{∗}(t); t^{∗}(p_{n}); B; t; A_{Σn}; p_{n}; p_{n−1}^{∗}(a_{n}); A_{n}; a_{n}; A_{Σ2}; p_{1}^{∗}(a_{2}); p_{2}; A_{2}; a_{2}; A_{1}; !_{A_{1}}; p_{1}; A_{1}; a_{1}; 1; id_{1}; 1]

where p_{i} is the second projection of the pullback of a_{i} and p_{i−1}, for i = 1, …, n. Finally, we consider the associate sequence of fibred functors

Â_{1}, â_{2}[p_{1}], â_{3}[p_{2}], ..., â_{n}[p_{n−1}], t̂[p_{n}]

where Â_{1} ≡ â_{1}, hence we introduce a new dependent type t^{−1} and finally we state that

t^{−1}[x_{1} ∈ A_{1}, ..., x_{n} ∈ a_{n}^{−1}] is [figure: B_{Σ}; t̂[p_{n}]; A_{Σn}; â_{n}[p_{n−1}]; A_{Σ1}; Â_{1}; 1]

where the Σ subscript is used for the interpretation of the series of judgements of proper types introduced by an object of P gr(U).

Moreover, given a sequence of fibred functors α_{1}, α_{2}, ..., α_{n}, β of P gf(U), for every morphism c of P gr(U) [figure: A_{n}; c; id; B; β(id); 1; A_{1}; !_{A_{1}}; A_{n}] we introduce a new term c and we state that

c ∈ β(id)[x_{1} ∈ A_{1}, ..., x_{n} ∈ α_{n}] is [figure: A_{n}; \overline{c}(id); id; B; β(id); A_{n}]

where \overline{c}(id) ≡ c. Finally, we add all the types and terms of the typed calculus Au, defined as for the interpretation in section 4.2.1. All the equality rules in Au are satisfied by the validity theorem proved in 4.2.2.

Remark 6.2 Our definition of internal language of a category follows [LS86], for instance, and it is different from that in [Tay97].

6.1 The relation between the Au type theories and arithmetic universes

There is a biequivalence between the internal type theories of arithmetic universes described in section 6 and the category of arithmetic universes. As a consequence of this, we can state that the type theory T (U) is the internal language of the arithmetic universe U. First of all, we define the following categories:

1. T h(Au) whose objects are the type theories of arithmetic universes, whose initial type theory is Au and whose morphisms are translations: they send types to types so as to preserve the type and term constructors; we call T h(Au)^{∗} the category whose objects are those of T h(Au), but whose morphisms are translations preserving type and term constructors up to isomorphisms;

2. AU_{o} whose objects are arithmetic universes with a fixed choice of arithmetic universe structure and whose morphisms are strict logical functors, that is functors preserving the arithmetic universe structure with respect to the fixed choices; we call AU the category whose objects are those of AU_{o}, but whose morphisms are functors preserving the arithmetic universe structure up to isomorphisms.

Now, we define a functor from arithmetic universes to type theories

T : AU_{o} ⟶ T h(Au)

that associates to every arithmetic universe U the internal type theory T (U) described in the previous section. The functor T associates to every morphism F : U → D of AU_{o} the translation T (F) : T (U) → T (D) defined as follows. Given a fibred functor σ : U/A → U^{→}, corresponding to a type judgement, and a natural transformation c, corresponding to a term judgement, we define T (F)(σ) and T (F)(c) in the same way as we have defined the interpretation of a type theory in section 4.2.1. If σ = b̂ for any b : B → A of U, then we put F (σ) = F̂ (b), since the chosen pullbacks of U are sent into the chosen pullbacks of D by F. If σ is introduced by an inference rule of Au, then we simply define F (σ) such that F (σ)(id) = F (σ(id)), in order to make T (F) be a translation. For example, we put F (Σ_{β}(γ)) ≡ Σ_{F (β)}(F (γ)). This definition of T (F) is good, since the functor F preserves the arithmetic universe structure with respect to the fixed choices used in the internal type theories of U and D.

Moreover, we define a functor from type theories to arithmetic universes

P : T h(Au) ⟶ AU_{o}

that associates to every type theory T the category P (T ), whose objects are closed types A, B, C, ... and whose morphisms are the expressions (x)b(x) corresponding to b(x) ∈ B[x ∈ A], where the type B does not depend on A. We can prove that P (T ) is an arithmetic universe by fixing a choice of its structure as in section 3. The functor P associates to every morphism of T h(Au) L : T → T′ the functor P (L) : P (T ) → P (T′) defined as follows. For every closed type A, we put P (L)(A) ≡ L(A), which is well defined since a translation sends closed types to closed types. For every morphism b(x) ∈ B[x ∈ A] of P (T ) we put

P (L)(b(x) ∈ B[x ∈ A]) ≡ L(b(x)) ∈ L(B)[x ∈ L(A)]

Since L is a translation, then P (L) is a functor preserving the arithmetic universe structure. In order to describe the relation between type theories and arithmetic universes, we have to consider a type theory T as a category. We think of T as the category whose objects correspond to those of P gr(P (T )), but whose morphisms are sequences of morphisms by which we built a series of commutative squares. More precisely, the objects of T are the dependent types under a context B(x_{1}, ..., x_{n})[x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}]. The morphisms of T exist only from B[x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}] to B′[x′_{1} ∈ A′_{1}, ..., x′_{n} ∈ A′_{n}] and they are^{1}

b′ ∈ B′(a′_{1}, ..., a′_{n})[x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}, y ∈ B(x_{1}, ..., x_{n})]

such that a_{1} ∈ A′_{1}[x_{1} ∈ A_{1}] and a′_{i} ∈ A′_{i}(a′_{1}, ..., a′_{i−1})[x_{1} ∈ A_{1}, ..., x_{i} ∈ A_{i}] for i = 1, ..., n. The composition is the substitution and the identity is y ∈ B(x_{1}, ..., x_{n})[x_{1} ∈ A_{1}, ..., x_{n} ∈ A_{n}, y ∈ B]. Therefore, we can consider equivalences of type theories. In the following we mean by ID the identity functor.

Proposition 6.3 Let T : AU_{o} → T h(Au) and P : T h(Au) → AU_{o} be the functors defined above. There are two natural transformations: η from ID to T · P, thought as functors from T h(Au) to T h(Au)^{∗}, and ϵ from P · T to ID, thought as functors from AU_{o} to AU, such that for every type theory T and for every arithmetic universe U, η_{T} : T → T (P (T )) and ϵ_{U} : P (T (U)) → U are equivalences.

Proof. In order to obtain the natural transformation η, for every type theory T we define

η_{T} : T → T (P (T ))

as follows. For any closed type η_{T} (A[ ]) ≡ Â(id) : A_{Σ} → 1. For dependent type judgements, η_{T} (C(x, y)[x ∈ A, y ∈ B(x)]) is the type judgement of T (P (T )) corresponding to the sequence

[figure: Σ_{z∈B̃}C(x)_{Σ}; q_{3}(id); Σ_{x∈A}B(x)_{Σ}; q_{2}(id); A_{Σ}; Â(id); 1]

where B̃ ≡ Σ_{x∈A}B(x) and q_{i} ≡ π̂_{1}[p_{i−1}] for i = 2, 3. This is the dependent type judgement arising from the following sequence

[figure: Σ_{z∈Σ_{x∈A}B(x)}C(x); π_{1}; Σ_{x∈A}B(x); π_{1}; A; ∗; 1]

in the internal type theory T (P (T )), as it is described in the previous section. For term judgements, η_{T} (c ∈ C(x, y)[x ∈ A, y ∈ B(x)]) is

[figure: Σ_{x∈A}B(x)_{Σ}; \overline{⟨z,c̃⟩}[p_{2}](id); id; Σ_{z∈Σ_{x∈A}B(x)}\overline{C}(z)_{Σ}; q_{3}(id); 1; A_{Σ}; Â(id); _{Σ_{x∈A}B(x)_{Σ}}; q_{2}(id)]

where c̃ ≡ c[x/π_{1}(z), y/π_{2}(z)][z ∈ Σ_{x∈A}B(x)]. This is the term judgement arising from ⟨z, c̃⟩ in the internal type theory T (P (T )), as it is described in definition 6.1. We can obviously imagine how η_{T} is defined in the case of having a generic context of n types. We can see that η is a natural transformation, since translations preserve indexed sum types and projections. η_{T} is a translation up to isomorphisms by proposition 5.2 and it is an equivalence of categories since the functor is faithful, full and essentially surjective. Indeed, we can define a natural transformation η^{−1} such that, given a type theory T , the

1One could also consider the usual morphisms of contexts.

component η_{T}^{−1} : T (P (T )) → T is defined as follows. Given a type judgement [figure: B; β(id); A; α(id); 1] of T (P (T )) we define

η_{T}^{−1}(α(id), β(id)) ≡ β(id)^{−1}(x)[x ∈ A]

where β(id)^{−1}(x) ≡ Σ_{z∈B}Eq(A, β(id)(z), x), that is the fibers of β(id). Given the term judgement

[figure: A; c(id); id; B; β(id); 1; A; α(id)] of T (P (T )), provided that c(id) is c(x) ∈ B[x ∈ A], η_{T}^{−1} associates to it the term

judgement of T

⟨c(x), eq⟩ ∈ Σ_{z∈B}Eq(A, β(id)(z), x)[x ∈ A]

We can see that η^{−1} is a natural transformation, since translations preserve indexed sum types, projections and equality types. We can prove that, for every type theory T , η_{T} and η_{T}^{−1} give rise to an equivalence of categories (also see [See84]).

Moreover, we define a natural transformation ϵ such that for every arithmetic universe U the component

ϵ_{U} : P (T (U)) → U

is defined as follows. ϵ_{U} associates to every object [figure: A; σ(id); 1] of P (T (U)) the object A and it associates to

the morphism [figure: A; b(id); id; A×B; β(!_{A}); 1; A; σ(id)] the morphism q(!_{A}, β(id)) · b(id) : A → B. We can easily prove that ϵ_{U} is

a functor preserving the arithmetic universe structure up to isomorphisms^{2}. We have that ϵ_{U} gives rise to a natural transformation, since the functors preserve the arithmetic universe structure with respect to the fixed choices. Moreover, ϵ_{U} is an equivalence of categories, since it is faithful by uniqueness of morphisms towards pullbacks, full because every section of a fibred functor has got a name in the language, and essentially surjective. Indeed, we can define a natural transformation ϵ^{−1} such that for every arithmetic universe U the component ϵ_{U}^{−1} : U → P (T (U)) is defined as follows. For every object

A of U, ϵ_{U}^{−1}(A) is the closed type corresponding to [figure: A_{Σ}; Â(id); 1]. For every morphism b : A → B of U,

ϵ_{U}^{−1}(b) is the term corresponding to [figure: A_{Σ}; \overline{⟨id,b′⟩}(id); id; A_{Σ}×B_{Σ}; B̂(!_{A_{Σ}} ); 1; A_{Σ}; Â(id)] where b′ = π_{B}^{−1} · b · π_{A} and where π_{B} and π_{A}

are the second projections of the pullbacks of !_{A} and !_{B} along the identity. We conclude that for every arithmetic universe U, ϵ_{U} and ϵ_{U}^{−1} give rise to an equivalence of categories.

7 The free arithmetic universe

The main idea is to generate an arithmetic universe from a given category C by considering its objects as closed types and its morphisms as terms with a free variable. We can prove the universal property by the construction of the category of paths, which represents the dependent types in a categorical way.

Given a category C, we consider the dependent type theory T (C) generated by the inference rules as follows:

1. For every object A of ObC we introduce a new type A and we state the closed type judgement A [ ].

Given A ∈ ObC and B ∈ ObC we state A = B [ ], if they are the same object in ObC.

2This due to the fact that the split fibration selects a choice of structure different from the choice given with an arithmetic universe: see, for instance, the terminal object.

2. For every morphism b : A → B in C, we introduce a new term b(x) and we state b(x) ∈ B [x ∈ A], where A and B are closed types.

Given b : A → B and d : A → B in C, we state b(x) = d(x) ∈ B [x ∈ A], provided that b and d are the same morphism in C.

Given b : A → B and a : D → A in C, we state about composition b(x)[x := a(y)] = (b · a)(y) ∈ B [y ∈ D].

3. There are all the inference rules of the type theory Au for arithmetic universes.

Therefore, T (C) is a type theory of arithmetic universes.

Now, we can prove:

Proposition 7.1 Let P : T h(Au) ⟶ AU_{o} be the functor described in section 6. The category P (T (C)) is the free arithmetic universe generated by the category C in P (T h(Au)).

Proof. We know that P (T (C)) is an arithmetic universe from the definition of P. Given a functor G : C → U, from the category C to the arithmetic universe U, we claim that there exists a unique functor

G̃ : P (T (C)) → U in AU_{o} such that the diagram [figure: C; I; G; P (T (C)); G̃; U] commutes, where I : C → P (T (C)) is

the following functor: for every object A ∈ ObC we put I(A) ≡ A [ ] and for every morphism b : A → B we put I(b) ≡ b(x) ∈ B[x ∈ A].

In order to define G̃ on P (T (C)), we define an interpretation J : T (C) → P gr(U), by passing to P gf(U), with the warning that we have to normalize the interpretation. This is done by adding the value of every fibred functor σ ∈ F ib(U/1, U^{→}) on the empty context,^{3} such that a type judgement will be interpreted by a sequence of P gr(U) like

α_{1}(∅), α_{2}(id_{A_{1}}), ..., α_{n}(id_{A_{n−1}})

The interpretation is given in the same way as for the type theory Au in section 4.2.1, except for closed types and terms, which are interpreted in fibred functors evaluated on ∅. The reason is that we want to put G̃(A[ ]) ≡ domJ (A[ ]) and G̃(b ∈ B[x ∈ A]) ≡ q(J (A[ ]), J (B[ ])) · J (b ∈ B[x ∈ A]), but if we adopt for J the semantics defined in section 4.2.1, then G̃ would commute with G up to isomorphisms. So, for every object A of ObU, we extend the functor Â by adding Â(∅) ≡!_{A} and for every object B, q(!_{B}, Â(∅)) is the second projection of the pullback of !_{B} and Â(∅). For example for the terminal type

J (⊤[ ]) ≡ ˆ1(id_{∅}) and J (⋆ ∈ ⊤[ ]) is [figure: 1; id_{1}; id_{1}; 1; ˆ1(id_{∅}); 1] . Then, given a proper type arising from an object

A ∈ ObC, we put J (A[ ]) ≡ { \atop G(A)}(∅) and given a proper term arising from a morphism b : A → B of

C, we put J (b ∈ B[x ∈ A]) ≡ ⟨id_{G(A)}, G(b)⟩ section of { \atop G(B)}({ \atop G(A)}(∅)) : G(A) × G(B) → G(A). By

definition G̃ preserves the arithmetic universe structure and we get G̃ · I = G. Moreover, G̃ is obviously unique for fixed choices of the arithmetic universe structure, which are required to interpret the type theory T (C) into P gr(U).

The free structure gives rise to a monad. AU_{o} should be monadic on Cat and Graph. Or at least, if we prove that AU_{o} is essentially algebraic, we would get a representation theorem of AU_{o} into a category of presheaves [AR94].

3In a rigorous way, we consider the free category U/1^{⊤} with terminal object ∅ generated from U/1. So a type and a term with empty context are interpreted respectively as functor σ^{⊤} and natural transformation ρ^{⊤} of [U/1^{⊤}, U^{→}] such that σ^{⊤} and ρ^{⊤} restricted to U/1 are in F ib(U/1, U^{→}). We extend the fibred functors as described above. For short we still write σ for σ^{⊤}.

8 Free internal categories and diagrams

In this section we show how we can define free internal categories and diagrams within an arithmetic universe by means of its internal languages. The key point to do these constructions is to face the lack of a recursion principle available on proper subsets 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.

8.1 Useful operations on list types

We describe some useful operations on list types that we are using in the following to build free categories and diagrams internal to an arithmetic universe. Firt of all note that List(⊤) represents the natural numbers type and we call it N. Given s, s′ ∈ List(A) we abbreviate

s · s′  for  Rec_{s}(s, cons, s′)

which is the operation appending a list to another one. For short, if there is no danger of ambiguity, 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. 8.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. 8.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)

Now we prove a proposition, which might be useful to prove properties about our operations on the list types.

Proposition 8.3 List(A) is isomorphic to

Σ_{w∈List(A)} (w =_{List(A)} ϵ) + (Σ_{s∈List(A)} Σ_{x∈A} w =_{List(A)} cons(s, x))

Proof. We put the following abbreviations: for w ∈ List(A)

\begin{matrix}A(w) ≡ w =_{List(A)} ϵ B(w) ≡ Σ_{s∈List(A)} Σ_{x∈A}w =_{List(A)} cons(s, x) \\ C(w) ≡ A(w) + B(w) \end{matrix}

We define

Ψ(z) ∈ List(A) [z ∈ Σ_{w∈List(A)}C(w)] as Ψ(z) ≡ π_{1}(z)

and its inverse

Ψ^{−1}(z′) ∈ Σ_{w∈List(A)}C(w) [z′ ∈ List(A)] as Ψ^{−1}(z′) ≡ Rec_{s}(c_{1}, c_{2}, z′)

where

c_{1} ≡ ⟨ϵ, inl(eq)⟩ c_{2} ≡ ⟨s · x, inr(⟨s, ⟨x, eq⟩⟩)⟩

It is easy to check by the elimination rule on the list type that Ψ(Ψ^{−1}(z)) = z for z ∈ List(A). In order to prove that Ψ(Ψ^{−1}(z′)) = z′ for z′ ∈ Σ_{w∈List(A)}C(w), knowing that π_{1}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′))) = π_{1}(z′) we only need to derive

π_{2}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′)) =_{C(π_{1}(z′))} π_{2}(z′) [z′ ∈ Σ_{w∈List(A)}C(w)]

To this purpose we derive the following more general type judgement

π_{2}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′))) =_{C(π_{1}(z′))} z [z′ ∈ Σ_{w∈List(A)}C(w), z ∈ C(π_{1}(z′))]

by the elimination rule on the sum type C(π_{1}(z′)) ≡ A(π_{1}(z′)) + B(π_{1}(z′)). Now, we derive the premisses to apply the elimination rule on the above sum type. Given x ∈ A(π_{1}(z′)) we get

π_{1}(z′) = ϵ x = eq

where the second equation holds by the conversion rule on the equality type. Hence we obtain

π_{2}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′))) = π_{2}(Rec_{s}(c_{1}, c_{2}, ϵ)) = inl(eq) = inl(x)

Moreover, given y ∈ B(π_{1}(z′)) we get

π_{1}(z′) = s · x ⟨s, ⟨x, eq⟩⟩ = y

where s ≡ π_{1}(y), x ≡ π_{1}(π_{2}(y)) and eq = π_{2}(π_{2}(y)) holds by the conversion rule on the equality type. Hence we obtain

π_{2}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′))) = π_{2}(Rec_{s}(c_{1}, c_{2}, s · x)) = inr(⟨s, ⟨x, eq⟩⟩) = inr(y)

This sufficies to apply the elimination rule on the sum type and get

π_{2}(Rec_{s}(c_{1}, c_{2}, π_{1}(z′))) =_{C(π_{1}(z′))} z [z ∈ C(π_{1}(z′))]

Then substituting z for π_{2}(z′) in the above proposition, by the elimination rule for the equality type we conclude that Ψ(Ψ^{−1}(z′)) = z′ for z′ ∈ Σ_{w∈List(A)}C(w).

Def. 8.4 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. In the following lemma we abbreviate

\overline{x · s} ≡ ⟨x · s, ⟨x, ⟨s, eq⟩⟩⟩ \overline{x} ≡ ⟨x, ⟨x, ⟨ϵ, eq⟩⟩⟩

Proposition 8.5 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}

Proof. The following definition,

h^{∗}(z) ≡ Rec_{s}( h_{1}(π_{1}(π_{2}(z))) , h_{2}^{∗}(π_{1}(π_{2}(z))) , π_{1}(π_{2}(π_{2}(z))) )

where

h_{2}^{∗}(π_{1}(π_{2}(z))) (s, y, w) ≡ h_{2}( π_{1}(π_{2}(z)) , s, y, w )

satisfies our claim.

Remark 8.6 Another possibility to define terms from List^{∗}(A) is to use the elimination rule for List(A) provided that we know how to extend the claimed proof-term on the empty list. Indeed, we can use the elimination rule on the corresponding full list type, dealing with the case where we add an element to the list, by differentiating it in two subcases, that is when the length of a list is 1 or more. This is possible because from n + 1 = 0 we get a proof of falsum using disjointness with

Rec_{s}(inl(∗), inr(∗), n) ∈ ⊤ + ⊤ [n ∈ N]

Once we have got this derivation, we can prove by elimination on the list type that for s ∈ List(A) if lh(s) = 0 then s = ϵ and if lh(s) = 1 then s = a for some a ∈ A, by using proposition 8.3.

In the next when we define the operations on List^{∗}(A) we will simply write a non-empty list s for an element ⟨s, ⟨x, ⟨s′, eq⟩⟩⟩ of List^{∗}(A). Moreover, given an operation t(s) ∈ B [s ∈ List(A)] we simply write t(z) instead of t(π_{1}(z)) for z ∈ List^{∗}(A).

Def. 8.7 On List^{∗}(A), we define the operation top from List^{∗}(A) to List(A) taking the top of a non-empty list

top(s) ∈ List(A) [s ∈ List^{∗}(A)]

top(a) ≡ a top(s · a) ≡ \begin{cases}a & if lh(s) = 1 \\ top(s) · a & if lh(s) ≥ 2 \end{cases}

the operation front which strictly takes the top of a non-empty list

front(s) ∈ List(A) [s ∈ List^{∗}(A)]

front(a) ≡ ϵ front(s · a) ≡ front(s) · a the operation back that takes the back of non-empty list

back(s) ∈ List(A) [s ∈ List^{∗}(A)]

back(a) ≡ a back(s · a) ≡ s and finally the operation tail that strictly takes the tail of a non-empty list:

tail(s) ∈ List(A) [s ∈ List^{∗}(A)]

tail(a) ≡ ϵ tail(s · a) ≡ s Moreover, we define the projections of the first and last element of a list

first(s) ∈ A [s ∈ List^{∗}(A)]

first(a) ≡ a first(s · a) ≡ first(s)

last(s) ∈ A [s ∈ List^{∗}(A)]

last(a) ≡ a last(s · a) ≡ a

We also define the reverse operation of a list

rev(s) ∈ List(A) [s ∈ List(A)]

rev(ϵ) ≡ ϵ rev(s · a) ≡ a · rev(s)

Proposition 8.8 We can derive a proof-term of

rev(rev(s)) =_{List(A)} s [s ∈ List(A)]
top(rev(s)) =_{List(A)} rev(back(s)) [s ∈ List^{∗}(A)]
back(rev(s)) =_{List(A)} rev(top(s)) [s ∈ List^{∗}(A)]

Proof. We prove the first two equations by induction on the list type. For the first equation, we need to prove in advanced by induction on t that rev(a · t) = rev(t) · a for a ∈ A and t ∈ List^{∗}(A). For the second equation, we need to prove first by induction on t that top(a · t) = t for a ∈ A and t ∈ List^{∗}(A). The last equation follows from the first two.

Now we define projections on non-empty lists.

Def. 8.9 For every n ∈ N we define the n-th projection

p_{n}(s) ∈ A [s ∈ List^{∗}(A)]

by the elimination rule on the positive natural numbers expressed in proposition 8.5 as follows

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

Now we prove some lemmas about projections that will be useful in the next.

Lemma 8.10 For every s, t ∈ List^{∗}(A) we can derive

p_{n}(s) =_{A} p_{l+n}(t · s)

where lh(t) = l.

Proof. Instead of proving the above statement first we prove by induction on t that

p_{n}(rev(s)) =_{A} p_{l+n}(rev(s · t))

If t ≡ ϵ then l = 0 and the claim holds. If t ≡ t′ · a then by definition of projections and top p_{l−1+n+1}(rev(s · (t′ · a))) = p_{l−1+n}(top(rev(s · (t′ · a)))) = = p_{l−1+n}(rev(back(s · (t′ · a)))) = p_{l−1+n}(rev(s · t′)) = p_{n}(rev(s)) where the last but one equation holds since top · rev = back · rev and the last by inductive hypothesis. Then our claim follows since

p_{n}(s) = p_{n}(rev(rev(s))) = p_{l+n}(rev(rev(s) · rev(t))) = p_{l+n}(rev(rev(t · s))) = p_{l+n}(t · s)

where the second equation holds by proposition 8.8 and because we can easily derive by induction on s

rev(t · s) =_{List(A)} rev(s) · rev(t) [s ∈ List(A), t ∈ List(A)]

Now, our aim is to prove also that for s, t ∈ List^{∗}(A) p_{n}(s · t) = p_{n}(s) for n ≤ lh(s), but since we can not reason by induction on the natural numbers we need to prove first some other useful lemmas. Note that we use the following abbreviation

n ≤ lh(s) ≡ Σ_{x∈N}lh(s) =_{N} x + n

where + is the sum recursive function.

Lemma 8.11 We can derive

\begin{matrix}( Σ_{v∈List^{∗}(A)} Σ_{v′∈List^{∗}(A)} lh(v) =_{N} n × v · v′ =_{List^{∗}(A)} s ) + ( n ≥ lh(s) − 1 ) \\ [s ∈ List^{∗}(A), n ∈ N] \end{matrix}

Proof. We perform the derivation by the elimination rule on the non-empty list type over s. If s = a then the claim easily follows. If s = s′ · a, supposing n ≤ lh(s′) − 1 then by inductive hypothesis we have that s′ = v · v′ and then s′ · a = v · (v′ · a) as claimed. If n = lh(s) − 1 then we put v = s′ and v′ = a.

Lemma 8.12 For every s ∈ List^{∗}(A), a ∈ A we can derive

p_{lh(s)}(s) =_{A} p_{lh(s)}(s · t)

Proof. The proof follows by the elimination rule on the non-empty list type. If s = a then by definition of projection p_{lh(a)}(a) = p_{1}(a) = first(a) = a = first(a · t) = p_{1}(a · t) = p_{lh(a)}(a · t). Indeed we can easily prove by induction over t that

first(a · t) =_{A} a [a ∈ A, t ∈ List^{∗}(A)]

Moreover, if s = s′ · a and lh(s′) ≥ 2, then by definition of projection and of top we get p_{lh(s)}(s′ · a) = p_{lh(s)−1}(top(s′ · a)) = p_{lh(s)−1}(top(s′) · a). Hence by lemma 8.10, since lh(top(s′)) = lh(s′) − 1 = lh(s) − 2, and by definition of first projection p_{lh(s)−1}(top(s′) · a) = p_{1}(a) = a = p_{1}(a · t) and again by lemma 8.10 p_{1}(a · t) = p_{lh(s)−1}(top(s′) · (a · t)). Finally by the fact that we can derive by induction over s′

\begin{matrix}( top(s′ · t) =_{List^{∗}(A)} top(s′) · t × lh(s′) ≥ 2 ) + ( top(s′ · t) = t × lh(s′) = 1 ) \\ [s′ ∈ List^{∗}(A), t ∈ List^{∗}(A), n ∈ N] \end{matrix}

we conclude that p_{lh(s)−1}(top(s′) · (a · t)) = p_{lh(s)−1}(top(s′ · a · t)) = p_{lh(s)}(s · t). Now if lh(s′) = 1 then by definition of first projection and of top p_{lh(s′·a)}(s′ · a) = p_{1}(top(s′ · a)) = p_{1}(a) = p_{1}(a · t) and finally by the above property of top we conclude p_{1}(a · t) = p_{1}(top(s′ · a · t)) = p_{2}(s′ · a · t) = p_{lh(s)}(s · t).

Lemma 8.13 For every s ∈ List^{∗}(A), a ∈ A we can derive

( p_{n}(s) =_{A} p_{n}(s · t) × n ≤ lh(s) ) + ( n ≥ lh(s) + 1 )

Proof. We focus on how we derive the first disjunct of the above type. If n = lh(s) then the claim holds by lemma 8.12. Now suppose that n ≤ lh(s) − 1. Then by lemma 8.11 we find v, v′ ∈ List^{∗}(A) such that lh(v) = n and s = v · v′. Hence by using lemma 8.12 we get

p_{n}(s) = p_{lh(v)}(v · v′) = p_{lh(v)}(v) = p_{lh(v)}(v · (v′ · t)) = p_{n}(s · t)

This sufficies to derive the above types by the decidability of natural numbers order.

Now we prove a lemma saying the last projection on a list correspond to its last element.

Lemma 8.14 For s ∈ List^{∗}(A) we can derive

p_{lh(s)}(s) =_{A} last(s)

Proof. We use the elimination rule of non-empty list type on s. If s = a then we conclude by definition of first projection and of last. If s = s′ · a then by lemma 8.10, since lh(s′) = lh(s) − 1, and by definition of last we conclude p_{lh(s)}(s′ · a) = p_{1}(a) = last(s′ · a).

Now we use projections to define parts of lists.

Def. 8.15 The n-th part of a list

part(s, n) List(A) [s ∈ List(A), n ∈ N]

is defined by the elimination rule 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}

Now, we prove a useful lemma on list parts.

Lemma 8.16 For every s, t ∈ List(A) we can derive

part(s · t, n) =_{List(A)} part(s, n)

for n ≤ lh(s).

Proof. The proof goes by induction on natural numbers with respect to

( part(s · t, n) =_{List(A)} part(s, n) × n ≤ lh(s) ) + ( n ≥ lh(s) + 1 )

We show only the relevant part of this induction. If n = 0 then the claim follows by definition of part. If n ≥ 1 and n ≤ lh(s) then by definition of part, by inductive hypothesis and by lemma 8.13 part(s · t, n) = part(s · t, n − 1) · p_{n}(s · t) = part(s, n − 1) · p_{n}(s) = part(s, n).

Lemma 8.17 For every s ∈ List(A) we can derive

part(s, lh(s)) =_{List(A)} s

Proof. The proof goes by induction on the list type. If s = ϵ then the claim follows by definition of part. If s = s′ · a then by definition of part and by lemma 8.14 we get part(s′ · a, lh(s)) = part(s′ · a, lh(s) − 1) · p_{lh(s)}(s′ · a) = part(s′ · a, lh(s) − 1) · a. Now, by lemma 8.16 part(s′·a, lh(s)−1) = part(s′, lh(s′)) and by inductive hypothesis part(s′, lh(s′)) = s′. Hence we conclude that part(s′ · a, lh(s) − 1) · a = s′ · a = s.

8.2 An arithmetic universe has got coequalizers

Now we are going to prove that an arithmetic universe U has got coequalizers, by using its internal language. Indeed, we show how to close a relation under the properties that make it into an equivalence relation by using the list type.

Proposition 8.18 Given two maps in the arithmetic universe U

[figure: C; a; b; A]

the coequalizer of the two map exists in U.

Proof. First we consider the following reflexive and symmetric relation of A⊕A to define the coequalizer of the two maps: for z, z′ ∈ A ⊕ 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 we can define its transitive closure as follows:

\begin{aligned}R_{t}(z, z′) ≡ & Σ_{s∈List(Σ_{w∈A×A}R(π_{1}(w),π_{2}(w)))} lh(s) ≥ 1 × \overline{π_{2}}(back(s)) =_{List(A)} \overline{π_{1}}(top(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 [−] : 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.

8.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 as follows (we refer to [Joh77] or [MM92] for a general account on these concepts about internal category theory).

Def. 8.19 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})} tail · \overline{δ_{1}}(w)

is the equalizer of the following maps:

[figure: List^{∗}(G_{1}); front·\overline{δ_{0}}; tail·\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 follows

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

The unit e(x) ∈ C_{1} [x ∈ G_{0}] is defined as

e(x) ≡ inl(x)

It follows immediately that

δ′_{0} · e = id δ′_{1} · e = id

The composition of morphisms

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

with C_{1} ×_{G_{0}} C_{1} ≡ Σ_{f∈C_{1}} Σ_{g∈C_{1}} δ′_{1}(f) =_{G_{0}} δ′_{0}(g) is basically defined as a restriction of 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})

where on the members with factor G_{0} we just project the list. Precisely the composition is defined by double elimination respectively on the sum type of π_{2}(δ(π_{1}(w))) and of π_{2}(δ(π_{1}(π_{2}(w)))) for w ∈ C_{1} ×_{G_{0}} C_{1}, with δ defined as in proposition 3.6, 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 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 δ′_{1} along δ′_{0}, and that is associative

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

by using double elimination on the same sum types used to define composition. In an analogous way, it is straightforward to prove that this composition admits the above define e as unit map, that is

comp_{C_{1}} · (e × id) = π′_{2} comp_{C_{1}} · (id × e) = π′_{1}

Now we are going to prove

Proposition 8.20 Given the graph

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

then the category defined above in 8.19 as

\xymatrix{C_{1} \ar[r]^{δ′_{0}} \ar[r]_{δ′_{1}} & G_{0} \ar[l]|{e}}

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(⟨cons(ϵ, f), eq⟩) for f ∈ G_{1}. Now, we prove the universal property. Given another internal category

\xymatrix{D_{1} \ar[r]^{ϕ_{o}} \ar[r]_{ϕ_{1}} & D_{0} \ar[l]|{ι}}

with the composition map

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}. We obviously define ψ̂_{0} ≡ ψ_{0}. Then we define

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

where app : D̂_{1} → D_{1} will be defined later, while the map m : Ĉ_{1} → D̂_{1} is obtained by the universal property of the equalizer with respect to the map List^{∗}(ψ_{1}) · j : Ĉ_{1} → List^{∗}(D_{1}), with List^{∗}(ψ_{1}) the map induced from ψ_{1} on the corresponding non-empty list type considering the internal category simply as a graph and j : Ĉ_{1} → List^{∗}(G_{1}) the equalizer map. The map List^{∗}(ψ_{1}) · j equalize front · \overline{ϕ_{0}} and tail · \overline{ϕ_{1}} by the property of graph morphism, namely that

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

The key point is to define the map app : D̂_{1} → D_{1} on D̂_{1}, on which we can not use an elimination rule as we did with the restricted List^{∗}(G_{1}) by proving proposition 8.5. In order to define app we fix 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.

Def. 8.21 We define

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

such that

ϕ(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}

ϕ is obtained by using the first projection and the elimination rule of the sum type on the corresponding the term defined by the elimination rule on the natural numbers object with respect to the following 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]

since 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. Finally we put

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

In order to prove that ψ̂_{1} is functorial we need some lemmas.

Lemma 8.22 For every z_{1} ∈ D̂_{1}, z_{2} ∈ D̂_{1} such that δ′_{1}(z_{1}) = δ′_{0}(z_{2}) then

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

with n ≤ lh(π_{1}(z_{1})).

Proof. We perform an induction on n ∈ N with respect to the following type

( ϕ(comp_{D_{1}}(z_{1}, z_{2}), n) =_{D_{1}} ϕ(z_{1}, n) × n ≤ lh(π_{1}(z_{1})) ) + ( n ≥ lh(π_{1}(z_{1})) + 1 )

by using the decidability of order between natural numbers. We show only the relevant part of this induction. For n = 0 we have

ϕ(z_{1}, 0) = p_{1}(π_{1}(z_{1})) = p_{1}(π_{1}(z_{1}) · π_{1}(z_{2})) = p_{1}(π_{1}(comp_{D_{1}}(z_{1}, z_{2}))) = ϕ(comp_{D_{1}}(z_{1}, z_{2}), 0)

where the second equality holds by lemma 8.13 and the last but one by definition of composition. Then, supposing n ≥ lh(π_{1}(z_{1})), the inductive step is dealt as follows ϕ(z_{1}, n + 1) = comp_{D_{1}}(ϕ(z_{1}, n), p_{n+1}(π_{1}(z_{1}))) = comp_{D_{1}}(ϕ(comp_{D_{1}}(z_{1}, z_{2}), n), p_{n+1}(π_{1}(z_{1}))) = = comp_{D_{1}}(ϕ(comp_{D_{1}}(z_{1}, z_{2}), n), p_{n+1}(π_{1}(z_{1}) · π_{1}(z_{2}))) = ϕ(comp_{D_{1}}(z_{1}, z_{2}), n + 1) where the second equality is obtained by inductive hypothesis and the last but one by lemma 8.13.

Note that for s ∈ D̂_{1}

ϕ_{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))

where the second equation holds by lemma 8.14. Hence the terms in the next lemma are well defined.

Lemma 8.23 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})).

Proof. We proceed by elimination rule on n ∈ N. The base case for n = 0 is dealt as follows: comp_{D_{1}}(ϕ(z_{1}, l_{1}), ϕ(z_{2}, 0)) =_{D_{1}} comp_{D_{1}}(ϕ(z_{1}, l_{1}), p_{1}(π_{1}(z_{2}))) by lemma 8.22 and 8.10 = comp_{D_{1}}(ϕ(comp_{D_{1}}(z_{1}, z_{2}), l_{1}), p_{l_{1}+1}(π_{1}(z_{1}) · π_{1}(z_{2}))) and by definition of ϕ = ϕ(comp_{D_{1}}(z_{1}, z_{2}), l_{1} + 1). The general case is dealt in an analogous way by using the same lemmas.

With the above lemmas and lemma it is easy to check that

ϕ_{0} · ψ̂_{1} = ψ̂_{0} · δ′_{0}  ϕ_{1} · ψ̂_{1} = ψ̂_{0} · δ′_{1}  ψ̂_{1} · e = ι · ψ̂_{0}
comp_{D_{1}} · (ψ̂_{1} × ψ̂_{1}) = ψ̂_{1} · comp_{C_{1}}

The uniqueness of ψ̂_{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 obviously ρ_{0} = ψ̂_{0} and it remains to prove that also ρ_{1} = ψ̂_{1}. To this purpose we prove the following lemma.

Lemma 8.24 Suppose that ρ_{1} : C_{1} → D_{1} is such that ρ_{1} · j_{1} = ψ_{1}, then given z ∈ Ĉ_{1} and n ∈ N we derive

ρ_{1}(inr(⟨part(π_{1}(z), n), eq⟩)) =_{D_{1}} ψ̂_{1}(inl(⟨part(π_{1}(z), n), eq⟩))

Proof. The base case, when n = 0 is easy since part(z, 1) = p_{1}(z) and then by hypothesis we get ρ_{1}(inr(⟨part(π_{1}(π_{1}(z)), 0), eq⟩)) = ρ_{1}(j_{1}(p_{1}(π_{1}(z)))) = ψ_{1}(p_{1}(π_{1}(z))) = ψ̂_{1}(inr(⟨part(π_{1}(z), 0), eq⟩)). The inductive case. By definition of composition in C_{1} we know that inr(⟨part(π_{1}(z), n + 1), eq⟩) = comp_{C_{1}}(inr(⟨part(π_{1}(z), n), eq⟩), inr(⟨p_{n+1}(π_{1}(z)), eq⟩)). Therefore we get ρ_{1}(inr(⟨part(π_{1}(z), n + 1), eq⟩)) = ρ_{1}(comp_{C_{1}}(⟨part(π_{1}(z), n), eq⟩, inr(⟨p_{n+1}(π_{1}(z)), eq⟩))) = since ρ_{1} is the morphisms part of an internal functor = comp_{D_{1}}(ρ_{1}(inr(⟨part(π_{1}(z), n), eq⟩)), ρ_{1}(inr(⟨p_{n+1}(π_{1}(z)), eq⟩))) = by inductive hypothesis and the base case = comp_{D_{1}}(ψ̂_{1}(inr(⟨part(π_{1}(z), n), eq⟩), ψ̂_{1}(inr(⟨p_{n+1}(π_{1}(z)), eq⟩)))) = by functoriality of ψ̂_{1} and definition of composition = ψ̂_{1}(inr(⟨part(π_{1}(z), n + 1), eq⟩)).

Finally by the elimination rule on the sum type C_{1} and lemmas 8.24 and 8.17 we can derive

ψ̂_{1}(z) =_{D_{1}} ρ_{1}(z) [z ∈ C_{1}]

All the above lemmas and checks let us conclude that the claimed construction is the free category internally to an arithmetic universe. (of proposition 8.20)

8.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 an arithmetic universe to internal diagrams on the free category generated by it. Indeed, also here, in order to prove the universal property of a free internal diagram we need to define an operation by induction on a proper subset of a list type and we define such operation by iteration on the chosen lists as we did to define the map app in the previous section. Now, we outline how to lift a internal diagram from a graph to a category (for an introduction to these concepts we refer to [Joh77], [MM92]).

Proposition 8.25 Given the internal graph

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

suppose we have 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 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)

that is μ̃ is an internal diagram on the underlying graph of the category C (given by C_{0}, C_{1}) such that

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

where π_{2} is the second projection with respect to 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}} δ′_{0}(z_{1}) × δ′_{1}(z_{1}) =_{G_{0}} δ′_{0}(z_{2})

Proof. We lift μ to an action

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

defined basically as π_{2} ⊕ μ̂, where μ̂ will be defined later, via composition under a suitable isomorphism since by distributivity of sum 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})

Precisely, by the elimination rule on the sum type of π_{2}(δ(π_{1}(w))) for w ∈ F ×_{G_{0}} C_{1}, with δ defined as in proposition 3.6, 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} \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. Given f ∈ F, s ∈ Ĉ_{1} such that π_{0}(f) = δ′_{0}(inr(s)) we define ν such that

ν(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 using the first projection and the elimination rule on the sum type on the corresponding term derived by the elimination rule on natural numbers with respect to the following 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]

It follows that μ̃ is an internal diagram, namely that

π_{0} · μ̃ = δ′_{1} · π_{2}  μ̃ · id × e = π_{2}  μ̃ · (μ̃ × id) = μ̃ · (id × comp_{C_{1}})

and that μ̃ is unique by proving similar lemmas to those about free categories regarding ψ̂_{1} in the previous section.

9 Conclusions

The typed calculus Au for arithmetic universes provides a tool to prove categorical properties about arithmetic universes since it is their internal logic. Here, we have used this calculus to show that arithmetic universes enjoy free internal categories and diagrams. In a forthcoming paper we will use Au to investigate the representations of free finite algebras internally to an arithmetic universe.

10 Acknowledgements

First of all I would like to express my gratitude to Martin Hyland, who introduced me to the problem of describing free finite algebras in an arithmetic universe and helped me with many fruitful discussions during my staying in Cambridge. There, I also enjoyed Peter Johnstone’s help, whom I thank for pointing me out R. Cockett’s paper.

Finally, I wish to thank Steven Vickers for providing me Gavin Wraith’s unpublished notes with the masterthesis of his student [Mor96] and for his interest in this work.

References

[AR94] J. Adamek and J. Rosicky. Locally presentable and accessible categories., volume 189 of Lecture Notes Series. Cambridge University Press, 1994.

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

[Car86] J. Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209–243, 1986.

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

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

[Hof97] M. Hofmann. Extensional Constructs in Intensional Type Theory. Distinguished Dissertations. Springer, 1997.

[HP89] J.M.E. Hyland and A. M. Pitts. The theory of constructions: Categorical semantics and topos theoretic models. In J. W. Gray and A. Scedrov, editors, Categories in Computer Science and Logic, volume 92 of Contemporary Mathematics, pages 137–199, 1989.

[Jac91] B. Jacobs. Categorical type theory. PhD thesis, University of Nijmegen, 1991.

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

[Law70] F.W. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Proc. Sympos. Pure Math., XVII:1–14, 1970.

[LS86] J. Lambek and P. J. Scott. An introduction to higher order categorical logic., volume 7 of Studies in Advanced Mathematics. Cambridge University Press, 1986.

[Mac71] S. Mac Lane. Categories for the working mathematician., volume 5 of Graduate text in Mathematics. Springer, 1971.

[Mai98a] M. E. Maietti. The type theory of categorical universes. PhD thesis, University of Padova, February 1998.

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

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

[Obt89] A. Obtulowicz. Categorical and algebraic aspects of Martin Löf’s type theory. Studia Logica, 3:299–317, 1989.

[Pit95] A.M. Pitts. Categorical logic. In Oxford University Press, editor, Logical Methods in Computer Science, volume VI of Handbook of Logic in Computer Science, page To appear, 1995.

[See83] R. A. G. Seely. Hyperdoctrines, natural deduction and the beck condition. Zeitschr. f. math. Logik. und Grundlagen d. Math., 29:505–542, 1983.

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

[Tay97] P. Taylor. Practical Foundations of Mathematics, volume 99 of Cambridge studies in advanced mathematics. Cambridge University Press, 1997.

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

[NPS90], [Mar84] , [Mai98b] [MR77], [See84], [Hof94] , [Jac91] [Mac71] [LS86][Obt89], [Law70] [See83]

[Jac99] [NPS90][Joh77] [Ben85]