This paper presents two extensions of the second order polymorphiclambda calculus, system F, with monotone (co)inductive types supporting(co)iteration, primitive (co)recursion and inversion principles asprimitives. One extension is inspired by the usual categoricalapproach to programming by means of initial algebras and finalcoalgebras; whereas the other models dialgebras, and can be seen as an extension of Hagino'scategorical lambda calculus within the framework of parametricpolymorphism. The systems are presented in Curry-style, and are proven to be terminating andtype-preserving. Moreovertheir expressiveness is shown by means of several programmingexamples, going from usual data types to lazy codata types such as streamsor infinite trees.
