4 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…