A Final Coalgebra Theorem in the Context of Algebraic Set Theory
Anthony Renard

Abstract:
A Final Coalgebra Theorem in the Context of Algebraic Set Theory
First presented by Joyal and Moerdijk, algebraic set theory is a novel way to look at models of set theory. Various theories such as CZF, IZF, ZF, BIST, CST have been successfully modelled into this framework as attests the work by Awodey et al. Despite this success, it turns out that only Van den Berg and De Marchi attempted to use the Joyal-Moerdijk axiomatisation to model a set theory containing Aczel's anti-foundation axiom. Van den Berg and De Marchi proved a final coalgebra theorem for a large class of functors acting on a Heyting pretopos with a class of small maps. As a special instance, they obtained a final coalgebra for the powerset functor determined by the class of small maps and proved it is to be a model of the non-well-founded set theory CZF_0 + AFA.
Their proof, relying on the formalism of indexed categories, is however very indirect. The aim of this thesis is to find a new, more insightful proof of Van den Berg and De Marchi’s final coalgebra theorem. We start with a review of Aczel and Mendler classical final coalgebra theorem, and show that an essentially constructive proof can be given to this result. Based on this review, we give a direct proof of the final coalgebra theorem in algebraic set theory by recasting Aczel and Mendler’s strategy in the internal logic of a Heyting pretopos with a class of small maps.