The Internal Type Theory of a Heyting Pretopos

Maria Emilia Maietti

Dipartimento di Matematica Pura ed Applicata, Università di Padova, via G. Belzoni n.7, I-35131 Padova, Italy e-mail: maietti@math.unipd.it

Abstract. We present the internal type theory of a Heyting pretopos with a natural numbers object. The resulting theory is based on dependent types and proofterms. We prove that there is a sort of equivalence between such type theories and the category of Heyting pretoposes. By using the type theory we also build the free Heyting pretopos generated by a category.

Introduction

An elementary topos can be viewed as a generalized universe of sets to develop mathematics. From a logical point of view, topos theory corresponds to an intuitionistic higher order logic with typed variables [LS86]. Suitable toposes provide models of restricted Zermelo set theory [MM92]. Recently, Joyal and Moerdijk built a model of the whole intuitionistic set theory by using the notion of small map and by taking a Heyting pretopos with a natural numbers object as the categorical universe [JM95]. The main difference w.r.t. a topos is that a Heyting pretopos (H-pretopos, for short) correspond to a first order logical framework, precisely to a first order dependent type theory with quotients, called the HP typed calculus in [Mai97]. This calculus is valid and complete w.r.t. the class of H-pretoposes. It consists of the following dependent types: the terminal type, the falsum type, the indexed sum type, the extensional equality type, the disjoint sum type with the disjointness axiom, the natural numbers type, as in the extensional version of Martin-Löf’s type theory [Mar84], the forall type, i.e. the product type restricted to types with at most one proof, and finally a particular quotient type satisfying an effectiveness axiom.

This type theory may be of interest to computer scientists expecially for the proposal of effective quotient types based only on proof-irrelevance equivalence relations. These particular quotient types are different from the extensional quotient types of Nuprl, where effectiveness is not always available (it holds certainly for decidable equivalence relations).

In this paper, we show that the internal type theory of a given H-pretopos is a particular HP type theory plus specific dependent types and terms. To this purpose, we prove that there is a sort of equivalence between such type theories and H-pretoposes. The type theory of a given H-pretopos P is described by a categorical semantics: it combines together the notion of model given by display maps [HP89], [See84] with the tools provided by contextual categories to interpret substitution correctly [Car86]. We shall emphasise 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 P 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. The specific dependent types of P correspond to sequences of fibred functors obtained by pullback from a sequence of morphisms of P.

By means of the type theory, we can build the free H-pretopos generated by a category: it is sufficient to consider the objects of the category as closed types and its morphisms as dependent terms. This is the free construction for categories corresponding to dependent typed lambda calculi. For example, in the same way, one can build both the free category with finite limits - corresponding to the type theory with the terminal type, the extensional equality type, the indexed sum type- and the free locally cartesian closed category with finite coproducts and a natural numbers object -corresponding to Martin-Löf’s type theory with extensional equality but without universes and well founded sets [Mar84].

The type theory of a H-pretopos constitutes a new tool to analyze, from a type theoretical point of view, the notion of small map used in [JM95] to provide a model of intuitionistic set theory. Moreover, it seems interesting to investigate how much of the type theory of H-pretoposes can be formalized within Martin-Löf’s type theory.

The paper is divided as follows: in section 1 we describe the categorical preliminaries to interpret the HP dependent typed calculus in a H-pretopos; in section 2 we show the HP type theory arising from a given H-pretopos, in section 3 we prove a sort of equivalence between the HP type theories and the category of H-pretoposes, in section 4 we build the free H-pretopos and finally we draw the conclusions.

1 Preliminaries

First of all we recall the categorical definition of Heyting pretopos [JM95]. The notion of pretopos was introduced by Grothendieck [MR77].

Definition 1. A pretopos is a category equipped with finite limits, stable finite disjoint coproducts and stable effective quotients of equivalence relations. A Heyting pretopos is a pretopos where pullback functors on subobjects have right adjoints.

In the following, by H-pretopos we shall mean a Heyting pretopos also with a natural numbers object. Since we intend to describe syntactically categorical properties, we shall assume that, with a H-pretopos, a given choice of categorical constructors is made, i.e. fixed choices of finite limits, initial object, coproducts, quotients of equivalence relations and right adjoints on subobjects.

An essential feature for the interpretation of a dependent typed calculus is the local property of a H-pretopos: for every object A of the H-pretopos P, the comma category P/A is a H-pretopos. Indeed, constructing a type, which depends on a context Γ, from other types corresponds to a categorical property of P/A, where A is determined by Γ. Moreover, since substitution corresponds to pullback, the various categorical properties must be stable under pullback. By the way, in a H-pretopos also Beck-Chevalley conditions for right adjoints are satisfied.

Given a H-pretopos P we want to describe its internal dependent type theory T (P). The type theory is based on the HP typed calculus for Hpretoposes (see the appendix), augmented with the specific type and term judgements of P. As in [Mai97], the idea is to consider a dependent type as a sequence of morphisms of P, 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 P: it is the category P gr(P).

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

[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 P 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 m = n and a_{i} = b_{i} for i = 1, ..., n − 1.

Remark 3. We would like to interpret substitution by means of pullback, using the indexed pseudofunctor F : P^{OP} ⟶ Cat defined as follows: F associates to every A ∈ ObP the category P/A and to every morphism f : B → A of P the pullback pseudofunctor f^{∗} : P/A → P/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 : P^{OP} ⟶ Cat [Ben85], [Jac91]. S is defined as follows. For every object A in P, S(A) ≡ F ib(P/A, P^{→}), where F ib(P/A, P^{→}) is the class of functors σ : P/A → P^{→}, fibred from dom_{A} to cod_{A} (they send cartesian morphisms of dom_{A} to cartesian morphisms of cod_{A}). A fibred functor σ : P/A → P^{→} associates to every trian-

gle [figure: C; t; b′; B; b; A] a pullback diagram [figure: C′; q(t,σ(b)); σ(b·t); B′; σ(b); C; t; B] . Moreover, for a mor-

phism f : B → A of P, the functor S(f) : F ib(P/A, P^{→}) → F ib(P/B, P^{→}) 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. Note that the pseudofunctor F : P^{OP} ⟶ Cat is equivalent to the functor S in the appropriate 2-category of pseudofunctors. The functors establishing such an equivalence can be described as follows. To define the functor from P/A to F ib(P/A, P^{→}), first we choose pullbacks, then we associate to every object b : B → A the fibred functor b̂, defined as b̂(t) ≡ t^{∗}(b) in the pullback^{1}

[figure: B_{Σ}; b^{∗}(t); t^{∗}(b); B; b; D; t; A] and extended to morphisms by the universal property of pull-

back. In order to define a functor from F ib(P/A, P^{→}) to P/A, we associate to every fibred functor its evaluation on the identity of the object A.

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(P), where the judgements of the typed calculus for H-pretoposes are preinterpreted. We put I(σ) = A if σ ∈ [P/A, P^{→}].

Definition 4. The objects of the category P gf(P) 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(P), where A_{i} = I(σ_{i}) for i = 1, ..., n. The morphisms of P gf(P) from σ_{1}, σ_{2}, ..., σ_{m} to τ_{1}, τ_{2}, ..., τ_{n} are defined only if m = n 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}

1 We call the second projection b^{∗}(t), since the notation q(t, b) is reserved for projections of functorial choices and not any choice of pullback is functorial.

the second member of ρ(b) is the identity (recall that ρ(b) is a morphism of

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

In the following, 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(P) 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 b^{∗}(ρ(id_{A_{n}})), that

is the unique morphism from σ_{n}(b) to τ_{n}(b), which are obtained respectively by the pullbacks of b and σ_{n}(id) and of b and τ_{n}(id).

Finally, for every A ∈ ObP, we define the fibred functor i_{A} : P/A →

P^{→} which associates to every triangle [figure: C; t; b′; B; b; A] the following pullback

diagram [figure: C; t; id; B; id; C; t; B] .

2 The type theory of P

The type theory T (P) of a H-pretopos P, with a fixed choice of its categorical structure, is a particular HP calculus plus type judgements and term judgements that are specific to P. It is formulated in the style of Martin-Löf’s type theory with four kinds of judgements [NPS90]. There are the type judgements and the judgements about equality between types, which are given by formation rules, the term judgements given by introduction and elimination rules, and the judgements about equality between terms of the same type given by conversion rules. Since the types are allowed to depend on variables of other types, the contexts are telescopic [dB91]. 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 finally, the substitution rules for all the four kinds of judgements [NPS90]. The dependent types are introduced under a context. A type judgement arises from a object of P gf(P), 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(P), 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 H-pretopos. The equality between types corresponds to the equality between objects of P gf(P), which implies the equality between objects of P gr(P). 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(P), 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(P) 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 P/A_{n}.

The equality between terms corresponds to the equality between morphisms of P gf(P). The contexts are generated from the following formation rules:

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

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.

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. We only show 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 P/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 (P) are described as follows. Proper type judgements arise from objects of P gr(P) and proper term judgements arise from morphisms of P gr(P). For every object of P gr(P) 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}; _{a_{n}}[p_{n−1}]; A_{Σ1}; _{A_{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(P).

Moreover, given a sequence of fibred functors α_{1}, α_{2}, ..., α_{n}, β of P gf(P), for every morphism c of P gr(P) [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 HP typed calculus (see the appendix for the inference rules). This calculus is valid and complete with respect to the class of H-pretoposes and is described as follows ^{2}. Given a Hpretopos the terminal type corresponds to the terminal object, the extensional equality types to the equalizers, the indexed sum types to pullbacks, the falsum type to the initial object, the disjoint sum types with the axiom of disjointness to disjoint coproducts, the natural numbers type to the natural numbers object and all these types are already presented in the extensional version of Martin-Löf’s type theory [Mar84]. The key point in finding the typed calculus of H-pretoposes is to have noticed that a monomorphism turns out to be the interpretation of a type with at most one proof, also called proofirrelevant in the literature, but here called mono type. Therefore, the novelty of this calculus lies in the presence of the forall type, that is the product type restricted to mono types, and also in the presence of the quotient types based only on mono equivalence relations such that the effectiveness holds. Here, we describe in details the forall type, the quotient type and the natural numbers type and we refer to [Mai97] and [Hof94] for details on the other types. Note that we define the fibred functors only on objects of the various slice categories P/A, since on morphisms they turn out to be defined by

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

the universal property of pullback. Moreover, they turn out to be fibred by stability or Beck-Chevalley conditions of the categorical property involved.

The F orall type corresponds to the right adjoint of pullback functor on subobjects:

∀) \frac{γ(y)[Γ_{n}, y ∈ β] d ∈ Eq(γ, w, z)[Γ_{n}, y ∈ β, w ∈ γ(y), z ∈ γ(y)]}{∀_{y∈β}γ(y) [Γ_{n}]}

is  [figure: C; γ; B; β; A_{n} …; ∀_{β}C; ∀_{β}γ; A_{n} …]

where ∀_{β}γ : P/A_{n} → P^{→} is the functor defined in the following manner: for every t : D → A_{n}, we put ∀_{β}γ(t) ≡ ∀_{β(t)}γ(q(t, β(id))). Note that γ(id) turns out to be a monomorphism, because the interpretation of z ∈ γ[Γ_{n}, y ∈ β, w ∈ γ(y), z ∈ γ(y)] and w ∈ γ[Γ_{n}, y ∈ β, w ∈ γ(y), z ∈ γ(y)], which are isomorphic with the same isomorphism respectively to the first and second projections of the product γ(id) × γ(id), are equal by hypothesis and by the validity of the extensional elimination rule for the equality type.

I-∀) \frac{c ∈ γ(y)[Γ_{n}, y ∈ β]}{λy.c ∈ ∀_{y∈β}γ(y)[Γ_{n}]} is [figure: B; c; C; A_{n}; (λy.c); ∀_{y∈β}C]

E-∀) \frac{b ∈ β[Γ_{n}] f ∈ ∀_{y∈β}γ(y)[Γ_{n}, y ∈ β]}{Ap(f, b) ∈ γ(b)[Γ_{n}]} is [figure: A_{n}; b; B; A_{n}; f; ∀_{β}C; A_{n}; Ap(f,b); A_{n} × C]

with (λy.c)(id) ≡ ψ(c(id)) and Ap(f, b)(id) ≡ b(id)^{∗}(ψ^{−1}(f(id))), where

ψ : Sub(B)(β(id)^{∗}(id_{A_{n}}), γ(id)) → Sub(A_{n})(id_{A_{n}}, ∀_{β(id)}(γ(id)))

is the bijection of the adjunction β(id)^{∗} ⊣ ∀_{β}, by putting β(id)^{∗}(t) ≡ q(t, β(id)) for every t : B → A_{n}, that is we are considering the choice of pullback given by the split fibration. The conversion rules, that are the usual β and η conversion rules as in the extensional version of Martin-Löf’s type theory [Mar84], are also valid.

The Quotient type corresponds to the effective quotients of equivalence relations (in the premisses we omit to add the generic context Γ_{n}):

Q) \frac{\begin{matrix}ρ(x, y) type [x ∈ α, y ∈ α], & d ∈ Eq(ρ, z, w)[x ∈ α, y ∈ α, z ∈ ρ, w ∈ ρ], \\ c_{1} ∈ ρ(x, x)[x ∈ α], & c_{2} ∈ ρ(y, x)[x ∈ α, y ∈ α, z ∈ ρ(x, y)], \\ c_{3} ∈ ρ(x, z)[x ∈ α, y ∈ α, z ∈ α, w ∈ ρ(x, y), w′ ∈ ρ(y, z)] \end{matrix}}{α/ρ [Γ_{n}]}

corresponds to

[figure: R; ρ(id); A × A; α(id)·π_{1}; A_{n} …; A/R; Q(α)(id); A_{n} …]

where π_{1} ≡ α(α(id)), π_{2} ≡ q(α(id), α(id)) and Q(α)(id) is defined as follows. In the case of the forall type, we have already noticed that a mono type corresponds to a monomorphism. Here, we can prove that ρ(id) turns out to be also an equivalence relation in P/A_{n}. Therefore, there exists the coequalizer c : A → A/R of π_{1} · ρ(id) and π_{2} · ρ(id). Moreover, as α(id) · (π_{1} · ρ(id)) = α(id) · (π_{2} · ρ(id)), we get Q(α(id)) such that the following triangle diagram commutes

[figure: R; π_{2}·ρ(id); π_{1}·ρ(id); A; c; α(id); A/R; Q(α(id)); A_{n}]

Therefore we define Q(α) : P/A_{n} → P^{→} in the following manner: for every t : D → A_{n} we put Q(α)(t) ≡ Q(α(t)), where Q(α(t)) is the unique morphism such that α(t) = Q(α(t)) · c(t) and c(t) is the coequalizer of the equivalence relation ρ(t). The introduction rule for the quotient type is the next one:

I-Q) \frac{a ∈ α [Γ_{n}]}{[a] ∈ α/ρ [Γ_{n}]} is  [figure: A_{n}; a(id); A; A_{n}; c·(a(id)); A/R]

and the following equality rule is valid

eq) \frac{a ∈ α[Γ_{n}] b ∈ α[Γ_{n}] d ∈ ρ(a, b)[Γ_{n}]}{[a] = [b] ∈ α/ρ [Γ_{n}]}

By using the indexed sum type, the elimination and conversion rules of the quotient type for dependent types (see the appendix) are equivalent to the following weaker elimination and conversion rules of the quotient type for types not depending on α or α/ρ, which are also derivable in T (P)

E_{s}-Q) \frac{m(x) ∈ μ [x ∈ α] m(x) = m(y) ∈ μ [x ∈ α, y ∈ α, d ∈ ρ(x, y)]}{Q_{s}(m, z) ∈ μ [z ∈ α/ρ]}

C_{1s}-Q) \frac{a ∈ α m(x) ∈ μ [x ∈ α] m(x) = m(y) ∈ μ [x ∈ α, y ∈ α, d ∈ ρ(x, y)]}{Q_{s}(m, [a]) = m(a) ∈ μ}

C_{2s}-Q) \frac{t(z) ∈ μ [z ∈ A/R]}{Q_{s}((x)t([x]), z) = t(z) ∈ μ [z ∈ α/ρ]}

where [figure: M; μ(id); A_{n}] and [figure: A; α(id); A_{n}] . In the weaker elimination rule E_{s}-Q

Q_{s}(m, z) ∈ μ [Γ_{n}, z ∈ α/ρ] is [figure: A/R; ⟨id,u⟩; A/R×M]

where u is the morphism in P/A_{n} such that u · c = q(α(id), μ(id)) · m(id), which exists because by hypothesis m(id)·(π_{1}·ρ(id)) = m(id)·(π_{2}·ρ(id)), and c is the coequalizer of π_{1} · ρ(id) and π_{2} · ρ(id). Moreover, since by hypothesis μ(id)·(q(α(id), μ(id))·m(id)) = α(id) we also have that by uniqueness μ(id)· u = Q(α(id)). The C_{1s} and C_{2s} conversion rules are valid. Besides, the axiom of Effectiveness also holds:

\frac{a ∈ α b ∈ α [a] = [b] ∈ α/ρ}{f(a, b) ∈ ρ(a, b)} is  [figure: A_{n}; a(id); A; A_{n}; b(id); A; A_{n}; ⟨id,t⟩; R]

where ⟨id, t⟩ is defined as follows. Since by hypothesis c · a(id) = c · b(id) and since the quotient is effective in P/A_{n}, then there exists a morphism t : A_{n} → R such that (π_{1} · ρ(id)) · t = a(id) and (π_{2} · ρ(id)) · t = b(id).

The Natural Numbers type corresponds to the natural numbers object:

nat) N[ ] is [figure: N_{Σ}; _{N}(id); 1]

where N̂ : P/1 → P^{→} is the functor defined in the following manner: for every !_{D} : D → 1 we put N̂(!_{D}) ≡ (!_{D})^{∗}(!_{N}) and N is a natural numbers object of P.

Now, we show the introduction rules.

I_{1}-nat) 0 ∈ N[Γ_{n}]  is  [figure: A_{n}; ⟨id,o·!_{An} ⟩; A_{n}×N]

where o : 1 → N is the zero map in the H-pretopos P. From now on, we call π_{1} ≡ N̂(!_{A_{n}}) and π_{2} ≡ q(!_{A_{n}}, N̂(id)).

I_{2}-nat) s(n) ∈ N[Γ_{n}, n ∈ N]  is  [figure: A_{n}×N; ⟨id,s̄·π_{2}⟩; A_{n}×N ×N]

where s : N → N is the successor map in the H-pretopos P, s̄ ≡ id_{1}^{∗}(s) and ⟨id, s̄ · π_{2}⟩ is the unique morphism towards the pullback of !_{A_{n}×N} and N̂(!_{1}). By using the indexed sum type, the elimination and conversion rules of the natural numbers type for dependent types, as in the extensional version of Martin-Löf’s type theory [NPS90], are equivalent to the following weaker elimination and conversion rules of the natural numbers type for types not depending on N, which are also derivable in T (P)

E_{s}-nat) \frac{a ∈ L l(y) ∈ L [y ∈ L]}{Rec_{s}(a, l, n) ∈ L [n ∈ N]}

C_{1}-nat) \frac{a ∈ L l(y) ∈ L [y ∈ L]}{Rec_{s}(a, l, 0) = a ∈ L}

C_{2}-nat) \frac{a ∈ L l(y) ∈ L [y ∈ L]}{Rec_{s}(a, l, s(n)) = l(Rec_{s}(a, l, n)) ∈ L [n ∈ N]}

C_{3}-nat) \frac{\begin{matrix}a ∈ L & l(y) ∈ L [y ∈ L] & f(n) ∈ L [n ∈ N] \\ f(0) = a ∈ L & f(s(n)) = l(f(n)) ∈ L \end{matrix}}{Rec_{s}(a, l, n) = f(n) ∈ L [n ∈ N]}

In the weaker elimination rule E_{s}-nat

Rec_{s}(a, l, n) is [figure: A_{n}×N; ⟨id,r⟩; (A_{n}×N)×L]

where r is the unique morphism that makes the diagram below commute, by the property of natural numbers object in P/A_{n} with π_{2}^{L} ≡ q(ξ(id), ξ(id))

[figure: A_{n}; ⟨id,0⟩; a(id); A_{n} × N; ⟨π_{1},s̄·π_{2}⟩; r; A_{n} × N; r; L; π_{2}^{L}·l(id); L]

The conversion rules for the natural numbers type are also valid.

3 The relation between the type theories and the H-pretoposes

There is a sort of equivalence between the type theories described in the previous section and the category of H-pretoposes. So we can state that the type theory T (P) is the internal language of the H-pretopos P. First of all, we define the following categories:

1. Lang whose objects are the type theories of H-pretoposes and whose morphisms are translations: they send types to types so as to preserve the type and term constructors, closed terms to closed terms and variables to variables; we call Lang^{∗} the category whose objects are those of Lang, but whose morphisms are translations preserving type and term constructors up to isomorphisms;

2. HP retop_{o} whose objects are H-pretoposes with a fixed choice of Hpretopos structure and whose morphisms are strict logical functors, that is functors preserving the H-pretopos structure w.r.t. the fixed choices; we call HP retop the category whose objects are those of HP retop_{o}, but whose morphisms are functors preserving the H-pretopos structure up to isomorphisms.

Now, we define a functor from H-pretoposes to type theories

T : HP retop_{o} ⟶ Lang

that associates to every H-pretopos P the internal type theory T (P) described in the previous section. The functor T associates to every morphism F : P → D of HP retop_{o} the translation T (F) : T (P) → T (D) defined as follows. Given a fibred functor σ : P/A → P^{→}, corresponding to a type judgement, and a natural transformation c, corresponding to a term judgement, we define T (F)(σ) and T (F)(c) by induction on the signature of T (P). Indeed, if σ = b̂ for any b : B → A of P, then we put F (σ) = F̂ (b), since the chosen pullbacks of P are sent into the chosen pullbacks of D by F. If σ is obtained by an inference rule, 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 H-pretopos structure w.r.t. the fixed choices used in the internal type theories of P and D.

Moreover, we define a functor from type theories to H-pretoposes

P : Lang ⟶ HP retop_{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 a H-pretopos by fixing a choice of its structure^{3} (see [Mai97]). The functor P associates to every morphism of Lang 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 H-pretopos structure. In order to describe the relation between type theories and Hpretoposes, we have to consider a type theory T as a category. We think of T as the category whose objects are the same as 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^{4}

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 with ID the identity functor.

3 For the choices of finite limits and right adjoints see [See84], for coproducts use

disjoint sum types and for quotients use quotient types with indexed sum types. 4 One could also consider the usual morphisms of contexts.

Proposition 5. Let T : HP retop_{o} → Lang and P : Lang → HP retop_{o} be the functors defined above. There are two natural transformations: η from ID to T · P, thought as functors from Lang to Lang^{∗}, and ϵ from P · T to ID, thought as functors from HP retop_{o} to HP retop, such that for every type theory T and for every H-pretopos P, η_{T} : T → T (P (T )) and ϵ_{P} : P (T (P)) → P 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_{Σ}; _{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)}C(x)_{Σ}; q_{3}(id); 1; A_{Σ}; _{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 the previous section. 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 and it is an equivalence of categories since the functor is faithfull, full and essentially surjective. Indeed, we can define a natural transformation η^{−1} such that, given a type theory T , the 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 Hpretopos P the component

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

is defined as follows. ϵ_{P} associates to every object [figure: A; σ(id); 1] of P (T (P)) 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 ϵ_{P} is a functor preserving the H-pretopos structure up to isomorphisms^{5}. We have that ϵ_{P} gives rise to a natural transformation, since the functors preserve the H-pretopos structure w.r.t. the fixed choices. Moreover, ϵ_{P} is an equivalence of categories, since it is faithfull 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 H-pretopos P the component ϵ_{P}^{−1} : P → P (T (P)) is defined as follows.

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

to [figure: A_{Σ}; \overline{⟨id,b′⟩}(id); id; A_{Σ}×B_{Σ}; _{B}(!_{A_{Σ}}); 1; A_{Σ}; _{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 H-pretopos P, ϵ_{P} and ϵ_{P}^{−1} give rise to an equivalence of categories.

5 This is due to the choices of split fibration: see, for instance, the terminal object.

4 The free H-pretopos

The main idea is to generate a H-pretopos 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.

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 typed calculus for H-pretoposes as in the appendix.

Therefore T (C) is a type theory of H-pretoposes.

Now, we can prove:

Proposition 6. Let P : Lang ⟶ HP retop_{o} be the functor described in section 3. The category P (T (C)) is the free H-pretopos generated by the category C.

Proof. We know that P (T (C)) is a H-pretopos from the definition of P. Given a functor G : C → P, from the category C to the H-pretopos P, we claim that there exists a unique functor G̃ : P (T (C)) → P in HP retop_{o} such that

the diagram [figure: C; I; G; P (T (C)); G̃; P] 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(P), by passing to P gf(P), with the warning that we have to normalize the evaluation. This is done by adding the value of every fibred functor σ ∈ F ib(P/1, P^{→}) on the empty, by induction on the signature, such that a type judgement will be interpreted by a sequence of P gr(P) like

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

The interpretation is the same as for the internal type theory, 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 2, then G̃ would commute with G up to isomorphisms. So, for every object A of ObP, 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 natural numbers J (N[ ]) ≡ N̂(∅) =!_{N}, instead of being interpreted as !_{1×N} like in the semantics defined in section

2. Moreover, J (0 ∈ N[ ]) is [figure: 1; _{o}(∅); id_{1}; N; _{N}(∅); 1] where ô(∅) ≡ o and o : 1 → N

is the zero map in P. Finally, given a proper type arising from an object A ∈ ObC, we put J (A[ ]) ≡ Ĝ(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 Ĝ(B)(Ĝ(A)(∅)) : G(A) × G(B) → G(A). By definition G̃ preserves the H-pretopos structure and we get G̃ · I = G. Moreover, G̃ is obviously unique for fixed choices of the H-pretopos structure, which are required to interpret the type theory T (C) into P gr(P).

The free structure gives rise to a monad. It would be interesting to investigate if the category HP retop_{o} is monadic on Cat and Graph. Or at least, if we prove that HP retop_{o} is essentially algebraic, as for the categorical models of IT T in[Obt89], we would get a representation theorem of HP retop_{o} into a category of presheaves [AR94].

5 Some other free structures: the Lex and IT T categories

A similar correspondence to that one between type theories and H-pretoposes can be established for the category Lex and IT T. The category Lex, whose objects are the categories with finite limits and whose morphisms are functors strictly preserving finite limits, provides a valid and complete semantics for the typed calculus with terminal type, extensional equality types and indexed sum types. In the same way, the IT T category, whose objects are the locally cartesian closed categories with finite coproducts and a natural numbers object and whose morphisms are functors strictly preserving the IT T structure, provides a valid and complete semantics for the fragment of Martin-Löf’s type theory with extensional equality and without universes and well-orders [Mar84]. These validity and completeness theorems can be proved in a similar way to that for H-pretoposes. We can easily notice that these dependent typed calculi allow us to build the free structure for Lex and IT T over Cat, in the same way we proved for the category HP retop_{o}. The free structures give a presentation of two monads, whose algebras correspond respectively to Lex and IT T, since Lex and IT T are monadic over Graph [Bur81] and admit an equational presentation.

Acknowledgements. I would like to thank Pino Rosolini and Silvio Valentini for helpful discussions, and Ieke Moerdijk for making my visit at Utrecht extremely useful. Finally, I want to thank the referees for their comments on the preliminary version of this paper.

6 Appendix: the HP typed 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)]}{s(d, m) ∈ M(d)}

C-Σ) \frac{b ∈ B c ∈ C(b) m(x, y) ∈ M(⟨x, y⟩) [x ∈ B, y ∈ C(x)]}{s(⟨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 = d ∈ C}{eq_{C} ∈ Eq(C, c, d)}

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 D type}{C ⊕ D type}  I_{1}-⊕) \frac{c ∈ C}{ϵ_{1}(c) ∈ C ⊕ D}  I_{2}-⊕) \frac{d ∈ D}{ϵ_{2}(d) ∈ C ⊕ D}

E-⊕) \frac{w ∈ C ⊕ D a_{C}(x) ∈ A(ϵ_{1}(x))[x ∈ C] a_{D}(y) ∈ A(ϵ_{2}(y))[y ∈ D]}{D(w, a_{C}, a_{D}) ∈ A(w)}

C_{1}-⊕) \frac{c ∈ C a_{C}(x) ∈ A(ϵ_{1}(x))[x ∈ C] a_{D}(y) ∈ A(ϵ_{2}(y))[y ∈ D]}{D(ϵ_{1}(c), a_{C}, a_{D}) = a_{C}(c) ∈ A(ϵ_{1}(c))}

C_{2}-⊕) \frac{d ∈ D a_{C}(x) ∈ A(ϵ_{1}(x))[x ∈ C] a_{D}(y) ∈ A(ϵ_{2}(y))[y ∈ D]}{D(ϵ_{2}(d), a_{C}, a_{D}) = a_{D}(d) ∈ A(ϵ_{2}(d))}

Disjointness

\frac{c ∈ C d ∈ D ϵ_{1}(c) = ϵ_{2}(d) ∈ C ⊕ D}{m(c, d) ∈ ⊥}

Forall type

∀) \frac{C(x) type[x ∈ B] d ∈ Eq(C(x), y, z)[x ∈ B, y ∈ C(x), z ∈ C(x)]}{∀_{x∈B}C(x) type}

I-∀) \frac{c ∈ C(x)[x ∈ B] d ∈ Eq(C(x), y, z)[x ∈ B, y ∈ C(x), z ∈ C(x)]}{λx^{B}.c ∈ ∀_{x∈B}C(x)}

E-∀) \frac{b ∈ B f ∈ ∀_{x∈B}C(x)}{Ap(f, b) ∈ C(b)}

βC-∀) \frac{b ∈ B c ∈ C(x)[x ∈ B] d ∈ Eq(C(x), y, z)[x ∈ B, y ∈ C(x), z ∈ C(x)]}{Ap(λx^{B}.c, b) = c(b) ∈ C(b)}

ηC-∀) \frac{f ∈ ∀_{x∈B}C(x)}{λx^{B}.Ap(f, x) = f ∈ ∀_{x∈B}C(x)}

Quotient type

Q) \frac{\begin{matrix}R(x, y) type [x ∈ A, y ∈ A], & d ∈ Eq(R(x, y), z, w)[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] ∈ A/R} eq-Q) \frac{a ∈ A b ∈ A d ∈ R(a, b)}{[a] = [b] ∈ A/R}

E-Q) \frac{s ∈ A/R l(x) ∈ L([x])[x ∈ A] l(x) = l(y) ∈ L([x])[x ∈ A, y ∈ A, d ∈ R(x, y)]}{Q(l, s) ∈ L(s)}

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

Natural Numbers type

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

E-nat) \frac{n ∈ N a ∈ L(0) l(x, y) ∈ L(s(x))[x ∈ N, y ∈ L(x)]}{Rec(a, l, n) ∈ L(n)}

C_{1}-nat) \frac{a ∈ L(0) l(x, y) ∈ L(s(x))[x ∈ N, y ∈ L(x)]}{Rec(a, l, 0) = a ∈ L(0)}

C_{2}-nat) \frac{n ∈ N a ∈ L(0) l(x, y) ∈ L(s(x))[x ∈ N, y ∈ L(x)]}{Rec(a, l, s(n)) = l(n, Rec(a, l, n)) ∈ L(s(n))}

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.

[Bur81] A. Burroni. Algebres graphiques. Cahiers de topologie et geometrie differentielle, 12:249–265, 1981.

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

[Con86] R. Constable et al. Implementing mathematics with the Nuprl Development System. Prentice Hall, 1986.

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

[DK83] E.J. Dubuc and G. M. Kelly. A presentation of topoi as algebraic relative to categories and graphs. Journal of Algebra, 81:420–433, 1983.

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

[Hof95] M. Hofmann. Extensional concept in intensional type theory. PhD thesis, University of Edinburgh, July 1995.

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

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

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

[Mai97] M.E. Maietti. The typed theory of Heyting Pretopoi. Preprint-University of Padova, January 1997.

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

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

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

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

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

[MR77], [MR77], [See84], [Hof94] ,[Hof95], [Jac91] [DK83] [Con86]