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?
 A: By iteration it suffices to consider the case with just one $x$. Replace $1$ by an arbitrary object $T$. Assume that $T$ is $\omega$-presentable. Assume that $C$ has an initial object $0$, and that $C$ has colimits of $\omega$-chains. Then $\mu F = \mathrm{colim}_n F^n(0)$, hence $\hom(T,\mu F) = \mathrm{colim}_n \hom(T,F^n(0))$. In particular, every morphism $x : T \to \mu F$ factors (essentially unique) as $T \to F^n(0) \to \mu F$ for some $n$. Hence, we can make induction on $n$ in order to prove some property $P(x)$. For example, if $C=\mathsf{Set}$, $F(S)=S+1$, and $T=1$, this is just the usual induction on $\mu F = \mathbb{N}$ in the form "$\leq n~ \Rightarrow ~\leq n+1$".
A: 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.
