Search

• < Previous
• 1
• Next >

---

On Small Types in Univalent Foundations

Tom de Jong ; Martín Hötzel Escardó.

We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot&nbsp;[&hellip;]

---

The Sierpinski Object in the Scott Realizability Topos

Tom de Jong ; Jaap van Oosten.

We study the Sierpinski object $\Sigma$ in the realizability topos based on Scott's graph model of the $\lambda$-calculus. Our starting observation is that the object of realizers in this topos is the exponential $\Sigma ^N$, where $N$ is the natural numbers object. We define order-discrete objects&nbsp;[&hellip;]

---