Search

• < Previous
• 1
• Next >

---

Every metric space is separable in function realizability

Andrej Bauer ; Andrew Swan.

We first show that in the function realizability topos every metric space is separable, and every object with decidable equality is countable. More generally, working with synthetic topology, every $T_0$-space is separable and every discrete space is countable. It follows that intuitionistic logic&nbsp;[&hellip;]

---

On the Nielsen-Schreier Theorem in Homotopy Type Theory

Andrew W Swan.

We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the&nbsp;[&hellip;]

---