Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Axioms of Arboreal Categories

Tomáš Jakl, Luca Reggio

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.

On the Axioms of Arboreal Categories

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.
Paper Structure (19 sections, 14 theorems, 50 equations)

This paper contains 19 sections, 14 theorems, 50 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Comonads and coalgebras
  4. Factorisation systems
  5. The posets of $\mathscr{M}$-subobjects.
  6. Game comonads and their categories of coalgebras
  7. Relational structures.
  8. Coalgebraic view.
  9. Modal comonad.
  10. Ehren-feucht--Fra"{i}ss'{e}{} comonad.
  11. Pebble comonad.
  12. The categories of coalgebras
  13. Game comonads and logic
  14. Arboreal categories and the failure of connectedness
  15. Arboreal categories redefined: tree-connectedness
  16. ...and 4 more sections

Key Result

lemma 1

Let $\mathbb C$ be a comonad on a category $\mathop{\mathrm{\mathscr{C}}}\nolimits$ with a proper factorisation system $(\mathscr{Q},\mathscr{M})$. If $\mathbb C$ preserves embeddings, then $\mathsf{EM}(\mathbb C)$ admits a proper factorisation system $(\overline{\mathscr{Q}}, \overline{\mathscr{M}}

Theorems & Definitions (35)

  • lemma 1
  • proof
  • remark 1
  • remark 2
  • definition 1: "Old definition" of arboreal category
  • lemma 2
  • proof
  • remark 3
  • remark 4
  • definition 2
  • ...and 25 more