A Mechanisation of Internal Galois Connections In Order Theory Formalised Without Meets

Abstract

Using the the dependently-typed programming language Agda, we formalise orders, with attention to the theory of Galois Connections, and showcase it by formalising a few results of the category of algebraic contexts with relational homomorphisms presented by Jipsen (2012) and Moshier (2013).

We aim to exhibit an internal theory of Galois Connections and Closure operators where the ambient space need not have a notion of meets (intersections), which are the usual medium in presenting antisymmetry of partial orders. Instead we consider `symmetric quotients' as being the relational counterpart of propositional calculus' primitive connective: equivalence. We argue that it as a more natural primitive than meet --- especially its connection with certain proof heuristics regarding posets. Moreover, not only do we constrain ourselves to an unconventional set of primitive operators, but in fact we discard the familiar setting of relations and sets in favour of the more general setting of ordered categories with converse (OCCs) --- in fact, a large portion does not require identities and so semigroupoids may be used instead.