代数余完备性与有限函子

Finitary Corecursion for the Infinitary Lambda Calculus

Kurz et al. have recently shown that infinite $λ$-trees with finitely many free variables modulo $α$-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational $λ$-trees, i.e. those $λ$-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational $λ$-trees.

从抽象微分几何视角看有限真空爱因斯坦引力与自由 Yang-Mills 理论中的函子性

Functoriality in Finitary Vacuum Einstein Gravity and Free Yang-Mills Theories from an Abstract Differential Geometric Perspective

本文沿用抽象微分几何的同调代数工具，致力于提出有限、因果且量子化的真空 Einstein Lorentz 引力与自由 Yang-Mills 理论表述。

Hilbert空间不承认任何有限离散虚象

Hilbert spaces admit no finitary discrete imaginaries

本文证明Hilbert空间范畴中不存在非平凡的有限离散虚象，扩展了Lieberman--Rosický--Vasey的结果。

Strongly Complete Logics for Coalgebras

Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations …

可数步下的终余代数

Terminal Coalgebras in Countably Many Steps

该研究证明了局部有限呈现范畴上有限自函子的终余代数可通过终余代数链的可数极限得到，并给出Vietoris多项式函子等多类函子终余代数的步长结果及相关证明。

A New Foundation for Finitary Corecursion

This paper contributes to a theory of the behaviour of "finite-state" systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). Mor…

How many adjunctions give rise to the same monad?

Given an adjoint pair of functors $F,G$, the composite $GF$ naturally gets the structure of a monad. The same monad may arise from many such adjoint pairs of functors, however. Can one describe all of the adjunctions giving rise to a given monad? In this paper we single out a class of adjunctions with especially good properties, and we develop methods for computing all such adjunctions, up to natural equivalence, which give rise to a given monad. To demonstrate these methods, we explicitly compute the finitary homological presentations of the free $A$-module monad on the category of sets, for …

Partial Evaluations and the Compositional Structure of the Bar Construction

The algebraic expression $3 + 2 + 6$ can be evaluated to $11$, but it can also be partially evaluated to $5 + 6$. In categorical algebra, such partial evaluations can be defined in terms of the $1$-skeleton of the bar construction for algebras of a monad. We show that this partial evaluation relation can be seen as the relation internal to the category of algebras generated by relating a formal expression to its total evaluation. The relation is transitive for many monads which describe commonly encountered algebraic structures, and more generally for BC monads on $\mathsf{Set}$ (which are tho…