Arboreal Categories: An Axiomatic Theory of Resources

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 very general, axiomatic setting, and applied to relational structures, where the recently introduced comonadic constructions for pebbling, Ehrenfeucht-Fra\"iss\'e and modal bisimulation games are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers.