Iterating until a diagram commutes I'm coming across the following 'commuting' diagram a lot in my work, and I think
it should have a neat categorical formulation. But I can't work it out for myself, and don't know what too google for. Maybe somebody can give me a pointer?
Assume I have 4 functions/morphisms.


*

*$f : A \rightarrow B$. 

*$down : A \rightarrow A'$. 

*$up : B' \rightarrow B$. 

*$g : A' \rightarrow A' \oplus B'$.


Here $\oplus$ is the disjoint sum of sets.
I want to say the following diagram 'commutes':

but it doesn't 'typecheck' because the codomain of $g$ doesn't match the domain of $up$. However, it does 'commute eventually' in the following sense. For all $a \in A$ the following  holds. There exist $a_0, ..., a_{n-1} \in A'$ and $b' \in B'$ such that:


*

*$down(a) = a_0$,

*$g(a_0) = inl(a_1)$,

*$g(a_1) = inl(a_2)$,

*...

*$g(a_{n-2}) = inl(a_{n-1})$,

*$g(a_{n-1}) = inr(b')$, and

*$up(b') = f(a)$. 


Here $inl(a)$ means $a$ is in the 'left' part of the sum
$A' \oplus B'$ while 
$inr(b)$ means $b$ is in the 'right' part of 
$A' \oplus B'$. 
In other words, for the diagram to 'commute', $g$ should be applied until it yields something of type $B$. In my application, this will always eventually happen. If we were sloppy and ignored the $inl/inr$
we could write: $\forall a\in A. \exists n. f(a) = up ( g^n(down(a)))$. 
What's a good categorical rendering of this? Some abstract conception of iteration or recursion? In which parts of mathematics do similar constructions crop up?
 A: Since you're interested in considering objects that have elements I'll assume we are working with $\mathbf{Sets}$ the category of sets and functions.
From the function $g \colon A' \to A' \oplus B'$ and from $inr \colon B' \to A' \oplus B'$ you can obtain the function $\bar g \colon A' \oplus B' \to A' \oplus B'$. By definition this function is such that


*

*for every $a \in A'$ we have $\bar g(inl(a))=g(a)$;

*for every $b \in B'$ we have $\bar g(inr(b))=b$.


Now using your notation we have that $inl(a_1)=\bar g(inl(a_0))$ and an easy induction shows that for every $n=1,\dots,n$ we have that $inl(a_n)=\bar g^n(inl(a_0))$.
So your requirement that the sequence of the $a_n$'s eventually falls in $B$ can be expressed as 
$$\forall a \in A'\ \exists b \in B'\ \exists n \in \mathbb N\ \bar g^n(inl(a))=inr(b)\ .$$
This should imply that $B'$ is the colimit of the diagram
$$A' \oplus B' \stackrel{\bar g}{\longrightarrow}A' \oplus B' \stackrel{\bar g}{\longrightarrow}A' \oplus B' \stackrel{\bar g}{\longrightarrow}A' \oplus B' \stackrel{\bar g}{\longrightarrow}A' \oplus B' \stackrel{\bar g}{\longrightarrow}A' \oplus B' \dots$$
where the colimit maps $(in^g_i \colon A' \oplus B' \to B')_{i \in \mathbb N}$ should send every $inl(a)$ into the eventual limit of the sequence $\{\bar g^n(inl(a))\}_{n \in \mathbb N}$ and every $inr(b)$ into $b$ (itself).
Now you could express your condition via the commutativity of the following diagram 
$$
\require{AMScd}
\begin{CD}
A @>{f}>> B \\
@V{down}VV @A{up}AA\\
A' @>{in^g_1 \circ inl}>>  B'
\end{CD}
$$
where $inl$ is the embedding of $A'$ into $A' \oplus B'$ while $in^g_1$ is  the first structure map of the above mentioned colimit diagram $(A' \oplus B' \stackrel{in^g_i}{\longrightarrow} B')_{i \in \mathbb N}$.
Hope this helps.
