一句话：提出公理化的 Arboreal 范畴与覆盖，统一有限模型论中的双模拟、来回博弈及资源计数。
本文针对博弈余单子（game comonads）给出的有限模型论无语法范畴方法，提出公理化框架以刻画余代数范畴的核心性质。作者引入 Arboreal 范畴，使其具有内在过程结构，从而可定义双模拟、来回博弈等动态概念以及博弈轮数等资源概念；并通过资源索引的余单子伴随（Arboreal cover）将这类动态结构与外延或静态结构相联系。该框架在关系结构上得到应用，恢复了 pebbling、Ehrenfeucht-Fraïssé 与模态双模拟博弈的余单子构造，表明有限模型论和描述复杂性中的许多基本概念均可视为 Arboreal cover 的实例。
Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.