On the Axioms of Arboreal Categories

TL;DR

This paper refines the axiomatic framework of arboreal categories used in logic model comparison games by introducing tree-connectedness, ensuring the framework's robustness and demonstrating the path functor's properties.

Contribution

It identifies a flaw in the existing axioms and proposes a new concept, tree-connectedness, to strengthen the theoretical foundation of arboreal categories.

Findings

The connectedness axiom is inadequate for arboreal categories.

Tree-connectedness preserves essential properties of arboreal categories.

The path functor is shown to be a Street fibration.

Abstract

Arboreal categories were introduced as an axiomatic framework for game comonads, which provide a comonadic view on many model-comparison games in logic. We demonstrate the inadequacy of the axiom stating that paths are connected. We then propose the notion of ``tree-connectedness'' to address this deficiency, and show that all the essential properties of arboreal categories that we are aware of remain valid under this new definition. Furthermore, we show that the path functor is a Street fibration.