Under advice from Toby Bartels, I am posting this question here; it falls under the general heading of constructing data types categorically as fixed points of functors.

The first question I have is a warm-up. There's a way to interpret a natural number n in any cartesian closed category C, as a dinatural transformation of the form

c^c --> c^c

which intuitively takes an element f: c --> c to its n-th iterate f^(n): c --> c. One may hope that if C is "nice", then every such dinatural transformation will be of this form, or better still, that the end

\int_{c: C} (c^c)^(c^c)

(assuming it exists) behaves as a natural numbers object in C. So first, I am interested in what "nice" might mean here: what are some general conditions on C that ensure we can construct a natural numbers object as an end in this way?

Second, this end can be rewritten as

\int_{c: C} c^(c^(1 + c))

provided that C has coproducts, and the assertion that this behaves as a natural numbers object is equivalent to saying it is an initial algebra for the endofunctor F(c) = 1 + c (that's algebra for an endofunctor, not for a monad), making it a "fixed point" of F by a famous old result of Lambek.

This suggests a second more general question: given an endofunctor F: C --> C on cartesian closed C with a strength (essentially, a structure of C-enrichment), I want to know what "nice" conditions on C and/or F guarantee that the end

e = int_{c: C} c^(c^F(c)),

if it exists, is an initial F-algebra. It's not hard to write down an an F-algebra structure for this end e, and show that it is weakly initial, i.e., show that if x is any F-algebra, then there at least exists an F-algebra map e --> x. The issue then is over the uniqueness of this map, or rather what nice conditions would guarantee that.

Discussion of specific cases like PER models would be alright, but I'd probably be a lot more excited if it led to consideration of more general abstract conditions on C or F.