Logical Construction of Final Coalgebras

Luigi Santocanale

We prove that every finitary polynomial endofunctor of a category $C$ has a final coalgebra if $C$ is locally Cartesian closed, has finite disjoint coproducts and a natural number…