On the Semantics of Coinductive Types in Martin-Löf Type Theory.

There are several approaches to the problem of giving a categorical semantics to Martin-Löf type theory with dependent sums and products and extensional equality types. The most established one relies on the notion of a type-category (or category with attributes) with Σ and Π types. We extend such a semantics by introducing coinductive types both on the syntactic level and in a type-category. Soundness of the semantics is preserved. As an example of such a category, we prove that the type-category built over a locally cartesian closed category admits coinductive types whenever has final coalgebras for all polynomial functors. [ABSTRACT FROM AUTHOR]