62 citations · 126 across the 28 of their papers we have counts for
29 papers
Initial algebras from constructive ordinals
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 al…
The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems
Wijnand van Woerkom, Benno van den Berg
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 u…
Examples and cofibrant generation of effective Kan fibrations
Benno van den Berg, Freek Geerligs
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 fundamenta…
Apartness and the elimination of strong forms of extensionality
Benno van den Berg
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 ver…
Conservativity of Type Theory over Higher-order Arithmetic
Benno van den Berg, Daniël Otten
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 conservati…
Arrow algebras
Benno van den Berg, Marcus Briet
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 we…
Converse extensionality and apartness
Benno van den Berg, Robert Passmann
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…
Effective Kan fibrations in simplicial sets
Benno van den Berg, Eric Faber
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…
A Kuroda-style j-translation
Benno van den Berg
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 translati…
A homotopy-theoretic model of function extensionality in the effective topos
Daniil Frumin, Benno van den Berg
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.…
Path categories and propositional identity types
Benno van den Berg
Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identi…
Exact completion of path categories and algebraic set theory -- Part I: Exact completion of path categories
Benno van den Berg, Ieke Moerdijk
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 prop…
Univalent completion
Benno van den Berg, Ieke Moerdijk
We review the concept of a univalent fibration and show by elementary means that every Kan fibration in simplicial sets can be embedded in a univalent Kan fibration.
Reverse Mathematics and parameter-free Transfer
Benno van den Berg, Sam Sanders
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…
A note on arithmetic in finite types
Benno van den Berg
We present a version of arithmetic in all finite types which allows for a definition of equality at higher types for which all congruence are derivable, for which the soundness of…
Extending obstructions to noncommutative functorial spectra
Benno van den Berg, Chris Heunen
Any functor from the category of C*-algebras to the category of locales that assigns to each commutative C*-algebra its Gelfand spectrum must be trivial on algebras of nxn-matrices…
Nonstandard functional interpretations and categorical models
Amar Hadzihasanovic, Benno van den Berg
Recently, the second author, Briseid and Safarik introduced nonstandard Dialectica, a functional interpretation that is capable of eliminating instances of familiar principles of n…
W-types in Homotopy Type Theory
Benno van den Berg, Ieke Moerdijk
We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of…
The Axiom of Multiple Choice and Models for Constructive Set Theory
Benno van den Berg, Ieke Moerdijk
We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it…
The Herbrand Topos
Benno van den Berg
We define a new topos, the Herbrand topos, inspired by the modified realizability topos and our earlier work on Herbrand realizability. We also introduce the category of Herbrand a…
Are There Enough Injective Sets?
Peter Aczel, Benno van den Berg, Johan Granstroem +1
The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough…
A functional interpretation for nonstandard arithmetic
Benno van den Berg, Eyvind Briseid, Pavol Safarik
We introduce constructive and classical systems for nonstandard arithmetic and show how variants of the functional interpretations due to Goedel and Shoenfield can be used to rewri…
Non-deterministic inductive definitions
Benno van den Berg
We study a new proof principle in the context of constructive Zermelo-Fraenkel set theory based on what we will call "non-deterministic inductive definitions". We give applications…
No-go theorems for functorial localic spectra of noncommutative rings
Benno van den Berg, Chris Heunen
Any functor from the category of C*-algebras to the category of locales that assigns to each commutative C*-algebra its Gelfand spectrum must be trivial on algebras of nxn-matrices…