Loops
The loop diagram, consisting of one object and one arrow
is least studied of all small categorical diagrams. The limit of a
loop f on an object X is its object Fix(f) of fixpoints
. Its colimit is the universal invariant
Universal(f). These ideas were used to characterise while-loops in Fixpoint and Loop Constructions as
Colimits .
When the canonical composite
Fix(f) ---> X ---> Universal(f)
is an isomorphism then iteration of f will always converge to a
fixpoint, and we say that f is a convergent loop. Examples
can be constructed in Sets, domains, metric spaces, etc. This supports
a direct definition of a tail recursive list object in terms of
convergence of the loop which performs one step in the recursion Tail recursion through universal
invariants .