Abstract A model of Martin-Löf extensional type theory with universes is formalized in Agda, an interactive proof system based on Martin-Löf intensional type theory. This may be understood, we claim, as a solution to the old problem of modeling the full extensional theory in the intensional theory. Types are interpreted as setoids, and the model is therefore a setoid model.We solve the problem of interpreting type universes by utilizing Aczel’s type of iterative sets and show how it can be made into a setoid of small setoids containing the necessary setoid constructions. In addition, we interpret the bracket types of Awodey and Bauer. Further quotient types should be interpretable.

Abstract In the present paper we use the theory of exact completions to study categorical properties of small setoids in Martin-Löf type theory and, more generally, of models of the Constructive Elementary Theory of the Category of Sets, in terms of properties of their subcategories of choice objects (i.e., objects satisfying the axiom of choice). Because of these intended applications, we deal with categories that lack equalisers and just have weak ones, but whose objects can be regarded as collections of global elements. In this context, we study the internal logic of the categories involved, and employ this analysis to give a sufficient condition for the local cartesian closure of an exact completion. Finally, we apply this result to show when an exact completion produces a model of CETCS.

We give an overview of the main ideas involved in the development of homotopy type theory and the univalent foundations of Mathematics programme. This serves as a background for the research papers published in the special issue.

A modified realisability interpretation of infinitary logic is formalised and proved sound in constructive type theory (CTT). The logic considered subsumes first order logic. The interpretation makes it possible to extract programs with simplified types and to incorporate and reason about them in CTT.

In this paper we interpret (fragments of) intuitionistic logic in categories with weak closure properties, such as quasi left exact categories and locally cartesian closed categories (LCCC) with sums. We also interpret the full choice scheme in an LCCC. The interpretation can be seen as a categorical form of the usual Brouwer–Heyting– Kolmogorov (BHK) interpretation. The standard interpretation of geometric logic in a pretopos is obtained by applying the image functor to the BHK-interpretation.

The notion of a hyperfinite set comes from nonstandard analysis. Such a set has the internal cardinality of a nonstandard natural number. By a transfer principle such sets share many properties of finite sets. Here we apply this notion to give a hyperfinite model of the Kleene-Kreisel continuous functionals. We also extend the method to provide a hyperfinite characterisation of certain transfinite type structures, thus, through the work of Waagbø [14], constructing a hyperfinite model for Martin-Löf type theory. This kind of application is not new. Normann [6] gave a characterisation of the Kleene-Kreisel continuous functionals using ‘hyperfinitary’ functionals. The novelty here is that we use a constructive version of hyperfinite functionals and also generalise the method to transfinite types. Many of the results of this paper are constructive, though not the characterisation theorems themselves. Our characterisation of the Kleene-Kreisel continuous functionals is a supplement to a number of previous characterisations of topological and recursion-theoretical nature, see [6] for a brief survey. Altogether these characterisations show that the original concept of Kleene and Kreisel forms the correct mathematical model of the idea of finitely based functions of finite types. There is, however, no a priori reason to believe that there is a canonical way to extend the continuous functionals to cover transfinite objects of transfinite type used in, e.g., type theory. Our characterisation of Waagbø's model indicates that the model is natural, not only seen from domain theory but from a higher perspective. Normann and Waagbø (unpublished) have subsequently obtained a limit-space characterisation that further supports this view.

In this paper, we give a constructive nonstandard model of intuitionistic arithmetic (Heyting arithmetic). We present two axiomatisations of the model: one finitary and one infinitary variant. Using the model these axiomatisations are proven to be conservative over ordinary intuitionistic arithmetic. The definition of the model along with the proofs of its properties may be carried out within a constructive and predicative metatheory (such as Martin-Löf's type theory). This paper gives an illustration of the use of sheaf semantics to obtain effective proof-theoretic results. The axiomatisations of nonstandard intuitionistic arithmetic (to be calledHAIandHAIωrespectively) as well as their model are based on the construction in [5] of a sheaf model for arithmetic using a site of filters. In this paper we present a “minimal” version of this model, built instead on a suitable site of provable filter bases. The construction of this site can be viewed as an extension of the well-known construction of the classifying topos for a geometric theory which uses “syntactic sites”. (Such sites can in fact be used to prove semantical completeness of first order logic in a strictly constructive framework, see [6].) We should mention that for classical nonstandard arithmetics there are several nonconstructive methods of proving conservativity over arithmetic, e.g. the compactness theorem, Mac Dowell–Specker's theorem [3].

The Kleene-Kreisel continuous functionals [6, 7] have been given several alternative characterisations: using Kuratowski's limit spaces (Scarpellini [20]), using their generalisation, filter spaces (Hyland [4]), via hyperfinite functionals (Normann [11]) and perhaps most elegantly using Scott-Ershov domains (Ershov [3], later generalised by Berger [1]). We propose to add yet another characterisation to this list, which may be called model-theoretic in contrast to the others, but which is in fact closely related to Ershov's approach. We use the notion of logically presented domains developed in Palmgren and Stoltenberg-Hansen [17] (originating in the work of [15]). Certain logical types, i.e., finitely consistent sets of formulas, over the full type structure built from ℕ correspond to the continuous functionals in the sense of Kreisel, or to Kleene's associates, while the elements realising the types correspond to functionals having associates (cf. [6]). To define these—the total types—we make a nonstandard extension of the full type structure. The set of nonstandard elements is sufficiently rich to single out the total types. The nonstandard extension also makes it possible to relate the logical presentation to Ershov's approach. The logical form of the domain constructions allows us to use a (generalised) Fréchet power as a nonstandard extension. This extension is constructive, in the sense that it avoids the axiom of choice, as distinguished from the one employed in [11].

We connect the theory of Scott-Ershov domains to first order model theory. The completeness property of domains is related to the model theoretic notion of saturation. In constraint programming this analogy is already used on the level of finite approximations. A simple relation to structures used in nonstandard analysis (ultra powers, Frechet powers) is obtained. This leads to natural logical presentations of domain constructions such as function space, products and the Smyth power domain. Sufficient conditions on models for constructing function spaces are given.

In the paper Mathematics of infinity, Martin-Löf extends his intuitionistic type theory with fixed “choice sequences”. The simplest, and most important instance, is given by adding the axioms to the type of natural numbers. Martin-Löf's type theory can be regarded as an extension of Heyting arithmetic (HA). In this note we state and prove Martin-Löf's main result for this choice sequence, in the simpler setting of HA and other arithmetical theories based on intuitionistic logic (Theorem A). We also record some remarkable properties of the resulting systems; in general, these lack the disjunction property and may or may not have the explicit definability property. Moreover, they represent all recursive functions by terms.

In this note we construct Martin-Löf's inconsistent type theory, Type: Type (Martin-Löf [1971]), inside partial type theory with one universe. Thus adding a fixed point operator to type theory with one predicative universe gives impredicativity. We may describe the theory Type:Type as follows. It contains the rules for the product construction (II) of Martin-Löf [1984] except the η-rule and it contains the usual rules for definitional equality (=). Moreover it contains the following strongly impredicative universe This theory is inconsistent (i.e. every set is inhabited), and this is seen by proving a variant of the Burali—Forti paradox—Girard's paradox—cf. Troelstra and van Dalen [1988]. Coquand [199?] has shown that by adding the well-order type and the strong dependent sum to the universe, the fixed point operator becomes definable. It is an open problem whether it is definable without the well-order type. The present result could be seen as a converse, namely by adding the fixed point operator to type theory with one universe, Type:Type becomes definable and, as is already known, so does the well-order type.