Non-well-founded trees in categories
Benno van den Berg, Federico de Marchi

TL;DR
This paper explores the categorical foundations of non-well-founded trees, or M-types, establishing their existence and stability properties in certain logical categories relevant to mathematics and computer science.
Contribution
It formalizes the notion of paths in non-well-founded trees within locally cartesian closed pretoposes with natural number objects, proving key existence and stability results.
Findings
Existence of M-types in the specified categories.
Stability of these categories under slicing and sheaf constructions.
Formalization of paths in non-well-founded trees within the internal logic.
Abstract
Non-well-founded trees are used in mathematics and computer science, for modelling non-well-founded sets, as well as non-terminating processes or infinite data-structures. Categorically, they arise as final coalgebras for polynomial endofunctors, which we call M-types. In order to reason about trees, we need the notion of path, which can be formalised in the internal logic of any locally cartesian closed pretopos with a natural number object. In such categories, we derive existence results about M-types, leading to stability of locally cartesian closed pretoposes with a natural number object and M-types under slicing, formation of coalgebras (for a cartesian comonad), and sheaves for an internal site.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization
