In this work, we describe a computational model for categories and functors. The categories that are handled by this model are locally finitely presentable categories which can be "sufficiently finitely" described to a computer. As an application of this model, we introduce a criterion to show whether a functor, as described in the model, is a left adjoint. The verification of this criterion can be partially automatised, if not fully in some cases, as witnessed by an implementation. While this work is focused on computational aspects, it is relevant to the broader categorical community, as it presents a new way to check whether functors are left adjoints and outlines a new computational methodology in category theory.

翻译：本文提出了一种用于范畴与函子的计算模型。该模型处理的范畴是局部有限可表现范畴，这些范畴能够以"充分有限"的方式向计算机描述。作为该模型的应用，我们引入了一个判定准则，用于检验模型中描述的函子是否为左伴随函子。该准则的验证过程可实现部分自动化，在某些情况下甚至可能完全自动化，这一点已通过具体实现得到验证。虽然本研究聚焦于计算层面，但其对更广泛的范畴论学界具有重要价值：它提供了一种检验函子是否为左伴随的新方法，并勾勒出范畴论中一种全新的计算方法论。