Mechanised Relation-Algebraic Order Theory in Ordered Categories without Meets

In formal concept analysis, complete lattices of “concepts” are represented by entity-attribute relations called “contexts”. Using the dependently-typed programming language Agda, we build on a previous formalisation of the category of contexts to obtain a fully verified abstract implementation of the duality between contexts and complete lattices in the abstract setting of locally ordered categories with converse, residuals, symmetric quotients, and direct powers.