Tom de Jong: Domain theory in constructive and predicative HoTT/UF

Speaker: Tom de Jong (University of Birmingham, UK)

Homotopy Type Theory, also known as Univalent Foundations (HoTT/UF), is a modern foundation for mathematics that is constructive and predicative by default. By constructive and predicative we respectively mean that excluded middle (and choice) and propositional resizing axioms are not assumed. I will explain how to develop domain theory within this framework, highlighting the main challenges and contributions of my PhD research.

In the first half I will illustrate the use of domain theory by focussing on the Scott model of the programming language PCF, where we will use the lifting monad to construct free directed complete posets with a least element. In the second half I will present some no-go theorems regarding constructivity and predicativity in domain theory. In turns out that within our framework nontrivial directed complete posets are necessarily large and necessarily lack decidable equality.