Poset-enriched pretoposes and compact ordered spaces

TL;DR

This paper characterizes the category of Nachbin's compact ordered spaces as a unique poset-enriched pretopos with specific properties, using internal language techniques to explore its structure and compactness features.

Contribution

It provides a novel categorical characterization of compact ordered spaces as a poset-enriched pretopos with distinctive properties.

Findings

$ ext{KOrd}$ is the only non-degenerate poset-enriched pretopos with a discrete generator.

Objects are covered by order-filtral objects satisfying compactness and separation.

Extensive use of internal language clarifies the structure of $ ext{KOrd}$.

Abstract

We provide a characterisation of the category $\mathsf{KOrd}$ of Nachbin's compact ordered spaces as a poset-enriched category. Up to equivalence, $\mathsf{KOrd}$ is the only non-degenerate poset-enriched pretopos whose terminal object is a (discrete) generator and in which every object is covered by an order-filtral object. Order-filtral objects satisfy an appropriate form of compactness and separation. Throughout, we make extensive use of the internal language of poset-enriched pretoposes.