Non-well-founded trees in categories

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. We derive existence results for M-types in locally cartesian closed pretoposes with a natural numbers object, using their internal logic. These are then used to prove stability of such categories with M-types under various topostheoretic constructions; namely, slicing, formation of coalgebras (for a cartesian comonad), and sheaves for an internal site.

• Type: Journal
• Year: 2007
• Where: APAL
• Authors: Benno van den Berg, Federico De Marchi
• Keywords: APAL 2007, Data Structures, Non-terminating Processes, Various Topostheoretic Constructions