Zobrazeno 1 - 10
of 58
pro vyhledávání: '"Berg, Benno van den"'
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 F
Externí odkaz:
http://arxiv.org/abs/2404.15443
Autor:
Berg, Benno van den, Geerligs, Freek
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 Mal
Externí odkaz:
http://arxiv.org/abs/2402.10568
Autor:
Berg, Benno van den
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
Externí odkaz:
http://arxiv.org/abs/2310.16493
Autor:
Berg, Benno van den, Otten, Daniël
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 th
Externí odkaz:
http://arxiv.org/abs/2308.15288
Autor:
Berg, Benno van den, Briet, Marcus
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 realizabilit
Externí odkaz:
http://arxiv.org/abs/2308.14096
Autor:
Figueroa, Daniel, Berg, Benno van den
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 Grothendi
Externí odkaz:
http://arxiv.org/abs/2107.10543
Autor:
Berg, Benno van den, Passmann, Robert
Publikováno v:
Logical Methods in Computer Science, Volume 18, Issue 4 (December 20, 2022) lmcs:7306
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,
Externí odkaz:
http://arxiv.org/abs/2103.14482
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 t
Externí odkaz:
http://arxiv.org/abs/2102.00905
Autor:
Berg, Benno van den, Faber, Eric
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 fibra
Externí odkaz:
http://arxiv.org/abs/2009.12670
Autor:
Berg, Benno van den
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
Externí odkaz:
http://arxiv.org/abs/1803.10113