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.

First-order logic with dependent sorts, such as Makkai's first-order logic with dependent sorts (FOLDS), or Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL), may be regarded as logic enriched dependent type theories. Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Löf type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and DFOL fit in this semantical framework. A soundness and completeness theorem is proved for DFOL. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

In this article we examine the natural interpretation of a ramified type hierarchy into Martin-Lof type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell's reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematical analysis in the style of Bishop. We present a ramified type theory suitable for this purpose. One may regard the results of this article as an alternative solution to the problem of the proliferation of levels of real numbers in Russell's theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here also suggests that there is a natural associated notion of predicative elementary topos.

In this note we remark on the problem of equality of objects in categories formalized in Martin-Löf’s constructive type theory. A standard notion of category in this system is E-category, where no such equality is specified. The main observation here is that there is no general extension of E-categories to categories with equality on objects, unless the principle Uniqueness of Identity Proofs (UIP) holds. We also introduce the notion of an H-category with equality on objects, which makes it easy to compare to the notion of univalent category proposed for Univalent Type Theory by Ahrens, Kapulkin and Shulman.

When formalizing mathematics in constructive type theories, or more practically in proof assistants such as Coq or Agda, one is often using setoids (types with explicit equivalence relations). In this note we consider two categories of setoids with equality on objects and show, within intensional Martin-Lof type theory, that they are isomorphic. Both categories are constructed from a fixed proof-irrelevant family F of setoids. The objects of the categories form the index setoid I of the family, whereas the definition of arrows differs. The first category has for arrows triples where f is an extensional function. Two such arrows are identified if appropriate composition with transportation maps (given by F) makes them equal. In the second category the arrows are triples where R is a total functional relation between the subobjects of the setoid sum of the family. This category is simpler to use as the transportation maps disappear. Moreover we also show that the full image of a category along an E-functor into an E-category is a category.

We present a Brouwerian example showing that the classical statement 'Every Lipschitz mapping f : [0; 1] -> [0; 1] has rectifiable graph' is essentially nonconstructive. We turn this Brouwerian example into an explicit recursive example of a Lipschitz function on [0; 1] that is not rectifiable. Then we deal with the connections, if any, between the properties of rectifiability and having a variation. We show that the former property implies the latter, but the statement 'Every continuous, real-valued function on [0; 1] that has a variation is rectifiable' is essentially nonconstructive.

Categories with families (cwfs) is an established semantical structure for dependent type theories, such as Martin-Lö type theory. Makkai's first-order logic with dependent sorts (FOLDS) is an example of a so-called logic enriched type theory. We introduce in this article a notion of hyperdoctrine over a cwf, and show how FOLDS and Aczel's and Belo's dependently typed (intuitionistic) first-order logic (DFOL) fit in this semantical framework. A soundness and completeness theorem is proved for such a logic. The semantics is functorial in the sense of Lawvere, and uses a dependent version of the Lindenbaum-Tarski algebra for a DFOL theory. Agreement with standard first-order semantics is established. Some applications of DFOL to constructive mathematics and categorical foundations are given. A key feature is a local propositions-as-types principle.

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.

In this paper we consider the problem of building rich categories of setoids, in standard intensional Martin-Lo ̈f type theory (MLTT), and in particular how to handle the problem of equality on objects in this context. Any (proof-irrelevant) family F of setoids over a setoid A gives rise to a category C(A,F) of setoids with objects A. We may regard the family F as a setoid of setoids, and a crucial issue in this article is to construct rich or large enough such families. Depending on closure conditions of F , the category C(A, F ) has corresponding categorical constructions. We exemplify this with finite limits. A very large family F may be obtained from Aczel’s model construction of CZF in type theory. It is proved that the category so obtained is isomorphic to the internal category of sets in this model. Set theory can thus establish (categorical) properties of C(A,F) which may be used in type theory. We also show that Aczel’s model construction may be extended to include the elements of any setoid as atoms or urelements. As a byproduct we obtain a natural extension of CZF, adding atoms. This extension, CZFU, is validated by the extended model. The main theorems of the paper have been checked in the proof assistant Coq which is based on MLTT. A possible application of this development is to integrate set-theoretic and type-theoretic reasoning in proof assistants.