A Mechanised Abstract Formalisation of Concept Lattices

Using the dependently-typed programming language Agda, we formalise a category of algebraic contexts with relational homomorphisms presented by [Jip12], [Mos13]. We do this in the abstract setting of locally ordered categories with converse (OCCs) with residuals and direct powers, without requiring meets (as in allegories) or joins (as in Kleene categories). The abstract formalisation has the advantage that it can be used both for theoretical reasoning, and for executable implementations, by instantiating it with appropriate choices of concrete OCCs.