1: \begin{definition}[Lattice isomorphism for cofinality map]

2:   Suppose $t \concur t'$ with $\target{\residual{t'}{t}} = Q$ and

3:   $\target{\residual{t}{t'}} = Q'$. By Theorem 1 of \cite{perera16},

4:   there exists a unique $\braiding{t,t'}$ witnessing $Q = Q'$, $Q

5:   \freeBraid Q'$ or $Q \boundBraid Q'$. Define the following pair of

6:   monotone functions between $\down{Q}$ and $\down{Q'}$.

7: 

8:   \vspace{3pt}

9:   \input{fig/transition/concur/cofin/galois-connection}

10: \end{definition}

11: