Johan Lindberg: Logical Spaces

Abstract: In this presentation we describe an ongoing project of giving a more explicitly logical proof of the Joyal-Tierney representation theorem for Grothendieck toposes.

A key aspect of our approach is the use of complete Heyting Algebra (cHA) valued sets instead of sheaves. One reason for pursuing this line of research is to further develop the constructive model theory for geometric and first-order intuitionistic logic with respect to cHA-valued sets, and to clarify its connections with more general topos-theoretic machinery.

This is joint work with Henrik Forssell.