Bilimits in categories of partial maps

TL;DR

This paper proves that the category of dcpos and partial maps is closed under bilimits, clarifying a foundational aspect of constructive domain theory and enabling applications in models of axiomatic and synthetic domain theory.

Contribution

It provides a topos-valid proof of bilimit closure in the category of dcpos and partial maps, addressing gaps in previous constructive approaches.

Findings

Category of dcpos and partial maps is closed under bilimits.

Constructive proof of bilimit closure in topos setting.

Applications to models of axiomatic and synthetic domain theory.

Abstract

The closure of chains of embedding-projection pairs (ep-pairs) under bilimits in some categories of predomains and domains is standard and well-known. For instance, Scott's $D_\infty$ construction is well-known to produce directed bilimits of ep-pairs in the category of directed-complete partial orders, and de Jong and Escard\'o have formalized this result in the constructive domain theory of a topos. The explicit construcition of bilimits for categories of predomains and partial maps is considerably murkier as far as constructivity is concerned; most expositions employ the constructive taboo that every lift-algebra is free, reducing the problem to the construction of bilimits in a category of pointed domains and strict maps. An explicit construction of the bilimit is proposed in the dissertation of Claire Jones, but no proof is given so it remained unclear if the category of dcpos and partial maps was closed under directed bilimits of ep-pairs in a topos. We provide a (Grothendieck)-topos-valid proof that the category of dcpos and partial maps between them is closed under bilimits; then we describe some applications toward models of axiomatic and synthetic domain theory.