Proof by induction in categorical terms Given a category cartesian closed $C$ and a functor $F : C \to C$, I consider the initial object in the category of $F$-algebras. This initial object $\mu F$ seems to codify an "inductive object" in $C$.
Now I'm trying to prove some property that I would "normally" prove by induction on the structure of $\mu F$.
Let's suppose that the category is well-pointed. I want to prove a property that goes "for all $x,y : 1 \to \mu F$, $P(x,y)$" such that $P(x,y)$ is some mathematical statement in the language of category theory. In "set mathematics" I'd use induction on the structure of the set: first prove it for the base cases, and then use the induction hypothesis in the other cases. How can I prove this using the initiality of $\mu F$ rather than induction on its structure?

Martin's answer may be a bit deceptive, since it reduces to usual induction. But there is a brighter side to the story: if you only want to define a map from $\mu F$, to some object $A$, then all you need is to equip $A$ with $F$-algebra structure and let initiality of $\mu F$ apply. This is similar to defining a function by pattern-matching in a functional programming language.
To extend from maps to predicates, I expect you'll need your ambient category to model the logic as well. Maybe by moving to some topos over $C$? I'm no expert on this, so cannot really say more, sorry.
