[FOM] Replacement

Andrej Bauer Andrej.Bauer at fmf.uni-lj.si
Wed Aug 15 05:26:14 EDT 2007

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

More information about the FOM mailing list