Fixpoint operators are tools to reason on recursive programs and data types obtained by induction (e.g. lists, trees) or coinduction (e.g. streams). They were given a categorical treatment with the notion of categories with fixpoints. A theorem by Plotkin and Simpson characterizes existence and uniqueness of fixpoint operators for categories satisfying some conditions on bifree algebras and recovers the standard examples of the category Cppo ($\omega$-complete pointed partial orders and continuous functions) in domain theory and the relational model in linear logic. We present a categorification of this result and develop the theory of 2-categorical fixpoint operators where the 2-dimensional framework allows to model the execution steps for languages with (co)inductive principles. We recover the standard categorical constructions of initial algebras and final coalgebras for endofunctors as well as fixpoints of generalized species and polynomial functors.

翻译：不动点算子是用于推理递归程序及通过归纳（如列表、树）或余归纳（如流）得到的数据类型的工具。它们在范畴论中通过带不动点的范畴概念得到了范畴化处理。普洛特金和辛普森的一个定理刻画了满足双自由代数某些条件的范畴上不动点算子的存在性与唯一性，并恢复了域论中的标准例子Cppo范畴（$\omega$完备的尖偏序集与连续函数）以及线性逻辑中的关系模型。我们对该结果进行了范畴化推广，发展了2-范畴不动点算子的理论，其中二维框架允许对具有（余）归纳原理的语言的执行步骤进行建模。我们恢复了自函子上的初始代数与终余代数的标准范畴构造，以及广义种与多项式函子的不动点。