Showing 1–2 of 2 results for author: De Marchi, F

Models of Non-Well-Founded Sets via an Indexed Final Coalgebra Theorem

Authors: Benno van den Berg, Federico De Marchi

Abstract: The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on categories with finite limits and colimits. As an instance of this result, we build the final coalgebra for the powerclass functor, in the context of a Heyting pretopos with a class of small maps. This is then… ▽ More The paper uses the formalism of indexed categories to recover the proof of a standard final coalgebra theorem, thus showing existence of final coalgebras for a special class of functors on categories with finite limits and colimits. As an instance of this result, we build the final coalgebra for the powerclass functor, in the context of a Heyting pretopos with a class of small maps. This is then proved to provide a model for various non-well-founded set theories, depending on the chosen axiomatisation for the class of small maps. △ Less

Submitted 30 January, 2006; v1 submitted 26 August, 2005; originally announced August 2005.

MSC Class: 03C62;03G30;18C50

Non-well-founded trees in categories

Authors: Benno van den Berg, Federico de Marchi

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 cartesi… ▽ More 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. △ Less

Submitted 9 September, 2004; originally announced September 2004.

Comments: Submitted for publication

MSC Class: 18A15;68Q55;68Q65