Non-well-founded trees in categories
范畴论
2007-05-23 v1
摘要
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.
引用
@article{arxiv.math/0409158,
title = {Non-well-founded trees in categories},
author = {Benno van den Berg and Federico de Marchi},
journal= {arXiv preprint arXiv:math/0409158},
year = {2007}
}
备注
Submitted for publication