Orthogonality is a notion based on the duality between programs and their environments used to determine when they can be safely combined. For instance, it is a powerful tool to establish termination properties in classical formal systems. It was given a general treatment with the concept of orthogonality category, of which numerous models of linear logic are instances, by Hyland and Schalk. This paper considers the subclass of focused orthogonalities. We develop a theory of fixpoint constructions in focused orthogonality categories. Central results are lifting theorems for initial algebras and final coalgebras. These crucially hinge on the insight that focused orthogonality categories are relational fibrations. The theory provides an axiomatic categorical framework for models of linear logic with least and greatest fixpoints of types. We further investigate domain-theoretic settings, showing how to lift bifree algebras, used to solve mixed-variance recursive type equations, to focused orthogonality categories.

翻译：正交性是基于程序与其环境之间对偶性的概念，用于确定它们何时可以安全组合。例如，它是经典形式系统中建立终止性质的有力工具。Hyland和Schalk通过正交性范畴这一概念对其进行了统一处理，而线性逻辑的众多模型都是该范畴的实例。本文聚焦于正交性的子类——聚焦正交性。我们在聚焦正交性范畴中发展了不动点构造理论。核心结果是初始代数与终结余代数的提升定理。这些定理的关键在于认识到聚焦正交性范畴是关系纤维化。该理论为具有类型最小与最大不动点的线性逻辑模型提供了公理化的范畴框架。我们进一步研究了域论设定，展示了如何将用于求解混合变体递归类型方程的双自由代数提升到聚焦正交性范畴中。