4 papers · 1 filter
Generalized Decidability via Brouwer Trees
Tom de Jong, Nicolai Kraus, Aref Mohammadzadeh +1
In the setting of constructive mathematics, we suggest and study a framework for decidability of properties, which allows for finer distinctions than just "decidable, semidecidable…
Constructive Ordinal Exponentiation
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg +1
Cantor's ordinal numbers, a powerful extension of the natural numbers, are a cornerstone of set theory. They can be used to reason about the termination of processes, prove the con…
Formalizing equivalences without tears
Tom de Jong
This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique…
Domain theory in univalent foundations I: Directed complete posets and Scott's
Tom de Jong
We develop domain theory in constructive and predicative univalent foundations (also known as homotopy type theory). That we work predicatively means that we do not assume Voevodsk…