arXiv subjects
Publications and source records attributed to Benno van den Berg.
We define a notion of weak omega-category internal to a model of Martin-Löf type theory, and prove that each type bears a canonical weak omega-category structure obtained from the tower of iterated identity types over that type. We show that the omega-categories arising in this way are in fact omega-groupoids.
This is the second in a series of papers on the relation between algebraic set theory and predicative formal systems. In part I, we introduced the notion of a predicative category of small maps and obtained the result that such categories always contain a model of set theory. In the present paper, we show that the familiar realizability models of the constructive set theories CZF and IZF can be obtained as an application of this result. For this purpose, we show that predicative categories with small maps are closed under an internal notion of realizability.
The paper provides an introduction to the field of Algebraic Set Theory (AST). AST is a flexible categorical framework for studying different kinds of set theories: both classical and constructive, predicative and impredicative. We discuss the basic results in this area, with a particular emphasis on applications to the constructive set theories IZF and CZF. (This paper is a summary of a tutorial on categorical logic given by the second named author at the Logic Colloquium 2006 in Nijmegen.)
This is the first in a series of three papers on Algebraic Set Theory. Its main purpose is to lay the necessary groundwork for the next two parts, one on Realisability and the other on Sheaf Models in Algebraic Set Theory.
The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on categories with finite limits and colimits. As an instance of this result, we build the final coalgebra for the powerclass functor, in the context of a Heyting pretopos with a class of small maps. This is then proved to provide a model for various non-well-founded set theories, depending on the chosen axiomatisation for the class of small maps.
In this paper, we identify some categorical structures in which one can model predicative formal systems: in other words, predicative analogues of the notion of a topos, with the aim of using sheaf models to interprete predicative formal systems. Among our technical results, we prove that all the notions of a ``predicative topos'' that we consider, are stable under presheaves, while most are stable under sheaves.
Non-well-founded trees are used in mathematics and computer science, for modelling non-well-founded sets, as well as non-terminating processes or infinite data-structures. Categorically, they arise as final coalgebras for polynomial endofunctors, which we call M-types. In order to reason about trees, we need the notion of path, which can be formalised in the internal logic of any locally cartesian closed pretopos with a natural number object. In such categories, we derive existence results about M-types, leading to stability of locally cartesian closed pretoposes with a natural number object and M-types under slicing, formation of coalgebras (for a cartesian comonad), and sheaves for an internal site.