9 citations · 19 across the 11 of their papers we have counts for
5 papers · 1 filter
Univalent polymorphism
Benno van den Berg
We show that Martin Hyland's effective topos can be exhibited as the homotopy category of a path category . Path categories are categories of fibrant objects in the s…
A topos for a nonstandard functional interpretation
Benno van den Berg
We introduce a new topos in order to give a semantic account of the nonstandard functional interpretation introduced by Eyvind Briseid, Pavol Safarik and the author.
Predicative toposes
Benno van den Berg
We explain the motivation for looking for a predicative analogue of the notion of a topos and propose two definitions. For both notions of a predicative topos we will present the b…
W-types in sheaves
Benno van den Berg, Ieke Moerdijk
We give a concrete description of W-types in categories of sheaves.
Non-well-founded trees in categories
Benno van den Berg, Federico de Marchi
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. Categori…