Order polarities
We define an order polarity to be a polarity (X,Y,R) where X and Y are partially ordered, and we define an extension polarity to be a triple (eX,eY,R) such that eX:P→X and eY:P→Y are poset extensions and (X,Y,R) is an order polarity. We define a hierarchy of increasingly strong coherence conditions for extension polarities, each equivalent to the existence of a pre-order structure on X∪Y such that the natural embeddings, ιX and ιY, of X and Y, respectively, into X∪Y preserve the order structures of X and Y in increasingly strict ways. We define a Galois polarity to be an extension polarity where eX and eY are meet- and join-extensions respectively, and we show that for such polarities there is a unique pre-order on X∪Y such that ιX and ιY satisfy particularly strong preservation properties. We define morphisms for polarities, providing the class of Galois polarities with the structure of a category, and we define an adjunction between this category and the category of Δ1-completions and appropriate homomorphisms. We formalize the theory of extension polarities and prove a duality principle to the effect that if a statement is true for all extension polarities then so too must be its dual statement.