The notion of (co)datatype can be modeled satisfactorily in category theory as fixed-points of polynomial functors. Then, (co)induction principles are derived from initial algebras/terminal coalgebras structures.
I was wondering (following Harper's idea of computational trinitarianism), if such a nice model exists in the context of type theory.
Somewhat related is the situation in the Isabelle and Coq proof assistants. In Isabelle, the (co)datatype package builds on the notion of bounded natural functor (thus, category theory). The situation in Coq and other systems looks like codatatypes are constructed in terms of datatypes (similarly for coinduction/induction).
I have seen several discussions about how Coq or other systems that reduce coinduction to induction produce, when sound, formalisms that restrict syntactically the users. Thus, the engineering question here is, could Coq given its type theory foundations implement a similar (co)datatype package as Isabelle?
Note that Isabelle/HOL formalism can be understood as a form of weakly typed set theory.
