[FOM] Replacement

[Andrej Bauer]

Isn't replacement required for construction of initial algebras (and 
final coalgebras) of functors? For example, given a functor F:Set->Set, 
one often considers the colimit of the diagram

   0 --> F0 --> F(F0) --> F(F(F0)) --> ...

The colimit is constructed as a quotient of the disjoint sum of the 
family {0, F0, F(F0), F(F(F0)), ...}. But how do we form this family if 
not by replacement?

This is certainly "ordinary math" as such constructions are used in 
topology, algebra and theoretical computer science, at least.

Andrej Bauer