Logical Construction of Final Coalgebras
Luigi Santocanale · Electronic Notes in Theoretical Computer Science · 2003
We prove that every finitary polynomial endofunctor of a category C has a final coalgebra, provided that C is locally Cartesian closed, it has finite coproducts and is an extensive category, it has a natural number object.