A computational method for left-adjointness

TL;DR

This paper presents a computational method to determine when functors between locally finitely presentable categories are left adjoints, using presheaf category descriptions and profunctor presentations, with practical OCaml implementations.

Contribution

It introduces a new computational approach for establishing left-adjointness of functors in a broad class of categories, including practical implementation and examples.

Findings

Method effectively determines left-adjointness in locally finitely presentable categories

Implementation in OCaml demonstrates practical applicability

Method also aids in verifying cartesian closedness of categories

Abstract

In this work, we investigate an effective method for showing that functors between categories are left adjoints. The method applies to a large class of categories, namely locally finitely presentable categories, which are ubiquitous in practice and include standard examples like Set, Grp, etc. Our method relies on a known description of these categories as orthogonal sub-classes of presheaf categories. The functors on which our method applies are the ones that can be presented as particular profunctors, called Kan models in this context. The method for left-adjointness then relies on computing that a particular criterion is satisfied. From this method, we also derive another method for showing that a category is cartesian closed. As proofs of concept and effectivity, we give a concrete implementation of the structures and of the left-adjointness criterion in OCaml and apply it on several examples.