arXiv subjects
Publications and source records attributed to Benno van den Berg.
We show how a standard constructive notion of ordinal supports a useful constructive theory of transfinite recursion. We do this by giving constructive proofs of various initial algebra theorems, like Adamek's theorem, and a version of Quillen's small object argument for constructing cofibrantly generated algebraic weak factorisation systems.
To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.
Bourke and Garner described how to cofibrantly generate algebraic weak factorisation systems by a small double category of morphisms. However they did not give an explicit construction of the resulting factorisations as in the classical small object argument. In this paper we give such an explicit construction, as the colimit of a chain, which makes the result applicable in constructive settings; in particular, our methods provide a constructive proof that the effective Kan fibrations introduced by Van den Berg and Faber appear as the right class of an algebraic weak factorisation system.
In this paper we introduce arrow algebras, simple algebraic structures which induce elementary toposes through the tripos-to-topos construction. This includes localic toposes as well as various realizability toposes, in particular, those realizability toposes which are obtained from partial combinatory algebras. Since there are many examples of arrow algebras and arrow algebras have a number of closure properties, including a notion of subalgebra given by a nucleus, arrow algebras provide a flexible tool for constructing toposes; we illustrate this by providing some general tools for creating toposes for Kreisel's modified realizability.
We will show make two contributions to the theory of effective Kan fibrations, which are a more explicit version of the notion of a Kan fibration, a notion which plays a fundamental role in simplicial homotopy theory. We will show that simplicial Malcev algebras are effective Kan complexes and that the effective Kan fibrations can be seen as the right class in an algebraic weak factorisation system. In addition, we will introduce two strengthenings of the notion of an effective Kan fibration, the symmetric effective and degenerate-preferring Kan fibrations, and show that the previous results holds for these strengthenings as well.
If a locally cartesian closed category carries a weak factorisation system, then the left maps are stable under pullback along right maps if and only if the right maps are closed under pushforward along right maps. We refer to this statement as the Frobenius equivalence and in this paper we state and prove an analogical statement for algebraic weak factorisation systems. These algebraic weak factorisation systems are an explicit variant of the more traditional weak factorisation systems in that the factorisation and the lifts are part of the structure of an algebraic weak factorisation system and are not merely required to exist. Our work has been motivated by the categorical semantics of type theory, where the Frobenius equivalence provides a useful tool for constructing dependent function types. We illustrate our ideas using split fibrations of groupoids, which are the backbone of the groupoid model of Hofmann and Streicher.
We introduce a new version of arithmetic in all finite types which extends the usual versions with primitive notions of extensionality and extensional equality. This new hybrid version allows us to formulate a strong form of extensionality, which we call converse extensionality. Inspired by Brouwer's notion of apartness, we show that converse extensionality can be eliminated in a way which improves on results from our previous work. We also explain how standard proof-theoretic interpretations, like realizability and functional interpretations, can be extended to such hybrid systems, and how that might be relevant to proof-mining.
We investigate how much type theory is able to prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservative over Heyting Arithmetic (HA). We build on this result by showing that type theories with one level of universes are conservative over Higher-order Heyting Arithmetic (HAH). Although this clearly depends on the specific type theory, we show that the interpretation of logic also plays a major role. For proof-irrelevant interpretations, we will see that strong versions of type theory prove exactly the same higher-order arithmetical formulas as HAH. Conversely, proof-relevant interpretations prove strictly more second-order arithmetical formulas than HAH, however they still prove exactly the same first-order arithmetical formulas. Along the way, we investigate the different interpretations of logic in type theory, and to what extent dependent type theories can be seen as extensions of higher-order logic. We apply our results by proving De Jongh's theorem for type theory.
In this paper we try to find a computational interpretation for a strong form of extensionality, which we call "converse extensionality". Converse extensionality principles, which arise as the Dialectica interpretation of the axiom of extensionality, were first studied by Howard. In order to give a computational interpretation to these principles, we reconsider Brouwer's apartness relation, a strong constructive form of inequality. Formally, we provide a categorical construction to endow every typed combinatory algebra with an apartness relation. We then exploit that functions reflect apartness, in addition to preserving equality, to prove that the resulting categories of assemblies model a converse extensionality principle.
We introduce the notion of an effective Kan fibration, a new mathematical structure that can be used to study simplicial homotopy theory. Our main motivation is to make simplicial homotopy theory suitable for homotopy type theory. Effective Kan fibrations are maps of simplicial sets equipped with a structured collection of chosen lifts that satisfy certain non-trivial properties. This contrasts with the ordinary, unstructured notion of a Kan fibration. We show that fundamental properties of Kan fibrations can be extended to explicit constructions on effective Kan fibrations. In particular, we give a constructive (explicit) proof showing that effective Kan fibrations are stable under push forward, or fibred exponentials. This is known to be impossible for ordinary Kan fibrations. We further show that effective Kan fibrations are local, or completely determined by their fibres above representables. We also give an (ineffective) proof saying that the maps which can be equipped with the structure of an effective Kan fibration are precisely the ordinary Kan fibrations. Hence implicitly, both notions still describe the same homotopy theory. By showing that the effective Kan fibrations combine all these properties, we solve an open problem in homotopy type theory. In this way our work provides a first step in giving a constructive account of Voevodsky's model of univalent type theory in simplicial sets.
We suggest an ordering for the predicates in continuous logic so that the semantics of continuous logic can be formulated as a hyperdoctrine. We show that this hyperdoctrine can be embedded into the hyperdoctrine of subobjects of a suitable Grothendieck topos. For this embedding we use a simplification of the hyperdoctrine for continuous logic, whose category of equivalence relations is equivalent to the category of complete metric spaces and uniformly continuous maps.
We introduce a modification of standard Martin-Lof type theory in which we eliminate definitional equality and replace all computation rules by propositional equalities. We show that type checking for such a system can be done in quadratic time and that it has a natural homotopy-theoretic semantics.
Recently, conservative extensions of Peano and Heyting arithmetic in the spirit of Nelson's axiomatic approach to Nonstandard Analysis, have been proposed. In this paper, we study the Transfer axiom of Nonstandard Analysis restricted to formulas without parameters. Based on this axiom, we formulate a base theory for the Reverse Mathematics of Nonstandard Analysis and prove some natural reversals, and show that most of these equivalences do not hold in the absence of parameter-free Transfer.
In topos theory it is well-known that any nucleus j gives rise to a translation of intuitionistic logic into itself in a way which generalises the Goedel-Gentzen negative translation. Here we show that there exists a similar j-translation which is more in the spirit of Kuroda's negative translation. The key is to apply the nucleus not only to the entire formula and universally quantified subformulas, but to conclusions of implications as well. The development is entirely syntactic and no knowledge of topos theory is required to read this small note.
We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category $\mathbb{EFF}$. Path categories are categories of fibrant objects in the sense of Brown satisfying two additional properties and as such provide a context in which one can interpret many notions from homotopy theory and Homotopy Type Theory. Within the path category $\mathbb{EFF}$ one can identify a class of discrete fibrations which is closed under push forward along arbitrary fibrations (in other words, this class is polymorphic or closed under impredicative quantification) and satisfies propositional resizing. This class does not have a univalent representation, but if one restricts to those discrete fibrations whose fibres are propositions in the sense of Homotopy Type Theory, then it does. This means that, modulo the usual coherence problems, it can be seen as a model of the Calculus of Constructions with a univalent type of propositions. We will also build a more complicated path category in which the class of discrete fibrations whose fibres are sets in the sense of Homotopy Type Theory has a univalent representation, which means that this will be a model of the Calculus of Constructions with a univalent type of sets.
We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, $Σ$- and $Π$-types, and functional extensionality. We apply the method to the effective topos with the interval object $\nabla 2$. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten.
We introduce the notion of a "category with path objects", as a slight strengthening of Kenneth Brown's classic notion of a "category of fibrant objects". We develop the basic properties of such a category and its associated homotopy category. Subsequently, we show how the exact completion of this homotopy category can be obtained as the homotopy category associated to a larger category with path objects, obtained by freely adjoining certain homotopy quotients. In a second part of this paper, we will present an application to models of constructive set theory. Although our work is partly motivated by recent developments in homotopy type theory, this paper is written purely in the language of homotopy theory and category theory, and we do not presuppose any familiarity with type theory on the side of the reader.
In this paper we present a proof of Goodman's Theorem, a classical result in the metamathematics of constructivism, which states that the addition of the axiom of choice to Heyting arithmetic in finite types does not increase the collection of provable arithmetical sentences. Our proof relies on several ideas from earlier proofs by other authors, but adds some new ones as well. In particular, we show how a recent paper by Jaap van Oosten can be used to simplify a key step in the proof. We have also included an interesting corollary for classical systems pointed out to us by Ulrich Kohlenbach.