A computational method for left-adjointness
Simon Forest
TL;DR
The paper develops a computational framework for verifying when functors between locally finitely presentable categories are left adjoints, leveraging presheaf models and Kan models to encode categories and functors. It introduces a concrete reflection construction and an explicit left-adjointness criterion based on preserving certain colimits and orthogonality conditions, together with a game of reflection to guide finite approximations. A detailed OCaml implementation demonstrates encoding finite sets, finite categories, and presheaves, and implements left Kan extensions, colimits, and the reflection moves to decide adjointness on concrete examples. The work bridges abstract category theory with computable reasoning tools, enabling automated or semi-automated proofs of left adjointness and cartesian-closure properties in practical settings.
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.